Abstract
Satisfiability (SAT) solvers—and software in general—sometimes have serious bugs. We mitigate these effects by validating the results. Today’s SAT solvers emit proofs that can be checked with reasonable efficiency. However, these checkers are not trivial and can have bugs as well. We propose to check proofs using a formally verified program that adds little overhead to the overall process of proof validation. We have implemented a sequence of increasingly efficient, verified checkers using the ACL2 theorem proving system, and we discuss lessons from this effort. This work is already being used in industry and is slated for use in the next SAT competition.
This work was supported by NSF under Grant No. CCF-1526760. We thank the reviewers for useful feedback.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Checking a claim of satisfiability is easy.
- 2.
“A Computational Logic for Applicative Common Lisp”.
- 3.
More accurately, first is a macro expanding to a corresponding call of the function car, whose guard specifies that the argument is a pair or the empty list.
- 4.
Thus, stobjs play a role somewhat like monads in higher-order functional languages.
- 5.
- 6.
- 7.
We used ACL2 GitHub commit 639ef8760d30a63e2f21e160cdf02b75e1154fcc and SBCL Version 1.3.15, on a 3.5 GHz Intel(R) Xeon(R) with 32 GB of memory running on Ubuntu Linux.
- 8.
- 9.
The hand proof may be found in a comment near the top of the book satisfiable-add-proof-clause.lisp (see for example community books directory projects/sat/list-based/). That informal proof is annotated with names of lemmas from the actual proof script.
- 10.
The subsidiary correspondence theorems all state equivalences, so the suffix “-equiv” was used in the names of correspondence theorems, even though the top-level theorem, refutation-p-equiv, is actually an implication.
- 11.
The mv-nth expression extracts the returned formula from a multiply-valued result.
- 12.
projects/sat/lrat/incremental/print-formula.lisp in the community books.
References
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, Cham (2016). doi:10.1007/978-3-319-40229-1_4
Boyer, R.S., Moore J S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 9–27. Springer, Heidelberg (2002). doi:10.1007/3-540-45587-6_3
Cruz-Filipe, L., Heule, M.J.H., Hunt Jr., W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNAI, vol. 10395, pp. 220–236. Springer, Cham (2017). doi:10.1007/978-3-319-63046-5_14
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201–215 (1960)
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, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_37
Greve, D.A., Kaufmann, M., Manolios, P., Moore J S., Ray, S., Ruiz-Reina, J.L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1), 15–46 (2008)
Heule, M.J.H., Biere, A.: Clausal proof compression. In: 11th International Workshop on the Implementation of Logics. EPiC Series in Computing, vol. 40, pp. 21–26 (2016)
Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 181–188 (2013)
Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 345–359. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_24
Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_28
Kaufmann, M., Manolios, P., Moore J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)
Kaufmann, M., Moore J S.: Rough diamond: an extension of equivalence-based rewriting. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNAI, vol. 8558, pp. 537–542. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_35
Kaufmann, M.: Modular proof: the fundamental theorem of calculus. In: Kaufmann, M., Manolios, P., Moore J S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. Advances in Formal Methods, vol. 4, pp. 75–91. Springer, Boston (2000). doi:10.1007/978-1-4757-3188-0_6
Kaufmann, M., Moore J S.: ACL2 home page. http://www.cs.utexas.edu/users/moore/acl2. Accessed 2016
Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE 2017. LNAI, vol. 10395, pp. 237–254. Springer, Cham (2017). doi:10.1007/978-3-319-63046-5_15
Lescuyer, S., Conchon, S.: A reflexive formalization of a SAT solver in Coq. In: International Conference on Theorem Proving in Higher Order Logics (TPHOLs) (2008)
Marić, F.: Formalization and implementation of modern SAT solvers. J. Autom. Reason. 43(1), 81–119 (2009)
Marić, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci. 411(50), 4333–4356 (2010)
Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 4, pp. 131–153. IOS Press, Amsterdam (2009)
McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine (part I). CACM 3(4), 184–195 (1960)
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, Heidelberg (2012). doi:10.1007/978-3-642-27940-9_24
Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver. Electron. Notes Theor. Comput. Sci. 269, 3–17 (2011)
Steele Jr., G.L.: Common Lisp the Language, 2nd edn. Digital Press, Burlington (1990)
Swords, S.: Private communication, March/April 2017
Wetzler, N.D., Heule, M.J.H., Hunt Jr., W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 229–244. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_18
Wetzler, N.D., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_31
Wilding, M.: Design goals for ACL2. Tech. Rep. CLI Technical Report 101, Computational Logic, Inc., August 1994. https://www.cs.utexas.edu/users/moore/publications/km94.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Heule, M., Hunt, W., Kaufmann, M., Wetzler, N. (2017). Efficient, Verified Checking of Propositional Proofs. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-66107-0_18
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66106-3
Online ISBN: 978-3-319-66107-0
eBook Packages: Computer ScienceComputer Science (R0)