__
Revision #1 to TR19-020 | 25th March 2019 13:46
__
#### On Tseitin formulas, read-once branching programs and treewidth

**Abstract:**
We show that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an $n\times n$ grid graph has size at least $2^{\Omega(n)}$. Then using the Excluded Grid Theorem by Robertson and Seymour we show that for 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 of $G$ (for planar graphs and some other classes of graphs the statement holds for $\delta=1$). We also show an upper bound $O(|E| 2^{pw(G)})$, where $pw(G)$ is the pathwidth of $G$.

We apply the mentioned results in the analysis of the complexity of derivation in the proof system $OBDD(\land, reordering)$ and show that any $OBDD(\land, reordering)$-refutation of an unsatisfiable Tseitin formula based on a graph $G$ has size at least $2^{\Omega(tw(G)^\delta)}$.

**Changes to previous version:**
Several typos were fixed.

__
TR19-020 | 4th February 2019 10:31
__

#### On Tseitin formulas, read-once branching programs and treewidth

**Abstract:**
We show that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an $n\times n$ grid graph has size at least $2^{\Omega(n)}$. Then using the Excluded Grid Theorem by Robertson and Seymour we show that for 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 of $G$ (for planar graphs and some other classes of graphs the statement holds for $\delta=1$). We also show an upper bound $O(|E| 2^{pw(G)})$, where $pw(G)$ is the pathwidth of $G$.

We apply the mentioned results in the analysis of the complexity of derivation in the proof system $OBDD(\land, reordering)$ and show that any $OBDD(\land, reordering)$-refutation of an unsatisfiable Tseitin formula based on a graph $G$ has size at least $2^{\Omega(tw(G)^\delta)}$.