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

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

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
DOIs
Publication statusPublished - 12 Mar 2018

Fingerprint

Functional programming
Computer programming languages
Data structures
Concretes
Experiments

Keywords

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

Cite this

Blanchette, Jasmin Christian ; Fleury, Mathias ; Lammich, Peter ; Weidenbach, Christoph. / A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. In: Journal of Automated Reasoning. 2018 ; Vol. 2018. pp. 1-33.
@article{44ee03ef180e478ebfc65b5db8013893,
title = "A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality",
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.",
keywords = "CDCL, DPLL, Isabelle/HOL, Proof assistants, SAT solvers",
author = "Blanchette, {Jasmin Christian} and Mathias Fleury and Peter Lammich and Christoph Weidenbach",
year = "2018",
month = "3",
day = "12",
doi = "10.1007/s10817-018-9455-7",
language = "English",
volume = "2018",
pages = "1--33",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",

}

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. / Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph.

In: Journal of Automated Reasoning, Vol. 2018, 12.03.2018, p. 1-33.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

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

AU - Blanchette, Jasmin Christian

AU - Fleury, Mathias

AU - Lammich, Peter

AU - Weidenbach, Christoph

PY - 2018/3/12

Y1 - 2018/3/12

N2 - 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.

AB - 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.

KW - CDCL

KW - DPLL

KW - Isabelle/HOL

KW - Proof assistants

KW - SAT solvers

UR - http://www.scopus.com/inward/record.url?scp=85043697141&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85043697141&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-9455-7

DO - 10.1007/s10817-018-9455-7

M3 - Article

VL - 2018

SP - 1

EP - 33

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -