2026-07-20T05:03:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16680 2024-03-06T10:58:02Z ddc:004 open_access

Tight Bounds for Tseitin Formulas Itsykson, Dmitry Riazanov, Artur Smirnov, Petr Proof complexity Tseitin formulas treewidth resolution OBDD-based proof systems 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dmitry Itsykson and Artur Riazanov and Petr Smirnov 2022 Is Part Of LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2022.6 urn:nbn:de:0030-drops-166805 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.6 eng https://creativecommons.org/licenses/by/4.0/legalcode