Document Open Access Logo

Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs

Authors Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.49.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Nicola Galesi
  • Dipartimento di Informatica, Sapienza Università di Roma, Via Salaria 113, Rome, Italy
Dmitry Itsykson
  • St. Petersburg Department of V.A. Steklov Institute of Mathematics of the , Russian Academy of Sciences, Fontanka 27, St. Petersburg, Russia
Artur Riazanov
  • St. Petersburg Department of V.A. Steklov Institute of Mathematics of the , Russian Academy of Sciences, Fontanka 27, St. Petersburg, Russia
Anastasia Sofronova
  • St. Petersburg Department of V.A. Steklov Institute of Mathematics of the , Russian Academy of Sciences, Fontanka 27, St. Petersburg, Russia
  • St. Petersburg State University, 7-9 Universitetskaya Emb., St. Petersburg, Russia

Funding

The research is supported by Russian Science Foundation (project 16-11-10123).

Acknowledgements

The authors thank Navid Talebanfard for discussions on the lower bound. Nicola also thanks Paul Wollan for introducing him to the tree-cutwidth. Dmitry is a Young Russian Mathematics award winner and would like to thank sponsors and jury of the contest.

Cite As Get BibTex

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.49

Abstract

We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2^{tw(G)^{O(1/d)}} poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational complexity and cryptography
Keywords
  • Tseitin formula
  • treewidth
  • AC0-Frege

Metrics

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

Related Versions

References

  1. Miklós Ajtai. The Complexity of the Pigeonhole Principle. Combinatorica, 14(4):417-433, 1994. URL: https://doi.org/10.1007/BF01302964.
  2. Michael Alekhnovich and Alexander A. Razborov. Satisfiability, Branch-Width and Tseitin tautologies. Computational Complexity, 20(4):649-678, 2011. URL: https://doi.org/10.1007/s00037-011-0033-1.
  3. Paul Beame, Chris Beck, and Russell Impagliazzo. Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space. SIAM J. Comput., 45(4):1612-1645, 2016. URL: https://doi.org/10.1137/130914085.
  4. 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. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/SFCS.1996.548486.
  5. Stephen Bellantoni, Toniann Pitassi, and Alasdair Urquhart. Approximation and Small-Depth Frege Proofs. SIAM J. Comput., 21(6):1161-1179, 1992. URL: https://doi.org/10.1137/0221068.
  6. Rémy Belmonte, Archontia Giannopoulou, Daniel Lokshtanov, and Dimitrios M. Thilikos. The Structure of of W₄-Immersion-Free Graphs. ICGT 2014, Arxiv: 1602.02002, February 2016. URL: http://arxiv.org/abs/1602.02002.
  7. Eli Ben-Sasson. Hard examples for the bounded depth Frege proof system. Computational Complexity, 11(3-4):109-136, 2002. URL: https://doi.org/10.1007/s00037-002-0172-5.
  8. 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.
  9. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover-Delayer games. Inf. Process. Lett., 110(23):1074-1077, 2010. URL: https://doi.org/10.1016/j.ipl.2010.09.007.
  10. Samuel R. Buss. Polynomial Size Proofs of the Propositional Pigeonhole Principle. J. Symb. Log., 52(4):916-927, 1987. URL: https://doi.org/10.2307/2273826.
  11. Julia Chuzhoy. Excluded Grid Theorem: Improved and Simplified. In Rocco A. Servedio and Ronitt Rubinfeld, editors, Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17, 2015, pages 645-654. ACM, 2015. URL: https://doi.org/10.1145/2746539.2746551.
  12. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  13. Stefan S. Dantchev and Søren Riis. Tree Resolution Proofs of the Weak Pigeon-Hole Principle. In Proceedings of the 16th Annual IEEE Conference on Computational Complexity, Chicago, Illinois, USA, June 18-21, 2001, pages 69-75. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/CCC.2001.933873.
  14. Zdenek Dvorák and Paul Wollan. A Structure Theorem for Strong Immersions. Journal of Graph Theory, 83(2):152-163, 2016. URL: https://doi.org/10.1002/jgt.21990.
  15. Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, Circuits, and the Polynomial-Time Hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. URL: https://doi.org/10.1007/BF01744431.
  16. Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-depth Frege complexity of Tseitin formulas for all graphs. Technical Report 19-069, Electronic Colloquium on Computational Complexity (ECCC), 2019. URL: https://eccc.weizmann.ac.il/report/2019/069.
  17. Nicola Galesi, Navid Talebanfard, and Jacobo Torán. Cops-Robber Games and the Resolution of Tseitin Formulas. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 311-326. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_19.
  18. Ludmila Glinskih and Dmitry Itsykson. On Tseitin formulas, read-once branching programs and treewidth. Electronic Colloquium on Computational Complexity (ECCC), 26:20, 2019. URL: https://eccc.weizmann.ac.il/report/2019/020.
  19. Armin Haken. The Intractability of Resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  20. Daniel J. Harvey and David R. Wood. The treewidth of line graphs. Journal of Combinatorial Theory, Series B, 132:157-179, 2018. URL: https://doi.org/10.1016/j.jctb.2018.03.007.
  21. J. Hastad. Computational Limitations of Small-Depth Circuits. MIT press, 1987. Google Scholar
  22. Johan Håstad. On Small-Depth Frege Proofs for Tseitin for Grids. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 97-108. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.18.
  23. Dmitry Itsykson and Vsevolod Oparin. Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP. In Andrei A. Bulatov and Arseny M. Shur, editors, Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings, volume 7913 of Lecture Notes in Computer Science, pages 162-173. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38536-0_14.
  24. Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, and Dmitry Sokolov. Tight Lower Bounds on the Resolution Complexity of Perfect Matching Principles. Fundam. Inform., 145(3):229-242, 2016. URL: https://doi.org/10.3233/FI-2016-1358.
  25. S. Jukna. Boolean Function Complexity: Advances and Frontiers. Springer, 2012. Google Scholar
  26. Jan Krajícek, Pavel Pudlák, and Alan R. Woods. An Exponenetioal Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole Principle. Random Struct. Algorithms, 7(1):15-40, 1995. URL: https://doi.org/10.1002/rsa.3240070103.
  27. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential Lower Bounds for the Pigeonhole Principle. Computational Complexity, 3:97-140, 1993. URL: https://doi.org/10.1007/BF01200117.
  28. Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, and Li-Yang Tan. Poly-logarithmic Frege depth lower bounds via an expander switching lemma. In Daniel Wichs and Yishay Mansour, editors, Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge, MA, USA, June 18-21, 2016, pages 644-657. ACM, 2016. URL: https://doi.org/10.1145/2897518.2897637.
  29. Pavel Pudlák and Samuel R. Buss. How to lie without being (easily) convicted and the lengths of proofs in propositional calculus. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, pages 151-162, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  30. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115-138, 2004. URL: https://doi.org/10.1145/972639.972640.
  31. A. Razborov. Lower Bounds on the Size of Bounded Depth Networks Over a Complete Basis with Logical Addition. Matematicheskie Zametki, 41:598-607, 1987. Google Scholar
  32. Alexander A. Razborov. Resolution lower bounds for the weak functional pigeonhole principle. Theor. Comput. Sci., 303(1):233-243, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00453-X.
  33. Alexander A. Razborov. Resolution lower bounds for perfect matching principles. J. Comput. Syst. Sci., 69(1):3-27, 2004. URL: https://doi.org/10.1016/j.jcss.2004.01.004.
  34. Roman Smolensky. Algebraic Methods in the Theory of Lower Bounds for Boolean Circuit Complexity. In Alfred V. Aho, editor, Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 77-82. ACM, 1987. URL: https://doi.org/10.1145/28395.28404.
  35. G.S. Tseitin. On the complexity of derivation in the propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic Part II. A. O. Slisenko, editor, a968. Google Scholar
  36. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
  37. Alasdair Urquhart and Xudong Fu. Simplified Lower Bounds for Propositional Proofs. Notre Dame Journal of Formal Logic, 37(4):523-544, 1996. URL: https://doi.org/10.1305/ndjfl/1040046140.
  38. David R. Wood. On tree-partition-width. European Journal of Combinatorics, 30(5):1245-1253, 2009. Part Special Issue on Metric Graph Theory. URL: https://doi.org/10.1016/j.ejc.2008.11.010.
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 About DROPS Imprint Privacy Contact