4
$\begingroup$

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?

$\endgroup$
0

1 Answer 1

4
$\begingroup$

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<d\}$ enumerate the edges incident to $v$, and for each $i<d$, 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<d$, thus $$0=\bigoplus_{u\in V'}l'(u)=l'(v)\oplus\bigoplus_{i<d}\bigoplus_{u\in V_i}l'(u)=l'(v)\oplus\bigoplus_{i<d}a(p_{e_i}),$$ that is, $\bigoplus_{e\ni v}a(p_e)=l'(v)$.

$\endgroup$
8
  • 1
    $\begingroup$ 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$ ? $\endgroup$
    – A. H.
    Commented Mar 1 at 20:33
  • 1
    $\begingroup$ (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. $\endgroup$ Commented Mar 1 at 22:40
  • $\begingroup$ 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′}$. $\endgroup$
    – A. H.
    Commented Mar 3 at 0:32
  • $\begingroup$ (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).$ $\endgroup$
    – A. H.
    Commented Mar 3 at 0:35
  • 1
    $\begingroup$ All right, I give in. I’ll include the proper argument in the answer. $\endgroup$ Commented Mar 3 at 9:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.