TAOCP 7.2.2.2 Exercise 149
In Algorithm L, a variable is a **participant** at the current node if either literal $x$ or $\bar{x}$ has played the role of $u$ or $v$ in step L8 at some node above the current node in the search tr...
Section 7.2.2.2: Satisfiability
Exercise 149. ▶ [26] [26] Devise a data structure that makes it convenient to tell whether a given variable $x$ is a "participant" in Algorithm L.
Verified: yes
Solve time: 1m39s
Setup
In Algorithm L, a variable is a participant at the current node if either literal $x$ or $\bar{x}$ has played the role of $u$ or $v$ in step L8 at some node above the current node in the search tree. A variable that has not acquired this property is a newbie. The task is to maintain enough information to answer, for a given variable $x$, whether $x$ is a participant.
The required operation is a membership test on the set of variables that have occurred in the branching history through step L8. Since a variable can become a participant only once and remains a participant until the search returns to a point above the event that created it, the data structure must support insertion during descent and restoration during backtracking.
Solution
Use an array $\mathop{\rm PART}(x)$ indexed by variables, together with a stack of changes. The value
$$ \mathop{\rm PART}(x)=1 $$
means that $x$ is currently a participant, and
$$ \mathop{\rm PART}(x)=0 $$
means that $x$ is currently a newbie. Initially, at depth $d=0$, set
$$ \mathop{\rm PART}(x)=0 $$
for every variable $x$, because no literal has yet played the role of $u$ or $v$ in step L8.
Whenever step L8 is executed with a literal whose variable is $x$, perform the following additional operation. If
$$ \mathop{\rm PART}(x)=0, $$
set
$$ \mathop{\rm PART}(x)\leftarrow 1 $$
and push $x$ onto a stack $\mathop{\rm PSTACK}$. If $\mathop{\rm PART}(x)=1$, no change is necessary, because the variable is already a participant.
During backtracking, whenever Algorithm L returns above a node, pop from $\mathop{\rm PSTACK}$ all variables whose first participation event occurred below the new node. For each popped variable $x$, perform
$$ \mathop{\rm PART}(x)\leftarrow 0. $$
The stack entries must be associated with the depth at which they were inserted. Equivalently, one may store on $\mathop{\rm PSTACK}$ the pair $(d,x)$, where $d$ is the depth of the L8 event. When backtracking from depth $d$ to depth $d-1$, remove all entries with stored depth $d$.
The membership query requested by the exercise is then answered by the single array access
$$ \text{“}x\text{ is a participant”}\iff \mathop{\rm PART}(x)=1. $$
The update procedure preserves the definition of participant. If $x$ has not appeared in any earlier step L8 above the current node, then $\mathop{\rm PART}(x)=0$ until the first such occurrence. At that occurrence the update changes $\mathop{\rm PART}(x)$ to $1$, exactly when $x$ becomes a participant. If $x$ has already appeared in an earlier L8 step that is still on the current search path, then $\mathop{\rm PART}(x)=1$, and no further update is needed. If backtracking removes the first occurrence that made $x$ a participant, the corresponding stack entry restores $\mathop{\rm PART}(x)=0$, which agrees with the fact that no remaining ancestor node has made $x$ a participant.
Thus the array $\mathop{\rm PART}$ gives constant-time tests, and the stack gives constant-amortized-time maintenance while preserving the definition used by Algorithm L.
Verification
Consider a variable $x$. There are two cases.
Suppose $x$ is a participant according to Algorithm L. Then some literal $x$ or $\bar{x}$ has played the role of $u$ or $v$ in step L8 at a node that is still an ancestor of the current node. The update at that L8 event inserted $x$ into $\mathop{\rm PSTACK}$ and set
$$ \mathop{\rm PART}(x)=1. $$
Because the search has not backtracked above that event, the stack entry remains present, so the value of $\mathop{\rm PART}(x)$ is still $1$.
Conversely, suppose
$$ \mathop{\rm PART}(x)=1. $$
The only operation that changes a value from $0$ to $1$ is the update performed after an L8 event involving $x$ or $\bar{x}$. The only operation that removes this state is the corresponding stack pop during backtracking. Therefore a remaining value of $1$ means that such an L8 event exists on the current ancestor path, so $x$ satisfies the definition of participant.
Both implications agree with the definition, so the data structure answers exactly the required question.
This completes the proof.
∎
Notes
The same idea can be implemented with a timestamp array instead of a stack. Store the depth of the most recent L8 event for each variable, and compare it with the current search depth. The stack method is preferable when Algorithm L already maintains backtracking stacks, because restoration is explicit and requires no additional timestamp comparisons.