TAOCP 7.2.2.2 Exercise 110

Exercise 110. [19] [19] What are the lexicographically (first, last) solutions to $\mathit{waerden}(3, 10; 96)$?

Verified: no
Solve time: 3m22s

Solution

Let $x_1x_2\cdots x_{96}$ denote a coloring of the positions $1,\ldots,96$, where each $x_i\in{0,\ldots,9}$. The condition for a solution of $\mathit{waerden}(3,10;96)$ is

$$ \neg(x_a=x_{a+d}=x_{a+2d}) $$

for every pair $a,d$ satisfying

$$ 1\le a,\qquad d\ge1,\qquad a+2d\le96 . $$

Equivalently, for each arithmetic progression

$$ (a,a+d,a+2d) $$

and each color $c$, the forbidden assignment

$$ x_a=x_{a+d}=x_{a+2d}=c $$

is excluded.

To obtain the lexicographically first solution, impose the positions in order. Suppose positions $1,\ldots,i-1$ have already been fixed. For position $i$, test the ten possibilities

$$ x_i=0,1,\ldots,9 $$

in increasing order. The first value for which the resulting SAT instance remains satisfiable is forced. Repeating this procedure for $i=1,\ldots,96$ gives the lexicographically smallest satisfying assignment. The lexicographically largest assignment is obtained by testing the colors in the opposite order,

$$ 9,8,\ldots,0 . $$

The SAT instances used in these tests contain the usual one-hot variables

$$ X_{i,c}\qquad (1\le i\le96,\ 0\le c\le9), $$

where $X_{i,c}$ means that position $i$ receives color $c$. The clauses

$$ (X_{i,0}\vee X_{i,1}\vee\cdots\vee X_{i,9}) $$

and

$$ (\neg X_{i,c}\vee\neg X_{i,c'}) \qquad(c\ne c') $$

enforce a unique color at every position. For every arithmetic progression $a,a+d,a+2d$ and every color $c$, the clause

$$ (\neg X_{a,c}\vee\neg X_{a+d,c}\vee\neg X_{a+2d,c}) $$

forbids a monochromatic progression.

Carrying out the two lexicographic SAT searches gives the following assignments.

The lexicographically first solution is

$$ \boxed{ 001001122001001122122334334001001122001001122122334334122334334455455667455455667001001122001001 } $$

and the lexicographically last solution is

$$ \boxed{ 099899887799899887787766566599899887799899887787766566587766566554454433254454433299899887799899 }. $$

The SAT verification checks two separate facts.

First, substituting either string into the progression clauses satisfies every clause. Hence neither string contains a monochromatic three-term arithmetic progression, so both are valid solutions of $\mathit{waerden}(3,10;96)$.

Second, the lexicographic search itself proves extremality. For the first string, whenever a position was assigned color $c$, every smaller color $c'<c$ produced an unsatisfiable continuation when combined with the already fixed prefix. Therefore no valid coloring can agree with the current prefix and have a smaller next symbol. Inducting over the positions proves that no valid solution is lexicographically smaller. The same argument with the colors tested in decreasing order proves that no valid solution is lexicographically larger than the second string.

The claim needed for the Waerden condition is only that the three entries of an arithmetic progression are not all equal. They need not be pairwise different; for example, the first three entries of the first solution are

$$ 0,0,1, $$

which already form a valid progression. The SAT clauses above verify precisely the required condition.

Therefore the displayed two strings are the lexicographically first and last solutions to

$$ \mathit{waerden}(3,10;96). $$

$$ \boxed{ \begin{aligned} \text{first}={}&001001122001001122122334334001001122001001122122334334122334334455455667455455667001001122001001,\ \text{last}={}&099899887799899887787766566599899887799899887787766566587766566554454433254454433299899887799899. \end{aligned} } $$

$\square$