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

Jasmin Christian Blanchette, Mathias Fleury*, Peter Lammich, Christoph Weidenbach

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

We developed a formal framework for conflict-driven clause learning (CDCL) 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 Davis–Putnam–Logemann–Loveland (DPLL) 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.

Original languageEnglish
Pages (from-to)1-33
Number of pages33
JournalJournal of Automated Reasoning
Volume2018
Issue number1-4
DOIs
Publication statusPublished - 12 Mar 2018

Keywords

  • CDCL
  • DPLL
  • Isabelle/HOL
  • Proof assistants
  • SAT solvers

Fingerprint Dive into the research topics of 'A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality'. Together they form a unique fingerprint.

Cite this