Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2017: Automated Deduction – CADE 26 pp 220–236Cite as

Efficient Certified RAT Verification

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10395))

Abstract

Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.

Supported by the National Science Foundation under grant CCF-1526760 and by the Danish Council for Independent Research, Natural Sciences, grant DFF-1323-00247.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    see http://satcompetition.org.

  2. 2.

    DRAT proofs and LRAT proofs are syntactic objects that do not necessarily represent valid proofs. However, they are produced by tools that should only generate objects that correspond to semantically valid proofs, so we adopt this terminology. By “validating a DRAT/LRAT proof”, we mean verifying by independent means that such an object indeed represents a valid proof.

  3. 3.

    With the exception of integers, which are only used as labels and therefore can be extracted to a native type without compromising soundness of the extracted code.

  4. 4.

    Termination seems to occur due to an error condition of the underlying LISP runtime system (CCL) used, and could not be reproduced using another system (SBCL).

References

  1. ACL2 Community. ACL2 documentation topic: FAST-ALISTS. http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____FAST-ALISTS

  2. ACL2 Community. ACL2 documentation topic: STOBJ. http://www.cs.utexas.edu/users/moore/acl2/v7-2/manual/?topic=ACL2____STOBJ

  3. ACL2 Community. ACL2 system and libraries on GitHub. https://github.com/acl2/acl2/

  4. ACL2 LRAT checker. https://github.com/acl2/acl2/tree/master/books/projects/sat/lrat/

  5. Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science 404(3), 256–274 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. Balyo, T., Heule, M.J.H., Järvisalo, M.: Sat competition 2016: Recent developments. In: AAAI 2017 (2017)

    Google Scholar 

  7. 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 (LNAI), vol. 9706, pp. 25–44. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_4

    Google Scholar 

  8. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

  9. Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001). doi:10.1007/3-540-44585-4_43

    Chapter  Google Scholar 

  10. The Coq proof assistant. https://coq.inria.fr/

  11. Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: \(KR\tilde{O}\) 1996, pp. 148–159. Morgan Kaufmann (1996)

    Google Scholar 

  12. Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118–135. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54577-5_7

    Chapter  Google Scholar 

  13. Cryptominisat v5. http://baldur.iti.kit.edu/sat-competition-2016/solvers/main/cmsat5_main2.zip

  14. Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 260–274. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14808-8_18

    Chapter  Google Scholar 

  15. Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10886–10891 (2003)

    Google Scholar 

  16. Heule, M.J.H.: The DRAT format and DRAT-trim checker. CoRR, abs/1610.06229 (2016). Source code, https://github.com/marijnheule/drat-trim

  17. Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All about Proofs, Proofs for All (APPA), July 2014. http://www.easychair.org/smart-program/VSL2014/APPA-index.html

  18. Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Trimming while checking clausal proofs. In: FMCAD, pp. 181–188 (2013)

    Google Scholar 

  19. Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test., Verif. Reliab. 24(8), 593–607 (2014)

    Google Scholar 

  20. Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591–606. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_40

    Chapter  Google Scholar 

  21. Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228–245. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_15

    Google Scholar 

  22. Kaufmann, M., Moore, J S.: An industrial strength theorem prover for a logic based on common LISP. IEEE Trans. Softw. Eng. 23(4), 203–213 (1997)

    Google Scholar 

  23. Lammich, P.: Efficient verified (UN)SAT certificate checking. In: CADE-26. LNCS. Springer (to appear, 2017)

    Google Scholar 

  24. Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008). doi:10.1007/978-3-540-69407-6_39

    Chapter  Google Scholar 

  25. Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 102–117. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39611-3_14

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  27. Maric, F., Janicic, P.: Formalization of abstract state transition systems for SAT. Logical Methods in Comput. Sci. 7(3) (2011)

    Google Scholar 

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

    MATH  Google Scholar 

  29. Van Gelder, A.: Producing and verifying extremely large propositional refutations - have your cake and eat it too. Ann. Math. Artif. Intell. 65(4), 329–372 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  30. 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

    Chapter  Google Scholar 

  31. 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

    Google Scholar 

  32. Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE, pp. 10880–10885 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark

    Luís Cruz-Filipe & Peter Schneider-Kamp

  2. Department of Computer Science, The University of Texas at Austin, Austin, USA

    Marijn J. H. Heule, Warren A. Hunt Jr. & Matt Kaufmann

Authors
  1. Luís Cruz-Filipe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marijn J. H. Heule
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Warren A. Hunt Jr.
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Matt Kaufmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luís Cruz-Filipe .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P. (2017). Efficient Certified RAT Verification. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63046-5_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63045-8

  • Online ISBN: 978-3-319-63046-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation