sat-solver

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.

Usage

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/ and toy_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

Developers

This SAT Solver was built by Karan Kashyap and Erica Song for Brown University's Prescriptive Analytics course.