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 - http://www.scopus.com/inward/record.url?scp=85031905825&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85031905825&partnerID=8YFLogxK
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 -