TAOCP 7.2.2.2 Exercise 129
Let $\mathcal{C}(l)$ denote the set of clauses in which the literal $l$ is currently being watched in Algorithm D.
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: yes
Solve time: 1m01s
Solution
Let $\mathcal{C}(l)$ denote the set of clauses in which the literal $l$ is currently being watched in Algorithm D. In the state of the algorithm, each clause maintains two watched literals, and a literal is “watched in a clause” exactly when it occupies one of these two positions. The global assignment maintained by the algorithm assigns each literal a value in ${0,1}$, with $l=0$ meaning that the literal is currently false.
The required subroutine must return $1$ if there exists a clause $C \in \mathcal{C}(l)$ such that every literal in $C$ other than $l$ is currently false, and must return $0$ otherwise.
For a fixed clause $C \in \mathcal{C}(l)$, write $C = {l, l_2, \ldots, l_k}$ with all literals strictly distinct. The condition that “the other literals are entirely false” is the conjunction
$\bigwedge_{i=2}^k (l_i = 0).$
The subroutine therefore examines each clause in $\mathcal{C}(l)$ and tests this condition.
Define the procedure $W(l)$ as follows.
For each clause $C \in \mathcal{C}(l)$, scan the literals of $C$ distinct from $l$. If for every such literal $l' \in C$ with $l' \ne l$ we have $l' = 0$, then $C$ contains no currently true or unassigned literal other than $l$, hence $l$ is the unique potentially satisfiable literal in $C$ under the current partial assignment. In this case the condition required by the problem is satisfied, and the procedure returns $1$ immediately.
If no clause $C \in \mathcal{C}(l)$ satisfies this test, then no clause watched by $l$ has all its other literals false, and the procedure returns $0$.
Formally,
$$ W(l) = \begin{cases} 1, & \exists C \in \mathcal{C}(l)\ \text{such that}\ \forall l' \in C \setminus {l},\ l' = 0,\ 0, & \text{otherwise}. \end{cases} $$
The procedure inspects only clauses in $\mathcal{C}(l)$ and within each such clause inspects only its non-watched literals. The return value depends solely on the existence of a clause satisfying the stated universal condition on its remaining literals.
This completes the construction of the required subroutine. ∎