Skip to content

README.md

Latest commit

 

History

History
24 lines (19 loc) · 1.25 KB

README.md

File metadata and controls

24 lines (19 loc) · 1.25 KB
Raw

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.