TAOCP 7.2.2.2 Exercise 144

The statement is true.

Section 7.2.2.2: Satisfiability

Exercise 144. [15] [15] True or false: If $l$ doesn't appear in any clause, $h'(l) = 0.1$ in (65).

Verified: no
Solve time: 2m09s


Solution

The statement is true.

By equation (65), the refined heuristic value is

$$ h'(l)=0.1+\alpha\sum_{u\in \operatorname{BIMP}(l)}\frac{h(u)}{h_{\rm ave}} +\sum_{(u,v)\in \operatorname{TIMP}(l)} \frac{h(u)h(v)}{h_{\rm ave}^{2}}, $$

where the sums range over the binary and ternary implications associated with the literal $l$.

Suppose that $l$ does not appear in any clause. Then no binary clause can contain $l$ or require information from $l$, so

$$ \operatorname{BIMP}(l)=\varnothing . $$

Likewise, no ternary clause can contain $l$, so

$$ \operatorname{TIMP}(l)=\varnothing . $$

Both summations in (65) are therefore empty sums, and each contributes $0$. Hence

$$ h'(l)=0.1+\alpha\cdot 0+0=0.1 . $$

Therefore every literal absent from all clauses receives the default heuristic contribution in (65), and the assertion is true.

$$ \boxed{\text{True}} $$

This completes the proof.