# Tseitin formula on 2-connected graph

How can we prove that for $$\\\\$$ every $$\\\\$$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a single clause, it becomes satisfiable?

Clearly, whether a formula is minimally unsatisfiable depends on the exact details of how it is formulated, so let me give a specific definition of Tseitin formulas. Given a graph $$G=(V,E)$$ and a vertex labelling $$l\colon V\to\{0,1\}$$, the CNF $$T_{G,l}$$ uses variables $$\{p_e:e\in E\}$$, and it includes clauses expressing for each vertex $$v$$ that the parity of its incident edges $$\bigoplus_{e\ni v}p_e$$ is $$l(v)$$: $$\tag{C_{v,\vec c}}\let\LOR\bigvee\LOR_{e\ni v}p_e^{1-c_e}$$ for each $$v\in V$$ and each $$\{0,1\}$$-vector $$\langle c_e:e\ni v\rangle$$ such that $$\bigoplus_{e\ni v}c_e=\overline{l(v)}$$, where $$p_e^1=p_e$$ and $$p_e^0=\overline{p_e}$$. The formula $$T_{G,l}$$ is unsatisfiable if $$\bigoplus_{v\in V}l(v)=1$$, because any satisfying assignment would have to satisfy $$1=\bigoplus_{v\in V}l(v)=\bigoplus_{v\in V}\bigoplus_{e\ni v}p_e=\bigoplus_{e\in E}\bigoplus_{v\in e}p_e=\bigoplus_{e\in E}0=0.$$

Now, let us try to show that for any given $$v$$ and $$\langle c_e:e\ni v\rangle$$, $$T_{G,l}\let\bez\smallsetminus\bez\{C_{v,\vec c}\}$$ is satisfiable. To guide our search, notice that since $$T_{G,l}$$ is unsatisfiable, any satisfying assignment of $$T_{G,l}\let\bez\smallsetminus\bez\{C_{v,\vec c}\}$$ must refute $$C_{v,\vec c}$$, i.e., it must extend the partial assignment $$a$$ such that $$a(p_e)=c_e$$ for all edges $$e$$ incident to $$v$$. But it is easy to see that if we restrict $$T_{G,l}\bez\{C_{v,\vec c}\}$$ with $$a$$, we end up with another Tseitin formula $$T_{G',l'}$$, where $$G'$$ is $$G$$ with $$v$$ and all its incident edges deleted, and $$l'(u)=\begin{cases}l(u)\oplus c_{\{u,v\}}&\text{if }\{u,v\}\in E,\\ l(u)&\text{otherwise.}\end{cases}$$ Thus, it suffices to show that $$T_{G',l'}$$ is satisfiable. Crucially, observe that $$\bigoplus_{u\ne v}l'(u)=\bigoplus_{u\ne v}l(u)\oplus\bigoplus_{e\ni v}c_e=\bigoplus_{u\ne v}l(u)\oplus(l(v)\oplus1)=\bigoplus_{u\in V}l(u)\oplus1=0.$$ Moreover, if we assume $$G$$ is $$2$$-connected, then $$G'$$ is connected. Thus, it remains to prove the following:

Lemma. If $$G'=(V',E')$$ is connected and $$l'\colon V'\to\{0,1\}$$ satisfies $$\bigoplus_{v\in V'}l'(v)=0$$, then $$T_{G',l'}$$ is satisfiable.

To prove this, we may assume without loss of generality that $$G'$$ is a tree (we may take an arbitrary spanning tree of $$G'$$, which is still connected, and set the remaining edges to $$0$$). Then the $$\mathbb F_2$$-linear system $$\{\bigoplus_{e\ni v}p_e=l'(v):v\in V'\}$$ has a unique solution that can be determined by working inwards from the leaves; the condition $$\bigoplus_vl'(v)=0$$ ensures that it works out in the root.

In fact, the unique satisfying assignment $$a$$ has a simple explicit description: any given edge $$e$$ splits the tree in two trees with vertex sets $$V_0$$ and $$V_1$$ (that is, $$V_0$$ and $$V_1$$ are the two components of the graph $$(V',E'\bez\{e\})$$), and we put $$a(p_e):=\bigoplus_{v\in V_0}l'(v)=\bigoplus_{v\in V_1}l'(v).$$ To see that $$a(T_{G',l'})=1$$, consider any vertex $$v\in V'$$, let $$\{e_i:i enumerate the edges incident to $$v$$, and for each $$i, let $$V_i$$ be the component of $$(V',E'\bez\{e_i\})$$ that does not contain $$v$$. Then by definition, $$a(p_{e_i})=\bigoplus_{u\in V_i}l'(u)$$, and $$V'\bez\{v\}$$ is a disjoint union of the sets $$V_i$$ for $$i, thus $$0=\bigoplus_{u\in V'}l'(u)=l'(v)\oplus\bigoplus_{i that is, $$\bigoplus_{e\ni v}a(p_e)=l'(v)$$.

• Op maybe happy, when he got this type of legendary answer from you. I am struggling to understand your two concepts (1) "any satisfying assignment would have to satisfy 1=0", what you mean actually here? What does mean of 1=0? how is it possible 1=0? (2) how can you infer that $T_{G',l'}$ is satisfiable after tree in two parts $G_0$ and $G_1$ ? Commented Mar 1 at 20:33
• (1) It isn't possible. That's the whole point. The formula is unsatisfiable because the existence of any satisfying assignment leads to a contradiction. (2) The sentence involving the splitting gives a recipe that defines an assignment $a$. Then you have to show that this assignment $a$ actually satisfies $T_{G',l'}$. This is left as an exercise, and I won't spoil it here. Commented Mar 1 at 22:40
• would you please check my comments are right for $T_{G',l'}$ is satisfiable. To complete the proof that $T_{G',l'}$ is satisfiable, we need to show that the unique satisfying assignment $a$, described as putting $a(p_e)$ equal to $\bigoplus_{v\in V_0}l'(v)$ for any edge $e$ splitting the tree into two sets $V_0$ and $V_1$, indeed satisfies all the clauses of $T_{G′,l′}$. Commented Mar 3 at 0:32
• (continued)..Let's denote the two sets of vertices by $V_0$ and $V_1$ as described, where $V_0$ and $V_1$ are separated by the edge $e$. Then, for any vertex $v$ in $V_0, l'(v) = l(v) ⊕ c_{\{u,v\}}$ (since ${\{u,v\}}$ is an edge in $G$), and for any vertex $u$ in $V_1, l'(u) = l(u).$ Commented Mar 3 at 0:35
• All right, I give in. I’ll include the proper argument in the answer. Commented Mar 3 at 9:37