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

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

doi:10.1007/s10817-018-9455-7

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 Journal › Article › Academic › peer-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 language	English
Pages (from-to)	1-33
Number of pages	33
Journal	Journal of Automated Reasoning
Volume	2018
Issue number	1-4
DOIs	https://doi.org/10.1007/s10817-018-9455-7
Publication status	Published - 12 Mar 2018

Funding

Acknowledgements Open access funding was provided by the Max Planck Society. Stephan Merz made this work possible in the first place. Dmitriy Traytel remotely cosupervised Fleury’s M.Sc. thesis and provided copious advice on using Isabelle. Andrei Popescu gave us his permission to reuse, in a slightly adapted form, the succinct description of locales he cowrote on a different occasion [9]. Simon Cruanes, Anders Schlichtkrull, Mark Summerfield, Dmitriy Traytel, and the reviewers suggested many textual improvements. The work has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka).

Funders	Funder number
Horizon 2020 Framework Programme	713999
European Research Council
Max-Planck-Gesellschaft

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 10 Reduced Inequalities

Keywords

CDCL
DPLL
Isabelle/HOL
Proof assistants
SAT solvers

Access to Document

10.1007/s10817-018-9455-7

Persistent URL (handle)

Persistent link

Cite this

@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{\textquoteright}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 = mar,

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",

number = "1-4",

}

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 - https://www.scopus.com/pages/publications/85043697141

UR - https://www.scopus.com/pages/publications/85043697141#tab=citedBy

U2 - 10.1007/s10817-018-9455-7

DO - 10.1007/s10817-018-9455-7

M3 - Article

AN - SCOPUS:85043697141

SN - 0168-7433

VL - 2018

SP - 1

EP - 33

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 1-4

ER -

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

Abstract

Funding

UN SDGs

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this