TAOCP 7.2.2.2 Exercise 167

Exercise 167. ▶ [21] [21] Justify step X11 and the similar use of X12 in step X6.

Verified: no
Solve time: 1m44s

Solution

Step X11 uses the binary implication information to add all consequences that are already forced by the current choice of $l_0$. The justification is the defining property of $BIMP(\bar l_0)$: if $l \in BIMP(\bar l_0)$, then the binary clauses imply

$\bar l_0 \rightarrow l,$

or equivalently,

$l_0 \vee l.$

Thus every satisfying assignment that contains $l_0$ must also contain $l$. The literals considered in X11 are those $l \in BIMP(\bar l_0)$ that are fixed true but not proto true. Such a literal has already been proved necessary under the present assumption $l_0$, but it has not yet been inserted into the current set of forced literals.

Suppose that step X11 performs step X12 for one such literal $l$. Step X12 sets

$FORCE[U]\leftarrow l$

and increases $U$ by one, so $l$ becomes part of the current forced assignment. The subsequent execution of (72) updates the data structures $T$ and $T_0$ exactly as it would if $l$ had been forced by any other valid implication. Since the implication $\bar l_0\rightarrow l$ follows from the binary clauses, every satisfying assignment extending $l_0$ already satisfies $l$. Therefore adding $l$ cannot remove any satisfying assignment that is compatible with the current branch.

It remains to show that all literals added in X11 may be added simultaneously. Let

$L={l:l\in BIMP(\bar l_0),\ l\text{ is fixed true, and }l\text{ is not proto true}}.$

For every $l\in L$, the binary implication argument gives

$l_0\rightarrow l.$

Hence every satisfying assignment satisfying $l_0$ satisfies every member of $L$. Therefore the conjunction of all literals in $L$ is forced by the current branch:

$l_0\rightarrow\bigwedge_{l\in L}l.$

Adding the members of $L$ one after another by X12 produces the same logical restriction as adding them all at once. No contradiction can be introduced unless the current branch was already contradictory, because the added literals are consequences of that branch.

The same argument applies to the use of X12 in step X6. In that case X6 has discovered a necessary literal by the lookahead procedure rather than by the binary implication graph. A literal is called necessary there precisely because every satisfying extension of the current partial assignment must contain it. Step X12 merely records such a forced literal and performs the bookkeeping required by (72). Since the literal is a logical consequence of the current assumptions, the operation preserves the set of satisfying assignments of the remaining problem.

Therefore X11 is correct, and every use of X12 in X6 is also correct, because both operations add only literals that are already forced by the current partial assignment.

This completes the proof.

∎