Document Open Access Logo

Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP

Author Theodoros Papamakarios

PDF
Thumbnail PDF

File

LIPIcs.CCC.2024.22.pdf
  • Filesize: 0.73 MB
  • 17 pages

Document Identifiers

Author Details

Theodoros Papamakarios
  • Department of Computer Science, University of Chicago, IL, USA

Acknowledgements

I would like to thank Alexander Razborov for numerous remarks and suggestions that greatly improved the presentation of the paper.

Cite AsGet BibTex

Theodoros Papamakarios. Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CCC.2024.22

Abstract

We show that for any integer d > 0, depth-d Frege systems are NP-hard to automate. Namely, given a set S of depth-d formulas, it is NP-hard to find a depth-d Frege refutation of S in time polynomial in the size of the shortest such refutation. This extends the result of Atserias and Müller [JACM, 2020] for the non-automatability of resolution - a depth-1 Frege system - to Frege systems of any depth d > 0.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • Automatability
  • Bounded-depth Frege

Metrics

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

References

  1. Michael Alekhnovich and Alexander Razborov. Resolution is not automatizable unless W[P] is tractable. SIAM Journal of Computing, 38:1347-1363, 2008. Google Scholar
  2. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. Journal of the ACM, 67:31:1-31:17, 2020. Google Scholar
  3. Arnold Beckmann and Samuel Buss. Separation results for the size of constant-depth propositional proofs. Annals of Pure and Applied Logic, 136:30-55, 2005. Google Scholar
  4. Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth frege proofs. Computational Complexity, 13:47-68, 2004. Google Scholar
  5. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for frege systems. SIAM Journal of Computing, 29:1939-1967, 2000. Google Scholar
  6. Stefan Dantchev and Søren Riis. On relativisation and complexity gap. In Proceedings of the 12th Annual Conference of the EACSL, pages 142-154, 2003. Google Scholar
  7. Susanna de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, and Dmitry Sokolov. Automating algebraic proof systems is NP-hard. In Proccedings of the 53rd Annual ACM Symposium on Theory of Computing, pages 209-222, 2021. Google Scholar
  8. Merrick Furst, James Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17:13-27, 1984. Google Scholar
  9. Michal Garlík. Resolution lower bounds for refutation statements. In Proccedings of the 44th International Symposium on Mathematical Foundations of Computer Science, volume 138, pages 37:1-37:13, 2019. Google Scholar
  10. Michal Garlík. Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it. Electronic Colloqium on Computational Complexity, 2020. Google Scholar
  11. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is NP-hard. In Proccedings of the 52nd Annual ACM Symposium on Theory of Computing, pages 68-77, 2020. Google Scholar
  12. Johan Håstad. Almost optimal lower bounds for small depth circuits. In Proceedings of the 18th Annual ACM Symposium on Theory of Computing, pages 6-20, 1986. Google Scholar
  13. Russell Impagliazzo and Jan Krajícek. A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly, 48:375-377, 2002. Google Scholar
  14. Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 59:73-86, 1994. Google Scholar
  15. Jan Krajíček. Proof Complexity. Cambridge University Press, 2019. Google Scholar
  16. Pavel Pudlák. On reducibility and symmetry of disjoint NP pairs. Theoretical Computer Science, 295:323-339, 2003. Google Scholar
  17. Pavel Pudlák. Reflection principles, propositional proof systems, and theories, 2020. arXiv:2007.14835. URL: https://arxiv.org/abs/2007.14835.
  18. Nathan Segerlind, Samuel Buss, and Russell Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM Journal of Computing, 33:1171-1200, 2004. Google Scholar
  19. Michael Sipser. Borel sets and circuit complexity. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pages 61-69, 1983. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact