A Fast SAT Solver for Isabelle in Standard ML

Armin Heller

December 9, 2009

Abstract

This contribution contains a fast SAT solver for Isabelle written in Standard ML. By loading the theory DPT_SAT_Solver, the SAT solver installs itself (under the name “dptsat”) and certain Isabelle tools like Refute will start using it automatically. This is a port of the DPT (Decision Procedure Toolkit) SAT Solver written in OCaml.

License

BSD License

Topics

Session DPT-SAT-Solver