Exponential Separations Using Guarded Extension Variables

Authors Emre Yolcu , Marijn J. H. Heule

Thumbnail PDF


  • Filesize: 0.83 MB
  • 22 pages

Document Identifiers

Author Details

Emre Yolcu
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA


We thank Jakob Nordström for useful discussions and the ITCS reviewers for their comments.

Cite AsGet BibTex

Emre Yolcu and Marijn J. H. Heule. Exponential Separations Using Guarded Extension Variables. In 14th Innovations in Theoretical Computer Science Conference (ITCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 251, pp. 101:1-101:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula Γ in conjunctive normal form, deriving clauses that are not necessarily logically implied by Γ but whose addition to Γ preserves satisfiability. When the derived clauses are allowed to introduce variables not occurring in Γ, the systems we consider become equivalent to extended resolution. We are concerned with the versions of these systems without new variables. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution. Each of these systems formalizes some restricted version of the ability to make assumptions that hold "without loss of generality," which is commonly used informally to simplify or shorten proofs. Except for SBC⁻, these systems are known to be exponentially weaker than extended resolution. They are, however, all equivalent to it under a relaxed notion of simulation that allows the translation of the formula along with the proof when moving between proof systems. By taking advantage of this fact, we construct formulas that separate RAT⁻ from GER⁻ and vice versa. With the same strategy, we also separate SBC⁻ from RAT⁻. Additionally, we give polynomial-size SBC⁻ proofs of the pigeonhole principle, which separates SBC⁻ from GER⁻ by a previously known lower bound. These results also separate the three systems from BC⁻ since they all simulate it. We thus give an almost complete picture of their relative strengths.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • proof complexity
  • separations
  • resolution
  • extended resolution
  • blocked clauses


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Noriko H. Arai and Alasdair Urquhart. Local symmetries in propositional logic. In Proceedings of the 9th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), number 1847 in Lecture Notes in Computer Science, pages 40-51. Springer, 2000. URL: https://doi.org/10.1007/10722086_3.
  2. Lee A. Barnett, David Cerna, and Armin Biere. Covered clauses are not propagation redundant. In Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR), number 12166 in Lecture Notes in Computer Science, pages 32-47. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_3.
  3. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, The University of Chicago, 1937. Google Scholar
  4. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17(2:12), 2021. URL: https://doi.org/10.23638/LMCS-17(2:12)2021.
  5. Chin-Liang Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, 1970. URL: https://doi.org/10.1145/321607.321618.
  6. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Symposium on Theory of Computing (STOC), pages 174-183. Association for Computing Machinery, 1996. URL: https://doi.org/10.1145/237814.237860.
  7. Stephen A. Cook. A short proof of the pigeon hole principle using extended resolution. ACM SIGACT News, 8(4):28-32, 1976. URL: https://doi.org/10.1145/1008335.1008338.
  8. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  9. William Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  10. Evgueni Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Proceedings of the Design, Automation and Test in Europe Conference (DATE), pages 886-891. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/DATE.2003.1253718.
  11. Alexander Hertel, Philipp Hertel, and Alasdair Urquhart. Formalizing dangerous SAT encodings. In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT), number 4501 in Lecture Notes in Computer Science, pages 159-172. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_18.
  12. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. 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), number 11427 in Lecture Notes in Computer Science, pages 41-58. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_3.
  13. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533-554, 2020. URL: https://doi.org/10.1007/s10817-019-09516-0.
  14. Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. PRuning through satisfaction. In Proceedings of the 13th Haifa Verification Conference (HVC), number 10629 in Lecture Notes in Computer Science, pages 179-194. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-70389-3_12.
  15. Matti Järvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), number 7364 in Lecture Notes in Computer Science, pages 355-370. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  16. Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, and Armin Biere. Simulating strong practical proof systems with extended resolution. Journal of Automated Reasoning, 64(7):1247-1267, 2020. URL: https://doi.org/10.1007/s10817-020-09554-z.
  17. Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere. Local redundancy in SAT: Generalizations of blocked clauses. Logical Methods in Computer Science, 14(4:3), 2018. URL: https://doi.org/10.23638/LMCS-14(4:3)2018.
  18. Jan Krajíček. Proof Complexity. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108242066.
  19. Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta Informatica, 22(3):253-275, 1985. URL: https://doi.org/10.1007/BF00265682.
  20. Oliver Kullmann. Worst-case analysis, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms. In Satisfiability Problem: Theory and Applications, number 35 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 261-313. American Mathematical Society, 1997. URL: https://doi.org/10.1090/dimacs/035.
  21. Oliver Kullmann. New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science, 223(1-2):1-72, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00017-6.
  22. Oliver Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  23. László Lovász and Alexander Schrijver. Cones of matrices and set-functions and 0-1 optimization. SIAM Journal on Optimization, 1(2):166-190, 1991. URL: https://doi.org/10.1137/0801013.
  24. João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  25. Christos H. Papadimitriou and Mihalis Yannakakis. The complexity of facets (and some facets of complexity). Journal of Computer and System Sciences, 28(2):244-259, 1984. URL: https://doi.org/10.1016/0022-0000(84)90068-0.
  26. Toniann Pitassi and Rahul Santhanam. Effectively polynomial simulations. In Proceedings of the 1st Innovations in Computer Science (ICS), pages 370-382. Tsinghua University Press, 2010. Google Scholar
  27. John A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  28. Stefan Szeider. The complexity of resolution with generalized symmetry rules. Theory of Computing Systems, 38(2):171-188, 2005. URL: https://doi.org/10.1007/s00224-004-1192-0.
  29. Grigori S. Tseitin. On the complexity of derivation in propositional calculus. Zapiski Nauchnykh Seminarov LOMI, 8:234-259, 1968. Google Scholar
  30. Alasdair Urquhart. The symmetry rule in propositional logic. Discrete Applied Mathematics, 96-97:177-193, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00039-6.
  31. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In Proceedings of the 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM), 2008. Google Scholar
  32. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, 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), number 8561 in Lecture Notes in Computer Science, pages 422-429. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail