A verified SAT solver framework with learn, forget, restart, and incrementality

Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach

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

5 Downloads (Pure)

Abstract

We developed a formal framework for SAT solving using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL (conflictdriven clause learning) calculus is connected to a SAT solver that always terminates with correct answers. The framework offers a convenient way to prove theorems about the SAT solver and experiment with variants of the calculus. Compared with earlier verifications, the main novelties are the inclusion of the CDCL rules for forget, restart, and incremental solving and the use of refinement.

Original languageEnglish
Title of host publicationProceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017
EditorsCarles Sierra
PublisherInternational Joint Conferences on Artificial Intelligence, AAAI Press
Pages4786-4790
Number of pages5
ISBN (Electronic)9780999241103
DOIs
Publication statusPublished - 2017
Event26th International Joint Conference on Artificial Intelligence, IJCAI 2017 - Melbourne, Australia
Duration: 19 Aug 201725 Aug 2017

Publication series

NameIJCAI International Joint Conference on Artificial Intelligence
Volume0
ISSN (Print)1045-0823

Conference

Conference26th International Joint Conference on Artificial Intelligence, IJCAI 2017
Country/TerritoryAustralia
CityMelbourne
Period19/08/1725/08/17

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