TAOCP 7.2.2.2 Exercise 226

Section 7.2.2.2: Satisfiability

Exercise 226. [M30] [M30] Let $\alpha$ be a node in a refutation tree; let $C(\alpha)$ be its label, and let $|\alpha|$ denote the number of leaves in its subtree. Show that, given a refutation tree with $N$ leaves, the Prover can find a node with $|\alpha| \le N/2^s$ for which the current assignment falsifies $C(\alpha)$, whenever the Delayer has scored $s$ points in the Prover–Delayer game.

Verified: yes
Solve time: 2m10s

---

Edit

Solution

Let (T) be the given resolution refutation tree with (N) leaves. For a node (\alpha), let (C(\alpha)) be its clause label and let (|\alpha|) be the number of leaves in the subtree rooted at (\alpha).

We describe a Prover strategy that maintains the following invariant:

After the Delayer has scored (s) points, the Prover can have reached a node (\alpha) such that the current assignment falsifies (C(\alpha)) and

[ |\alpha|\leq \frac{N}{2^s}. ]

The initial position is the root of the refutation tree. Its label is the empty clause, which is false under every assignment. Since the root contains all (N) leaves,

[ |\text{root}|=N=\frac{N}{2^0}, ]

so the invariant holds when the Delayer has scored (0) points.

Now suppose that the invariant holds after the Delayer has scored (s) points, and let (\alpha) be the node guaranteed by the invariant. If (\alpha) is a leaf, then (C(\alpha)) is an initial axiom and the required node has already been reached. Therefore assume that (\alpha) is an internal node.

Write the resolution step at (\alpha) in the form

[ \frac{A\vee x \qquad A\vee \bar{x}}{A}. ]

Thus the two children of (\alpha) have labels

[ C_0=A\vee x,\qquad C_1=A\vee\bar{x}, ]

while

[ C(\alpha)=A. ]

The current assignment falsifies (A). Therefore the only remaining question is the value assigned to the pivot variable (x). If (x=0), then (A\vee x) is false; if (x=1), then (A\vee\bar{x}) is false. Hence exactly one of the two children has a label falsified by the current assignment.

The connection with the Prover–Delayer game is the following. At this node, the Prover queries the pivot variable (x). If the Delayer assigns a value to (x) without scoring, the falsified child is determined by that assignment, and the Prover continues with that child. If the Delayer scores a point, the rules of the game give the Prover the choice between the two possible continuations corresponding to the two values of (x). The Prover chooses the child whose subtree contains fewer leaves.

Let the two child subtrees have sizes (n_0) and (n_1). They partition the leaves below (\alpha), so

[ n_0+n_1=|\alpha|. ]

Consequently,

[ \min(n_0,n_1)\leq \frac{|\alpha|}{2}. ]

When the Delayer scores a point, the Prover chooses this smaller child. The resulting child (\beta) is therefore a node whose clause is falsified by the corresponding continuation of the assignment and satisfies

[ |\beta|\leq \frac{|\alpha|}{2}. ]

Using the induction hypothesis,

[ |\beta| \leq \frac{1}{2}|\alpha| \leq \frac{1}{2}\cdot\frac{N}{2^s} =\frac{N}{2^{s+1}}. ]

Thus one additional point scored by the Delayer allows the Prover to maintain the invariant with (s+1) in place of (s).

By induction, whenever the Delayer has scored (s) points, the Prover can reach a node (\alpha) whose clause is falsified by the current assignment and for which

[ \boxed{|\alpha|\leq \frac{N}{2^s}}. ]

This proves the claim.