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

Jasmin Christian Blanchette; Mathias Fleury; Christoph Weidenbach

doi:10.24963/ijcai.2017/667

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 proceeding › Conference contribution › Academic › peer-review

18 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 language	English
Title of host publication	Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017
Editors	Carles Sierra
Publisher	International Joint Conferences on Artificial Intelligence, AAAI Press
Pages	4786-4790
Number of pages	5
ISBN (Electronic)	9780999241103
DOIs	https://doi.org/10.24963/ijcai.2017/667
Publication status	Published - 2017
Event	26th International Joint Conference on Artificial Intelligence, IJCAI 2017 - Melbourne, Australia Duration: 19 Aug 2017 → 25 Aug 2017

Publication series

Name	IJCAI International Joint Conference on Artificial Intelligence
Volume	0
ISSN (Print)	1045-0823

Conference

Conference	26th International Joint Conference on Artificial Intelligence, IJCAI 2017
Country/Territory	Australia
City	Melbourne
Period	19/08/17 → 25/08/17

Funding

We thank everyone who helped us with the conference version of this paper. This work has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).

Funders	Funder number
Horizon 2020
European Research Council
Horizon 2020 Framework Programme	713999

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 10 Reduced Inequalities

Access to Document

10.24963/ijcai.2017/667

A Verified SAT Solver Framework with Learn, Forget, Restart, and IncrementalityFinal published version, 104 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Blanchette, J. C., Fleury, M., & Weidenbach, C. (2017). A verified SAT solver framework with learn, forget, restart, and incrementality. In C. Sierra (Ed.), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017 (pp. 4786-4790). (IJCAI International Joint Conference on Artificial Intelligence; Vol. 0). International Joint Conferences on Artificial Intelligence, AAAI Press. https://doi.org/10.24963/ijcai.2017/667

Blanchette, Jasmin Christian ; Fleury, Mathias ; Weidenbach, Christoph. / A verified SAT solver framework with learn, forget, restart, and incrementality. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017. editor / Carles Sierra. International Joint Conferences on Artificial Intelligence, AAAI Press, 2017. pp. 4786-4790 (IJCAI International Joint Conference on Artificial Intelligence).

@inproceedings{9797d7e995504912a1d6aaa1bda18608,

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

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.",

author = "Blanchette, \{Jasmin Christian\} and Mathias Fleury and Christoph Weidenbach",

year = "2017",

doi = "10.24963/ijcai.2017/667",

language = "English",

series = "IJCAI International Joint Conference on Artificial Intelligence",

publisher = "International Joint Conferences on Artificial Intelligence, AAAI Press",

pages = "4786--4790",

editor = "Carles Sierra",

booktitle = "Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017",

note = "26th International Joint Conference on Artificial Intelligence, IJCAI 2017 ; Conference date: 19-08-2017 Through 25-08-2017",

}

Blanchette, JC, Fleury, M & Weidenbach, C 2017, A verified SAT solver framework with learn, forget, restart, and incrementality. in C Sierra (ed.), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017. IJCAI International Joint Conference on Artificial Intelligence, vol. 0, International Joint Conferences on Artificial Intelligence, AAAI Press, pp. 4786-4790, 26th International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19/08/17. https://doi.org/10.24963/ijcai.2017/667

A verified SAT solver framework with learn, forget, restart, and incrementality. / Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017. ed. / Carles Sierra. International Joint Conferences on Artificial Intelligence, AAAI Press, 2017. p. 4786-4790 (IJCAI International Joint Conference on Artificial Intelligence; Vol. 0).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Blanchette, Jasmin Christian

AU - Fleury, Mathias

AU - Weidenbach, Christoph

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85031905825

UR - https://www.scopus.com/pages/publications/85031905825#tab=citedBy

UR - https://www.ijcai.org/proceedings/2017/

U2 - 10.24963/ijcai.2017/667

DO - 10.24963/ijcai.2017/667

M3 - Conference contribution

AN - SCOPUS:85031905825

T3 - IJCAI International Joint Conference on Artificial Intelligence

SP - 4786

EP - 4790

BT - Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017

A2 - Sierra, Carles

PB - International Joint Conferences on Artificial Intelligence, AAAI Press

T2 - 26th International Joint Conference on Artificial Intelligence, IJCAI 2017

Y2 - 19 August 2017 through 25 August 2017

ER -

Blanchette JC, Fleury M, Weidenbach C. A verified SAT solver framework with learn, forget, restart, and incrementality. In Sierra C, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017. International Joint Conferences on Artificial Intelligence, AAAI Press. 2017. p. 4786-4790. (IJCAI International Joint Conference on Artificial Intelligence). doi: 10.24963/ijcai.2017/667

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

Abstract

Publication series

Conference

Funding

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this