TAOCP 7.2.2.2 Exercise 146

When Algorithm L is extended to clauses of arbitrary length, the heuristic should continue to estimate the "support" for setting a literal $l$ to true by combining the contributions of all clauses con...

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 146. [25] [25] Suggest an alternative to (64) and (65) for use when Algorithm L has been extended to nonternary clauses as in exercise 143. (Strive for simplicity.)

Verified: no
Solve time: 3m53s

Solution

When Algorithm L is extended to clauses of arbitrary length, the heuristic should continue to estimate the "support" for setting a literal $l$ to true by combining the contributions of all clauses containing $l$. For a clause

$$ C={l,l_1,\ldots,l_{k-1}}, $$

the clause is satisfied by setting $l$ true. If $l$ is not chosen, the remaining literals must satisfy the clause, and the heuristic evidence for this event is naturally represented by the product of the heuristic values of their complements. Thus the contribution of $C$ is

$$ \prod_{i=1}^{k-1} h(\bar l_i). $$

This is exactly the ternary formula when $k=3$, and it extends uniformly to all clause lengths.

A simple replacement for (65) is therefore

$$ \boxed{ s(l)=\sum_{C\ni l} \prod_{l'\in C\setminus{l}} h(\bar l'). } $$

Here $s(l)$ denotes the unnormalized support accumulated from all clauses containing $l$.

Instead of introducing additive constants as in the original recurrence, one may normalize the supports directly. This gives a corresponding replacement for (64):

$$ \boxed{ h'(l)= \frac{s(l)} {s(l)+s(\bar l)}. } $$

The updated heuristic values automatically satisfy

$$ h'(l)+h'(\bar l)=1, $$

so no separate normalization step is required. The pair of formulas is therefore self-contained.

This proposal also behaves correctly for every clause length:

  • If $C$ is a unit clause ${l}$, the product is the empty product, equal to $1$. Thus a unit clause contributes the maximum possible support for $l$.
  • If $C={l,m}$ is binary, the contribution is $h(\bar m)$.
  • If $C={l,m,n}$ is ternary, the contribution is $h(\bar m)h(\bar n)$, exactly as in the original heuristic.
  • For longer clauses, the contribution is the product over all remaining literals, with no special cases.

No clause length dependent scaling is introduced. The product already decreases as the number of remaining literals increases, reflecting the fact that a longer clause imposes a weaker constraint on any single literal. Additional length dependent factors would complicate the heuristic without providing a comparably simple interpretation.

Hence a simple alternative to (64) and (65) for arbitrary clause lengths is the pair

$$ \boxed{ s(l)=\sum_{C\ni l} \prod_{l'\in C\setminus{l}} h(\bar l'), } $$

$$ \boxed{ h'(l)= \frac{s(l)} {s(l)+s(\bar l)}. } $$

These formulas reduce to the original ternary heuristic when every clause has three literals, apply uniformly to clauses of every size, and eliminate the need for a separate normalization formula.