TAOCP 7.2.2.2 Exercise 131
Let Algorithm D be in the state described after completion of step D3 with no unit clauses discovered.
Section 7.2.2.2: Satisfiability
Exercise 131. ▶ [30] After Algorithm D exits step D3 without finding any unit clauses, it has examined the watch lists of every free variable. Therefore it could have computed the lengths of those watch lists, with little additional cost; and information about those lengths could be used to make a more informed decision about the variable that's chosen for branching in step D4. Experiment with different branching heuristics of this kind.
Verified: yes
Solve time: 1m01s
Setup
Let Algorithm D be in the state described after completion of step D3 with no unit clauses discovered. In this state every free variable $x_k$ has two associated watch lists, one for the literal $k$ and one for the literal $\bar{k}$, consisting of clauses in which the corresponding literal is currently watched.
Let
$$ W(k) \quad\text{be the number of clauses in the watch list of } k, \qquad W(\bar{k}) \quad\text{be the number of clauses in the watch list of } \bar{k}. $$
Since step D3 has scanned all watch lists of all free variables, these quantities are available without additional traversals of the clause database.
Step D4 chooses a free variable $x_k$ for branching. The goal is to refine this choice using the information in the values $W(k)$ and $W(\bar{k})$.
Solution
A natural refinement is to interpret watch list sizes as a measure of current constraint density. A variable whose literals appear in many watched positions participates in many clauses that are still “active” under the current partial assignment, so branching on it has greater potential to simplify the remaining formula quickly.
Define the total activity of a variable by
$$ A(k) = W(k) + W(\bar{k}). $$
A first heuristic chooses a variable $x_k$ maximizing $A(k)$ among all free variables. This rule prefers variables that occur in many currently relevant clauses, so either assignment of $x_k$ is likely to satisfy or falsify many watched literals and thereby trigger propagation or clause simplification in step D2 of subsequent iterations.
A second refinement distinguishes polarity imbalance. Define
$$ \Delta(k) = \lvert W(k) - W(\bar{k}) \rvert. $$
After selecting $x_k$ maximizing $A(k)$, one may choose the branching value of $x_k$ so that the literal with larger watch count is set to true first. Concretely, if $W(k) \ge W(\bar{k})$, then branch first with $x_k = 1$, otherwise with $x_k = 0$. This increases the probability that many clauses immediately lose a watched false literal and become simpler under unit propagation.
A third refinement uses normalized activity to avoid bias toward variables that appear frequently but symmetrically. Define
$$ R(k) = \frac{\min(W(k), W(\bar{k}))}{\max(W(k), W(\bar{k})) + 1}. $$
Choosing variables minimizing $R(k)$ favors variables whose occurrences are highly polarized. Assigning such a variable first tends to eliminate many clauses in one branch while leaving the other branch significantly more constrained, increasing asymmetry in the search tree.
A fourth refinement combines both effects into a single score
$$ S(k) = A(k) - \lambda \Delta(k), $$
for a fixed parameter $\lambda \ge 0$. Larger $\lambda$ emphasizes polarity balance, while smaller $\lambda$ emphasizes total activity. Step D4 can then select a variable maximizing $S(k)$.
Each of these heuristics can be integrated into Algorithm D without altering its correctness, since only the variable selection rule in D4 is modified and no inference rule is changed.
Verification
The quantities $W(k)$ and $W(\bar{k})$ are determined entirely by the state of the watch lists after D3, since every clause maintains exactly two watched literals and each watch list entry corresponds to one clause currently tracking that literal.
For each proposed heuristic, the selection function depends only on these counts and the set of free variables, so it is well-defined at the moment of branching.
Correctness of Algorithm D is unaffected because D4 only selects a variable; all satisfiability-preserving transformations occur in steps D1–D3 and subsequent propagation. Thus replacing the selection criterion in D4 does not change the logical invariant that a satisfying assignment is found if one exists.
The computation of $A(k)$, $\Delta(k)$, and $R(k)$ requires only arithmetic on the already-available watch list sizes, so no additional traversal of clauses is required beyond the work already performed in D3.
This completes the verification. ∎
Notes
The heuristic $A(k)$ corresponds closely to activity-based scoring methods used in modern SAT solvers, where variables appearing in many recently active clauses are preferred for branching. The polarity-aware term $\Delta(k)$ anticipates a strategy that biases early assignments toward assignments that immediately satisfy many watched literals, increasing propagation density.
In practice, dynamic variants refine $W(k)$ and $W(\bar{k})$ over time by decaying older contributions and increasing weights when a clause participates in a conflict. The structure of Algorithm D already supports such refinements because watch lists encode a sparse and localized view of clause activity, allowing incremental updates without global recomputation.