BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

On 1-BP complexity of satisfiable Tseitin formulas and how it relates to regular resolution Itsykson, Dmitry


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))}$ [Alekhnovich, Razborov, FOCS-2002], 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 transformed to a read-once branching program of size $S^{log n}$ computing a satisfiable Tseitin formula $T(G,c')$. 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 result of [Glinskih, Itsykson, CSR-2019] and together with the transformation implies the main result. Talk is based on joint work with Artur Riazanov, Danil Sagunov and Petr Smirnov.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International