Document Open Access Logo

Tight Bounds for Tseitin Formulas

Authors Dmitry Itsykson, Artur Riazanov, Petr Smirnov

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.6.pdf
  • Filesize: 0.83 MB
  • 21 pages

Document Identifiers

Author Details

Dmitry Itsykson
  • St. Petersburg Department of V.A. Steklov Mathematical Institute of RAS, Russia
Artur Riazanov
  • St. Petersburg Department of V.A. Steklov Mathematical Institute of RAS, Russia
  • The Henry and Marylin Taub Faculty of Computer Science, Technion, Israel
Petr Smirnov
  • HSE University at Saint Petersburg, Russia
  • St. Petersburg Department of V.A. Steklov Mathematical Institute of RAS, Russia

Funding

  • Riazanov, Artur: The author is supported under the agreement 075-15-2022-289 and has also received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 802020-ERC-HARMONIC.
  • Smirnov, Petr: The author is supported under the agreement 075-15-2022-289.

Cite AsGet BibTex

Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight Bounds for Tseitin Formulas. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.6

Abstract

We show that for any connected graph G the size of any regular resolution or OBDD(∧, reordering) refutation of a Tseitin formula based on G is at least 2^Ω(tw(G)), where tw(G) is the treewidth of G. These lower bounds improve upon the previously known bounds and, moreover, they are tight. For both of the proof systems, there are constructive upper bounds that almost match the obtained lower bounds, hence the class of Tseitin formulas is almost automatable for regular resolution and for OBDD(∧, reordering).

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • Tseitin formulas
  • treewidth
  • resolution
  • OBDD-based proof systems

Metrics

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

References

  1. 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.
  2. Albert Atserias and Moritz Müller. Automating Resolution is NP-Hard. J. ACM, 67(5):31:1-31:17, 2020. URL: https://doi.org/10.1145/3409472.
  3. 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.
  4. Hans L. Bodlaender, Pål Grønås Drange, Markus S. Dregi, Fedor V. Fomin, Daniel Lokshtanov, and Michal Pilipczuk. A c^kn 5-Approximation Algorithm for Treewidth. SIAM J. Comput., 45(2):317-378, 2016. URL: https://doi.org/10.1137/130947374.
  5. Randal E. Bryant. Symbolic manipulation of Boolean functions using a graphical representation. In Hillel Ofek and Lawrence A O'Neill, editors, Proceedings of the 22nd ACM/IEEE conference on Design automation, DAC 1985, Las Vegas, Nevada, USA, 1985., pages 688-694. ACM, 1985. URL: https://doi.org/10.1145/317825.317964.
  6. Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov. Lower Bounds on OBDD Proofs with Several Orders. ACM Trans. Comput. Log., 22(4):26:1-26:30, 2021. URL: https://doi.org/10.1145/3468855.
  7. Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering Rule Makes OBDD Proof Systems Stronger. In Rocco A. Servedio, editor, 33rd Computational Complexity Conference, CCC 2018, June 22-24, 2018, San Diego, CA, USA, volume 102 of LIPIcs, pages 16:1-16:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CCC.2018.16.
  8. Julia Chuzhoy and Zihan Tan. Towards Tight(er) Bounds for the Excluded Grid Theorem. In Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2019, San Diego, California, USA, January 6-9, 2019, pages 1445-1464, 2019. URL: https://doi.org/10.1137/1.9781611975482.88.
  9. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  10. 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, 2001. URL: https://doi.org/10.1109/CCC.2001.933873.
  11. Adnan Darwiche and Pierre Marquis. A Knowledge Compilation Map. J. Artif. Intell. Res., 17:229-264, 2002. URL: https://doi.org/10.1613/jair.989.
  12. Alexis de Colnet and Stefan Mengel. Characterizing Tseitin-Formulas with Short Regular Resolution Refutations. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 116-133. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_9.
  13. Alexis de Colnet and Stefan Mengel. Lower Bounds on Intermediate Results in Bottom-Up Knowledge Compilation. CoRR, abs/2112.12430, 2021. URL: http://arxiv.org/abs/2112.12430.
  14. 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 Samir Khuller and Virginia Vassilevska Williams, editors, STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing, Virtual Event, Italy, June 21-25, 2021, pages 209-222. ACM, 2021. URL: https://doi.org/10.1145/3406325.3451080.
  15. Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 49:1-49:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.49.
  16. Michal Garlík. Failure of Feasible Disjunction Property for k-DNF Resolution and NP-hardness of Automating It. Electron. Colloquium Comput. Complex., page 37, 2020. URL: https://eccc.weizmann.ac.il/report/2020/037.
  17. Ludmila Glinskih and Dmitry Itsykson. Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 26:1-26:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.26.
  18. Ludmila Glinskih and Dmitry Itsykson. On Tseitin Formulas, Read-Once Branching Programs and Treewidth. Theory Comput. Syst., 65(3):613-633, 2021. URL: https://doi.org/10.1007/s00224-020-10007-8.
  19. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating Cutting Planes is NP-Hard. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, pages 68-77, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3357713.3384248.
  20. Daniel J. Harvey and David R. Wood. The treewidth of line graphs. J. Comb. Theory, Ser. B, 132:157-179, 2018. URL: https://doi.org/10.1016/j.jctb.2018.03.007.
  21. Johan Håstad. On Small-Depth Frege Proofs for Tseitin for Grids. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 97-108, 2017. URL: https://doi.org/10.1109/FOCS.2017.18.
  22. Dmitry Itsykson, Alexander Knop, Andrei E. Romashchenko, and Dmitry Sokolov. On OBDD-based Algorithms and Proof Systems that Dynamically Change the order of Variables. J. Symb. Log., 85(2):632-670, 2020. URL: https://doi.org/10.1017/jsl.2019.53.
  23. Dmitry Itsykson, Artur Riazanov, Danil Sagunov, and Petr Smirnov. Near-Optimal Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs. Comput. Complex., 30(2):13, 2021. URL: https://doi.org/10.1007/s00037-021-00213-2.
  24. Ephraim Korach and Nir Solel. Tree-Width, Path-Width, and Cutwidth. Discret. Appl. Math., 43(1):97-101, 1993. URL: https://doi.org/10.1016/0166-218X(93)90171-J.
  25. Jan Krajíček. Proof Complexity. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108242066.
  26. Knot Pipatsrisawat and Adnan Darwiche. New Compilation Languages Based on Structured Decomposability. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 517-522. AAAI Press, 2008. URL: http://www.aaai.org/Library/AAAI/2008/aaai08-082.php.
  27. Neil Robertson and Paul D. Seymour. Graph Minors. II. Algorithmic Aspects of Tree-Width. J. Algorithms, 7(3):309-322, 1986. URL: https://doi.org/10.1016/0196-6774(86)90023-4.
  28. Neil Robertson and Paul D. Seymour. Graph minors. X. Obstructions to tree-decomposition. J. Comb. Theory, Ser. B, 52(2):153-190, 1991. URL: https://doi.org/10.1016/0095-8956(91)90061-N.
  29. Neil Robertson, Paul D. Seymour, and Robin Thomas. Quickly Excluding a Planar Graph. J. Comb. Theory, Ser. B, 62(2):323-348, 1994. URL: https://doi.org/10.1006/jctb.1994.1073.
  30. 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, 1968. Google Scholar
  31. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
  32. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. URL: http://ls2-www.cs.uni-dortmund.de/monographs/bdd/.
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