ams-dist

A distributed cube-n-conquer solver intended for hard combinatorial problems.
Authors: Maxim Zhulin, Piyush Jha, Zhengyu Li

Note

Currently supports only kochen-specker instances. The symmetry breaker for these problems is currently hard-coded into the pipeline. Furthermore since we run all-sat, we expect the whole instance to be unsatisfiable.

---

Build

Compile with Make. Requires MPI.

git clone --recursive https://github.com/map0te/ams-dist.git
cd ams-dist
make

Usage

ams-dist [OPTION]... ORDER FILE PATH

Solve FILE with order ORDER in the working directory PATH.

Arguments

Argument	Description
ORDER	Solver order parameter
FILE	Input CNF file to solve
PATH	Working directory for solver execution

Options

Option	Long Option	Description	Default
-h	--help	show help message	—
-v	--verbose	enable verbose solver status output	Disabled
-t VAL	--twarmup VAL	time before interrupt (seconds)	10
-c	--no_share_cas	turn off CAS clause sharing	Disabled

---

Example

Generating a Kochen-Specker instance:

python gen_instance/generate.py <order> 0.5
python gen_instance/generate.py 17 0.5

Running the distributed solver

mpirun -n <ncores> ams-dist <order> <instance> <workspace>
mpirun -n 16 ams-dist 17 ks_17.cnf temp/

---