CDCL SAT Solver

Implementation of a SAT solver using watches, restarts and clause learning. Based on the SAT Solving course of Prof. Armin Biere at Freiburg University.

To compile run ./configure && make for optimized compilation and ./configure --debug && make if you want to include symbols and disable assertion checking. See ./configure -l for more options.

The code is supposed to be kept formatted with clang-format for which you need to install it first and then issue make format.

There are regression tests included, see make test.

• cdcl-sat : the executable binary after compilation.
• cdcl-sat.cpp : the self-contained actual C++ solver code.
• cnfs : test files in DIMACS format and test runner test/run.sh.
• config.hpp : generated by generate to capture build information.
• configure : the configure script generates makefile.
• generate : the generate script generates config.hpp.
• LICENSE : the license file (currently MIT license).
• makefile : the actual makefile generated from makefile.in.
• makefile.in : the makefile template instantiated to makefile.
• README.md : this overview file.
• VERSION : the version number.