## A Pearl on SAT and SMT Solving in Prolog

The solver is (SICStus) available as sat_solver.pl.

Some code for static variable ordering is also included,
static_var_order.pl.

The benchmarks from the paper are also included,
flopsbenchmarks.tar.
Please
cite satlib.org from where a number of these files come.

A version of the solver to produce statistics on timings and
assignments is also included,
sat_solver_instrumented.pl.

### SWI code

There are two version that work with SWI. The first uses when
sat_solver_when.pl. The second uses the more common
Prolog feature, freeze: sat_solver_freeze.pl.
### SMT

Code for SMT solving is now available. The smt framework is
in smt.pl and a decision procedure for
conjunctions of literals in linear real arithmetic is also
available, theory.pl. It is suggested that
this is used with a SAT solver with state restoration,
sat_solver_restore.pl.
## Distribution

A complete bundle of code is available: distribution.tar.
This includes:
the files mentioned above
further solvers illustrating learning and backjumping
a parser for dimacs SAT files and a harness for running experiments
a theory file for equality logic with uninterpreted
functors
code for generating SAT instances from Sudoku puzzles (provided by
"A.D.")
a number of benchmark files
## Papers

If using this code, please cite the following papers:

"A Pearl on SAT Solving in Prolog",
Jacob
M. Howe and Andy King. In
FLOPS 2010,
Proceedings of the 10th International Symposium on Function and Logic Programming
(eds Matthias Blume, Naoki Kobayashi and Germán Vidal).
Volume 6009 of Lecture Notes in Computer Science, pages 165-174.
Springer, 2010.
Slides from the talk are also available.

"A Pearl on SAT and SMT Solving in Prolog", Jacob M. Howe and Andy King.
Theoretical Computer Science. **435:43-55**,2012.