TAOCP 7.2.2.2 Exercise 166

Section 7.2.2.2: Satisfiability

Exercise 166. [30] [30] Justify the operations of step X9. Hint: Prove that an autarky can be constructed, if $w = 0$ in (72) has been performed.

Verified: no
Solve time: 1m04s

Setup

In Algorithm X, step X8 performs the lookahead computation (72) after choosing a literal $l$. The computation assumes that $l$ is tentatively set true and propagates all forced consequences. During this process, $l_0$ denotes the literal whose truth is being investigated, and $w$ is the number of clauses that become satisfied only because of the new forced information discovered in this lookahead. Step X9 uses the case $w=0$ to claim that $l_0$ itself can be exploited as an autarky.

The goal is to justify the operation in X9 by proving that, after (72) has been performed and $w=0$, there exists an autarky containing $l_0$.

Solution

Let the lookahead beginning with $l_0$ assign $l_0$ the value true and perform the forced assignments generated by (72). Let $A$ be the set of all literals assigned true during this process. The literal $l_0$ belongs to $A$ by construction.

The defining property of an autarky is that every clause of $F$ either contains a literal of $A$ or contains none of the complementary literals $\bar A$. Equivalently, every clause touched by $A$ must already be satisfied by $A$.

Consider any clause $C$ that contains a literal $a\in A$. Since $a$ was forced true during the lookahead, the clause $C$ is satisfied unless the satisfaction of $C$ required some further literal not belonging to the lookahead assignment. Such a clause would be a clause whose status changes only after the newly discovered forced information is taken into account.

The quantity $w$ in (72) counts precisely these additional clauses that become satisfied because of the propagation. When $w>0$, step X8 records this improvement by increasing $H(l_0)$ and does not regard $l_0$ as an autarky. When $w=0$, no additional clause is gained from the propagation. Hence every clause that is touched by one of the literals in $A$ was already satisfied by the literals in $A$ at the moment the lookahead assignment was made.

It remains to show that no clause can contain a complementary literal from $\bar A$ without also being satisfied by $A$. Suppose that a clause $C$ contains $\bar a$ for some $a\in A$ and contains no literal of $A$. Because $a$ was forced true, the literal $\bar a$ is forced false under the lookahead assignment. Since $C$ contains no other literal of $A$, the clause would have lost its last possible satisfying literal during the lookahead. Therefore the propagation process would have detected a conflict, and step X13 would have been invoked. The assumption that the lookahead reached step X9 excludes this possibility.

Therefore every clause containing a complement of a literal in $A$ also contains a literal of $A$, unless it is completely untouched by $A$. Consequently every clause of $F$ either contains a member of $A$ or contains no member of $\bar A$. This is exactly the definition of an autarky.

In particular, the set of literals generated by the lookahead, including $l_0$, is an autarky whenever $w=0$. Step X9 is therefore justified: if $H(l_0)=0$ after (72), then $l_0$ can safely be forced true by step X12, because it belongs to an autarky.

This completes the proof.

∎

Verification

The argument uses both directions of the autarky condition. Every clause touched by the generated literals is satisfied because $w=0$ means that the lookahead created no unresolved new satisfactions requiring additional information. Every clause containing a falsified complementary literal would have caused a conflict during propagation, so no such untouched clause exists. Hence the generated assignment is self-sufficient.

The alternative branch of X9 is also consistent with this characterization. When $w>0$, the lookahead has found information that does not arise from a self-contained autarky, so the algorithm records the gain in $H(l_0)$ and continues searching rather than forcing $l_0$ immediately.