Document Open Access Logo

Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It

Author Michal Garlík

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2024.33.pdf
  • Filesize: 0.87 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • reflection principle
  • feasible disjunction property
  • k-DNF Resolution

Metrics

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

Abstract

We show that for every integer k ≥ 2, the Res(k) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a result of Atserias and Müller [Atserias and Müller, 2019] to Res(k). We show that if NP is not included in P (resp. QP, SUBEXP) then for every integer k ≥ 1, Res(k) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.

Cite As Get BibTex

Michal Garlík. Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 33:1-33:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CCC.2024.33

Author Details

Michal Garlík
  • Department of Computing, Imperial College London, UK

Funding

  • Garlík, Michal: Supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 101002742). Part of this work was carried out at the Euler International Mathematical Institute and supported by a grant from the Ministry of Science and Higher Education of the Russian Federation (agreement No. 075-15-2019-1620 dated 08/11/2019 and 075-15-2022-289 dated 06/04/2022). Part of this work was supported by European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreement ERC-2014-CoG 648276 (AUTAR).

Acknowledgements

I am grateful to Albert Atserias and Jan Krajíček for their valuable comments on an earlier version of the paper. I would like to thank Ilario Bonacina and Moritz Müller for several related conversations.

References

  1. Michael Alekhnovich and Alexander A. Razborov. Resolution is not automatizable unless W[P] is tractable. SIAM Journal on Computing, 38(4):1347-1363, 2008. URL: https://doi.org/10.1137/06066850X.
  2. Albert Atserias and Maria Luisa Bonet. On the automatizability of resolution and related propositional proof systems. Information and Computation, 189(2):182-201, 2004. Google Scholar
  3. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. In 60th Annual Symposium on Foundations of Computer Science (FOCS), pages 498-509. IEEE, 2019. Google Scholar
  4. Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, Toniann Pitassi, and Ran Raz. Non-automatizability of bounded-depth Frege proofs. Computational Complexity, 13(1-2):47-68, 2004. URL: https://doi.org/10.1007/s00037-004-0183-5.
  5. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM J. Comput., 29(6):1939-1967, 2000. URL: https://doi.org/10.1137/S0097539798353230.
  6. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  7. Stefan Dantchev and Søren Riis. On relativisation and complexity gap for resolution-based proof systems. In M. Baaz and J. A. Makowsky, editors, Computer Science Logic (CSL 2003), volume 2803 of Lecture Notes in Computer Science, pages 142-154. Springer, 2003. Google Scholar
  8. Michal Garlík. Resolution Lower Bounds for Refutation Statements. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1-37:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.37.
  9. M Göös, S Koroth, I Mertz, and T Pitassi. Automating cutting planes is np-hard. STOC 2020: Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, 2020. URL: https://doi.org/10.1145/3357713.3384248.
  10. M Göös, J Nordström, T Pitassi, R Robere, D Sokolov, and S deRezende. Automating algebraic proof systems is np-hard. Preprint available at the Electronic Colloquium on Computational Complexity (ECCC), TR20-064, 2020. URL: https://eccc.weizmann.ac.il/report/2020/064/.
  11. Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. The Journal of Symbolic Logic, 59(1):73-86, 1994. URL: https://doi.org/10.2307/2275250.
  12. Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. URL: https://doi.org/10.2307/2275541.
  13. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-2):123-140, 2001. URL: https://doi.org/10.4064/fm170-1-8.
  14. Jan Krajíček. On the proof complexity of the Nisan-Wigderson generator based on a hard NP ∩ coNP function. Journal of Mathematical Logic, 11(01):11-27, 2011. URL: https://doi.org/10.1142/S0219061311000979.
  15. Jan Krajíček. Proof Complexity. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108242066.
  16. Jan Krajíček and Pavel Pudlák. Some consequences of cryptographical conjectures for S₂¹ and EF. Information and Computation, 140(1):82-94, 1998. URL: https://doi.org/10.1006/inco.1997.2674.
  17. Jan Krajíček, Pavel Pudlák, and Alan Woods. An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures & Algorithms, 7(1):15-39, 1995. URL: https://doi.org/10.1002/rsa.3240070103.
  18. Theodoros Papamakarios. Depth d frege systems are not automatable unless p = np. Preprint available at the Electronic Colloquium on Computational Complexity (ECCC), TR23-121, 2023. URL: https://eccc.weizmann.ac.il/report/2023/121/.
  19. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity, 3(2):97-140, 1993. URL: https://doi.org/10.1007/BF01200117.
  20. Pavel Pudlák. On reducibility and symmetry of disjoint NP-pairs. Theoretical Computer Science, 295:323-339, 2003. Google Scholar
  21. Nathan Segerlind, Samuel R. Buss, and Russel Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM Journal on Computing, 33(5):1171-1200, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact