TAOCP 7.2.2.2 Exercise 131

In Algorithm D, after step D3 has failed to find a unit clause, every free variable $x_k$ has had its watch lists examined.

taocpmathematicsalgorithmsvolume-4hard

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: no
Solve time: 2m06s

Setup

In Algorithm D, after step D3 has failed to find a unit clause, every free variable $x_k$ has had its watch lists examined. Let $W(l)$ denote the watch list associated with a literal $l$, and let

$w(l)=|W(l)|.$

At this point the algorithm has available, with negligible additional work, the values $w(x_k)$ and $w(\bar{x}_k)$ for every free variable $x_k$. The purpose of the exercise is to use these values to choose a better branching variable in step D4.

A branching heuristic assigns a score to each possible branching choice and selects the choice with the most promising score. The watch lists measure how many clauses currently depend on a literal, so large values indicate literals whose truth assignments may cause many clauses to require further attention.

Solution

The simplest heuristic uses the total number of watched occurrences of a variable. Define

$s_1(x_k)=w(x_k)+w(\bar{x}_k).$

At step D4, choose a free variable $x_k$ maximizing $s_1(x_k)$. The sign of the first branch can be chosen by comparing the two watch-list lengths. If

$w(x_k)>w(\bar{x}_k),$

the first branch assigns $x_k=1$, while if

$w(\bar{x}_k)>w(x_k),$

the first branch assigns $x_k=0$. Ties may be broken arbitrarily.

A more refined heuristic distinguishes clauses that would become critical after a branch. A watched literal is especially significant when the other watched literal in its clause is already false or nearly forced. Let

$u(l)=|{C:l\in W(C)\text{ and every other watched literal of }C\text{ is false}}|.$

The subroutine of Exercise 129 provides the information needed to compute whether a literal is watched in such a clause. A variable score based on this quantity is

$s_2(x_k)=u(x_k)+u(\bar{x}_k).$

Choosing a variable with maximum $s_2(x_k)$ attempts to branch on variables that are most likely to produce short clauses and contradictions quickly.

A combined heuristic uses both kinds of information:

\alpha\bigl(w(x_k)+w(\bar{x}_k)\bigr) +\beta\bigl(u(x_k)+u(\bar{x}_k)\bigr),$$ where $\alpha$ and $\beta$ are experimentally chosen constants. The choice $$\alpha=1,\qquad \beta=1$$ gives a direct combination of activity and immediate constraint pressure. The sign choice can also be improved. Instead of always selecting the larger watch list, define $$p(x_k)=u(x_k)-u(\bar{x}_k).$$ If $p(x_k)>0$, branch first on $x_k=1$; if $p(x_k)<0$, branch first on $x_k=0$. This attempts to make the first branch expose contradictions sooner. An experiment consists of running Algorithm D on the same collection of SAT instances while changing only the step D4 selection rule. The measured quantities are the number of recursive calls, the number of executions of steps D5 and D6, and the total running time. The comparison should include the original branching rule and the modified rules based on $s_1$, $s_2$, and $s_3$. The expected behavior is that $s_1$ improves the choice when many clauses depend on a small set of variables, while $s_2$ and $s_3$ perform better on instances where contradictions arise from chains of nearly forced assignments. No single score dominates all SAT instances, because the useful branching information depends on the structure of the formula. ## Verification The heuristic uses only information already available after step D3. During that step, Algorithm D examines the watch lists of every free variable, so computing $$w(x_k),\qquad w(\bar{x}_k)$$ requires no additional clause traversal. For each free variable $x_k$, the scores $s_1(x_k)$, $s_2(x_k)$, or $s_3(x_k)$ depend only on the current state of the search. Therefore changing the step D4 rule changes only the order in which assignments are explored. The set of assignments eventually examined by complete backtracking remains the same, and satisfiable instances still produce a satisfying assignment while unsatisfiable instances still exhaust the search tree. The sign-selection rule is also consistent with Algorithm D. Both branches $x_k=1$ and $x_k=0$ remain available, but the branch with the larger predicted constraint effect is examined first. Hence the heuristic affects efficiency without changing correctness. ## Notes Modern SAT solvers use more elaborate descendants of these ideas. The most influential family of methods assigns each variable an activity score that changes during the search, rather than relying only on the current watch lists. The watch-list heuristic in this exercise is a local version of that principle, using the data structures already maintained by Algorithm D.