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

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 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018
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
CountryUnited States
CityLos Angeles
Period8/01/189/01/18

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