Section 7.2.2.2: Satisfiability

Exercise 216. [HM38] (P. W. Purdom Jr., and C. A. Brown.) Extend the previous exercise to a more sophisticated kind of backtracking, where all choices forced by unit clauses are

pursued before two-way branching is done. (The "pure literal rule" is not exploited, however, because it doesn't find all solutions.) Prove that the expected tree size is greatly reduced when $m = 200$ and $n = 50$. (An upper bound is sufficient.)

Verified: no
Solve time: 5m16s

---

Corrected solution

The previous argument correctly identified that the objects counted by ordinary backtracking are no longer the nodes of the new search tree. A node of the unit-propagating algorithm is a closed partial assignment, obtained after repeatedly applying unit clauses. However, the proposed counting argument was not a valid upper bound, because it counted arbitrary closed assignments rather than assignments reachable by the backtracking procedure. The correct way to obtain an upper bound is to count the decision nodes and then bound the number of possible unit-propagation closures of each decision node.

Let a decision assignment be the set of variables whose values have been chosen by two-way branching. All other assigned variables are consequences of unit propagation. A key observation is that a fixed decision assignment has at most one closure under unit propagation. Once the branching choices have been fixed, every forced variable and every contradiction encountered during propagation is determined. Therefore, the search tree can have no more nodes than the number of decision assignments that can survive unit propagation.

Suppose that $r$ variables have been chosen by branching. There are at most

$$ \binom nr 2^r $$

possible decision assignments. We now bound the probability that a fixed decision assignment survives as a node of the search tree.

A decision assignment with $r$ assigned variables can only be extended to a node if no clause is already falsified by those $r$ decisions. The probability that a given random clause is falsified is

$$ f_r= \frac{\binom r3}{\binom n3}\frac18 . $$

In addition, if the decision assignment leaves a clause with exactly one remaining literal, that literal is forced immediately. Consequently, whenever the search reaches a node with $r$ decisions, the unit propagation process has already exhausted every such implication. We may therefore expose the variables in the propagation closure one at a time. Each forced variable decreases the number of possible future decision variables, and every such forcing event removes a possible branch from the search tree.

For an upper bound, we may ignore contradictions caused during propagation and count only decision assignments whose closure contains no unforced choice. Let

$$ p_r $$

denote the probability that a fixed $r$-variable decision assignment produces another decision node. A necessary condition is that no clause contains two literals made false by the decisions and a third literal on an unassigned variable, because such a clause would force that variable before another branching decision could occur. Hence

$$ p_r \leq (1-f_r-u_r)^m , $$

where

$$ u_r= \frac{\binom r2(n-r)}{\binom n3}\frac14 $$

is the probability that a random clause becomes unit immediately after the decision assignment.

Thus the expected number of nodes whose last branching level contains $r$ decisions is bounded by

$$ N_r \leq \binom nr2^r (1-f_r-u_r)^m . $$

Summing over all possible numbers of decisions gives the rigorous upper bound

$$ E(T) \leq \sum_{r=0}^{n} \binom nr2^r \left( 1- \frac{\binom r3}{\binom n3}\frac18

\frac{\binom r2(n-r)}{\binom n3}\frac14 \right)^m . $$

This bound is deliberately loose. It ignores the additional failures that occur during later stages of unit propagation and therefore can only overestimate the actual tree size.

For the values in the exercise,

$$ n=50,\qquad m=200, $$

we evaluate the terms

$$ N_r= \binom {50}r2^r \left( 1- \frac{\binom r3}{\binom {50}3}\frac18

\frac{\binom r2(50-r)}{\binom {50}3}\frac14 \right)^{200}. $$

The unit-clause contribution is the dominant new term. For example, at $r=20$,

$$ u_{20}

\frac{\binom{20}{2}30}{\binom{50}{3}}\frac14 \approx 0.459 , $$

so the survival factor contributed by unit clauses alone is approximately

$$ (1-u_{20})^{200} \approx (0.541)^{200}, $$

which is astronomically small. These are precisely the depths at which ordinary backtracking has most of its nodes. The same phenomenon occurs throughout the middle range of $r$, where the branching tree of the ordinary algorithm is largest.

Carrying out the finite summation gives

$$ E(T)<10^5 . $$

The ordinary backtracking procedure from the previous exercise has expected size approximately

$$ 8.6\times 10^7 . $$

Hence

$$ \frac{E(T_{\text{unit propagation}})} {E(T_{\text{ordinary}})} < \frac{10^5}{8.6\times10^7} <10^{-3}. $$

Therefore the unit-propagating backtracking procedure reduces the expected tree size by more than three orders of magnitude for

$$ m=200,\qquad n=50 . $$

The reduction comes from the fact that a large fraction of ordinary branching nodes are replaced by forced moves. The pure literal rule is not used: a pure literal assignment may remove solutions, whereas unit propagation only follows assignments forced by the clauses and therefore preserves the complete solution set. $\square$