Document Open Access Logo

A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion

Authors Anastasia Sofronova , Dmitry Sokolov

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CCC.2025.32.pdf
  • Filesize: 1.07 MB
  • 27 pages
HTML5 Logo HTML (experimental)
LIPIcs.CCC.2025.32.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • random CNFs

Metrics

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

Abstract

Random Δ-CNF formulas are one of the few candidates that are expected to be hard for proof systems and SAT algotirhms. Assume we sample m clauses over n variables. Here, the main complexity parameter is clause density, χ := m/n. For a fixed Δ, there exists a satisfiability threshold c_Δ such that for χ > c_Δ a formula is unsatisfiable with high probability. and for χ < c_Δ it is satisfiable with high probability. Near satisfiability threshold, there are various lower bounds for algorithms and proof systems [Eli Ben-Sasson, 2001; Eli Ben-Sasson and Russell Impagliazzo, 1999; Michael Alekhnovich and Alexander A. Razborov, 2003; Dima Grigoriev, 2001; Grant Schoenebeck, 2008; Pavel Hrubes and Pavel Pudlák, 2017; Noah Fleming et al., 2017; Dmitry Sokolov, 2024], and for high-density regimes, there exist upper bounds [Uriel Feige et al., 2006; Sebastian Müller and Iddo Tzameret, 2014; Jackson Abascal et al., 2021; Venkatesan Guruswami et al., 2022]. 
One of the frontiers in the direction of proving lower bounds on these formulas is the k-DNF Resolution proof system (aka Res(k)). There are several known results for k = 𝒪(√{log n}/{log log n}}) [Nathan Segerlind et al., 2004; Michael Alekhnovich, 2011], that are applicable only for density regime near the threshold. In this paper, we show the first Res(k) lower bound that is applicable in higher-density regimes. Our results work for slightly larger k = 𝒪(√{log n}).

Cite As Get BibTex

Anastasia Sofronova and Dmitry Sokolov. A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 32:1-32:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CCC.2025.32

Author Details

Anastasia Sofronova
  • École Polytechnique Fédérale de Lausanne, Switzerland
Dmitry Sokolov
  • École Polytechnique Fédérale de Lausanne, Switzerland

Funding

This work was supported by the Swiss State Secretariat for Education, Research and Innovation (SERI) under contract number MB22.00026.

Acknowledgements

The authors would like to thank Edward Hirsch for comments on the draft, as well as the anonymous reviewers.

References

  1. Jackson Abascal, Venkatesan Guruswami, and Pravesh K. Kothari. Strongly refuting all semi-random boolean csps. In Dániel Marx, editor, Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, Virtual Conference, January 10 - 13, 2021, pages 454-472. SIAM, 2021. URL: https://doi.org/10.1137/1.9781611976465.28.
  2. Miklós Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417-433, 1994. URL: https://doi.org/10.1007/BF01302964.
  3. Michael Alekhnovich. Lower bounds for k-dnf resolution on random 3-cnfs. Comput. Complex., 20(4):597-614, 2011. URL: https://doi.org/10.1007/s00037-011-0026-0.
  4. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Pseudorandom generators in propositional proof complexity. SIAM J. Comput., 34(1):67-88, 2004. URL: https://doi.org/10.1137/S0097539701389944.
  5. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics, 242:18-35, 2003. Available at http://people.cs.uchicago.edu/~razborov/files/misha.pdf. Preliminary version in FOCS '01.
  6. Sarah R. Allen, Ryan O'Donnell, and David Witmer. How to refute a random CSP. In Venkatesan Guruswami, editor, IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 689-708. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/FOCS.2015.48.
  7. Omar Alrabiah, Venkatesan Guruswami, Pravesh K. Kothari, and Peter Manohar. A near-cubic lower bound for 3-query locally decodable codes from semirandom CSP refutation. In Barna Saha and Rocco A. Servedio, editors, Proceedings of the 55th Annual ACM Symposium on Theory of Computing, STOC 2023, Orlando, FL, USA, June 20-23, 2023, pages 1438-1448. ACM, 2023. URL: https://doi.org/10.1145/3564246.3585143.
  8. Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Alexander A. Razborov. Clique is hard on average for regular resolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 866-877. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188856.
  9. Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban. Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Inf. Comput., 176(2):136-152, 2002. URL: https://doi.org/10.1006/inco.2002.3114.
  10. Paul Beame, Russell Impagliazzo, Jan Krajícek, 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. URL: https://doi.org/10.1109/SFCS.1994.365714.
  11. Paul Beame, Richard M. Karp, Toniann Pitassi, and Michael E. Saks. The efficiency of resolution and davis-putnam procedures. SIAM J. Comput., 31(4):1048-1075, 2002. URL: https://doi.org/10.1137/S0097539700369156.
  12. Eli Ben-Sasson. Expansion in proof complexity. PhD thesis, Hebrew University of Jerusalem, Israel, 2001. URL: https://huji-primo.hosted.exlibrisgroup.com/permalink/f/13ns5ae/972HUJI_ALMA21159933340003701.
  13. Eli Ben-Sasson and Russell Impagliazzo. 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, pages 415-421. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814613.
  14. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
  15. Vašek Chvátal and Endre Szemerédi. Many hard examples for resolution. J. ACM, 35(4):759-768, October 1988. URL: https://doi.org/10.1145/48014.48016.
  16. Susanna F. de Rezende, Jakob Nordström, Kilian Risse, and Dmitry Sokolov. Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs. CoRR, abs/1912.00534, 2019. URL: https://arxiv.org/abs/1912.00534.
  17. Susanna F. de Rezende, Aaron Potechin, and Kilian Risse. Clique is hard on average for unary sherali-adams. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023, pages 12-25. IEEE, 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00008.
  18. Uriel Feige. 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, page 5. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/CCC.2002.10006.
  19. Uriel Feige, Jeong Han Kim, and Eran Ofek. 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, pages 497-508. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/FOCS.2006.78.
  20. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-cnfs are hard for cutting planes. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109-120. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.19.
  21. Konstantinos Georgiou, Avner Magen, and Madhur Tulsiani. Optimal sherali-adams gaps from pairwise independence. In Irit Dinur, Klaus Jansen, Joseph Naor, and José Rolim, editors, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, pages 125-139, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-03685-9_10.
  22. Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259(1):613-622, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00157-2.
  23. Venkatesan Guruswami, Pravesh K. Kothari, and Peter Manohar. Algorithms and certificates for boolean CSP refutation: smoothed is no harder than random. In Stefano Leonardi and Anupam Gupta, editors, STOC '22: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pages 678-689. ACM, 2022. URL: https://doi.org/10.1145/3519935.3519955.
  24. Johan Håstad. On small-depth frege proofs for tseitin for grids. J. ACM, 68(1):1:1-1:31, 2021. URL: https://doi.org/10.1145/3425606.
  25. Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 121-131. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.20.
  26. Pravesh K. Kothari and Peter Manohar. An exponential lower bound for linear 3-query locally correctable codes. In Bojan Mohar, Igor Shinkar, and Ryan O'Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 776-787. ACM, 2024. URL: https://doi.org/10.1145/3618260.3649640.
  27. Pravesh K. Kothari, Ryuhei Mori, Ryan O'Donnell, and David Witmer. Sum of squares lower bounds for refuting any CSP. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 132-145. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055485.
  28. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170:123-140, January 2001. URL: https://doi.org/10.4064/fm170-1-8.
  29. Sebastian Müller and Iddo Tzameret. Short propositional refutations for dense random 3cnf formulas. Ann. Pure Appl. Log., 165(12):1864-1918, 2014. URL: https://doi.org/10.1016/j.apal.2014.08.001.
  30. Ryan O'Donnell. Analysis of Boolean Functions. Cambridge University Press, 2014. URL: https://doi.org/10.1017/CBO9781139814782.
  31. Shuo Pang. Large clique is hard on average for resolution. In Rahul Santhanam and Daniil Musatov, editors, Computer Science - Theory and Applications - 16th International Computer Science Symposium in Russia, CSR 2021, Sochi, Russia, June 28 - July 2, 2021, Proceedings, volume 12730 of Lecture Notes in Computer Science, pages 361-380. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79416-3_22.
  32. Prasad Raghavendra, Satish Rao, and Tselil Schramm. Strongly refuting random csps below the spectral threshold. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 121-131. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055417.
  33. Alexander A. Razborov. Pseudorandom generators hard for k-dnf resolution and polynomial calculus resolution. Ann. of Math., 181:415-472, 2015. URL: https://doi.org/10.4007/annals.2015.181.2.1.
  34. Grant Schoenebeck. Linear level lasserre lower bounds for certain k-csps. In 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA, pages 593-602. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/FOCS.2008.74.
  35. 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. URL: https://doi.org/10.1137/S0097539703428555.
  36. Dmitry Sokolov. (semi)algebraic proofs over ±1 variables. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 78-90. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384288.
  37. Dmitry Sokolov. Random (log n)-cnf are hard for cutting planes (again). In Bojan Mohar, Igor Shinkar, and Ryan O'Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 2008-2015. ACM, 2024. URL: https://doi.org/10.1145/3618260.3649636.
  38. Salil P. Vadhan. Pseudorandomness. Now Publishers Inc., Hanover, MA, USA, 2012. Google Scholar
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