Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Itsykson, Dmitry; Riazanov, Artur; Smirnov, Petr https://www.dagstuhl.de/lipics License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-166805
URL:

; ;

Tight Bounds for Tseitin Formulas

pdf-format:


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).

BibTeX - Entry

@InProceedings{itsykson_et_al:LIPIcs.SAT.2022.6,
  author =	{Itsykson, Dmitry and Riazanov, Artur and Smirnov, Petr},
  title =	{{Tight Bounds for Tseitin Formulas}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16680},
  URN =		{urn:nbn:de:0030-drops-166805},
  doi =		{10.4230/LIPIcs.SAT.2022.6},
  annote =	{Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems}
}

Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems
Seminar: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue date: 2022
Date of publication: 28.07.2022


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI