Semester project for Design of Parallel and High Performance Computing class at ETHZ. Includes two communication models for DPLL algorithm that could be combined with local CDCL. If you want to find out more about communication models or other techniques that we have used please refer to our final report.
Please follow these steps in order to successfully compile the source code:
git clone https://github.com/limo1996/SAT-Solver.git
cd SAT-Solver
cmake .
make
Three executables are available:
./sequential_main [-s CDCL/DPLL] <CNF_input_file>
Example usage of sequential version:
./sequential_main -s CDCL cnfs/benchmark_formulas/flat75-4.cnf
./parallel_main [-local-cdcl branching_factor : int] <CNF_input_file>
Example usage of parallel version:
./parallel_main -local-cdcl 3 cnfs/benchmark_formulas/ais8.cnf
./stealing_main [-local-cdcl branching_factor : int] <CNF_input_file>
Example usage of stealing version:
./stealing_main -local-cdcl 2 cnfs/benchmark_formulas/anomaly.cnf
We have developed a testing python wrapper whose documentation can be found here The python wrapper can also be used to run the solver on the Euler Supercompute Cluster of ETH.