TAOCP 7.2.2.2 Exercise 119

The formula $F=\mathit{warden}(3,3;9)$ is the van der Waerden formula forbidding monochromatic arithmetic progressions of length $3$ among the variables $x_1,\ldots,x_9$.

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 119. [18] [18] Let $F = \mathit{warden}(3,3;9)$ be the 32 clauses in (9). For which literal $l$ is the reduced formula $F|l$ smallest? Exhibit the resulting clauses.

Verified: no
Solve time: 2m

Solution

The formula $F=\mathit{warden}(3,3;9)$ is the van der Waerden formula forbidding monochromatic arithmetic progressions of length $3$ among the variables $x_1,\ldots,x_9$. The sixteen progressions are

$$ \begin{aligned} &123,135,147,159,234,246,258,345,\ &357,369,456,468,567,579,678,789 . \end{aligned} $$

For each progression $ijk$, the formula contains the two clauses

$$ (x_i\vee x_j\vee x_k),\qquad (\bar x_i\vee\bar x_j\vee\bar x_k). $$

We examine the effect of assigning a literal $l$. By symmetry, the literals $x_i$ and $\bar x_i$ give the same reduced formula size, since complementing all variables is a symmetry of $F$. Reflection $x_i\mapsto x_{10-i}$ is also a symmetry. Therefore it is enough to compare the cases $x_1,x_2,x_3,x_4,x_5$.

A direct reduction gives the following numbers of remaining clauses:

$$ \begin{array}{c|ccccc} l&x_1&x_2&x_3&x_4&x_5\ \hline |F|l|&28&28&26&26&24 \end{array} $$

The reflected cases give the same values:

$$ |F|x_i|=|F|x_{10-i}|. $$

Hence the smallest reduced formulas occur for the central literals

$$ l=x_5\quad\text{or}\quad l=\bar x_5 . $$

Consider $l=x_5$. Every clause containing $x_5$ disappears, and every clause containing $\bar x_5$ loses that literal. The resulting reduced formula is

$$ \begin{aligned} &(x_1\vee x_2\vee x_3) \wedge(\bar x_1\vee\bar x_2\vee\bar x_3)\ &\wedge(\bar x_1\vee\bar x_3) \wedge(x_1\vee x_4\vee x_7) \wedge(\bar x_1\vee\bar x_4\vee\bar x_7)\ &\wedge(\bar x_1\vee\bar x_9) \wedge(x_2\vee x_3\vee x_4) \wedge(\bar x_2\vee\bar x_3\vee\bar x_4)\ &\wedge(x_2\vee x_4\vee x_6) \wedge(\bar x_2\vee\bar x_4\vee\bar x_6) \wedge(\bar x_2\vee\bar x_8)\ &\wedge(\bar x_3\vee\bar x_4) \wedge(\bar x_3\vee\bar x_7) \wedge(x_3\vee x_6\vee x_9)\ &\wedge(\bar x_3\vee\bar x_6\vee\bar x_9) \wedge(\bar x_4\vee\bar x_6)\ &\wedge(x_4\vee x_6\vee x_8) \wedge(\bar x_4\vee\bar x_6\vee\bar x_8)\ &\wedge(\bar x_6\vee\bar x_7) \wedge(\bar x_7\vee\bar x_9) \wedge(x_6\vee x_7\vee x_8)\ &\wedge(\bar x_6\vee\bar x_7\vee\bar x_8) \wedge(x_7\vee x_8\vee x_9) \wedge(\bar x_7\vee\bar x_8\vee\bar x_9). \end{aligned} $$

There are $24$ clauses in this reduction. Since all possible literals are equivalent under the complement and reflection symmetries except for their distance from the center, and the complete comparison above gives the clause counts for the five possible positions, no other literal can produce fewer clauses.

Therefore the smallest reduced formula is obtained by assigning either

$$ \boxed{l=x_5\ \text{or}\ l=\bar x_5} $$

and its size is

$$ \boxed{24\text{ clauses}} . $$