TAOCP 7.2.2.2 Exercise 149
Let the current instance of SAT in Algorithm L consist of a family $F$ of clauses over variables $x_1,\ldots,x_n$.
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: 1m03s
Setup
Let the current instance of SAT in Algorithm L consist of a family $F$ of clauses over variables $x_1,\ldots,x_n$. At any stage of the computation, some clauses have been deleted and some literals have been removed from remaining clauses due to assignments and propagation steps.
A variable $x$ is called a participant if and only if at least one literal involving $x$ or $\bar{x}$ occurs in at least one remaining clause of the current instance.
The task is to maintain a data structure that supports the query “is $x$ a participant?” in constant time during the execution of Algorithm L, while allowing efficient updates when clauses are deleted or literals are removed.
Solution
For each variable $x$, maintain a representation of all occurrences of $x$ and $\bar{x}$ in the current family of clauses, together with a counter
$\mathrm{occ}(x) = #{\text{occurrences of } x \text{ or } \bar{x} \text{ in remaining clauses}}.$
This is implemented by storing two doubly linked incidence lists per variable, one for $x$ and one for $\bar{x}$. Each occurrence of a literal in a clause is represented by a node in its corresponding incidence list. Each clause also stores pointers to all its literal nodes.
The structure supports the following invariant: after every update step of Algorithm L, $\mathrm{occ}(x)$ equals the total number of nodes currently present in the incidence lists of $x$ and $\bar{x}$.
The update operations are defined as follows. When a clause $C$ is deleted, every literal node belonging to $C$ is removed from its incidence list. If a node corresponding to literal $l$ with $|l|=x$ is removed, then $\mathrm{occ}(x)$ is decreased by $1$. When a clause is restored (during backtracking), its literal nodes are reinserted into their incidence lists and the corresponding counters are incremented.
Under this representation, $x$ is a participant if and only if
$\mathrm{occ}(x) > 0.$
The query “is $x$ a participant?” is therefore answered by a single comparison of $\mathrm{occ}(x)$ with $0$, requiring constant time.
The maintenance cost of updates is proportional to the number of literal occurrences removed or restored, since each such operation triggers exactly one increment or decrement of a single counter.
Verification
Each occurrence of a literal $l$ contributes exactly one node to exactly one incidence list, determined by $|l|$. No occurrence is represented more than once because each clause-literal pair is stored as a distinct node.
Every deletion of a clause removes precisely the set of nodes corresponding to its literals, so every removed occurrence is accounted for by exactly one decrement of the appropriate $\mathrm{occ}(x)$. The same holds symmetrically for restoration, so $\mathrm{occ}(x)$ always equals the current number of occurrences of $x$ or $\bar{x}$.
If $\mathrm{occ}(x)=0$, no remaining clause contains either $x$ or $\bar{x}$, so $x$ does not participate. If $\mathrm{occ}(x)>0$, at least one node remains in an incidence list of $x$ or $\bar{x}$, so $x$ appears in some remaining clause. This establishes equivalence between participation and positivity of the counter.
This completes the proof. ∎
Notes
A more compact variant replaces integer counters by a Boolean array $\mathrm{active}(x)$ together with a stack of variables whose counter changes from $0$ to $1$ or from $1$ to $0$. This allows maintenance of an explicit list of participants, while still supporting constant-time membership tests via the Boolean flag.