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

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

36 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	CPP 2018
Subtitle of host publication	Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Place of Publication	New York, NY
Publisher	Association for Computing Machinery, Inc
Pages	158-171
Number of pages	14
ISBN (Electronic)	9781450355865
DOIs	https://doi.org/10.1145/3167080
Publication status	Published - Jan 2018
Event	7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 - Los Angeles, United States Duration: 8 Jan 2018 → 9 Jan 2018

Conference

Conference	7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
Country/Territory	United States
City	Los Angeles
Period	8/01/18 → 9/01/18

Funding

Max Haslbeck, Anders Schlichtkrull, Mark Summerfield, and the anonymous reviewers suggested many textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).

Funders	Funder number
European Union's Horizon 2020 research and innovation program
Horizon 2020 Framework Programme	713999
European Research Council

Keywords

Conflict-driven clause learning (CDCL)
Isabelle/HOL
Sat solving
Stepwise refinement

Access to Document

10.1145/3167080

A verified SAT solver with watched literals using imperative HOLFinal published version, 641 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Copy link address

Cite this

@inproceedings{8bda2d66d76b4ef2bfea9dbfe75bb189,

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

keywords = "Conflict-driven clause learning (CDCL), Isabelle/HOL, Sat solving, Stepwise refinement",

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

year = "2018",

month = jan,

doi = "10.1145/3167080",

language = "English",

pages = "158--171",

booktitle = "CPP 2018",

publisher = "Association for Computing Machinery, Inc",

note = "7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 ; Conference date: 08-01-2018 Through 09-01-2018",

}

Fleury, M, Blanchette, JC & Lammich, P 2018, A verified SAT solver with watched literals using Imperative HOL. in CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, Inc, New York, NY, pp. 158-171, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, United States, 8/01/18. https://doi.org/10.1145/3167080

A verified SAT solver with watched literals using Imperative HOL. / Fleury, Mathias; Blanchette, Jasmin Christian; Lammich, Peter.
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, NY: Association for Computing Machinery, Inc, 2018. p. 158-171.

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

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/1

Y1 - 2018/1

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.

KW - Conflict-driven clause learning (CDCL)

KW - Isabelle/HOL

KW - Sat solving

KW - Stepwise refinement

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

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

U2 - 10.1145/3167080

DO - 10.1145/3167080

M3 - Conference contribution

AN - SCOPUS:85044279547

SP - 158

EP - 171

BT - CPP 2018

PB - Association for Computing Machinery, Inc

CY - New York, NY

T2 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018

Y2 - 8 January 2018 through 9 January 2018

ER -

A verified SAT solver with watched literals using Imperative HOL

Abstract

Conference

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this