TAOCP 7.2.2.2 Exercise 138

In step L9 of Algorithm L, the clause under consideration is the binary clause $u \vee v$.

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 138. [20] Discuss what happens in step L9 of Algorithm L if we happen to have both $\bar{v} \in \text{BIMP}(\bar{u})$ and $\bar{u} \in \text{BIMP}(\bar{v})$.

Verified: no
Solve time: 1m55s

Solution

In step L9 of Algorithm L, the clause under consideration is the binary clause $u \vee v$. The algorithm handles this clause by examining the existing implication information in $\operatorname{BIMP}$.

The two assumptions are

$$ \bar{v} \in \operatorname{BIMP}(\bar{u}) $$

and

$$ \bar{u} \in \operatorname{BIMP}(\bar{v}). $$

The first condition says that the implication digraph already contains the edge

$$ \bar{u}\to\bar{v}. $$

The second condition says that it also contains the edge

$$ \bar{v}\to\bar{u}. $$

Therefore $\bar{u}$ and $\bar{v}$ are mutually implying. In particular, if $\bar{u}$ is true, then $\bar{v}$ is already forced to be true.

Now step L9 is being applied to the clause

$$ u\vee v. $$

The clause contributes the implication

$$ \bar{u}\to v, $$

because if $u$ is false, then $v$ must be true in order for $u\vee v$ to hold. However, the existing BIMP entry gives

$$ \bar{u}\to\bar{v}. $$

Consequently, assuming $\bar{u}$ would force both $v$ and $\bar{v}$. Thus $\bar{u}$ cannot occur in any satisfying assignment, and $u$ is forced to be true.

This is exactly the first case of step L9. Since

$$ \bar{v}\in\operatorname{BIMP}(\bar{u}), $$

Algorithm L performs

$$ (62)\quad l\leftarrow u. $$

The second membership,

$$ \bar{u}\in\operatorname{BIMP}(\bar{v}), $$

does not create an additional action. Step L9 is an ordered sequence of tests. Once the first test succeeds, the later alternatives are not examined. The symmetric implication merely shows that the same phenomenon would occur if the clause were considered from the other direction: assuming $\bar{v}$ would force both $\bar{u}$ and $u$.

Hence the effect of the two simultaneous BIMP entries is that both $\bar{u}$ and $\bar{v}$ are impossible, so the binary clause $u\vee v$ forces either literal. In the actual execution of step L9, the first test is decisive, and the algorithm fixes

$$ \boxed{u=1}. $$

This completes the proof. ∎