ECCC-Report TR19-178https://eccc.weizmann.ac.il/report/2019/178Comments and Revisions published for TR19-178en-usSat, 07 Dec 2019 03:51:51 +0200
Paper TR19-178
| Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs |
Dmitry Itsykson,
Artur Riazanov,
Petr Smirnov,
Danil Sagunov
https://eccc.weizmann.ac.il/report/2019/178We 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].Sat, 07 Dec 2019 03:51:51 +0200https://eccc.weizmann.ac.il/report/2019/178