TAOCP 7.2.2.2 Exercise 153
Let $p$ be a candidate generated in step X3, and let $C(p)$ denote the number of clauses already satisfied by the partial assignment $p$.
Section 7.2.2.2: Satisfiability
Exercise 153. [17] [17] What's a good way to weed out unwanted candidates in step X3, if $C > C_{\max}$?
Verified: yes
Solve time: 1m53s
Corrected Solution
Let $p$ be a candidate generated in step X3, and let $C(p)$ denote the number of clauses already satisfied by the partial assignment $p$. Let $C_{\max}$ be the current upper bound on admissible candidates (i.e., the best value allowed so far in the search).
The key property is monotonicity: extending a partial assignment cannot decrease the number of already satisfied clauses. Formally, if $p' \supseteq p$, then
$$ C(p') \ge C(p). $$
Hence, if a partial candidate already violates the bound,
$$ C(p) > C_{\max}, $$
then every extension $p' \supseteq p$ also satisfies
$$ C(p') \ge C(p) > C_{\max}. $$
Therefore, no extension of $p$ can ever lead to an acceptable candidate under the bound $C_{\max}$.
A good way to weed out unwanted candidates in step X3 is therefore:
Discard immediately every candidate $p$ for which $C(p) > C_{\max}$.
This pruning rule is safe because such candidates are permanently infeasible with respect to the bound and cannot contribute to any solution that respects $C_{\max}$. Consequently, step X3 need not propagate or expand them further, reducing the search space without affecting correctness.