TAOCP 7.2.2.2 Exercise 158

Exercise 158. [15] [15] If $l$ is a pure literal, will Algorithm X discover it?

Verified: no
Solve time: 2m23s

Solution

Yes. Algorithm X will discover every pure literal that occurs in the current formula.

Let $l$ be a pure literal of $F$. By definition, $\bar l$ occurs in no clause of $F$. Consider the exploration of $l$ in Algorithm X. When $l$ is assumed true, every clause containing $l$ is satisfied, and no clause is made harder to satisfy because there are no clauses containing $\bar l$. Therefore the set ${l}$ is an autarky for $F$.

In the lookahead exploration, Algorithm X evaluates the consequences of each candidate literal. For the candidate $l$, the autarky property means that the clauses touched by $l$ are all removed, while the untouched clauses contain neither $l$ nor $\bar l$. Hence the exploration produces no additional reduction that depends on a nontrivial consequence of $l$. In the notation of Algorithm X, the resulting heuristic increment satisfies $H(l)=0$.

Step X9 is precisely the autarky detection step. When $H(l_0)=0$, it performs step X12 with $l\leftarrow l_0$. Taking $l_0=l$, step X12 places $l$ into the $FORCE$ array, so Algorithm X discovers that $l$ is forced true.

Therefore every pure literal is found by Algorithm X.

$$ \boxed{\text{Yes, Algorithm X discovers every pure literal.}} $$