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