We show that the size of any regular resolution refutation of Tseitin formula $T(G,c)$ based on a graph $G$ is at least $2^{\Omega(tw(G)/\log n)}$, where $n$ is the number of vertices in $G$ and $tw(G)$ is the treewidth of $G$. For constant degree graphs there is known upper bound $2^{O(tw(G))}$ [AR11, GTT18], so our lower bound is tight up to a logarithmic factor in the exponent.

In order to prove this result we show that any regular resolution proof of Tseitin formula $T(G,c)$ of size $S$ can be converted to a read-once branching program computing satisfiable Tseitin formula $T(G,c')$ of size $S^{O(\log n)}$. Then we show that any read-once branching program computing satisfiable Tseitin formula $T(G,c')$ has size at least $2^{\Omega(tw(G))}$; the latter improves the recent result of Glinskih and Itsykson [GI19].