TAOCP 7.2.2.2 Exercise 129
Algorithm D maintains, for each literal $l$, a watch list containing the clauses in which $l$ is one of the currently watched literals.
Section 7.2.2.2: Satisfiability
Exercise 129. [20] In the context of Algorithm D, design a subroutine that, given a literal $l$, returns 1 or 0 according as $l$ is or is not being watched in some clause whose other literals are entirely false.
Verified: no
Solve time: 2m32s
Solution
Algorithm D maintains, for each literal $l$, a watch list containing the clauses in which $l$ is one of the currently watched literals. The purpose of the present subroutine is not to determine from first principles whether the remaining literals of a clause are false. That information is already encoded by the watched-literal invariant maintained by Algorithm D.
For a clause $C$, let its two watched literals be denoted by $a$ and $b$. The watched-literal invariant is that, unless the clause is satisfied, the watched literals are chosen so that all literals of $C$ other than $a$ and $b$ are false only when both watches are forced to be examined. In particular, if $a$ is being watched and every literal of $C-{a}$ is false, then the other watched literal $b$ must also be false. Conversely, if $a$ is watched and $b$ is false, then Algorithm D's watch maintenance has already determined that no literal of $C-{a,b}$ is nonfalse, because otherwise $b$ would have been moved to such a literal instead of remaining watched.
Therefore the required test can be performed by inspecting only the clauses appearing in the watch list of $l$. For each such clause, the only information that must be checked is the status of the other watched literal.
Let $W(l)$ be the watch list of $l$, as maintained by Algorithm D. The subroutine is
$$ \begin{array}{l} \textsc{Watched}(l):\[2mm] \qquad \textbf{for each clause }C\in W(l)\textbf{ do}\ \qquad\qquad\text{let }w\text{ be the other watched literal of }C;\ \qquad\qquad\textbf{if }w\text{ is false then return }1;\ \qquad\textbf{return }0. \end{array} $$
The cases in this test correspond exactly to the possible states of the other watch. If $w$ is true, then $C$ is satisfied, so it is impossible that every literal of $C-{l}$ is false. If $w$ is unassigned, then $C-{l}$ also contains a literal that is not false, so again the required condition fails. If $w$ is false, the watched-literal invariant implies that every other literal of $C$ besides $l$ is false. Hence $l$ is being watched in a clause whose other literals are entirely false, and the subroutine correctly returns $1$.
It remains to prove the converse. Suppose that $l$ is being watched in a clause $C$ and that every literal of $C-{l}$ is false. The other watched literal $w$ of $C$ belongs to $C-{l}$, so $w$ is false. When the loop reaches $C\in W(l)$, the test $w$ is false succeeds, and the procedure returns $1$.
If the procedure returns $0$, then every clause in $W(l)$ has an other watched literal that is either true or unassigned. In either case that literal is not false, so no such clause has all literals other than $l$ false. Therefore no occurrence of $l$ in the maintained watch lists satisfies the required condition.
Thus the subroutine returns $1$ exactly when $l$ is being watched in a clause whose other literals are entirely false, and it uses the watched-literal information maintained by Algorithm D rather than rescanning the clauses. $\square$