Open Collections

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

Banff International Research Station for Mathematical Innovation and Discovery

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.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: Steklov Institute of Mathematics at St. Petersburg

2020-07-22

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/75237

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/