TAOCP 7.2.2.2 Exercise 172

Exercise 172. [21] Explain why '+LO[j]' appears in step Y2's formula for BT.

Verified: yes
Solve time: 1m14s

Solution

In Algorithm Y, the quantity $BT$ in step Y2 measures the net effect on the heuristic score when a literal is chosen as a branch variable. The score is built from local contributions of occurrences of literals in clauses, recorded by the arrays $LO[j]$ and $LO[\bar{j}]$, which count occurrences of the positive and negative literals of variable $j$ in the current formula state used by the heuristic.

The term $+LO[j]$ appears because each occurrence of the positive literal $j$ contributes positively to the desirability of assigning $x_j = 1$. When $x_j$ is set to $1$, every clause containing the literal $j$ is immediately satisfied. Each such clause is therefore removed from further consideration in the search tree, producing a direct increase in the branching score associated with choosing $j$.

This contribution is not duplicated elsewhere in the $BT$ expression, because occurrences of the complementary literal $\bar{j}$ correspond to clauses that are instead affected when $x_j = 0$. Those effects are accounted for separately through the corresponding term involving $LO[\bar{j}]$ in the symmetric part of the formula. The decomposition of $BT$ separates the influence of the two polarities of the same variable, so that each clause occurrence contributes exactly once through either $LO[j]$ or $LO[\bar{j}]$, depending on its sign.

The appearance of $+LO[j]$ is therefore forced by the structure of the branching measure: it represents the full positive contribution of all clauses that become satisfied when selecting the positive literal $j$, before any cancellati