Document Open Access Logo

Lower Bounds for Set-Blocked Clauses Proofs

Author Emre Yolcu

PDF
Thumbnail PDF

File

LIPIcs.STACS.2024.59.pdf
  • Filesize: 0.8 MB
  • 17 pages

Document Identifiers

Author Details

Emre Yolcu
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the National Science Foundation under grant CCF-2015445.

Acknowledgements

I thank Sam Buss, Marijn Heule, Jakob Nordström, and Ryan O'Donnell for useful discussions. I thank Jeremy Avigad, Ryan O'Donnell, and Bernardo Subercaseaux for feedback on an earlier version of the paper. Finally, I thank the STACS reviewers for their highly detailed comments and suggestions.

Cite AsGet BibTex

Emre Yolcu. Lower Bounds for Set-Blocked Clauses Proofs. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 59:1-59:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.STACS.2024.59

Abstract

We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all "without new variables." They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC⁻, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC⁻ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC⁻. Using this new separation, we prove that both RAT⁻ and GER⁻ are exponentially separated from SBC⁻. This completes the picture of their relative strengths.

Subject Classification

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

Metrics

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

Related Versions

References

  1. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, The University of Chicago, 1937. Google Scholar
  2. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17(2):12:1-12:31, 2021. URL: https://doi.org/10.23638/LMCS-17(2:12)2021.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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):1-23, 2018. URL: https://doi.org/10.23638/LMCS-14(4:3)2018.
  13. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-2):123-140, 2001. Google Scholar
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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
  19. Pavel Pudlák. Proofs as games. The American Mathematical Monthly, 107(6):541-550, 2000. URL: https://doi.org/10.2307/2589349.
  20. 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.
  21. Grigori S. Tseitin. On the complexity of derivation in propositional calculus. Zapiski Nauchnykh Seminarov LOMI, 8:234-259, 1968. Google Scholar
  22. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
  23. Emre Yolcu and Marijn J. H. Heule. Exponential separations using guarded extension variables. In Proceedings of the 14th Innovations in Theoretical Computer Science (ITCS), number 251 in Leibniz International Proceedings in Informatics, pages 101:1-101:22. Schloss Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPIcs.ITCS.2023.101.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact