Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP
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.
Proof complexity
Automatability
Bounded-depth Frege
Theory of computation~Proof complexity
22:1-22:17
Regular Paper
I would like to thank Alexander Razborov for numerous remarks and suggestions that greatly improved the presentation of the paper.
Theodoros
Papamakarios
Theodoros Papamakarios
Department of Computer Science, University of Chicago, IL, USA
https://orcid.org/0009-0009-2814-5256
10.4230/LIPIcs.CCC.2024.22
Michael Alekhnovich and Alexander Razborov. Resolution is not automatizable unless W[P] is tractable. SIAM Journal of Computing, 38:1347-1363, 2008.
Albert Atserias and Moritz Müller. Automating resolution is NP-hard. Journal of the ACM, 67:31:1-31:17, 2020.
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.
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.
Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for frege systems. SIAM Journal of Computing, 29:1939-1967, 2000.
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.
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.
Merrick Furst, James Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17:13-27, 1984.
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.
Michal Garlík. Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it. Electronic Colloqium on Computational Complexity, 2020.
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.
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.
Russell Impagliazzo and Jan Krajícek. A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly, 48:375-377, 2002.
Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 59:73-86, 1994.
Jan Krajíček. Proof Complexity. Cambridge University Press, 2019.
Pavel Pudlák. On reducibility and symmetry of disjoint NP pairs. Theoretical Computer Science, 295:323-339, 2003.
Pavel Pudlák. Reflection principles, propositional proof systems, and theories, 2020. arXiv:2007.14835. URL: https://arxiv.org/abs/2007.14835.
https://arxiv.org/abs/2007.14835
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.
Michael Sipser. Borel sets and circuit complexity. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pages 61-69, 1983.
Theodoros Papamakarios
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode