TAOCP 7.2.2.2 Exercise 168

Let $F$ be the clause set at step L3, and let Algorithm X have produced heuristic scores $H(l)$ for every literal $l$ based on step L2.

taocpmathematicsalgorithmsvolume-4hard

Section 7.2.2.2: Satisfiability

Exercise 168. [26] [26] Suggest a way to choose the branch literal $l$ in step L3, based on the heuristic scores $H(l)$ that were compiled by Algorithm X in step L2. Hint: Experience shows that it's good to have both $H(l)$ and $H(\bar{l})$ large.

Verified: yes
Solve time: 1m04s

Setup

Let $F$ be the clause set at step L3, and let Algorithm X have produced heuristic scores $H(l)$ for every literal $l$ based on step L2. For each variable $v$, the two associated literals are $v$ and $\bar v$.

Step L3 requires selecting a branch literal $l$ to guide the search split.

The goal is to choose $l$ so that both subproblems induced by assigning $l=1$ and $l=0$ are made as favorable as possible according to the heuristic information already computed.

Solution

Define a selection score for each variable $v$ by

$$ B(v) = \min\bigl(H(v), H(\bar v)\bigr), $$

and a secondary score

$$ S(v) = H(v) + H(\bar v). $$

Choose a variable $v^\ast$ that maximizes $B(v)$ over all variables $v$. If several variables achieve the same maximum value of $B(v)$, choose among them one that maximizes $S(v)$. Finally, take the branch literal $l$ to be either $v^\ast$ or $\overline{v^\ast}$; the choice between these two is immaterial at the selection stage and may be fixed arbitrarily or by a consistent convention such as selecting the positive literal.

This rule ensures that the selected variable has both literals with large heuristic weight, since maximizing $\min(H(v), H(\bar v))$ forces neither branch to be weak according to the score produced by Algorithm X. The secondary maximization of $H(v)+H(\bar v)$ breaks ties in favor of variables that are globally more influential in the clause set.

Verification

For the chosen variable $v^\ast$, suppose $B(v^\ast)$ is maximal. Then for every variable $v$,

$$ \min\bigl(H(v^\ast), H(\bar v^\ast)\bigr) \ge \min\bigl(H(v), H(\bar v)\bigr), $$

so neither branch of $v^\ast$ can be dominated in score by both branches of any competing variable simultaneously.

If one branch were significantly weaker, say $H(v^\ast) \ll H(\bar v^\ast)$, then $B(v^\ast)$ would be small, and another variable with more balanced scores would achieve a larger minimum, contradicting maximality. Thus both $H(v^\ast)$ and $H(\bar v^\ast)$ are forced to be large relative to competing choices.

The secondary criterion ensures that among variables with equal worst-branch strength, the selected variable contributes maximal total heuristic weight, preserving global clause influence while maintaining branch balance.

This completes the proof. ∎