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: yes
Solve time: 1m44s

Solution

The purpose of (64) and (65) is to estimate the desirability of choosing a branch literal $l$ in step L3 from information gathered about the clauses containing $l$ and $\bar l$. The formulas are specialized to ternary clauses because the contribution of a clause is determined by the three literals in that clause. After exercise 143, a clause $c$ may have arbitrary positive size, so the contribution of a clause should depend on its current number of active literals, namely $CSIZE(c)$.

A direct extension is obtained by assigning each active clause a weight that decreases as the clause becomes longer. Let

$$ w(c)=\frac{1}{CSIZE(c)} . $$

For every active clause $c$, the value $w(c)$ measures the pressure created by that clause. A unit clause receives weight $1$, a binary clause receives weight $1/2$, a ternary clause receives weight $1/3$, and longer clauses receive progressively smaller weights. Thus short clauses influence the heuristic more strongly, as required by the role of short clauses in Algorithm L.

Define the preliminary score of a literal $l$ by

$$ h(l)=\sum_{\substack{c:,l\in CINX(c)\ c\ {\rm active}}} w(c)

\sum_{\substack{c:,l\in CINX(c)\ c\ {\rm active}}} \frac{1}{CSIZE(c)} . $$

The corresponding normalized score can be defined by replacing (65) with

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

The extra $1$ prevents a zero denominator. If neither $l$ nor $\bar l$ occurs in an active clause, then $h(l)=h(\bar l)=0$ and hence

$$ h'(l)=0 . $$

This choice is preferable to assigning an artificial large value, because a variable that has disappeared from the remaining formula gives no information for the branch decision.

The branch decision in step L3 can then use the same rule as before, choosing a literal for which both $h'(l)$ and $h'(\bar l)$ are large, but with these new scores computed from arbitrary clause lengths.

For a ternary formula in which every active clause has $CSIZE(c)=3$, the new definition gives

$$ h(l)=\frac{1}{3}#{c:l\in CINX(c)}. $$

The constant factor $1/3$ is common to every literal and therefore does not affect the relative ordering of literals in step L3. Hence the new heuristic reduces to the same ordering principle as the original ternary-clause heuristic.

For clauses of different lengths, the new definition gives a stronger preference to literals occurring in short clauses. A literal occurring in a unit clause contributes $1$, while a literal occurring in a clause of length $k$ contributes only $1/k$. Therefore the heuristic preserves the behavior required by unit propagation and short-clause reasoning while extending naturally to the KINX and CINX representation of exercise 143.

Thus a simple replacement for (64) and (65) is to use the weighted clause count above, with clause weights determined by the current values of $CSIZE(c)$:

$$ \boxed{ h(l)=\sum_{\substack{c:,l\in CINX(c)\ c\ {\rm active}}} \frac{1}{CSIZE(c)}, \qquad h'(l)=\frac{h(l)}{h(l)+h(\bar l)+1} } $$