A Fast SAT Solver for Isabelle in Standard ML

Armin Heller

December 9, 2009

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session DPT-SAT-Solver