A verified SAT solver with watched literals using imperative HOL

Mathias Fleury; Jasmin Christian Blanchette; Peter Lammich

doi:10.1145/3167080

A verified SAT solver with watched literals using imperative HOL

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

Bio-Health Informatics

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

210 Downloads (Pure)

Abstract

Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.

Original language	English
Title of host publication	Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Pages	158-171
Number of pages	13
DOIs	https://doi.org/10.1145/3167080
Publication status	Published - 2018
Event	the 7th ACM SIGPLAN International Conference - Los Angeles, CA, USA Duration: 8 Jan 2018 → 9 Jan 2018

Conference

Conference	the 7th ACM SIGPLAN International Conference
Period	8/01/18 → 9/01/18

Access to Document

10.1145/3167080

CPP_2018_paper_7Accepted author manuscript, 636 KB

http://dl.acm.org/citation.cfm?doid=3176245.3167080

Cite this

@inproceedings{558eb8166c114df39a210e6802167c54,

title = "A verified SAT solver with watched literals using imperative HOL",

abstract = "Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.",

author = "Mathias Fleury and Blanchette, {Jasmin Christian} and Peter Lammich",

year = "2018",

doi = "10.1145/3167080",

language = "English",

pages = "158--171",

booktitle = "Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs",

note = "the 7th ACM SIGPLAN International Conference ; Conference date: 08-01-2018 Through 09-01-2018",

}

TY - GEN

T1 - A verified SAT solver with watched literals using imperative HOL

AU - Fleury, Mathias

AU - Blanchette, Jasmin Christian

AU - Lammich, Peter

PY - 2018

Y1 - 2018

N2 - Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.

AB - Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.

U2 - 10.1145/3167080

DO - 10.1145/3167080

M3 - Conference contribution

SP - 158

EP - 171

BT - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

T2 - the 7th ACM SIGPLAN International Conference

Y2 - 8 January 2018 through 9 January 2018

ER -

A verified SAT solver with watched literals using imperative HOL

Abstract

Conference

Access to Document

Fingerprint

Cite this