An iterative DPLL SAT solver implemented in C++.
For information on how we built this SAT solver, our custom variable selection heuristic (ClauseReducer
), optimizations made, and more, read our report.
All the code for our solver is within the src/solver/sat
subdirectory.
Initially, you need to compile the code into a binary. To do this, run
./compile.sh
After this, to run the SAT solver on an individual input, run
./run.sh <input-file>
- For example, to solve the instance in the
input/C140.cnf
file, you would run:./run.sh input/C140.cnf
Note: The input files are expected to be in the DIMACS CNF format. All the instances in the
input/
andtoy_inputs/
directories can serve as examples.
If you want to run the solver on all the input files in a directory, you can run
./runAll.sh <input-folder> <timeout (in seconds)> <output-filename>
- For example, to generate the results.log file containing solver results on all the instances in the
input/
directory with a 300 second timeout (per instance), we ran./runAll.sh input/ 300 results.log
This SAT Solver was built by Karan Kashyap and Erica Song for Brown University's Prescriptive Analytics course.