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

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 publication26th International Joint Conference on Artificial Intelligence, IJCAI 2017
EditorsCarles Sierra
PublisherInternational Joint Conferences on Artificial Intelligence, AAAI Press
Pages4786-4790
Number of pages5
ISBN (Electronic)9780999241103
DOIs
Publication statusPublished - 1 Jan 2017
Event26th International Joint Conference on Artificial Intelligence, IJCAI 2017 - Melbourne, Australia
Duration: 19 Aug 201725 Aug 2017

Conference

Conference26th International Joint Conference on Artificial Intelligence, IJCAI 2017
CountryAustralia
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