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.