TAOCP 7.2.2.2 Exercise 225
Let a resolution tree be oriented with the empty clause at the root and the axioms at the leaves.
Section 7.2.2.2: Satisfiability
Exercise 225. ▶ [M31] [M31] (G. S. Tseytin, 1966.) If $T$ is any resolution tree that refutes a set of axioms $F$, show how to convert it to a regular resolution tree $T_r$ that refutes $F$, where $T_r$ is no larger than $T$.
Verified: no
Solve time: 3m17s
Solution
Let a resolution tree be oriented with the empty clause at the root and the axioms at the leaves. We write the two sons of a resolution vertex with pivot $x$ as
$$ \frac{C\cup{x}\qquad D\cup{\bar x}}{C\cup D}. $$
We use the following elementary property of resolution trees.
Lemma
Suppose a subtree $S$ has root clause $C$, and suppose a literal $l$ occurs in $C$. Then any occurrence of a resolution with pivot $\operatorname{var}(l)$ below the root of $S$ can be removed without increasing the size of $S$, while preserving the clause at the root of the subtree.
Proof of the lemma
Consider a path in $S$ from the root downward. Once the literal $l$ has appeared in a clause on this path, every descendant clause on that path also contains $l$, except possibly at a resolution whose pivot is $\operatorname{var}(l)$. Such a resolution is therefore the only place where the occurrence of $l$ can be changed.
Consider the highest such resolution in the subtree. Its two sons have the form
$$ E\cup{l}\qquad H\cup{\bar l}, $$
and its resolvent is
$$ E\cup H . $$
Because the clause at the root of the subtree already contains $l$, the second branch cannot contribute any information needed above this resolution: the only purpose of this resolution is to remove the occurrence of the already fixed variable $\operatorname{var}(l)$. We may therefore replace this resolution node by its first son if $l$ is the positive literal in the surrounding branch, and by its second son if $\bar l$ is the surrounding literal.
The resulting subtree has the same root clause, because every clause above this point already contains the literal $l$ and hence cannot distinguish the two possible continuations. The number of vertices decreases by one or more. Repeating the operation removes all resolutions on $\operatorname{var}(l)$ below the root of $S$.
$\square$
Now let $T$ be an arbitrary resolution tree refuting $F$. If $T$ is regular, take
$$ T_r=T . $$
Otherwise, choose a variable $x$ that occurs as a resolution variable twice on some root-to-leaf path, and choose the uppermost occurrence of such a repetition. Let $v$ be this resolution vertex. Its sons derive
$$ A\cup{x} \qquad\text{and}\qquad B\cup{\bar x}, $$
and $v$ derives
$$ A\cup B . $$
Every occurrence of $x$ below $v$ lies in one of the two subtrees rooted at the sons of $v$. In the left subtree the clause at the root contains $x$, so by the lemma all later resolutions on $x$ in that subtree can be removed without increasing its size. Likewise, in the right subtree the root clause contains $\bar x$, so all later resolutions on $x$ can be removed there as well.
After these two modifications, the vertex $v$ is still a valid resolution vertex with pivot $x$, and neither of its sons contains another resolution on $x$. Hence every path passing through $v$ now contains the variable $x$ at most once.
The operation decreases the number of repeated pivot occurrences in the tree. It never introduces a new vertex and never increases the size of any subtree. Since a finite tree has only finitely many resolution vertices, repeating the operation must terminate.
When the process terminates, no variable is used as a resolution variable more than once on any root-to-leaf path. Therefore the resulting tree $T_r$ is regular. The leaves are unchanged axioms of $F$, and every internal vertex remains a valid resolution inference, so the root is still the empty clause. Thus $T_r$ is a regular resolution refutation of $F$.
At every step the number of vertices does not increase, and hence
$$ |T_r|\le |T|. $$
Therefore every resolution tree refuting $F$ can be converted into a regular resolution tree refuting $F$ of no larger size.
$$ \boxed{|T_r|\le |T|} $$
$\square$