All reports by Author Petr Smirnov:

__
TR19-178
| 5th December 2019
__

Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov#### Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs

Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov

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))}$ ... more >>>