On Tseitin Formulas, Read-Once Branching Programs and Treewidth

摘要

We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an n x n grid graph has size at least 2(Omega(n)). Then using the Excluded Grid Theorem by Robertson and Seymour we show that for an arbitrary graph G(V, E) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on G has size at least 2(Omega(tw(G)delta)) for all delta 1/36, where tw(G) is the treewidth ofG(for planar graphs and some other classes of graphs the statement holds for delta = 1). We apply the mentioned results to the analysis of the complexity of derivations in the proof system OBDD(Lambda, reordering) and show that any OBDD(Lambda, reordering)-refutation of an unsatisfiable Tseitin formula based on a graph G has size at least 2(Omega(tw(G)delta)). We also show an upper bound O(vertical bar E vertical bar 2(pw(G))) on the size of OBDD representations of a satisfiable Tseitin formula based on G and an upper bound O(vertical bar E vertical bar vertical bar V vertical bar(2pw(G)) + vertical bar TSG,c vertical bar(2)) on the size of OBDD(Lambda)-refutation of an unsatisifable Tseitin formula TSG,c, where pw( G) is the pathwidth of G.