×

DRAT and propagation redundancy proofs without new variables. (English) Zbl 07350778

Summary: We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses \(\Gamma\) derive the set of clauses \(\Gamma \cup \{C\}\) where, due to some syntactic condition, \( \Gamma \cup \{C\}\) is satisfiable if \(\Gamma\) is, but where \(\Gamma\) does not necessarily imply \(C\). These inference rules include BC, RAT, SPR and PR (respectively short for blocked clauses, resolution asymmetric tautologies, subset propagation redundancy and propagation redundancy), which arose from work in satisfiability (SAT) solving. We introduce a new, more general rule SR (substitution redundancy).
If the new clause \(C\) is allowed to include new variables then the systems based on these rules are all equivalent to extended resolution. We focus on restricted systems that do not allow new variables. The systems with deletion, where we can delete a clause from our set at any time, are denoted DBC\(^-\), DRAT\(^-\), DSPR\(^-\), DPR\(^-\) and DSR\(^-\). The systems without deletion are BC\(^-\), RAT\(^-\), SPR\(^-\), PR\(^-\) and SR\(^-\). With deletion, we show that DRAT\(^-\), DSPR\(^-\) and DPR\(^-\) are equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC\(^-\). Without deletion, we show that SPR\(^-\) can simulate PR\(^-\) provided only short clauses are inferred by SPR inferences. We also show that many of the well-known “hard” principles have small SPR\(^-\) refutations. These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies and clique-coloring tautologies. SPR\(^-\) can also handle or-fication and xor-ification, and lifting with an index gadget. Our final result is an exponential size lower bound for RAT\(^-\) refutations, giving exponential separations between RAT\(^-\) and both DRAT\(^-\) and SPR\(^-\).

MSC:

03B70 Logic in computer science
68-XX Computer science

Software:

DRAT-trim
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] A. Atserias and V. Dalmau. A combinatorial characterization of resolution width.Journal of Computer and System Sciences, 74(3):323-334, 2008. · Zbl 1133.03034
[2] M. Ajtai. Parity and the pigeonhole principle. InFeasible Mathematics: A Mathematical Sciences Institute Workshop held in Ithaca, New York, June 1989, pages 1-24. Birkh¨auser, 1990. · Zbl 0781.03045
[3] Paul Beame, Trinh Huynh, and Toniann Pitassi. Hardness amplification in proof complexity. In Proc. 42nd Annual ACM Symposium on Theory of Computing (STOC’10), pages 87-96, 2010. · Zbl 1293.03030
[4] Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning.Journal of Artificial Intelligence Research, 22:319-351, 2004. · Zbl 1080.68651
[5] Eli Ben-Sasson. Size space tradeoffs for resolution.SIAM Journal on Computing, 38(6):2511-2525, 2009. · Zbl 1191.68617
[6] Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution.Combinatorica, 24(4):585-603, 2004. · Zbl 1063.03043
[7] Eli Ben-Sasson and Ave Wigderson. Short proofs are narrow — resolution made simple.Journal of the ACM, 48:149-169, 2001. · Zbl 1089.03507
[8] Sam Buss and Neil Thapen. DRAT proofs, propagation redundancy, and extended resolution. InProc. 22nf Intl. Conference on Theory and Applications of Satisfiability Testing (SAT 2019), Springer-Verlag Lecture Notes in Computer Science 11628, pages 71-89, 2019. · Zbl 1441.03043
[9] Samuel R. Buss.Bounded Arithmetic. Bibliopolis, Naples, Italy, 1986. Revision of 1985 Princeton University Ph.D. thesis.
[10] C. L. Chang. The unit proof and the input proof in theorem proving.J. ACM, 17(4):698-707, 1970. · Zbl 0212.34202
[11] Stephen A. Cook. Feasibly constructive proofs and the propositional calculus. InProceedings of the Seventh Annual ACM Symposium on Theory of Computing, pages 83-97. Association for · Zbl 0357.68061
[12] Stephen A. Cook and Robert A. Reckhow. On the lengths of proofs in the propositional calculus, preliminary version. InProceedings of the Sixth Annual ACM Symposium on the Theory of · Zbl 0375.02004
[13] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36-50, 1979. · Zbl 0408.03044
[14] Evguenii I. Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. InDesign, Automation and Test in Europe Conference (DATE), pages 10886-10891. IEEE Computer Society, 2003.
[15] Joachim Grollmann and Alan Selman. Complexity measures for public-key cryptosystems.SIAM Journal on Computing, 17(2):309-335, 1988. · Zbl 0644.94016
[16] Marijn J. H. Heule and Armin Biere. What a difference a variable makes. InTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference (TACAS 2018), Lecture Notes in Computer Science 10806, pages 75-92. Springer Verlag, 2018. · Zbl 1423.68419
[17] Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. InFormal Methods in Computer-Aided Design (FMCAD), pages 181-188. IEEE, 2013. · Zbl 1423.68475
[18] Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. InAutomated Deduction - 24th International Conference (CADE), Lecture Notes in Computer Science 7898, pages 345-359. Springer Verlag, 2013. · Zbl 1381.68270
[19] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Short proofs without new variables. In Automated Deduction - 26th International Conference (CADE), Lecture Notes in Computer · Zbl 1468.03010
[20] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, pages 1-22, 2019. Extended version of [HKB17]. · Zbl 1468.03011
[21] Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. PRuning through satisfaction. InHardware and Software: Verification and Testing - 13th International Haifa Verification
[22] Trinh Huynh and Jakob Nordstr¨om. On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity (Extended abstract). InProc. · Zbl 1286.68234
[23] Matti J¨arvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. InAutomated Reasoning - 6th International Joint Conference (IJCAR), Lecture Notes in Computer Science 7364, pages
[24] Jan Kraj´ıˇcek, Pavel Pudl´ak, and Alan Woods. Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle.Random Structures and Algorithms, 7:15-39, · Zbl 0843.03032
[25] Jan Kraj´ıˇcek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic.Journal of Symbolic Logic, 62:457-486, 1997. · Zbl 0891.03029
[26] Benjamin Kiesl, Adri´an Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. InAutomated Reasoning - 6th International Joint Conference (IJCAR), Lecture Notes in Computer Science 10900, pages 516-531. Springer Verlag, 2018. · Zbl 1441.68278
[27] Oliver Kullmann. Worst-case analysis, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms.DIMACS Series in Discrete Mathematics and Theoretical Computer · Zbl 0889.03030
[28] Oliver Kullmann. New methods for 3-SAT decision and worst-case analysis.Theoretical Computer Science, 223(1):1-72, 1999. · Zbl 0930.68066
[29] Oliver Kullmann. On a generalizaton of extended resolution.Discrete Applied Mathematics, 96-97:149-176, 1999. · Zbl 0941.68126
[30] Klas Markstr¨om. Locality and hard SAT-instances.Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2:221-227, 2006. · Zbl 1113.68483
[31] Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle.Computational Complexity, 3:97-140, 1993. · Zbl 0784.03034
[32] Toniann Pitassi and Rahul Santhanam. Effectively polynomial simulations. InInnovations in Computer Science (ICS), pages 370-381, 2010.
[33] Pavel Pudl´ak. Lower bounds for resolution and cutting planes proofs and monotone computations. Journal of Symbolic Logic, 62(3):981-998, 1997. · Zbl 0945.03086
[34] Pavel Pudl´ak. Proofs as games.American Mathematical Monthly, 107(6):541-550, 2000. · Zbl 0983.03045
[35] Pavel Pudl´ak. On reducibility and symmetry of disjoint NP pairs.Theoretical Computer Science, 205:323-339, 2003. · Zbl 1045.68058
[36] Alexander A. Razborov. On provably disjoint NP-pairs. Technical Report TR94-006, Electronic Colloquium in Computational Complexity (ECCC), 1994. Also available as BRIC technical report RS-94-36.
[37] Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy.Combinatorica, 19(3):403-435, 1999. · Zbl 0977.68037
[38] Adri´an Rebola-Pardo and Martin Suda. A theory of satisfiability-preserving proofs in SAT solving. InProc., 22nd Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning · Zbl 1415.68203
[39] Jorg Siekmann and Graham Wrightson.Automation of Reasoning, volume 1&2. Springer-Verlag, Berlin, 1983. · Zbl 0567.03002
[40] Stefan Szeider. Homomorphisms of conjunctive normal forms.Discrete Applied Mathematics, 130:351-365, 2003. · Zbl 1033.68095
[41] G. S. Tsejtin. On the complexity of derivation in propositional logic.Studies in Constructive Mathematics and Mathematical Logic, 2:115-125, 1968. Reprinted in: [SW83, vol 2], pp. 466-483.
[42] Alasdair Urquhart. Hard examples for resolution.Journal of the ACM, 34:209-219, 1987. · Zbl 0639.68093
[43] Alasdair Urquhart. A near-optimal separation of regular and general resolution.SIAM Journal on Computing, 40(1):107-121, 2011. · Zbl 1222.03063
[44] AllenVanGelder.VerifyingRUPproofsofpropositionalunsatisfiability.In10th International Symposium on Artificial Intelligence and Mathematics (ISAIM),2008.
[45] Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. InTheory and Applications of Satisfiability Testing · 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.