×

zbMATH — the first resource for mathematics

Simulating strong practical proof systems with extended resolution. (English) Zbl 07268901
Summary: Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution – introduced by Tseitin in the sixties – allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that – from the viewpoint of proof complexity – these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann’s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Software:
Chaff; DRAT-trim
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alekhnovich, M., Mutilated chessboard problem is exponentially hard for resolution, Theoret. Comput. Sci., 310, 1-3, 513-525 (2004) · Zbl 1071.68028
[2] Baaz, M.; Leitsch, A., Methods of Cut-Elimination. No. 3 in Trends in Logic (2011), Berlin: Springer, Berlin
[3] Biere, A.: Two pigeons per hole problem. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, p. 103 (2013)
[4] Chatalic, P., Simon, L.: Multi-resolution on compressed sets of clauses. In: Proceedings of the 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2000), pp. 2-10 (2000)
[5] Cook, SA, A short proof of the pigeon hole principle using extended resolution, SIGACT News, 8, 4, 28-32 (1976)
[6] Cook, SA; Reckhow, RA, The relative efficiency of propositional proof systems, J. Symb. Log., 44, 1, 36-50 (1979) · Zbl 0408.03044
[7] Cruz-Filipe, L., Heule, M.J.H., Hunt, W. A. Jr.., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). LNCS, vol. 10395, pp. 220-236. Springer, Berlin (2017) · Zbl 06778406
[8] Dantchev, S.S,. Riis, S.: “Planar” tautologies hard for resolution. In: Proceedings of the 42nd Annual Symposium on Foundations of Computer Science (FOCS 2001), pp. 220-229. IEEE Computer Society, New York (2001)
[9] Haken, A., The intractability of resolution, Theoret. Comput. Sci., 39, 297-308 (1985) · Zbl 0586.03010
[10] Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), LNCS, vol. 10806, pp. 75-92. Springer, Berlin (2018) · Zbl 1423.68419
[11] Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016). LNCS, vol. 9710, pp. 228-245. Springer, Cham (2016) · Zbl 1403.68226
[12] Heule, M.J.H., Hunt, W.A. Jr., Kaufmann, M., Wetzler, N.D.: Efficient, verified checking of propositional proofs. In: Proceedings of the 8th International Conference on Interactive Theorem Proving (ITP 2017). LNCS, vol. 10499, pp. 269-284. Springer, Berlin (2017) · Zbl 06821857
[13] Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26), LNCS, vol. 10395, pp. 130-147. Springer, Cham (2017) · Zbl 06778401
[14] Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). LNCS, vol. 10629, pp. 179-194. Springer, Berlin (2017)
[15] Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). LNCS, vol. 11427, pp. 41-58. Springer, Berlin (2019)
[16] Heule, MJH; Kiesl, B.; Biere, A., Strong extension-free proof systems, J. Autom. Reason., 64, 533-554 (2019) · Zbl 07176609
[17] Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). LNCS, vol. 6015, pp. 129-144. Springer, Heidelberg (2010) · Zbl 1284.03208
[18] Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012). LNCS, vol. 7364, pp. 355-370. Springer, Heidelberg (2012) · Zbl 1358.68256
[19] Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006). LNCS, vol. 4121, pp. 54-60. Springer, Berlin (2006) · Zbl 1187.68550
[20] Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). LNCS, vol. 10900, pp. 516-531. Springer, Berlin (2018) · Zbl 1441.68278
[21] Konev, B.; Lisitsa, A., Computer-aided proof of Erdős discrepancy properties, Artif. Intell., 224, C, 103-118 (2015) · Zbl 1344.68205
[22] Kullmann, O., On a generalization of extended resolution, Discrete Appl. Math., 96-97, 149-176 (1999) · Zbl 0941.68126
[23] Lee, C.T.: A completeness theorem and a computer program for finding theorems derivable from given axioms. Ph.D. Thesis, University of California, Berkeley (1967)
[24] Marques-Silva, JP; Sakallah, KA, GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388
[25] McCarthy, J.: A tough nut for proof procedures. Memo 16, Stanford Artificial Intelligence Project (1964)
[26] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530-535. ACM, New York (2001)
[27] Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing. In: Procedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21), EasyChair, EPiC Series in Computing, vol. 46, pp. 65-84 (2017) · Zbl 1403.68244
[28] Rebola-Pardo, A., Suda, M.: A theory of satisfiability-preserving proofs in SAT solving. In: Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-22), EasyChair, EPiC Series in Computing, vol. 57, pp. 583-603 (2018) · Zbl 1415.68203
[29] Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Proceedings of the 1st International Computer Science Symposium in Russia (CSR 2006). LNCS, vol. 3967, pp. 600-611. Springer, Heidelberg (2006) · Zbl 1185.68635
[30] Tseitin, GS, On the complexity of derivation in propositional calculus, Stud. Math. Math. Log., 2, 115-125 (1968)
[31] Urquhart, A., Hard examples for resolution, J. ACM, 34, 1, 209-219 (1987) · Zbl 0639.68093
[32] Urquhart, A., The complexity of propositional proofs, Bull. Symb. Log., 1, 4, 425-467 (1995) · Zbl 0845.03025
[33] Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: Proceedings of the 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM 2008) (2008)
[34] Van Gelder, A., Producing and verifying extremely large propositional refutations, Ann. Math. Artif. Intell., 65, 4, 329-372 (2012) · Zbl 1273.68329
[35] Wetzler, N.D., Heule, M.J.H., Hunt, W.A. Jr: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014). LNCS, vol. 8561, pp. 422-429. Springer, Cham (2014) · Zbl 1423.68475
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.