Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2017: Automated Deduction – CADE 26 pp 237–254Cite as

Efficient Verified (UN)SAT Certificate Checking

  • Conference paper
  • First Online:

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

Abstract

We present an efficient formally verified checker for satisfiability and unsatisfiability certificates for Boolean formulas in conjunctive normal form. It utilizes a two phase approach: Starting from a DRAT certificate, the unverified generator computes an enriched certificate, which is checked against the original formula by the verified checker.

Using the Isabelle/HOL Refinement Framework, we verify the actual implementation of the checker, specifying the semantics of the formula down to the integer sequence that represents it.

On a realistic benchmark suite drawn from the 2016 SAT competition, our approach is more than two times faster than the unverified standard tool drat-trim. Additionally, we implemented a multi-threaded version of the generator, which further reduces the runtime.

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.

    Unfortunately, the available version history of drat-trim [9] only dates back to October 2016. We can only speculate whether the discovered bugs were present in the versions used for the 2014 and 2016 SAT competitions.

  2. 2.

    However, we expect that most of our optimizations can be transferred to their tools.

  3. 3.

    Our profiling data indicates that, depending on the problem, up to 93% of the time is spent for unit propagation.

  4. 4.

    Blocked lemmas are useless for unsat proofs, such that there is no point to include them into the certificate.

  5. 5.

    The name suffix instead of indicates that the data structure may be stored on the heap.

  6. 6.

    Element 0 is used as a guard in our implementation.

  7. 7.

    The current version at the time of writing this paper.

References

  1. Back, R.-J.: On the correctness of refinement steps in program development. Ph.D. thesis, Department of Computer Science, University of Helsinki (1978)

    Google Scholar 

  2. Back, R.-J., von Wright, J.: Refinement Calculus - A Systematic Introduction. Springer, New York (1998)

    Book  MATH  Google Scholar 

  3. Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art the Calculus of Inductive Constructions, 1st edn. Springer, New York (2010)

    Google Scholar 

  4. Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 307–321. Springer, Cham (2016). doi:10.1007/978-3-319-40648-0_23

    Chapter  Google Scholar 

  5. Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71067-7_14

    Chapter  Google Scholar 

  6. Cruz-Filipe, L., Heule, M., Hunt, W., Matt, K., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNAI, vol. 10395, pp. 220–236. Springer, Cham (2017)

    Google Scholar 

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

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

  9. DRAT-TRIM GitHub repository. https://github.com/marijnheule/drat-trim

  10. DRAT-TRIM homepage. https://www.cs.utexas.edu/~marijn/drat-trim/

  11. DRAT-TRIM issue tracker. https://github.com/marijnheule/drat-trim/issues

  12. Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463–478. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_31

    Chapter  Google Scholar 

  13. Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of DATE. IEEE (2003)

    Google Scholar 

  14. Gordon, M.: From LCF to HOL: a short history. In: Proof, Language, and Interaction, pp. 169–185. MIT Press (2000)

    Google Scholar 

  15. Haftmann, F.: Code generation from specifications in higher order logic. Ph.D. thesis, Technische Universität München (2009)

    Google Scholar 

  16. Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_10

    Chapter  Google Scholar 

  17. 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, Heidelberg (2010). doi:10.1007/978-3-642-12251-4_9

    Chapter  Google Scholar 

  18. Heule, M., Hunt, W., Wetzler, N.: Trimming while checking clausal proofs. In: 2013 Formal Methods in Computer-Aided Design, FMCAD 2013, pp. 181–188. IEEE (2013)

    Google Scholar 

  19. Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of POPL, pp. 179–192. ACM (2014)

    Google Scholar 

  20. Lammich, P.: Grat tool chain homepage. http://www21.in.tum.de/lammich/grat/

  21. Lammich, P.: Gratchk proof outline. http://www21.in.tum.de/lammich/grat/outline.pdf

  22. Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84–99. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_9

    Chapter  Google Scholar 

  23. Lammich, P.: Verified efficient implementation of gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 325–340. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_21

    Google Scholar 

  24. Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253–269. Springer, Cham (2015). doi:10.1007/978-3-319-22102-1_17

    Google Scholar 

  25. Lammich, P.: Refinement based verification of imperative data structures. In: CPP, pp. 27–36. ACM (2016)

    Google Scholar 

  26. Lammich, P., Lochbihler, A.: The isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339–354. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_24

    Chapter  Google Scholar 

  27. Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: CPP 2015, pp. 137–146. ACM, New York (2015)

    Google Scholar 

  28. Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 219–234. Springer, Cham (2016). doi:10.1007/978-3-319-43144-4_14

    Chapter  Google Scholar 

  29. Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166–182. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32347-8_12

    Chapter  Google Scholar 

  30. Milner, R., Harper, R., MacQueen, D., Tofte, M.: The Definition of Standard ML. MIT Press, Cambridge (1997)

    Google Scholar 

  31. MLton Standard ML compiler. http://mlton.org/

  32. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC, pp. 530–535. ACM (2001)

    Google Scholar 

  33. Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2–3), 284–315 (2014)

    Article  MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

  35. SAT competition (2013). http://satcompetition.org/2013/

  36. SAT competition (2014). http://satcompetition.org/2014/

  37. Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, vol. B-2016-1. University of Helsinki (2016)

    Google Scholar 

  38. SAT competition (2016). http://baldur.iti.kit.edu/sat-competition-2016/

  39. Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600–611. Springer, Heidelberg (2006). doi:10.1007/11753728_60

    Chapter  Google Scholar 

  40. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02777-2_24

    Chapter  Google Scholar 

  41. Wetzler, N., Heule, M.J.H., Hunt, 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 

  42. Wetzler, N., Heule, M.J.H., Hunt, 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 

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

    Article  MATH  Google Scholar 

Download references

Acknowledgements

We thank Jasmin Blanchette and Mathias Fleury for very useful comments on the draft version of this paper, and Lars Hupel for instant help on any problems related to the benchmark server.

Author information

Authors and Affiliations

  1. Technische Universität München, Munich, Germany

    Peter Lammich

Authors
  1. Peter Lammich
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Lammich .

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

Lammich, P. (2017). Efficient Verified (UN)SAT Certificate Checking. 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_15

Download citation

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

  • 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