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: 1m32s

Solution

Let $l$ be a pure literal in a formula $F$. By definition, the complementary literal $\bar{l}$ does not occur in any clause of $F$. Hence every clause of $F$ either contains $l$ or contains neither $l$ nor $\bar{l}$.

In Algorithm X, a choice of a literal corresponds to selecting it into the covering set $L$, after which every clause containing that literal is removed, since it is already covered. The only way a literal can be prevented from being chosen immediately is the existence of some clause in which its complement is required for coverage, forcing a conflict between selecting $l$ and satisfying that clause.

No such obstruction exists for a pure literal $l$, since $\bar{l}$ does not appear in $F$. Selecting $l$ removes every clause containing $l$ and does not endanger any remaining clause, because no clause requires $\bar{l}$ for coverage. Thus the choice of $l$ never introduces a contradiction with respect to clause coverage.

In the covering formulation with $T_n$, each variable contributes the clause ${l,\bar{l}}$. Since $\bar{l}$ appears only in $T_n$ and not in $F$, selecting $l$ covers all clauses of $F$ involving $l$ and leaves the corresponding clause in $T_n$ still coverable by $l$ itself. No alternative selection involving $\bar{l}$ is required.

Therefore, during execution of Algorithm X, $l$ is recognized immediately as a literal that can be chosen without branching, since it satisfies all constraints involving it and does not invalidate any clause.

This completes the proof. ∎