License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.6
URN: urn:nbn:de:0030-drops-166805
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16680/
Itsykson, Dmitry ;
Riazanov, Artur ;
Smirnov, Petr
Tight Bounds for Tseitin Formulas
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 |
|
Collection: |
|
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
28.07.2022 |
