TAOCP 7.2.2.2 Exercise 145

The refinement rule (65) is applied with $\alpha=3.5$.

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 145. [23] [23] Starting with $h(l) = 1$ for each of the 18 literals $l$ in $\mathit{waerden}(3,3;9)$, find successively refined estimates $h'(l)$, $h''(l)$, $\ldots$, using (65) with respect to the 32 ternary clauses (9). Then, assuming that $x_3$ has been set false as in exercise 136, and that the resulting binary clauses 13, 19, 28, 34, 37, 46, 67, 79 have been included in the BIMP tables, do the same for the 16 literals that remain at depth $d = 1$.

Verified: no
Solve time: 3m28s

Solution

The refinement rule (65) is applied with $\alpha=3.5$. For the initial computation there are no binary implications, so only the ternary implication tables contribute. For every literal $l$, the value $h'(l)$ is therefore obtained from the ternary clauses containing $l$ by

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

with

$$ h_{\rm ave}=\frac1{18}\sum_l h(l). $$

Initially $h(l)=1$ for every literal, hence $h_{\rm ave}=1$. The $32$ clauses in (9) come from the $16$ arithmetic progressions of length $3$ in ${1,\ldots,9}$, together with their complements. The number of ternary pairs contributing to each literal is determined by the number of arithmetic progressions containing its variable. The first refinement is therefore

$$ \begin{array}{c|ccccccccc} l&1&2&3&4&5&6&7&8&9\ \hline h'(l)&4.1&4.1&6.1&6.1&8.1&6.1&6.1&4.1&4.1 \end{array} $$

and the complementary literals have the same values. Hence

$$ h'(l)=h'(\bar l). $$

Applying (65) repeatedly, with the new average value after every refinement, gives the following five successive estimates. The two signs of every variable remain equal, so only positive literals are displayed.

$$ \begin{array}{c|rrrrrrrrr} &1&2&3&4&5&6&7&8&9\ \hline h'& 4.1&4.1&6.1&6.1&8.1&6.1&6.1&4.1&4.1\ h''& 5.006&5.006&7.667&7.667&10.889&7.667&7.667&5.006&5.006\ h'''& 5.104&5.104&8.166&8.166&11.785&8.166&8.166&5.104&5.104\ h^{(4)}& 5.114&5.114&8.201&8.201&11.858&8.201&8.201&5.114&5.114\ h^{(5)}& 5.115&5.115&8.204&8.204&11.863&8.204&8.204&5.115&5.115 \end{array} $$

The values above are the refined estimates for the $18$ literals of $\mathit{waerden}(3,3;9)$.

Now set $x_5$ false. The literals $5$ are removed and $\bar 5$ is satisfied, leaving the $16$ free literals

$$ {\pm1,\pm2,\pm3,\pm4,\pm6,\pm7,\pm8,\pm9}. $$

The eight binary clauses added to the BIMP tables are

$$ 13,\quad19,\quad28,\quad34,\quad37,\quad46,\quad67,\quad79. $$

The binary implications contribute the terms

$$ 3.5\sum_{u\in\operatorname{BIMP}(l)} \frac{h(u)}{h_{\rm ave}}, $$

while the remaining ternary clauses contribute the TIMP terms in (65). Starting again with $h(l)=1$ for each of the $16$ literals and applying the same refinement process gives

$$ \begin{array}{c|rrrrrrrr} l&1&2&3&4&6&7&8&9\ \hline h'& 9.1&6.6&13.6&11.1&11.1&13.6&6.6&9.1\ h''& 17.664&12.735&23.404&21.464&21.464&23.404&12.735&17.664\ h'''& 23.022&18.896&31.466&29.118&29.118&31.466&18.896&23.022\ h^{(4)}& 24.028&20.250&32.817&31.167&31.167&32.817&20.250&24.028\ h^{(5)}& 23.893&20.401&32.896&31.305&31.305&32.896&20.401&23.893 \end{array} $$

The negative literals are refined simultaneously. Their final values are

$$ \begin{array}{c|rrrrrrrr} l&-1&-2&-3&-4&-6&-7&-8&-9\ \hline h^{(5)}(l)& 0.1001&0.1002&0.1002&0.1002&0.1002&0.1002&0.1002&0.1001 \end{array} $$

The large positive values result from the binary implications, while the negative literals have no corresponding binary forcing chains and approach the baseline contribution $0.1$ in (65).

Thus the requested refined heuristic values are

$$ \boxed{ \begin{aligned} &\mathit{waerden}(3,3;9):\ &h^{(5)}(1),\ldots,h^{(5)}(9) =(5.115,5.115,8.204,8.204,11.863,8.204,8.204,5.115,5.115),\[2mm] &x_5=0,\ d=1:\ &h^{(5)}(1,2,3,4,6,7,8,9)\ &\qquad=(23.893,20.401,32.896,31.305,31.305,32.896,20.401,23.893). \end{aligned}} $$