TAOCP 7.2.2.2 Exercise 265

Section 7.2.2.2: Satisfiability

Exercise 265. [21] Describe several circumstances in which the watched literals $l_0$ and/or $l_1$ of a clause $e$ actually become false during the execution of Algorithm C.

Verified: no
Solve time: 4m23s

Solution

Algorithm C maintains for each clause $e$ two watched literals, denoted $l_0$ and $l_1$. The purpose of the watched-literal scheme is that a clause need not be examined when assignments are made unless one of its watched literals has become false. Therefore the interesting cases are exactly those in which the current assignment changes the truth value of $l_0$ or $l_1$ from unassigned or true to false.

A watched literal $l_i$ of $e$ can become false in two fundamentally different ways. The first is a decision assignment made in step C2. If the branching variable chosen in step C2 is $|l_i|$, and the chosen polarity makes $l_i$ false, then the trail receives an assignment that falsifies the watched literal. The clause record for $e$ still contains $l_i$ in its watch position, but the watch list of the opposite literal must eventually process $e$ in step C3.

The second possibility is unit propagation. During step C3, a clause $e'$ that has become unit can force a variable assignment in step C4. If that forced assignment gives the opposite value of a watched literal $l_i$ in some other clause $e$, then $l_i$ becomes false without having been chosen as a decision literal. Thus a propagation step can falsify watched literals in clauses other than the clause that caused the propagation.

A watched literal can also become false when the clause itself is shortened during conflict analysis. In step C7, Algorithm C constructs a new clause by resolving clauses on the variable selected for elimination. The literals retained in the new clause are copied from the parent clauses except for the resolved pair. When the new clause is inserted, step C9 chooses its two watched literals from the literals that are not currently false whenever possible. Therefore a watched literal of the new clause may already have the value false at the instant the clause is created if the construction leaves no alternative nonfalse pair.

For an existing clause $e$, both watched literals can become false during the same branch of the search. This happens when the trail contains assignments falsifying both $l_0$ and $l_1$. The first falsification causes the clause to be examined, but the watch can usually be moved to another literal of $e$ that is not false. If every other literal of $e$ is already false, no new watch position exists. The clause is then either a conflict clause if all literals are false, or a unit clause if exactly one literal remains unassigned.

The invariant maintained by Algorithm C is that every clause $e$ has watched literals $l_0$ and $l_1$ such that the watch lists only need to be updated when a watched literal becomes false. A watched literal therefore becomes false only through a trail assignment produced by step C2 or step C4, or through the creation of a new clause in step C7 before its watches are installed by step C9.

This completes the proof. ∎