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)}$.

Several typos were fixed.

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)}$.