TAOCP 7.2.2.2 Exercise 17

Let $M_n$ be McGregor's graph of order $n$.

taocpmathematicsalgorithmsvolume-4hard

Section 7.2.2.2: Satisfiability

Exercise 17. [26] [26] Let $f(n)$ and $g(n)$ be the smallest and largest values of $r$ such that McGregor's graph of order $n$ can be $4$-colored, and such that each color appears exactly $r$ times. Use a SAT solver to find as many values of $f(n)$ and $g(n)$ as you can.

Verified: no
Solve time: 2m34s

Solution

Let $M_n$ be McGregor's graph of order $n$. The exercise asks for the extremal values of $r$ such that $M_n$ has a proper $4$-coloring in which every color class has exactly $r$ vertices. Thus

$$ f(n)=\min{r:\ M_n\text{ has a proper }4\text{-coloring with four classes of size }r}, $$

and

$$ g(n)=\max{r:\ M_n\text{ has a proper }4\text{-coloring with four classes of size }r}. $$

A necessary condition for such a coloring is

$$ |V(M_n)|=4r. $$

This follows because the four color classes form a partition of the vertex set and each class has cardinality $r$. It is not a definition of the order of the graph, nor does it imply that every value of $r$ satisfying this equation is attainable. For a fixed graph $M_n$, there is at most one possible value of $r$, namely

$$ r=\frac{|V(M_n)|}{4}, $$

unless the notation $M_n$ refers to a family whose order has not yet been specified. Therefore the first computational step is to determine the order of each graph being tested and discard any graph whose number of vertices is not divisible by $4$.

For a graph with $N=|V(M_n)|$ vertices, a SAT formulation can be used to decide whether the balanced coloring exists. Introduce Boolean variables

$$ x_{v,c} $$

for every vertex $v\in V(M_n)$ and every color $c\in{1,2,3,4}$, where $x_{v,c}$ means that vertex $v$ receives color $c$.

The coloring constraints are as follows.

Every vertex must receive at least one color:

$$ (x_{v,1}\vee x_{v,2}\vee x_{v,3}\vee x_{v,4}) $$

for every $v\in V(M_n)$.

Every vertex receives at most one color:

$$ (\neg x_{v,c}\vee \neg x_{v,d}) $$

for every $v\in V(M_n)$ and all distinct $c,d\in{1,2,3,4}$.

Adjacent vertices must have different colors:

$$ (\neg x_{u,c}\vee \neg x_{v,c}) $$

for every edge ${u,v}$ of $M_n$ and every color $c\in{1,2,3,4}$.

Finally, the four color classes must all have size $r$. For each color $c$, add the cardinality constraint

$$ \sum_{v\in V(M_n)}x_{v,c}=r . $$

These exact cardinality constraints may be converted into CNF by a standard SAT encoding such as a sequential counter, totalizer, or sorting network.

The SAT instance is satisfiable exactly when a balanced $4$-coloring with four color classes of size $r$ exists. A satisfying assignment gives the required coloring. An unsatisfiable result proves that no such coloring exists for that value of $r$.

For each graph $M_n$, the computation is therefore:

  1. Construct $M_n$ and determine $N=|V(M_n)|$.
  2. If $4\nmid N$, then no integer $r$ can satisfy the required condition.
  3. Otherwise set

$$ r=\frac{N}{4}. $$

  1. Construct the SAT instance above and run a SAT solver.
  2. If the instance is satisfiable, then

$$ f(n)=g(n)=\frac{N}{4}. $$

  1. If the instance is unsatisfiable, then neither $f(n)$ nor $g(n)$ exists for that graph.

The encoding determines the decision problem, but it does not determine numerical values of $f(n)$ and $g(n)$. Those values require actual SAT solver executions on the corresponding McGregor graphs. A verified computational table must therefore contain, for each tested $n$, the graph order, the resulting candidate value of $r$, and the solver outcome together with enough information to reproduce the computation, such as the graph construction, generated SAT instances, solver version, and output.

No numerical values of $f(n)$ or $g(n)$ can be stated without those SAT runs. Any table of values not obtained from an actual computation would be unsupported.