zbMATH — the first resource for mathematics

Efficient verified (UN)SAT certificate checking. (English) Zbl 07176608
Summary: SAT solvers decide the satisfiability of Boolean formulas in conjunctive normal form. They are commonly used for software and hardware verification. Modern SAT solvers are highly complex and optimized programs. As a single bug in the solver may invalidate the verification of many systems, SAT solvers output certificates for their answer, which are then checked independently. However, even certificate checking requires highly optimized non-trivial programs. This paper presents the first SAT solver certificate checker that is formally verified down to the integer sequence representing the formula. Our tool supports the full DRAT standard, and is even faster than the unverified state-of-the-art tool drat-trim, on a realistic set of benchmarks drawn from the 2016 and 2017 SAT competitions. An optional multi-threaded mode further reduces the runtime, in particular for big certificates.
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI
[1] Back, R.-J.: On the correctness of refinement steps in program development. Ph.D. thesis, Department of Computer Science, University of Helsinki (1978)
[2] Back, R-J; Von Wright, J., Refinement Calculus—A Systematic Introduction (1998), Berlin: Springer, Berlin · Zbl 0949.68094
[3] Bertot, Y.; Castran, P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (2010), Berlin: Springer, Berlin
[4] Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. In: Proceedings of NFM, pp. 307-321. Springer (2016) · Zbl 1426.68162
[5] Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: TPHOL, volume 5170 of LNCS, pp. 134-149. Springer (2008) · Zbl 1165.68352
[6] Cruz-Filipe, L., Heule, M., Hunt, W., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: Proceedings of CADE. Springer (2017) · Zbl 06778406
[7] Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Proceedings of TACAS, pp. 118-135. Springer (2017)
[8] Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: Proceedings of ICTAC, pp. 260-274. Springer (2010)
[9] DRAT-trim homepage. https://www.cs.utexas.edu/ marijn/drat-trim/
[10] DRAT-trim issue tracker. https://github.com/marijnheule/drat-trim/issues
[11] Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: CAV, volume 8044 of LNCS, pp. 463-478. Springer (2013)
[12] Fleury, M., Blanchette, J. C., Lammich, P.: A verified SAT solver with watched literals using imperative HOL. In: Proceedings of CPP, pp. 158-171 (2018)
[13] Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of DATE, IEEE (2003)
[14] Gordon, M.; Plotkin, G.; Stirling, Cp; Tofte, M., From LCF to HOL: a short history, Proof, Language, and Interaction, 169-185 (2000), Cambridge: MIT Press, Cambridge
[15] Haftmann, F.: Code generation from specifications in higher order logic. Ph.D. Thesis, Technische Universität München (2009)
[16] Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Proceedings of ITP, pp. 100-115. Springer (2013) · Zbl 1317.68212
[17] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: FLOPS 2010, LNCS. Springer (2010) · Zbl 1284.68131
[18] Heule, M., Hunt, W., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: Proceedings of ITP. Springer (2017) · Zbl 06821857
[19] 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)
[20] Hupel, Lars; Nipkow, Tobias, A Verified Compiler from Isabelle/HOL to CakeML, Programming Languages and Systems, 999-1026 (2018), Cham: Springer International Publishing, Cham · Zbl 1418.68045
[21] Kirchmeier, M.: Functional implementation of an optimized UNSAT proof-checker. Bachelor’s Thesis, Technische Universität München (2017)
[22] Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of POPL, pp. 179-192. ACM (2014) · Zbl 1284.68405
[23] Lammich, P.: Grat tool chain homepage. http://www21.in.tum.de/ lammich/grat/ · Zbl 06807243
[24] Lammich, P.: Automatic data refinement. In: ITP, volume 7998 of LNCS, pp. 84-99. Springer (2013) · Zbl 1317.68216
[25] Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: ITP, volume 8558 of LNCS, pp. 325-340. Springer (2014) · Zbl 1416.68168
[26] Lammich, P.: Refinement to imperative/HOL. In: ITP, volume 9236 of LNCS, pp. 253-269. Springer (2015) · Zbl 06481868
[27] Lammich, P.: Refinement based verification of imperative data structures. In: CPP, pp. 27-36. ACM (2016)
[28] Lammich, P.: Efficient verified (UN)SAT certificate checking. In: Proceedings of CADE. Springer (2017) · Zbl 06778407
[29] Lammich, P.: The GRAT tool chain—efficient (UN)SAT certificate checking with formal correctness guarantees. In: SAT, pp. 457-463 (2017) · Zbl 06807243
[30] Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Proceedings of ITP, volume 6172 of LNCS, pp. 339-354. Springer (2010) · Zbl 1291.68357
[31] Lammich, Peter; Sefidgar, S. Reza, Formalizing the Edmonds-Karp Algorithm, Interactive Theorem Proving, 219-234 (2016), Cham: Springer International Publishing, Cham · Zbl 06644746
[32] Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Proceedings of ITP, volume 7406 of LNCS, pp. 166-182. Springer (2012) · Zbl 1360.68757
[33] Marić, F., Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theor. Comput. Sci., 411, 50, 4333-4356 (2010) · Zbl 1208.68205
[34] Milner, R.; Harper, R.; Macqueen, D.; Tofte, M., The Definition of Standard ML (1997), Cambridge: The MIT Press, Cambridge
[35] MLton Standard ML compiler. http://mlton.org/
[36] 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)
[37] Myreen, Mo; Owens, S., Proof-producing translation of higher-order logic into pure and stateful ML, J. Funct. Program., 24, 2-3, 284-315 (2014) · Zbl 1297.68053
[38] Nipkow, T.; Paulson, Lc; Wenzel, M., Isabelle/HOL—A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[39] Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: a verified modern SAT solver. In: VMCAI, volume 7148 of LNCS, pp. 363-378. Springer (2012) · Zbl 1326.68263
[40] SAT competition, 2013. http://satcompetition.org/2013/
[41] SAT competition, 2014. http://satcompetition.org/2014/
[42] SAT competition, 2016. http://baldur.iti.kit.edu/sat-competition-2016/
[43] SAT competition, 2017. https://baldur.iti.kit.edu/sat-competition-2017/
[44] Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In Proceedings of CSR, pp. 600-611. Springer (2006) · Zbl 1185.68635
[45] Wetzler, N., Heule, M. J. H., Hunt, W. A.: Mechanical verification of SAT refutations with extended resolution. In: Proceedings of ITP, pp. 229-244. Springer (2013) · Zbl 1317.68236
[46] Wetzler, N., Heule, M. J. H., Hunt, W. A.: Drat-trim: efficient checking and trimming using expressive clausal proofs. In: Proceedings of SAT 2014, pp. 422-429. Springer (2014) · Zbl 1423.68475
[47] Wimmer, Simon; Lammich, Peter, Verified Model Checking of Timed Automata, Tools and Algorithms for the Construction and Analysis of Systems, 61-78 (2018), Cham: Springer International Publishing, Cham · Zbl 1423.68294
[48] Wirth, N., Program development by stepwise refinement, Commun. ACM, 14, 4, 221-227 (1971) · Zbl 0214.43005
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.