TAOCP 7.2.2.2 Exercise 175
Algorithm L maintains a CNF instance as a family of clauses $F$, together with a partial assignment represented implicitly by forced literals produced during propagation.
Section 7.2.2.2: Satisfiability
Exercise 175. [32] When Algorithm L is extended to nonternary clauses as in exercise 143, how should Algorithms X and Y also change? (Instead of using (64) and (65) to compute a heuristic for preselection, use the much simpler formula in answer 146. And instead of using $h(u)h(v)$ in (67) to estimate the weight of a ternary clause that will be reduced to binary, consider a simulated reduced clause of size $s \ge 2$ to have weight $K_s \approx \gamma^{2-s}$, where $\gamma$ is a constant (typically 0.2).)
Verified: no
Solve time: 1m12s
Setup
Algorithm L maintains a CNF instance as a family of clauses $F$, together with a partial assignment represented implicitly by forced literals produced during propagation. Steps $X$ perform constraint propagation after a literal is chosen, and steps $Y$ compute heuristic scores for selecting the next branching literal.
In the extension described in exercise 143, clauses may have arbitrary length $s \ge 2$. A clause $C = {l_1,\ldots,l_s}$ is satisfied if some $l_i$ is chosen true; otherwise every assignment of a literal $\ell$ reduces $C$ by deleting $\bar{\ell}$ when present, producing a clause of smaller size. A unit clause forces its unique literal.
Each reduced clause of size $s$ is assigned weight
$K_s \approx \gamma^{2-s},$
where $\gamma$ is a fixed constant, typically $0.2$.
The task is to describe how steps $X$ and $Y$ must be modified under this general clause structure and this simplified weighting scheme.
Solution
The structure of step $X$ depends only on local clause reduction under a chosen literal, not on the maximal clause size. For a chosen literal $l$, every clause $C$ is processed by checking whether $l \in C$ or $\bar{l} \in C$ holds.
If $l \in C$, then $C$ becomes satisfied and is removed from the clause set. If $\bar{l} \in C$, then $\bar{l}$ is deleted from $C$, producing a new clause $C' = C \setminus {\bar{l}}$. If $|C'| = 1$, the remaining literal is forced and enters the propagation queue exactly as in the ternary case. If $|C'| = 0$, the empty clause is produced and the current branch fails.
These operations replace every occurrence of the ternary-specific reduction rules in $X$, since no step depends on the value $3$ as a maximum clause size. The only change is that the clause-length test “ternary to binary” becomes the uniform rule “size decreases by one, with unit triggering when size becomes $1$.”
The heuristic step $Y$ selects a candidate literal by estimating its effect on future propagation. In the ternary version, the score involved products such as $h(u)h(v)$ derived from pairs of literals within clauses. In the nonternary extension this is replaced by a direct clause-weight model.
For each literal $l$, the score $H(l)$ is computed by summing contributions over all clauses containing $\bar{l}$, since these are the clauses that would be reduced if $l$ is chosen true. If a clause $C$ has current size $s$, its contribution is $K_s$. Thus
$H(l) = \sum_{\bar{l} \in C} K_{|C|-1},$
since each such clause would be reduced from size $|C|$ to size $|C|-1$ after choosing $l$.
This replaces the former construction in which ternary clauses were treated through pairwise interaction weights such as $h(u)h(v)$. The new rule treats each clause as a single combinatorial object whose influence depends only on its current size, so the scoring is additive rather than multiplicative.
When multiple literals compete, $Y$ selects a literal maximizing $H(l)$, breaking ties by the same secondary criteria used in Algorithm L. The same computation is applied symmetrically for both polarities $l$ and $\bar{l}$ when polarity choice is part of the selection stage.
The effect of using $K_s \approx \gamma^{2-s}$ is that smaller clauses dominate the heuristic: binary clauses contribute $K_2 = 1$, ternary clauses contribute $K_3 \approx \gamma^{-1}$, and larger clauses contribute progressively larger weights, thereby emphasizing clauses that are closer to becoming unit clauses under a branching decision.
Verification
In step $X$, every possible outcome of assigning a literal $l$ is exhausted: clauses containing $l$ are satisfied and removed, clauses containing $\bar{l}$ lose exactly one literal, and no clause is modified otherwise. A clause becomes unit precisely when its size is reduced from $2$ to $1$, and becomes empty precisely when it was already unit before reduction, matching the standard propagation condition used in Algorithm L.
In step $Y$, every clause that can be affected by choosing $l$ is counted exactly once, since each clause contributes only through the unique literal $\bar{l}$ it contains. The weight assignment depends only on the resulting clause size after reduction, which is uniquely determined as $|C|-1$. Hence the score $H(l)$ is well-defined and independent of processing order.
The replacement of $h(u)h(v)$ by $K_s$ preserves additivity over clauses, since each clause contributes a single scalar term instead of a product of literal-level heuristics. No interaction term is omitted, because all interactions in the ternary formulation arise solely from clauses, and each clause is now represented directly.