Random (log đ)-CNF Are Hard for Cutting Planes (Again)
Pages 2008 - 2015
Abstract
The random Î-CNF model is one of the most important distribution over Î-SAT instances. It is closely connected to various areas of computer science, statistical physics, and is a benchmark for satisfiability algorithms. Fleming, Pankratov, Pitassi, and Robere and independently HrubeĆĄ and PudlĂĄk showed that when Î = Î(logn), any Cutting Planes proof for random Î-CNF on n variables requires size 2n / n in the regime where the number of clauses guarantees that the formula is unsatisfiable with high probability. In this paper we show tight lower bound 2Ω(n) on size -proofs for random (logn)-CNF formulas. Moreover, our proof is much simpler and self-contained in contrast with previous results based on Juknaâs lower bound for monotone circuits.
References
[1]
Michael Alekhnovich. 2011. Lower Bounds for k-DNF Resolution on Random 3-CNFs. Comput. Complex., 20, 4 (2011), 597â614. https://doi.org/10.1007/s00037-011-0026-0
[2]
Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. 2004. Pseudorandom Generators in Propositional Proof Complexity. SIAM J. Comput., 34, 1 (2004), 67â88. https://doi.org/10.1137/S0097539701389944
[3]
Michael Alekhnovich and Alexander A. Razborov. 2003. Lower Bounds for Polynomial Calculus: Non-Binomial Case. Proceedings of the Steklov Institute of Mathematics, 242 (2003), 18â35. Available at http://people.cs.uchicago.edu/ razborov/files/misha.pdf
[4]
Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Alexander A. Razborov. 2018. Clique is hard on average for regular resolution. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, Ilias Diakonikolas, David Kempe, and Monika Henzinger (Eds.). ACM, 866â877. https://doi.org/10.1145/3188745.3188856
[5]
Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban. 2002. Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution. Inf. Comput., 176, 2 (2002), 136â152. https://doi.org/10.1006/inco.2002.3114
[6]
Paul Beame, Richard M. Karp, Toniann Pitassi, and Michael E. Saks. 2002. The Efficiency of Resolution and DavisâPutnam Procedures. SIAM J. Comput., 31, 4 (2002), 1048â1075. https://doi.org/10.1137/S0097539700369156
[7]
Eli Ben-Sasson and Russell Impagliazzo. 1999. Random CNFâs are Hard for the Polynomial Calculus. In 40th Annual Symposium on Foundations of Computer Science, FOCS â99, 17-18 October, 1999, New York, NY, USA. IEEE Computer Society, 415â421. https://doi.org/10.1109/SFFCS.1999.814613
[8]
Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. 1997. Lower Bounds for Cutting Planes Proofs with Small Coefficients. J. Symb. Log., 62, 3 (1997), 708â728. https://doi.org/10.2307/2275569
[9]
VaĆĄek ChvĂĄtal and Endre SzemerĂ©di. 1988. Many Hard Examples for Resolution. J. ACM, 35, 4 (1988), Oct., 759â768. issn:0004-5411 https://doi.org/10.1145/48014.48016
[10]
William J. Cook, Collette R. Coullard, and György TurĂĄn. 1987. On the complexity of cutting-plane proofs. Discret. Appl. Math., 18, 1 (1987), 25â38. https://doi.org/10.1016/0166-218X(87)90039-4
[11]
Susanna F. de Rezende, Mika Göös, and Robert Robere. 2022. Guest Column: Proofs, Circuits, and Communication. SIGACT News, 53, 1 (2022), 59â82. https://doi.org/10.1145/3532737.3532746
[12]
Uriel Feige. 2002. Relations between Average Case Complexity and Approximation Complexity. In Proceedings of the 17th Annual IEEE Conference on Computational Complexity, Montréal, Québec, Canada, May 21-24, 2002. IEEE Computer Society, 5. https://doi.org/10.1109/CCC.2002.10006
[13]
Uriel Feige, Jeong Han Kim, and Eran Ofek. 2006. Witnesses for non-satisfiability of dense random 3CNF formulas. In 47th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2006), 21-24 October 2006, Berkeley, California, USA, Proceedings. IEEE Computer Society, 497â508. https://doi.org/10.1109/FOCS.2006.78
[14]
Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. 2022. Random Î ( ologn)-CNFs are Hard for Cutting Planes. J. ACM, 69, 3 (2022), 19:1â19:32. https://doi.org/10.1145/3486680
[15]
Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. 2018. Monotone circuit lower bounds from resolution. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, Ilias Diakonikolas, David Kempe, and Monika Henzinger (Eds.). ACM, 902â911. https://doi.org/10.1145/3188745.3188838
[16]
Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. 2020. Automating cutting planes is NP-hard. In Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy (Eds.). ACM, 68â77. https://doi.org/10.1145/3357713.3384248
[17]
Mika Göös and Toniann Pitassi. 2018. Communication Lower Bounds via Critical Block Sensitivity. SIAM J. Comput., 47, 5 (2018), 1778â1806. https://doi.org/10.1137/16M1082007
[18]
Dima Grigoriev. 2001. Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259, 1 (2001), 613â622. issn:0304-3975 https://doi.org/10.1016/S0304-3975(00)00157-2
[19]
Armin Haken and Stephen A. Cook. 1999. An Exponential Lower Bound for the Size of Monotone Real Circuits. J. Comput. System Sci., 58, 2 (1999), 326â335. issn:0022-0000 https://doi.org/10.1006/jcss.1998.1617
[20]
Pavel HrubeĆĄ. 2013. A note on semantic cutting planes. Electronic Colloquium on Computational Complexity (ECCC), 20 (2013), 128. http://eccc.hpi-web.de/report/2013/128
[21]
Pavel HrubeĆĄ and Pavel PudlĂĄk. 2017. Random Formulas, Monotone Circuits, and Interpolation. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, Chris Umans (Ed.). IEEE Computer Society, 121â131. https://doi.org/10.1109/FOCS.2017.20
[22]
Pavel HrubeĆĄ and Pavel PudlĂĄk. 2018. A note on monotone real circuits. Inf. Process. Lett., 131 (2018), 15â19. https://doi.org/10.1016/j.ipl.2017.11.002
[23]
Jan KrajĂcek. 1997. Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. J. Symb. Log., 62, 2 (1997), 457â486. https://doi.org/10.2307/2275541
[24]
Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. 2022. Lifting with Sunflowers. In 13th Innovations in Theoretical Computer Science Conference, ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, Mark Braverman (Ed.) (LIPIcs, Vol. 215). Schloss Dagstuhl - Leibniz-Zentrum fĂŒr Informatik, 104:1â104:24. https://doi.org/10.4230/LIPIcs.ITCS.2022.104
[25]
Michael Mitzenmacher and Eli Upfal. 2005. Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press. isbn:978-0-521-83540-4 https://doi.org/10.1017/CBO9780511813603
[26]
Sebastian MĂŒller and Iddo Tzameret. 2014. Short propositional refutations for dense random 3CNF formulas. Ann. Pure Appl. Log., 165, 12 (2014), 1864â1918. https://doi.org/10.1016/j.apal.2014.08.001
[27]
Pavel PudlĂĄk. 1997. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. J. Symb. Log., 62, 3 (1997), 981â998. https://doi.org/10.2307/2275583
[28]
Pavel PudlĂĄk. 2010. On extracting computations from propositional proofs (a survey). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India. 30â41. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.30
[29]
Alexander A. Razborov. 1995. Bounded Arithmetic and Lower Bounds in Boolean Complexity. In Feasible Mathematics II, Peter Clote and Jeffrey B. Remmel (Eds.). BirkhĂ€user Boston, Boston, MA. 344â386. isbn:978-1-4612-2566-9
[30]
Alexander A. Razborov. 2015. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Ann. of Math., 181 (2015), 415â472. https://doi.org/10.4007/annals.2015.181.2.1
[31]
Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo. 2004. A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM J. Comput., 33, 5 (2004), 1171â1200. https://doi.org/10.1137/S0097539703428555
[32]
Anastasia Sofronova and Dmitry Sokolov. 2022. A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion. Electron. Colloquium Comput. Complex., TR22-054 (2022), ECCC:TR22-054. https://eccc.weizmann.ac.il/report/2022/054
[33]
Dmitry Sokolov. 2017. Dag-Like Communication and Its Applications. In Computer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Kazan, Russia, June 8-12, 2017, Proceedings, Pascal Weil (Ed.) (Lecture Notes in Computer Science, Vol. 10304). Springer, 294â307. https://doi.org/10.1007/978-3-319-58747-9_26
[34]
Dmitry Sokolov. 2020. (Semi)Algebraic proofs over ± 1 variables. In Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy (Eds.). ACM, 78â90. https://doi.org/10.1145/3357713.3384288
Index Terms
- Random (log đ)-CNF Are Hard for Cutting Planes (Again)
Recommendations
The space complexity of cutting planes refutations
CCC '15: Proceedings of the 30th Conference on Computational ComplexityWe study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while ...
Automating cutting planes is NP-hard
STOC 2020: Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of ComputingWe show that Cutting Planes (CP) proofs are hard to find: Given an unsatisfiable formula F, It is -hard to find a CP refutation of F in time polynomial in the length of the shortest such refutation; and unless Gap-Hitting-Set admits a nontrivial ...
Random
\( \Theta (\log n) \) -CNFs are Hard for Cutting PlanesThe random k-SAT model is one of the most important and well-studied distributions over k-SAT instances. It is closely connected to statistical physics and is a benchmark for satisfiability algorithms. We show that when \( k = \Theta (\log n) \) , any ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2024
2049 pages
ISBN:9798400703836
DOI:10.1145/3618260
- General Chairs:
- Bojan Mohar,
- Igor Shinkar,
- Program Chair:
- Ryan O'Donnell
Copyright © 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 June 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
STOC '24
Sponsor:
Acceptance Rates
Overall Acceptance Rate 1,469 of 4,586 submissions, 32%
Upcoming Conference
STOC '25
- Sponsor:
- sigact
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 68Total Downloads
- Downloads (Last 12 months)68
- Downloads (Last 6 weeks)5
Reflects downloads up to 04 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in