TAOCP 7.2.2.2 Exercise 168

Algorithm L invokes Algorithm X in step L2 to compute heuristic scores $H(l)$ for every literal $l$.

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: 49s

Setup

Algorithm L invokes Algorithm X in step L2 to compute heuristic scores $H(l)$ for every literal $l$. Exercise 168 asks for a rule to choose the branch literal in step L3 from these scores.

The hint requires that the rule should favor variables for which both $H(l)$ and $H(\bar l)$ are large. Therefore the selection criterion must depend on the pair

$$ \bigl(H(l),H(\bar l)\bigr), $$

not on either score separately.

Solution

A suitable choice is to branch on the variable whose two heuristic scores have the largest product. Thus, for each variable $v$, define

$$ S(v)=H(v),H(\bar v), $$

and choose a literal $l$ such that

$$ |l|=\arg\max_v S(v). $$

After the variable has been chosen, orient the branch by taking the polarity with larger score:

$$ l= \begin{cases} v,&\text{if }H(v)\ge H(\bar v),\ \bar v,&\text{if }H(\bar v)>H(v). \end{cases} $$

The product criterion implements the hint directly. If either $H(v)$ or $H(\bar v)$ is small, then

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

is also small, regardless of the size of the other score. Consequently a variable whose influence is concentrated almost entirely in one polarity is not preferred. A large value of $S(v)$ is possible only when both $H(v)$ and $H(\bar v)$ are simultaneously large.

The choice of polarity is independent of the variable selection criterion. Once the variable has been selected because both polarities appear influential, the first branch should use the more promising polarity, namely the one with larger heuristic score. If that branch fails, the opposite polarity is explored immediately afterward, and it also has a comparatively large heuristic score because the product criterion has already guaranteed that both scores are large.

This rule uses only the information already computed in step L2, requires only one multiplication for each variable, and satisfies the stated heuristic objective.

The final branching rule is therefore

$$ \boxed{\text{Choose }|l|\text{ to maximize }H(l)H(\bar l),\text{ then branch first on the polarity with larger }H.} $$

Verification

Suppose two variables satisfy

$$ (H(v),H(\bar v))=(100,1),\qquad (H(w),H(\bar w))=(20,20). $$

Then

$$ S(v)=100,\qquad S(w)=400. $$

The proposed rule selects $w$, because both polarities are significant, whereas a rule based only on $\max(H(l),H(\bar l))$ would incorrectly prefer $v$.

If

$$ (H(v),H(\bar v))=(40,35),\qquad (H(w),H(\bar w))=(60,10), $$

then

$$ S(v)=1400,\qquad S(w)=600, $$

so the proposed rule again favors the variable whose two polarities are both strong, exactly as suggested by the hint.

Notes

Other symmetric functions that increase only when both arguments are large, such as

$$ \min{H(v),H(\bar v)} \quad\text{or}\quad \frac{2H(v)H(\bar v)}{H(v)+H(\bar v)}, $$

also satisfy the hint. The product

$$ H(v)H(\bar v) $$

is the simplest such criterion and naturally suppresses variables for which one polarity has negligible heuristic value.