×

zbMATH — the first resource for mathematics

Strong extension-free proof systems. (English) Zbl 07176609
Summary: We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not necessarily implied, but which are redundant in the sense that their addition preserves satisfiability. To guarantee that these added clauses are redundant, we consider various efficiently decidable redundancy criteria which we obtain by first characterizing clause redundancy in terms of a semantic implication relationship and then restricting this relationship so that it becomes decidable in polynomial time. As the restricted implication relation is based on unit propagation – a core technique of SAT solvers – it allows efficient proof checking too. The resulting proof systems are surprisingly strong, even without the introduction of new variables – a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of our proof systems on the famous pigeon hole formulas by providing short clausal proofs without new variables.

MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Software:
DRAT-trim
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: Proceedings of the 39th Annual Design Automation Conference (DAC 2002), pp. 725-730. ACM (2002)
[2] Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning sat solvers. In: Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI 2010). AAAI Press (2010)
[3] Balyo, T., Heule, M.J.H., Järvisalo, M.: SAT competition 2016: recent developments. To appear in: Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI 2017). AAAI Press (2017)
[4] Clarke, Em; Biere, A.; Raimi, R.; Zhu, Y., Bounded model checking using satisfiability solving, Form. Methods Syst. Des., 19, 1, 7-34 (2001) · Zbl 0985.68038
[5] Cook, Sa, A short proof of the pigeon hole principle using extended resolution, SIGACT News, 8, 4, 28-32 (1976)
[6] Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR 1996), pp. 148-159. Morgan Kaufmann (1996)
[7] Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice; Denecker, Marc, Improved Static Symmetry Breaking for SAT, Theory and Applications of Satisfiability Testing - SAT 2016, 104-122 (2016), Cham: Springer International Publishing, Cham · Zbl 06623508
[8] Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Conference on Design, Automation and Test in Europe (DATE 2003), pp. 10,886-10,891. IEEE Computer Society (2003)
[9] Haken, A., The intractability of resolution, Theor. Comput. Sci., 39, 297-308 (1985) · Zbl 0586.03010
[10] Heule, M.J.H.: Schur number five. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6598-6606. AAAI Press (2018)
[11] Heule, Marijn J. H.; Biere, Armin, What a Difference a Variable Makes, Tools and Algorithms for the Construction and Analysis of Systems, 75-92 (2018), Cham: Springer International Publishing, Cham · Zbl 1423.68419
[12] Heule, Marijn J. H.; Hunt, Warren A.; Wetzler, Nathan, Expressing Symmetry Breaking in DRAT Proofs, Automated Deduction - CADE-25, 591-606 (2015), Cham: Springer International Publishing, Cham · Zbl 06515534
[13] Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W., Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, Theory and Applications of Satisfiability Testing - SAT 2016, 228-245 (2016), Cham: Springer International Publishing, Cham · Zbl 1403.68226
[14] Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin, Short Proofs Without New Variables, Automated Deduction - CADE 26, 130-147 (2017), Cham: Springer International Publishing, Cham · Zbl 06778401
[15] Heule, Marijn J. H.; Kiesl, Benjamin; Seidl, Martina; Biere, Armin, PRuning Through Satisfaction, Hardware and Software: Verification and Testing, 179-194 (2017), Cham: Springer International Publishing, Cham
[16] Ivančić, F.; Yang, Z.; Ganai, Mk; Gupta, A.; Ashar, P., Efficient SAT-based bounded model checking for software verification, Theor. Comput. Sci., 404, 3, 256-274 (2008) · Zbl 1293.68079
[17] Järvisalo, M.; Biere, A.; Heule, Mjh, Simulating circuit-level simplifications on CNF, J. Autom. Reason., 49, 4, 583-619 (2012) · Zbl 1267.94144
[18] Järvisalo, Matti; Heule, Marijn J. H.; Biere, Armin, Inprocessing Rules, Automated Reasoning, 355-370 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1358.68256
[19] Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin, Super-Blocked Clauses, Automated Reasoning, 45-61 (2016), Cham: Springer International Publishing, Cham · Zbl 06623253
[20] Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H., Extended Resolution Simulates DRAT, Automated Reasoning, 516-531 (2018), Cham: Springer International Publishing, Cham · 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] Manthey, Norbert; Heule, Marijn J. H.; Biere, Armin, Automated Reencoding of Boolean Formulas, Hardware and Software: Verification and Testing, 102-117 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[24] Monien, B.; Speckenmeyer, E., Solving satisfiability in less than \(2^n\) steps, Discrete Appl. Math., 10, 3, 287-295 (1985) · Zbl 0603.68092
[25] Nordström, J., A simplified way of proving trade-off results for resolution, Inf. Process. Lett., 109, 18, 1030-1035 (2009) · Zbl 1202.68388
[26] Tseitin, Gs, On the complexity of derivation in propositional calculus, Stud. Math. Math. Log., 2, 115-125 (1968)
[27] Urquhart, A., The complexity of propositional proofs, Bull. Symb. Log., 1, 4, 425-467 (1995) · Zbl 1133.03037
[28] Van Gelder, A., Producing and verifying extremely large propositional refutations, Ann. Math. Artif. Intell., 65, 4, 329-372 (2012) · Zbl 1273.68329
[29] Weaver, S.; Franco, Jv; Schlipf, Js, Extending existential quantification in conjunctions of BDDs, JSAT, 1, 2, 89-110 (2006) · Zbl 1138.94401
[30] Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A., DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs, Lecture Notes in Computer Science, 422-429 (2014), Cham: Springer International Publishing, Cham · 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.