Exercise 246. ▶ [M28] [M28] (G. S. Tseytin.) Given a labeled graph $G$ with $m$ edges, $n$ vertices, and $N$ unsatisfiable clauses $\alpha(G)$ as in the previous exercise, explain how to refute those clauses with $O(mn + N)$ steps of extended resolution.

Verified: no
Solve time: 3m35s

Solution

Let $G=(V,E)$ be the labeled graph from the previous exercise. The variables are $c_e$, one for each edge $e\in E$. For every vertex $v$, the Tseytin clauses $\alpha(v)$ encode the condition

$$ \bigoplus_{e\ni v}c_e=l(v). $$

The labels satisfy

$$ \bigoplus_{v\in V}l(v)=1. $$

The XOR of all vertex equations is therefore inconsistent, because each edge variable occurs twice:

$$ \bigoplus_{v\in V}\bigoplus_{e\ni v}c_e=0, $$

while the right side is

$$ \bigoplus_{v\in V}l(v)=1. $$

The problem is to realize this XOR argument as an extended-resolution proof of size $O(mn+N)$.

Linear-size parity gadgets in extended resolution

We first describe the extension variables used in the proof.

For Boolean variables $x_1,\ldots,x_k$, introduce variables

$$ z_2,\ldots,z_k $$

with the definitions

$$ z_2\leftrightarrow x_1\oplus x_2 $$

and

$$ z_i\leftrightarrow z_{i-1}\oplus x_i \qquad (3\le i\le k). $$

The XOR definition

$$ z\leftrightarrow a\oplus b $$

has the constant-size CNF representation

$$ (\bar a\vee\bar b\vee\bar z) \wedge (\bar a\vee b\vee z) \wedge (a\vee\bar b\vee z) \wedge (a\vee b\vee\bar z). $$

Thus the complete chain of definitions requires $O(k)$ extension clauses.

The important point is that these definitions allow the corresponding parity relation to be used in resolution with the same linear bound. This follows by induction on the length of the chain. For $i=2$, the four defining clauses are exactly the truth table of

$$ z_2=x_1\oplus x_2. $$

Assume that the clauses expressing

$$ z_{i-1}=x_1\oplus\cdots\oplus x_{i-1} $$

have been derived. Resolving these clauses with the four defining clauses of

$$ z_i\leftrightarrow z_{i-1}\oplus x_i $$

on $z_{i-1}$ gives the four clauses expressing

$$ z_i=x_1\oplus\cdots\oplus x_i . $$

Only a constant number of resolutions is used at each step. Hence any parity equation involving $k$ variables can be represented and manipulated by $O(k)$ extension and resolution steps.

We shall use this fact repeatedly below.

Combining the Tseytin clauses

For a set $S\subseteq V$, define

$$ \delta(S)={e\in E:e\text{ has exactly one endpoint in }S}. $$

Let

$$ p_S=\bigoplus_{e\in\delta(S)}c_e . $$

We claim that the clauses belonging to the vertices in $S$ imply

$$ p_S=\bigoplus_{v\in S}l(v). $$

To derive this inside extended resolution, list the vertex equations for the vertices of $S$. Each vertex equation is already represented by the clauses $\alpha(v)$. Introduce extension variables for the running XOR of these vertex parities.

More explicitly, if

$$ S={v_1,\ldots,v_t}, $$

form a chain of extension variables representing

$$ r_i= \bigoplus_{j=1}^{i} \bigoplus_{e\ni v_j}c_e . $$

By the parity construction above, this requires

$$ O\left(\sum_{j=1}^{t}\deg(v_j)\right) $$

steps. The clauses $\alpha(v_j)$ imply that the same expression equals

$$ \bigoplus_{j=1}^{i}l(v_j). $$

Therefore the final variable $r_t$ represents both the XOR of all edge incidences inside $S$ and the XOR of the labels in $S$.

Every edge having both endpoints in $S$ occurs twice in the incidence XOR and cancels. Every edge in $\delta(S)$ occurs once. Therefore the resulting parity relation is

$$ p_S=\bigoplus_{v\in S}l(v). $$

The number of steps needed for a particular $S$ is

$$ O\left(\sum_{v\in S}\deg(v)\right). $$

Since this is at most $O(m)$, every such subset parity equation can be derived with $O(m)$ steps.

Applying the construction to a spanning tree

Choose a spanning tree of $G$ and root it at $r$. For each vertex $v$, let $S_v$ be the vertices in the subtree rooted at $v$. Apply the previous construction to each $S_v$.

For every $v$,

$$ p_{S_v}

\bigoplus_{u\in S_v}l(u). $$

For the root,

$$ S_r=V. $$

Because every edge has both endpoints in $V$,

$$ \delta(S_r)=\varnothing , $$

$$ p_{S_r}=0. $$

The derived parity equation gives

$$ p_{S_r}

\bigoplus_{u\in V}l(u)

Hence the proof derives the contradictory pair

$$ p_{S_r}=0 $$

and

$$ p_{S_r}=1. $$

The first gives the unit clause

$$ \neg p_{S_r}, $$

and the second gives

$$ p_{S_r}. $$

Resolving these two clauses yields the empty clause.

Size analysis

The initial Tseytin clauses contribute

$$ N $$

clauses.

There are at most $n$ subtree sets $S_v$. For each subtree, the derivation of its parity equation requires at most $O(m)$ steps, because the total number of incident edge occurrences in the subtree is at most $2m$. Therefore the total cost of all subtree derivations is

$$ O(mn). $$

The final contradiction requires one resolution step.

Consequently the complete extended-resolution refutation has size

$$ O(N)+O(mn)+O(1)

O(mn+N). $$

Thus the Tseytin clauses $\alpha(G)$ admit an extended-resolution refutation with $O(mn+N)$ steps. $\square$

TAOCP 7.2.2.2 Exercise 246