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

J.C. Blanchette, Mathias Fleury, Christoph Weidenbach

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

125 Downloads (Pure)

Abstract

We developed a formal framework for CDCL (conflict-driven clause learning) in Isabelle/HOL. Through a chain of refinements, an abstract CDCL calculus is connected to a SAT solver expressed in a functional programming language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants. Compared with earlier SAT solver verifications, the main novelties are the inclusion of rules for forget, restart, and incremental solving and the application of refinement.
Original languageEnglish
Title of host publicationAutomated Reasoning - 8th International Joint Conference
Subtitle of host publicationIJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings
PublisherSpringer
Pages25-44
ISBN (Print)978-3-319-40228-4
DOIs
Publication statusPublished - 2016
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9706

Fingerprint

Dive into the research topics of 'A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality'. Together they form a unique fingerprint.

Cite this