×

versat: a verified modern SAT solver. (English) Zbl 1326.68263

Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 363-378 (2012).
Summary: 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.
For the entire collection see [Zbl 1236.68007].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

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) · Zbl 1291.68318
[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) · Zbl 05587935 · doi:10.1007/978-3-642-02959-2_12
[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) · Zbl 1306.68155 · doi:10.1007/978-3-642-14186-7_6
[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) · Zbl 0985.68038 · doi:10.1023/A:1011276507260
[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) · doi:10.1145/1292535.1292541
[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) · Zbl 05776718 · doi:10.1007/978-3-642-14808-8_18
[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) · Zbl 1165.03320
[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) · doi:10.1109/FMCAD.2008.ECP.19
[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) · doi:10.1145/1629575.1629596
[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)
[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) · Zbl 1369.68124 · doi:10.1145/1111037.1111042
[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] Marić, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci. 411, 4333–4356 (2010) · Zbl 1208.68205 · doi:10.1016/j.tcs.2010.09.014
[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) · Zbl 1272.68362 · doi:10.1016/j.entcs.2005.12.005
[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) · Zbl 1134.68492 · doi:10.1007/978-3-540-78800-3_38
[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) · doi:10.1145/1670412.1670414
[18] Shankar, N., Vaucher, M.: The mechanical verification of a dpll-based satisfiability solver. Electr. Notes Theor. Comput. Sci. 269, 3–17 (2011) · Zbl 1347.68307 · doi:10.1016/j.entcs.2011.03.002
[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) · doi:10.1145/1707790.1707796
[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)
[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) · Zbl 1140.68357 · doi:10.1016/j.scico.2007.07.008
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.