Document Open Access Logo

Short Proofs Are Hard to Find

Authors Ian Mertz, Toniann Pitassi, Yuanhao Wei

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.84.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Ian Mertz
  • University of Toronto, Canada
Toniann Pitassi
  • University of Toronto, Canada
  • Institute for Advanced Study, Princeton, NJ, USA
Yuanhao Wei
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Mertz, Ian: Research supported by NSERC.
  • Pitassi, Toniann: Research supported by NSERC.
  • Wei, Yuanhao: Work done while a student at University of Toronto. Research supported by NSERC.

Acknowledgements

The authors thank Noah Fleming, Pravesh Kothari, Denis Pankratov, Robert Robere, Mika Göös, and Avi Wigderson for helpful conversations. We also thank Yijia Chen for providing more details on the construction in [Yijia Chen and Bingkai Lin, 2016], and Pasin Manurangsi for giving feedback on the parameters in [Parinya Chalermsook et al., 2017].

Cite AsGet BibTex

Ian Mertz, Toniann Pitassi, and Yuanhao Wei. Short Proofs Are Hard to Find. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 84:1-84:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ICALP.2019.84

Abstract

We obtain a streamlined proof of an important result by Alekhnovich and Razborov [Michael Alekhnovich and Alexander A. Razborov, 2008], showing that it is hard to automatize both tree-like and general Resolution. Under a different assumption than [Michael Alekhnovich and Alexander A. Razborov, 2008], our simplified proof gives improved bounds: we show under ETH that these proof systems are not automatizable in time n^f(n), whenever f(n) = o(log^{1/7 - epsilon} log n) for any epsilon > 0. Previously non-automatizability was only known for f(n) = O(1). Our proof also extends fairly straightforwardly to prove similar hardness results for PCR and Res(r).

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Hardware → Theorem proving and SAT solving
Keywords
  • automatizability
  • Resolution
  • SAT solvers
  • proof complexity

Metrics

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

Related Versions

References

  1. Michael Alekhnovich, Samuel R. Buss, Shlomo Moran, and Toniann Pitassi. Minimum Propositional Proof Length Is NP-Hard to Linearly Approximate. J. Symb. Log., 66(1):171-191, 2001. Google Scholar
  2. Michael Alekhnovich and Alexander A. Razborov. Resolution Is Not Automatizable Unless W[P] Is Tractable. SIAM J. Comput., 38(4):1347-1363, 2008. Google Scholar
  3. Noga Alon, Oded Goldreich, Johan Håstad, and René Peralta. Simple Construction of Almost k-wise Independent Random Variables. Random Struct. Algorithms, 3(3):289-304, 1992. Google Scholar
  4. Albart Atserias and Moritz Müller. Automating Resolution is NP-Hard. CoRR, abs/1904.02991, 2019. URL: http://arxiv.org/abs/1904.02991.
  5. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. Google Scholar
  6. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow Proofs May Be Maximally Long. ACM Trans. Comput. Log., 17(3):19:1-19:30, 2016. Google Scholar
  7. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower Bound on Hilbert’s Nullstellensatz and propositional proofs. In 35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, 20-22 November 1994, pages 794-806, 1994. Google Scholar
  8. Paul Beame and Toniann Pitassi. Simplified and Improved Resolution Lower Bounds. In 37th Annual Symposium on Foundations of Computer Science, FOCS '96, Burlington, Vermont, USA, 14-16 October, 1996, pages 274-282, 1996. Google Scholar
  9. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  10. Maria 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, 2004. Google Scholar
  11. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On Interpolation and Automatization for Frege Systems. SIAM J. Comput., 29(6):1939-1967, 2000. Google Scholar
  12. Michael Brickenstein and Alexander Dreyer. PolyBoRi: A Framework for GröBner-basis Computations with Boolean Polynomials. J. Symb. Comput., 44(9):1326-1345, 2009. Google Scholar
  13. Parinya Chalermsook, Marek Cygan, Guy Kortsarz, Bundit Laekhanukit, Pasin Manurangsi, Danupon Nanongkai, and Luca Trevisan. From Gap-ETH to FPT-Inapproximability: Clique, Dominating Set, and More. CoRR, abs/1708.04218, 2017. URL: http://arxiv.org/abs/1708.04218.
  14. Yijia Chen and Bingkai Lin. The Constant Inapproximability of the Parameterized Dominating Set Problem. In IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, 9-11 October 2016, Hyatt Regency, New Brunswick, New Jersey, USA, pages 505-514, 2016. Google Scholar
  15. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 174-183, 1996. Google Scholar
  16. Martin Davis, George Logemann, and Donald Loveland. A Machine Program for Theorem-Proving. J. ACM, 5(7):394-397, 1961. Google Scholar
  17. Martin Davis and Hilary Putnam. A Computing Procedure for Quantification Theory. J. ACM, 7(3):201-215, 1960. Google Scholar
  18. Irit Dinur. Mildly exponential reduction from gap 3SAT to polynomial-gap label-cover. Electronic Colloquium on Computational Complexity (ECCC), 23:128, 2016. Google Scholar
  19. K. Eickmeyer, M. Grohe, and M. Gruber. Approximation of natural W[P]-complete minimisation problems is hard. In 23rd Annual IEEE Conference on Computational Complexity, CCC, pages 8-18, 2008. Google Scholar
  20. Nicola Galesi and Massimo Lauria. On the Automatizability of Polynomial Calculus. Theory Comput. Syst., 47(2):491-506, 2010. Google Scholar
  21. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone Circuit Lower Bounds from Resolution. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, pages 902-911, 2018. Google Scholar
  22. Mika Göös, Toniann Pitassi, and Thomas Watson. Query-to-Communication Lifting for BPP. In IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, pages 132-143. IEEE Computer Society, 2017. Google Scholar
  23. Russell Impagliazzo and Ramamohan Paturi. On the Complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367-375, 2001. Google Scholar
  24. Stasys Jukna. Extremal Combinatorics: With Applications in Computer Science. Springer Publishing Company, Incorporated, 1st edition, 2010. Google Scholar
  25. Jan Krajíček and Pavel Pudlák. Some Consequences of Cryptographical Conjectures for S^1_2 and EF. Inf. Comput., 140(1):82-94, 1998. Google Scholar
  26. J. Lasserre. Global Optimization With Polynomials and the Problem of Moments. SIAM J. Optimization, 11(3):796-817, 2001. Google Scholar
  27. Pasin Manurangsi and Prasad Raghavendra. A Birthday Repetition Theorem and Complexity of Approximating Dense CSPs. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, pages 78:1-78:15, 2017. Google Scholar
  28. Hugues Marchand, Alexander Martin, Robert Weismantel, and Laurence Wolsey. Cutting planes in integer and mixed integer programming. Discrete Applied Mathematics, 123(1):397-446, 2002. Google Scholar
  29. Joao Marques-Silva and Karem A. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers, 48:506-521, 1999. Google Scholar
  30. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In DAC, 2001. Google Scholar
  31. Joseph Naor and Moni Naor. Small-Bias Probability Spaces: Efficient Constructions and Applications. SIAM J. Comput., 22(4):838-856, 1993. Google Scholar
  32. Jakob Nordström. On the Interplay Between Proof Complexity and SAT Solving. ACM SIGLOG News, 2(3):19-44, 2015. Google Scholar
  33. Ryan O'Donnell. SOS is not obviously automatizable, even approximately. Electronic Colloquium on Computational Complexity (ECCC), 23:141, 2016. Google Scholar
  34. Pablo Parrilo. Structured Semidefinite Programs and Semialgebraic Geometry. Methods in Robustness and Optimization, 2000. Google Scholar
  35. K. Pipatsrisawat and A. Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, 2011. Google Scholar
  36. Pavel Pudlák. Proofs as Games. The American Mathematical Monthly, 107(6):541-550, 2000. Google Scholar
  37. Prasad Raghavendra. Optimal Algorithms and Inapproximability Results for Every CSP? In Proceedings of the Fortieth Annual ACM Symposium on Theory of Computing, STOC '08, pages 245-254, 2008. Google Scholar
  38. Prasad Raghavendra, Tselil Schramm, and David Steurer. High-dimensional estimation via sum-of-squares proofs. CoRR, 2018. URL: http://arxiv.org/abs/1807.11419.
  39. Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo. A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM J. Comput., 33(5):1171-1200, 2004. Google Scholar
  40. H Sherali and W Adams. A Hierarchy of Relaxations Between the Continuous and Convex Hull Representations for Zero-One Programming Problems. SIAM J. Disc. Math, 3(3):411-430, 1990. Google Scholar
  41. Johan Thapper and Stanislav Zivny. The power of Sherali-Adams relaxations for general-valued CSPs. CoRR, 2016. URL: http://arxiv.org/abs/1606.02577.
  42. M. Vinyals, J. Elffers, J. Giráldez-Cru, S. Gocht, and J Nordström. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, 2011. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact