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 × n grid graph has size at least 2 Ω( 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^Ω (tw(G)^δ) for all δ < 1/36, where tw( G ) is the treewidth of G (for planar graphs and some other classes of graphs the statement holds for δ = 1). We apply the mentioned results to the analysis of the complexity of derivations in the proof system OBDD(∧,reordering) and show that any OBDD(∧,reordering)-refutation of an unsatisfiable Tseitin formula based on a graph G has size at least 2^Ω (tw(G)^δ) . We also show an upper bound O (| E |2 pw( G ) ) on the size of OBDD representations of a satisfiable Tseitin formula based on G and an upper bound O(|E||V| 2^pw(G)+|TS_G,c|^2) on the size of OBDD(∧)-refutation of an unsatisifable Tseitin formula TS G , c , where pw( G ) is the pathwidth of G .