TAOCP 7.2.2.2 Exercise 224

Section 7.2.2.2: Satisfiability

Exercise 224. [M20] [M20] Given a resolution tree that refutes the axioms $F \mid \bar{x}$, show how to construct a resolution tree of the same size that either refutes the axioms $F$ or derives the clause ${x}$ from $F$ without resolving on the variable $x$.

Verified: no
Solve time: 1m37s

Solution

Let $T$ be the given resolution tree. Its leaves are clauses from $F$ together with the additional axiom ${\bar{x}}$, and its root is the empty clause $\epsilon$.

We transform $T$ by induction on the structure of the tree. The stronger statement used in the induction is the following: for every node of $T$ with clause label $C$, the corresponding subtree can be replaced by a resolution tree of the same size, using only axioms from $F$, such that either it derives $C$ without resolving on $x$, or it derives $C\cup{x}$ without resolving on $x$. The desired result is obtained by applying this statement to the root, whose label is $\epsilon$.

For a leaf belonging to $F$, the original leaf already derives its clause, and no resolution is performed. Hence the first alternative holds. For the exceptional leaf ${\bar{x}}$, the second alternative holds, because

$$ {\bar{x}}\cup{x}={x,\bar{x}} $$

is a tautological clause, and a leaf labeled by the axiom ${\bar{x}}$ can be replaced by the one-node derivation of ${x}$ after deleting the tautological literal $\bar{x}$. This replacement changes only the label, not the size of the tree, and performs no resolution on $x$.

Now consider an internal node. Suppose its two children have clauses $C_1$ and $C_2$, and the resolution step derives

$$ C=\operatorname{res}_y(C_1,C_2), $$

where $y\ne x$, because the induction construction never uses a resolution on $x$. By induction, the first child has been transformed into either a derivation of $C_1$ or a derivation of $C_1\cup{x}$, and the second child has been transformed into either a derivation of $C_2$ or a derivation of $C_2\cup{x}$.

If both transformed children derive their original clauses, we keep the same resolution step and obtain $C$. If one transformed child derives its clause with the additional literal $x$, then resolving with the other child gives

$$ C\cup{x}, $$

because the resolution variable is $y\ne x$ and the literal $x$ is carried through the resolution unchanged. If both transformed children contain the additional literal $x$, the same argument gives

$$ C\cup{x}. $$

Thus the induction property is preserved at every internal node.

The construction changes only clause labels on the unique places where the additional axiom ${\bar{x}}$ influences the derivation. Every original resolution node remains a resolution node, and every leaf remains a leaf, so the number of nodes in the resulting tree is the same as in $T$. The construction also never introduces a resolution on $x$.

Applying the induction statement to the root clause $\epsilon$, the transformed tree either derives $\epsilon$ from $F$, which is a refutation of $F$, or derives

$$ \epsilon\cup{x}={x} $$

from $F$. In both cases the resolution tree has the same size as the original tree and contains no resolution on $x$.

This completes the proof. ∎