article

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Authors:

Jasmin Christian Blanchette,

Mathias Fleury,

Christoph WeidenbachAuthors Info & Claims

Journal of Automated Reasoning, Volume 61, Issue 1-4

Pages 333 - 365

https://doi.org/10.1007/s10817-018-9455-7

Published: 01 June 2018 Publication History

Abstract

We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solver expressed in a functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis---Putnam---Logemann---Loveland (DPLL) calculus. The imperative program relies on the two-watched-literal data structure and other optimizations found in modern solvers. We used Isabelle's Refinement Framework to automate the most tedious refinement steps. The most noteworthy aspects of our work are the inclusion of rules for forget, restart, and incremental solving and the application of stepwise refinement.

References

[1]

Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 19---99. Elsevier, Amsterdam (2001)

[2]

Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123---153 (2014)

Digital Library

[3]

Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Freuder, E.C. (ed.) CP96. LNCS, vol. 1118, pp. 46---60. Springer, Berlin (1996)

Digital Library

[4]

Becker, H., Blanchette, J.C., Fleury, M., From, A.H., Jensen, A.B., Lammich, P., Larsen, J.B., Michaelis, J., Nipkow, T., Popescu, A., Schlichtkrull, A., Tourret, S., Traytel, D., Villadsen, J.: IsaFoL: Isabelle Formalization of Logic. https://bitbucket.org/isafol/isafol/. Accessed 13 Feb 2018

[5]

Biere, A., Fröhlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 5584, pp. 237---243. Springer, Berlin (2015)

[6]

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)

Digital Library

[7]

Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109---128 (2013)

[8]

Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12---27. Springer, Berlin (2011)

Digital Library

[9]

Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 245---260. Springer, Berlin (2013)

[10]

Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. 56(2), 155---200 (2016)

Digital Library

[11]

Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 25---44. Springer, Berlin (2016)

Digital Library

[12]

Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149---179 (2017)

Digital Library

[13]

Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179---194. Springer, Berlin (2010)

Digital Library

[14]

Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134---149. Springer, Berlin (2008)

Digital Library

[15]

Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56---68 (1940)

[16]

Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE-26. LNCS, vol. 10395, pp. 220---236. Springer, Berlin (2017)

[17]

Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394---397 (1962)

Digital Library

[18]

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502---518. Springer, Berlin (2003)

[19]

Fleury, M.: Formalisation of Ground Inference Systems in a Proof Assistant. M.Sc. thesis, École normale supérieure de Rennes (2015). https://www.mpi-inf.mpg.de/fileadmin/inf/rg1/Documents/fleury_master_thesis.pdf. Accessed 13 Feb 2018

[20]

Fleury, M., Blanchette, J.C.: Formalization of Weidenbach's Automated Reasoning--The Art of Generic Problem Solving (2017). https://bitbucket.org/isafol/isafol/src/master/Weidenbach_Book/README.md, Formal proof development. Accessed 13 Feb 2018

[21]

Goel, A., Grundy, J.: Decision Procedure Toolkit. http://dpt.sourceforge.net/. Accessed 13 Feb 2018

[22]

Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer, Berlin (1979)

[23]

Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103---117. Springer, Berlin (2010)

Digital Library

[24]

Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs '98. LNCS, vol. 1479, pp. 153---170. Springer, Berlin (1998)

Digital Library

[25]

Kammüller, F., Wenzel, M., Paulson, L.C.: Locales--a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs '99. LNCS, vol. 1690, pp. 149---166. Springer, Berlin (1999)

Digital Library

[26]

Knuth, D.E.: The Art of Computer Programming, vol. 4, Fascicle 6: Satisfiability. Addison-Wesley, Boston (2015)

Digital Library

[27]

Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 589---603. Springer, Berlin (2006)

Digital Library

[28]

Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS, vol. 4720, pp. 1---27. Springer, Berlin (2007)

Digital Library

[29]

Lammich, P.: The Imperative Refinement Framework. Archive of Formal Proofs 2016. http://isa-afp.org/entries/Refine_Imperative_HOL.shtml, Formal proof development. Accessed 13 Feb 2018

[30]

Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84---99. Springer, Berlin (2013)

Digital Library

[31]

Lammich, P.: Refinement to imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253---269. Springer, Berlin (2015)

[32]

Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 27---36. ACM, New York (2016)

Digital Library

[33]

Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE-26. LNCS, vol. 10395, pp. 237---254. Springer, Berlin (2017)

[34]

Lescuyer, S.: Formalizing and implementing a reflexive tactic for automated deduction in Coq. Ph.D. thesis, Université Paris-Sud (2011)

[35]

Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173---180 (1993)

Digital Library

[36]

Margetson, J., Ridge, T.: Completeness theorem. Archive of Formal Proofs 2004. http://isa-afp.org/entries/Completeness.shtml, Formal proof development. Accessed 13 Feb 2018

[37]

Marić, F.: Formal verification of modern SAT solvers. Archive of Formal Proofs 2008. http://isa-afp.org/entries/SATSolverVerification.shtml, Formal proof development. Accessed 13 Feb 2018

[38]

Marić, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci. 411(50), 4333---4356 (2010)

Digital Library

[39]

Marić, F., Janiă?ić, P.: Formalization of abstract state transition systems for SAT. Log. Methods Comput. Sci. 7(3) (2011).

[40]

Marques-Silva, J.P., Sakallah, K.A.: GRASP---a new search algorithm for satisfiability. In: ICCAD '96, pp. 220---227. IEEE Computer Society Press, Silver Spring (1996)

Digital Library

[41]

Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mech. Math. Appl. 4(1), 3---24 (2005)

[42]

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC 2001, pp. 530---535. ACM, New York (2001)

Digital Library

[43]

Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis---Putnam---Logemann---Loveland procedure to DPLL(T). J. ACM 53(6), 937---977 (2006)

Digital Library

[44]

Nipkow, T.: Teaching semantics with a proof assistant: no more LSD trip proofs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 24---38. Springer, Berlin (2012)

Digital Library

[45]

Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, Berlin (2014)

Digital Library

[46]

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002)

Digital Library

[47]

Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: a verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012, LNCS, vol. 7148, pp. 363---378. Springer, Berlin (2012)

Digital Library

[48]

Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC, vol. 2, pp. 1---11. EasyChair (2012)

[49]

Pierce, B.C.: Lambda, the ultimate TA: using a proof assistant to teach programming language foundations. In: Hutton, G., Tolmach, A.P. (eds.) ICFP 2009, pp. 121---122. ACM, New York (2009)

Digital Library

[50]

Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) FMCAD 2014, pp. 195---202. IEEE Computer Society Press, Silver Spring (2014)

Digital Library

[51]

Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 341---357. Springer, Berlin (2016)

[52]

Shankar, N.: Metamathematics, Machines, and Gödel's Proof, Cambridge Tracts in Theoretical Computer Science, vol. 38. Cambridge University Press, Cambridge (1994)

Digital Library

[53]

Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver. Electr. Notes Theor. Comput. Sci. 269, 3---17 (2011)

[54]

Sörensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 9340, pp. 237---243. Springer, Berlin (2009)

Digital Library

[55]

Sternagel, C., Thiemann, R.: An Isabelle/HOL formalization of rewriting for certified termination analysis. http://cl-informatik.uibk.ac.at/software/ceta/. Accessed 13 Feb 2018

[56]

Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696---710. Springer, Berlin (2014)

Digital Library

[57]

Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday. LNCS, vol. 9360, pp. 172---188. Springer, Berlin (2015)

[58]

Wenzel, M.: Isabelle/Isar--a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23). University of Białystok (2007)

[59]

Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221 (1971)

Digital Library

[60]

Woodcock, J., Banach, R.: The verification grand challenge. J. Univers. Comput. Sci. 13(5), 661---668 (2007)

Cited By

Azar KKamali HFarahmandi FTehranipoor M(2024)Improving Bounded Model Checkers Scalability for Circuit De-Obfuscation: An ExplorationIEEE Transactions on Information Forensics and Security10.1109/TIFS.2024.335728619(2771-2785)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1109/TIFS.2024.3357286
From AJacobsen F(2024)Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09697-368:3Online publication date: 27-Jun-2024
https://dl.acm.org/doi/10.1007/s10817-024-09697-3
Bromberger MDesharnais MWeidenbach C(2023)An Isabelle/HOL Formalization of the SCL(FOL) CalculusAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_7(116-133)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38499-8_7
Show More Cited By

Index Terms

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Index terms have been assigned to the content through auto-classification.

Recommendations

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
Proceedings of the 8th International Joint Conference on Automated Reasoning - Volume 9706

We developed a formal framework for CDCL conflict-driven clause learning in Isabelle/HOL. Through a chain of refinements, an abstract CDCL calculus is connected to a SAT solver expressed in a functional programming language, with total correctness ...
A verified SAT solver framework with learn, forget, restart and incrementality
IJCAI'17: Proceedings of the 26th International Joint Conference on Artificial Intelligence

We developed a formal framework for SAT solving using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL (conflict-driven clause learning) calculus is connected to a SAT solver that always terminates with correct answers. ...
A modular CNF-based SAT solver
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system design

The state-of-the-art SAT solvers, such as Chaff [11], zChaff [18], BerkMin [5], and Minisat [2] usually share the same core techniques, for instance: the watched literals structures conflict clause recording and non-chronological backtracking. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 61, Issue 1-4

June 2018

547 pages

ISSN:0168-7433

Issue’s Table of Contents

Copyright © Copyright © 2018 Springer Science+Business Media B.V., part of Springer Nature.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 June 2018

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Azar KKamali HFarahmandi FTehranipoor M(2024)Improving Bounded Model Checkers Scalability for Circuit De-Obfuscation: An ExplorationIEEE Transactions on Information Forensics and Security10.1109/TIFS.2024.335728619(2771-2785)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1109/TIFS.2024.3357286
From AJacobsen F(2024)Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-024-09697-368:3Online publication date: 27-Jun-2024
https://dl.acm.org/doi/10.1007/s10817-024-09697-3
Bromberger MDesharnais MWeidenbach C(2023)An Isabelle/HOL Formalization of the SCL(FOL) CalculusAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_7(116-133)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38499-8_7
Fleury MLammich P(2023)A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)Automated Deduction – CADE 2910.1007/978-3-031-38499-8_12(207-219)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38499-8_12
Seisenberger Mter Beek MFan XFerrari AHaxthausen AJames PLawrence ALuttik Bvan de Pol JWimmer S(2022)Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in RailwayLeveraging Applications of Formal Methods, Verification and Validation. Practice10.1007/978-3-031-19762-8_20(246-268)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19762-8_20
Tourret SBlanchette JHriţcu CPopescu A(2021)A modular Isabelle framework for verifying saturation proversProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439912(224-237)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439912
Iordache VCiobâcă Ş(2021)Verifying the Conversion into CNF in DafnyLogic, Language, Information, and Computation10.1007/978-3-030-88853-4_10(150-166)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88853-4_10
Schlichtkrull ABlanchette JTraytel DWaldmann U(2020)Formalizing Bachmair and Ganzinger’s Ordered Resolution ProverJournal of Automated Reasoning10.1007/s10817-020-09561-064:7(1169-1195)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10817-020-09561-0
Schlichtkrull ABlanchette JTraytel DMahboubi AMyreen M(2019)A verified prover based on ordered resolutionProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294100(152-165)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294100
Blanchette JMahboubi AMyreen M(2019)Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294087(1-13)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294087
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents