A verified SAT solver with watched literals using Imperative HOL

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

12 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 languageEnglish
Title of host publicationCPP 2018
Subtitle of host publicationProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery, Inc
Pages158-171
Number of pages14
ISBN (Electronic)9781450355865
DOIs
Publication statusPublished - Jan 2018
Event7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 - Los Angeles, United States
Duration: 8 Jan 20189 Jan 2018

Conference

Conference7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
Country/TerritoryUnited States
CityLos Angeles
Period8/01/189/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).

FundersFunder number
European Union's Horizon 2020 research and innovation program
Horizon 2020 Framework Programme713999
European Research Council

    Keywords

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

    Fingerprint

    Dive into the research topics of 'A verified SAT solver with watched literals using Imperative HOL'. Together they form a unique fingerprint.

    Cite this