A SAT solver implementation of the Davis-Putnam-Logemann-Loveland algorithm written in C++, using watched literals for efficient unit propagation and pure literal elimination, and utilizing the DLIS heuristic when searching. Implemented for CSCI 2951O: Prescriptive Analytics at Brown University.
For implementation details and considerations, along with optimizations made, see the report.
Compiling the program requires gcc to be installed; to compile the program, run:
./compile.sh
For an input boolean expression, the program requires .cnf file describing the instance in CNF file format. To run the program, run:
./run.sh <input>.cnf
The program will output a JSON dictionary containing the instance name, the time taken, and the result (SAT or UNSAT). If SAT, the boolean solution is also provided, using the variable identifiers given in the input CNF file.
To solve multiple instances, you can run:
./runAll.sh <inputFolder> <timeLimit> <logFile>
where <inputFolder> is a folder containing instances as .cnf files, <timeLimit> is the enforced time limit for each instance to be solved by in seconds, and <logFile> is the name of the output file where the above outputs relevant to each instance will be logged to. See results.log for an example of such a logfile.