  Tseitin-formulas are systems of parity constraints whose structure is
described by a graph. These formulas have been studied extensively in proof
complexity as hard instances in many proof systems. In this paper, we prove
that a class of unsatisfiable Tseitin-formulas of bounded degree has regular
resolution refutations of polynomial length if and only if the treewidth of all
underlying graphs $G$ for that class is in $O(\log|V(G)|)$. To do so, we show
that any regular resolution refutation of an unsatisfiable Tseitin-formula with
graph $G$ of bounded degree has length $2^{\Omega(tw(G))}/|V(G)|$, thus
essentially matching the known $2^{O(tw(G))}poly(|V(G)|)$ upper bound up. Our
proof first connects the length of regular resolution refutations of
unsatisfiable Tseitin-formulas to the size of representations of
\textit{satisfiable} Tseitin-formulas in decomposable negation normal form
(DNNF). Then we prove that for every graph $G$ of bounded degree, every
DNNF-representation of every satisfiable Tseitin-formula with graph $G$ must
have size $2^{\Omega(tw(G))}$ which yields our lower bound for regular
resolution.
