Article

versat: a verified modern SAT solver

Authors:

Kevin ClancyAuthors Info & Claims

VMCAI'12: Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation

Pages 363 - 378

https://doi.org/10.1007/978-3-642-27940-9_24

Published: 22 January 2012 Publication History

Abstract

This paper presents versat, a formally verified SAT solver incorporating the essential features of modern SAT solvers, including clause learning, watched literals, optimized conflict analysis, non-chronological backtracking, and decision heuristics. Unlike previous related work on SAT-solver verification, our implementation uses efficient low-level data structures like mutable C arrays for clauses and other solver state, and machine integers for literals. The implementation and proofs are written in Guru, a verified-programming language. We compare versat to a state-of-the-art SAT solver that produces certified "unsat" answers. We also show through an empirical evaluation that versat can solve SAT problems on the modern scale.

References

[1]

Altenkirch, T.: Integrated verification in Type Theory. Lecture notes for a course at ESSLLI 1996, Prague (1996); Available from the author's website.

[2]

Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification, pp. 83-98 (2010).

Digital Library

[3]

Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: An Open, Trustable and Efficient SMT-Solver. In: Schmidt, R.A. (ed.) CADE-22 2009. LNCS, vol. 5663, pp. 151-156. Springer, Heidelberg (2009).

Digital Library

[4]

Brummayer, R., Lonsing, F., Biere, A.: Automated Testing and Debugging of SAT and QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44-57. Springer, Heidelberg (2010).

Digital Library

[5]

Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7-34 (2001).

Digital Library

[6]

Conchon, S., Filliâtre, J.-C.: A persistent union-find data structure. In: Proceedings of the 2007 Workshop on Workshop on ML, pp. 37-46. ACM (2007).

Digital Library

[7]

Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking. In: Cavalcanti, A., Déharbe, D., Gaudel, M.-C.,Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 260-274. Springer, Heidelberg (2010).

Digital Library

[8]

de Moura, L., Bjørner, N.: Proofs and Refutations, and Z3. In: Konev, B., Schmidt, R., Schulz, S. (eds.) 7th International Workshop on the Implementation of Logics, IWIL (2008).

[9]

Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Cimatti, A., Jones, R. (eds.) Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design, Portland, Oregon, pp. 109-117. IEEE (2008).

Digital Library

[10]

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Matthews, J., Anderson, T. (eds.) Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pp. 207-220. ACM (2009).

Digital Library

[11]

Kothari, N.,Millstein, T., Govindan, R.: Deriving state machines from tinyos programs using symbolic execution. In: Proceedings of the 7th International Conference on Information Processing in Sensor Networks, IPSN 2008, pp. 271-282. IEEE Computer Society,Washington, DC (2008).

Digital Library

[12]

Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In:Morrisett, G., Peyton Jones, S. (eds.) 33rd ACM Symposium on Principles of Programming Languages, pp. 42-54. ACM Press (2006).

Digital Library

[13]

Lescuyer, S., Conchon, S.: A Reflexive Formalization of a SAT Solver in Coq. In: Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs (2008).

[14]

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

Digital Library

[15]

McLaughlin, S., Barrett, C., Ge, Y.: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. Electr. Notes Theor. Comput. Sci. 144(2), 43-51 (2006).

Digital Library

[16]

Moskal, M.: Rocket-Fast Proof Checking for SMT Solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486-500. Springer, Heidelberg (2008).

Digital Library

[17]

Oe, D., Reynolds, A., Stump, A.: Fast and Flexible Proof Checking for SMT. In: Dutertre, B., Strichman, O. (eds.) Workshop on Satisfiability Modulo Theories, SMT (2009).

Digital Library

[18]

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

Digital Library

[19]

Stump, A., Austin, E.: Resource Typing in Guru. In: Filliâtre, J.-C., Flanagan, C. (eds.) Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, pp. 27-38. ACM (2010).

Digital Library

[20]

Stump, A., Deters, M., Petcher, A., Schiller, T., Simpson, T.: Verified Programming in Guru. In: Altenkirch, T., Millstein, T. (eds.) Programming Languges meets Program Verification, PLPV (2009).

Digital Library

[21]

Xian, F., Srisa-an, W., Jiang, H.: Garbage collection: Java application servers' Achilles heel. Science of Computer Programming 70(2-3), 89-110 (2008).

Digital Library

Cited By

Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 19-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-40247-0_15
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
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
Show More Cited By

Index Terms

versat: a verified modern SAT solver

Recommendations

On stateless multihead automata: Hierarchies and the emptiness problem

We look at stateless multihead finite automata in their two-way and one-way, deterministic and nondeterministic variations. The transition of a k-head automaton depends solely on the symbols currently scanned by its k heads, and every such transition ...
Pebble alternating tree-walking automata and their recognizing power

Pebble tree-walking automata with alternation were first investigated by Milo, Suciu and Vianu (2003), who showed that tree languages recognized by these devices are exactly the regular tree languages. We strengthen this by proving the same result for ...
Closure properties and descriptional complexity of deterministic regular expressions

We study the descriptional complexity of regular languages that are definable by deterministic regular expressions, i.e., we examine worst-case blow-ups in size when translating between different representations for such languages. As representations of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

VMCAI'12: Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation

January 2012

461 pages

ISBN:9783642279393

Editors:
Viktor Kuncak
Swiss Federal Institute of Technology Lausanne (EPFL), IC IIF LARA INR 318, Station 14, Lausanne, Switzerland
,
Andrey Rybalchenko
Institut für Informatik, Technische Universität München, Boltzmannstr. 3, Munich, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 January 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 19-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-40247-0_15
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
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
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
Fleury MBlanchette JLammich PAndronick JFelty A(2018)A verified SAT solver with watched literals using imperative HOLProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167080(158-171)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167080
Blanchette JFleury MLammich PWeidenbach C(2018)A Verified SAT Solver Framework with Learn, Forget, Restart, and IncrementalityJournal of Automated Reasoning10.1007/s10817-018-9455-761:1-4(333-365)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-018-9455-7
Blanchette JFleury MWeidenbach C(2017)A verified SAT solver framework with learn, forget, restart and incrementalityProceedings of the 26th International Joint Conference on Artificial Intelligence10.5555/3171837.3171958(4786-4790)Online publication date: 19-Aug-2017
https://dl.acm.org/doi/10.5555/3171837.3171958
Weitz KLyubomirsky SHeule STorlak EErnst MTatlock Z(2017)SpaceSearch: a library for building and verifying solver-aided toolsProceedings of the ACM on Programming Languages10.1145/31102691:ICFP(1-28)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110269
Heule MHunt WKaufmann MWetzler N(2017)Efficient, Verified Checking of Propositional ProofsInteractive Theorem Proving10.1007/978-3-319-66107-0_18(269-284)Online publication date: 26-Sep-2017
https://dl.acm.org/doi/10.1007/978-3-319-66107-0_18
Mebsout ATinelli CPiskac RTalupur M(2016)Proof certificates for SMT-based model checkers for infinite-state systemsProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077652(117-124)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077652
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents