TAOCP 7.2.2.2 Exercise 148
Equation (66) is used inside the search procedure after a partial assignment has already been made.
Section 7.2.2.2: Satisfiability
Exercise 148. [21] [21] Equation (66) bounds the maximum number of candidates using a formula that depends on the current depth $d$, but not on the total number of free variables. The same cutoffs are used in problems with any number of variables. Why is that a reasonable strategy?
Verified: yes
Solve time: 1m26s
Solution
Equation (66) is used inside the search procedure after a partial assignment has already been made. At depth $d$, the algorithm has fixed the first $d$ decisions along the current branch, and the remaining work is estimated from the clauses and literals that are still relevant at that point. The purpose of $C_{\max}$ is to decide whether continuing to examine a collection of candidates is worthwhile, not to estimate the entire original search space.
A partial assignment at depth $d$ can only influence the part of the formula that survives after the previous choices have been applied. Variables that have not yet been considered do not create a fundamentally different type of local situation merely because their total number is larger. The immediate candidates generated by the algorithm are constrained by the clauses near the current branch, and the number of useful alternatives is controlled mainly by the depth and the resulting reductions in the clause set.
If the cutoff depended on the total number of free variables, then the same local configuration at depth $d$ would receive different treatment merely because irrelevant variables had been added elsewhere in the formula. For example, a formula containing a difficult core on a small set of variables could be enlarged by adjoining many variables that occur only in already satisfied clauses. The satisfiability behavior of the core would be unchanged, but a cutoff depending on the total number of variables would increase unnecessarily. The algorithm would then spend more effort on a problem that has not become harder in the part being searched.
The depth $d$ provides a stable measure of progress in the search. As $d$ increases, more assignments have been made, more clauses have been simplified, and the candidate estimate can be reduced according to the actual state reached by the algorithm. A cutoff based only on $d$ therefore gives the same bound for equivalent subproblems reached at the same depth, independent of irrelevant extensions of the original formula.
The strategy is reasonable because the cutoff is intended to control the local branching behavior of the search tree, while the depth already records the amount of branching information accumulated along the current path. The total number of free variables affects the eventual size of the whole search tree, but it is not the appropriate parameter for limiting a single local decision in the search. Thus using the same values of $C_{\max}$ for all formulas with the same current depth avoids dependence on irrelevant variables while preserving control over the difficult parts of the search.
$\boxed{\text{The depth-based cutoff is reasonable because }d\text{ measures the relevant progress of the search, whereas the total number of free variables can include variables that do not affect the current subproblem.}}$