Document Open Access Logo

On the Automatability of Tree-Like k-DNF Resolution

Authors Gaia Carenini , Susanna F. de Rezende

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CCC.2025.14.pdf
  • Filesize: 0.94 MB
  • 21 pages
HTML5 Logo HTML (experimental)
LIPIcs.CCC.2025.14.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Proof Complexity
  • Tree-like k-DNF Resolution
  • Automatability

Metrics

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

Abstract

A proof system 𝒫 is said to be automatable in time f(N) if there exists an algorithm that given as input an unsatisfiable formula F outputs a refutation of F in the proof system 𝒫 in time f(N), where N is the size of the smallest 𝒫-refutation of F plus the size of F. Atserias and Bonet (ECCC 2002), observed that tree-like k-DNF resolution is automatable in time N^{c⋅klog N} for a universal constant c. We show that, under the randomized exponential-time hypothesis (rETH), this is tight up to a O(log k)-factor in the exponent, i.e., we prove that tree-like k-DNF resolution, for k at most logarithmic in the number of variables of F, is not automatable in time N^o((k/log k)⋅log N) unless rETH is false. Our proof builds on the non-automatability results for resolution by Atserias and Müller (FOCS 2019), for algebraic proof systems by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (STOC 2021), and for tree-like resolution by de Rezende (LAGOS 2021).

Cite As Get BibTex

Gaia Carenini and Susanna F. de Rezende. On the Automatability of Tree-Like k-DNF Resolution. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CCC.2025.14

Author Details

Gaia Carenini
  • University of Cambridge, UK
Susanna F. de Rezende
  • Lund University, Sweden

Funding

  • Carenini, Gaia: Trinity College CB European PhD Studentship.
  • de Rezende, Susanna F.: Knut and Alice Wallenberg grants KAW 2018.0371 and KAW 2021.0307, ELLIIT, and the Swedish Research Council grant 2021-05104.

Acknowledgements

The authors wish to thank Noel Arteche and Jonas Conneryd for feedback on the presentation. We are also grateful to the anonymous reviewers for their careful reading of our manuscript and their many insightful comments and suggestions. Part of this work was done while G. Carenini was a student at the Department of Computer Science of Ecole Normale Supérieure - PSL Research University, Paris, France.

References

  1. Michael Alekhnovich, Sam Buss, Shlomo Moran, and Toniann Pitassi. Minimum propositional proof length is NP-hard to linearly approximate. Journal of Symbolic Logic, 66(1):171-191, 2001. URL: https://doi.org/10.2307/2694916.
  2. Michael Alekhnovich and Alexander A. Razborov. Resolution is not automatizable unless W[P] is tractable. SIAM Journal on Computing, 38(4):1347-1363, 2008. Preliminary version in FOCS '01. URL: https://doi.org/10.1137/06066850X.
  3. Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum automating TC⁰-Frege is LWE-hard. In Proceedings of the 39th Computational Complexity Conference (CCC '24), volume 300 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:25, July 2024. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.15.
  4. Albert Atserias and María Luisa Bonet. On the automatizability of resolution and related propositional proof systems. Technical Report TR02-010, Electronic Colloquium on Computational Complexity (ECCC), 2002. URL: https://eccc.weizmann.ac.il/report/2002/010/.
  5. Albert Atserias and María Luisa Bonet. On the automatizability of resolution and related propositional proof systems. Information and Computation, 189(2):182-201, March 2004. Preliminary version in CSL '02. URL: https://doi.org/10.1016/j.ic.2003.10.004.
  6. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. Journal of the ACM, 67(5), 2020. Preliminary version in FOCS '19. URL: https://doi.org/10.1145/3409472.
  7. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In Proceedings of the 37th Annual IEEE Symposium on Foundations of Computer Science (FOCS '96), pages 274-282, October 1996. URL: https://doi.org/10.1109/SFCS.1996.548486.
  8. Zoë Bell. Automating regular or ordered resolution is NP-hard. Technical Report TR20-105, Electronic Colloquium on Computational Complexity (ECCC), 2020. URL: https://eccc.weizmann.ac.il/report/2020/105/.
  9. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
  10. John Adrian Bondy and Uppaluri Siva Ramachandra Murty. Graph theory. Springer, 2008. Google Scholar
  11. María Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth Frege proofs. Computational Complexity, 13(1-2):47-68, December 2004. Preliminary version in CCC '99. URL: https://doi.org/10.1007/s00037-004-0183-5.
  12. María Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM Journal on Computing, 29(6):1939-1967, 2000. Preliminary version in FOCS '97. URL: https://doi.org/10.1137/S0097539798353230.
  13. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC 96), pages 174-183, 1996. URL: https://doi.org/10.1145/237814.237860.
  14. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394-397, July 1962. URL: https://doi.org/10.1145/368273.368557.
  15. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  16. Susanna F. de Rezende. Automating tree-like resolution in time n^o(log n) is ETH-hard. In Proceedings of the 11th Latin and American Algorithms, Graphs and Optimization Symposium (LAGOS '21), May 2021. URL: https://doi.org/10.1016/j.procs.2021.11.021.
  17. Susanna F. de Rezende. Automating tree-like resolution in time n^o(log n) is ETH-hard. Technical Report TR21-033, Electronic Colloquium on Computational Complexity (ECCC), 2021. URL: https://eccc.weizmann.ac.il/report/2021/033/.
  18. Susanna F. de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, and Dmitry Sokolov. Automating algebraic proof systems is NP-hard. In Proceedings of the 53rd Annual ACM Symposium on Theory of Computing (STOC '21), June 2021. URL: https://doi.org/10.1145/3406325.3451080.
  19. Holger Dell, Thore Husfeldt, Dániel Marx, Nina Taslaman, and Martin Wahlén. Exponential time complexity of the permanent and the Tutte polynomial. ACM Trans. Algorithms, 10(4):21:1-21:32, August 2014. URL: https://doi.org/10.1145/2635812.
  20. Kord Eickmeyer, Martin Grohe, and Magdalena Grüber. Approximation of natural W[P]-complete minimisation problems is hard. In Proceedings of the 23rd Annual IEEE Conference on Computational Complexity (CCC '08), pages 8-18, June 2008. URL: https://doi.org/10.1109/CCC.2008.24.
  21. Nicola Galesi and Massimo Lauria. On the automatizability of polynomial calculus. Theory of Computing Systems, 47(2):491-506, 2010. URL: https://doi.org/10.1007/s00224-009-9195-5.
  22. Michal Garlík. Failure of feasible disjunction property for k-dnf resolution and NP-hardness of automating it. In Proceedings of the 39th Computational Complexity Conference (CCC '24), volume 300 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1-33:23, July 2024. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.33.
  23. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is NP-hard. In Proceedings of the 52nd Annual ACM Symposium on Theory of Computing (STOC '20), pages 68-77, June 2020. URL: https://doi.org/10.1145/3357713.3384248.
  24. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-SAT. Journal of Computer and System Sciences, 62(2):367-375, March 2001. Preliminary version in CCC '99. URL: https://doi.org/10.1006/jcss.2000.1727.
  25. Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In Proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS '22), volume 241 of Leibniz International Proceedings in Informatics (LIPIcs), pages 59:1-59:15, August 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.59.
  26. Kazuo Iwama. Complexity of finding short resolution proofs. In Proceedings of the 22nd International Symposium on Mathematical Foundations of Computer Science (MFCS '97), pages 309-318, 1997. URL: https://doi.org/10.1007/BFb0029974.
  27. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001. URL: https://doi.org/10.4064/fm170-1-8.
  28. Jan Krajícek 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.
  29. Jan Krajič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.
  30. Massimo Lauria. A note about k-DNF resolution. Information Processing Letters, 137:33-39, September 2018. URL: https://doi.org/10.1016/j.ipl.2018.04.014.
  31. Ian Mertz, Toniann Pitassi, and Yuanhao Wei. Short proofs are hard to find. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming (ICALP '19), pages 84:1-84:16, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.84.
  32. Ryan O'Donnell. SOS is not obviously automatizable, even approximately. In Proceedings of the 8th Innovations in Theoretical Computer Science Conference (ITCS), volume 67, pages 59:1-59:10. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPIcs.ITCS.2017.59.
  33. Theodoros Papamakarios. Depth-d Frege systems are not automatable unless P=NP. In Proceedings of the 39th Computational Complexity Conference (CCC '24), volume 300 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17, July 2024. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.22.
  34. Pavel Pudlák. On reducibility and symmetry of disjoint NP pairs. Theoretical Computer Science, 295:323-339, February 2003. URL: https://doi.org/10.1016/S0304-3975(02)00411-5.
  35. Prasad Raghavendra and Benjamin Weitz. On the bit complexity of sum-of-squares proofs. In Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (ICALP), pages 80:1-80:13, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.80.
  36. Alexander A Razborov. On provably disjoint NP-pairs. Aarhus Universitet. Basic Research in Computer Science [BRICS], November 1994. URL: https://doi.org/10.7146/brics.v1i36.21607.
  37. John Alan Robinson. The generalized resolution principle. In Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pages 135-151. Springer, 1968. URL: https://doi.org/10.1007/978-3-642-81955-1_9.
  38. Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM Journal on Computing, 33(5):1171-1200, 2004. Preliminary version in FOCS '02. URL: https://doi.org/10.1109/SFCS.2002.1181984.
  39. Michael Sipser. The history and status of the p versus NP question. In Proceedings of the 24th Annual ACM Symposium on Theory of Computing (STOC '92), 1992. URL: https://doi.org/10.1145/129712.129771.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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