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

摘要

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 ( t w ( G ) log n ) , where n is the number of vertices in G and t w ( G ) is the treewidth of G . For constant degree graphs there is known upper bound 2 O ( t w ( 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 ( t w ( G )) ; the latter improves the recent result of Glinskih and Itsykson [GI19].