Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR19-178 | 5th December 2019 01:07

#### Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs

TR19-178
Authors: Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov
Publication: 7th December 2019 03:51
Downloads: 86
Keywords:

Abstract:

We show that the size of any regular resolution refutation of Tseitin formula \$T(G,c)\$ based on a graph \$G\$ is at least \$2^{\Omega(tw(G)/\log n)}\$, where \$n\$ is the number of vertices in \$G\$ and \$tw(G)\$ is the treewidth of \$G\$. For constant degree graphs there is known upper bound \$2^{O(tw(G))}\$ [AR11, GTT18], so our lower bound is tight up to a logarithmic factor in the exponent.

In order to prove this result we show that any regular resolution proof of Tseitin formula \$T(G,c)\$ of size \$S\$ can be converted to a read-once branching program computing satisfiable Tseitin formula \$T(G,c')\$ of size \$S^{O(\log n)}\$. Then we show that any read-once branching program computing satisfiable Tseitin formula \$T(G,c')\$ has size at least \$2^{\Omega(tw(G))}\$; the latter improves the recent result of Glinskih and Itsykson [GI19].

ISSN 1433-8092 | Imprint