A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Jasmin Christian Blanchette (1, 2, 3) , Mathias Fleury (4) , Peter Lammich (5) , Christoph Weidenbach (4)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
2 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 VU - Vrije Universiteit Amsterdam [Amsterdam]
4 MPII - Max-Planck-Institut für Informatik
5 TUM - Technische Universität Munchen - Technical University Munich - Université Technique de Munich

We developed a formal framework for CDCL (conflict-driven clause learning) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solver expressed in a functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants, including the DPLL (Davis-Putnam-Logemann-Loveland) calculus. The imperative program relies on the two-watched-literal data structure and other optimizations found in modern solvers. We used Isabelle's Refinement Framework to automate the most tedious refinement steps. The most noteworthy aspects of our work are the inclusion of rules for forget, restart, and incremental solving and the application of stepwise refinement.

Mots clés: Proof assistants; Isabelle/HOL; SAT solvers; CDCL; DPLL

Domaines: Logique en informatique [cs.LO]

Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Journal of Automated Reasoning, 2018, 61 (1-4), pp.333-365. ⟨10.1007/s10817-018-9455-7⟩. ⟨hal-01904579⟩