microsat is a simple CDCL SAT solver, originally created by Marijn Heule and Armin Biere.

This fork adds the following features:

• Deduce implicit variable decisions by propagating a (partial) assignment of the SAT problem variables
• Check the status of a (partial) assignment of the SAT problem variables:
  • BUILDABLE: The problem will evaluate to true after completing the assignment by setting all undecided variables implicitely to false.
  • INCOMPLETE: Otherwise.

./configure && make

./configure && sudo make install

microsat

microsat --version

microsat DIMACS_FILE

microsat --propagate DIMACS_FILE

The (partial) assignment is denoted as a DIMACS comment line which has to be added somewhere before the problem line:

c v<NUMBER_OF_ASSIGNED_VARIABLES> <ASSIGNED_VARIABLES>

For example:

c v4 5 -7 18 -20
p cnf ...

Two demo files (one for each status described above) can be found in the test subdirectory.