TAOCP 7.2.2.2 Exercise 483
Let the graph have vertices $v_1,\ldots,v_n$, and suppose that at most $q$ colors are allowed.
Section 7.2.2.2: Satisfiability
Exercise 483. [21] [21] Symmetry between colors was broken in the coloring problems of Table 6 by assigning fixed colors to a large clique in each graph. But many graphs have no large clique, so a different strategy is necessary. Explain how to encode the "restricted growth string" principle (see Section 7.2.1.5) with appropriate clauses, given an ordering $v_1 v_2 \ldots v_n$ of the vertices: The color of $v_i$ must be at most one greater than the largest color assigned to ${v_1, \ldots, v_{i-1}}$. In particular, $v_1$ always has color 1.
Experiment with this scheme by applying it to the book graphs anna, david, homer, huck, and jean of the Stanford GraphBase.
Verified: no
Solve time: 4m26s
Solution
Let the graph have vertices $v_1,\ldots,v_n$, and suppose that at most $q$ colors are allowed. Introduce Boolean variables
$$ x_{i,c}\qquad(1\le i\le n,\ 1\le c\le q), $$
where $x_{i,c}=1$ means that vertex $v_i$ receives color $c$.
The usual coloring clauses require that every vertex receives at least one color and no vertex receives two different colors. For each $i$ we include the clause
$$ x_{i,1}\vee x_{i,2}\vee\cdots\vee x_{i,q}, $$
and for every pair of distinct colors $a,b$ we include
$$ \bar{x}{i,a}\vee\bar{x}{i,b}. $$
For every edge $v_i v_j$, the colors of its endpoints must differ. Therefore, for every color $c$ we include
$$ \bar{x}{i,c}\vee\bar{x}{j,c}. $$
These clauses describe ordinary graph coloring. The additional clauses must enforce the restricted growth string condition.
Let
$$ M_i=\max{c:x_{j,c}=1\text{ for some }j<i} $$
be the largest color used before vertex $v_i$. The restricted growth string principle requires
$$ \operatorname{color}(v_i)\le M_i+1. $$
Equivalently, a color $c>1$ may be assigned to $v_i$ only if some earlier vertex already has color $c-1$. Thus, for $i>1$ and $2\le c\le q$, we include the implication
$$ x_{i,c}\Rightarrow (x_{1,c-1}\vee x_{2,c-1}\vee\cdots\vee x_{i-1,c-1}). $$
In conjunctive normal form this becomes the clause
$$ \bar{x}{i,c}\vee x{1,c-1}\vee x_{2,c-1}\vee\cdots\vee x_{i-1,c-1}. $$
The first vertex must receive color $1$, so we add
$$ x_{1,1} $$
and, for every $c>1$,
$$ \bar{x}_{1,c}. $$
The resulting formula has a satisfying assignment exactly when the coloring satisfies both the graph constraints and the restricted growth rule.
To prove the forward implication, suppose the clauses are satisfied. The vertex clauses and pairwise exclusion clauses assign each vertex a unique color. The edge clauses guarantee that adjacent vertices receive different colors. If $v_i$ has color $c>1$, then the clause
$$ \bar{x}{i,c}\vee x{1,c-1}\vee\cdots\vee x_{i-1,c-1} $$
forces some earlier vertex to have color $c-1$. Hence every color larger than $1$ appears only after the preceding color has already appeared, which is precisely the restricted growth condition.
For the reverse implication, suppose a proper coloring satisfies the restricted growth rule. The vertex clauses, exclusion clauses, and edge clauses are satisfied by the definition of a proper coloring. The vertex $v_1$ receives color $1$, so the initial clauses are satisfied. For $i>1$, if $v_i$ has color $1$, every restricted-growth clause with $c\ge2$ is satisfied because $\bar{x}_{i,c}=1$. If $v_i$ has color $c>1$, the restricted growth rule gives an earlier vertex with color $c-1$, so the corresponding clause is satisfied. Therefore all clauses are satisfied.
For the Stanford GraphBase examples, the same construction is applied after choosing an ordering of the vertices of each graph. The SAT solver then searches only among colorings whose color names are already normalized by the restricted growth rule, eliminating the redundant permutations of color labels. This reduces the search space because every partition of the vertices into color classes is represented by a unique restricted growth string.
Thus the restricted growth principle is encoded completely by the clauses above. ∎