In the April, 1975 issue of Scientific American, Martin
Gardner, in his column “Mathematical Games” published a list of
what he claimed were 6 major mathematical discoveries of 1974
that “for one reason or another were inadequately
reported to both the scientific community and the public at
large.”
One was a planar, 110-node graph, attributed to William McGregor of
Wappingers Falls, New York, that he asserted
could not be colored with less
than 5 colors, thereby disproving the as-yet unproven conjecture
that 4 colors were sufficient to color any planar graph. What
many readers did not appreciate was the month of publication of the issue.
More about the story can be found here.
Here is the graph, drawn as a map
Trying to encode possible coloring of this graph as a BDD is not
really feasible. I estimate it would take well over one billion
nodes (since a min-cut of the graph is 20 nodes wide, and the
BDD would need to exponentially encode almost all combinations
of the colors for these nodes.)
Graph Coloring as a SAT Problem
On the other hand, coloring the graph with a Boolean satisfiability
(SAT) solver is quite
feasible. The solver need only find one possible solution, and so
it does not face the daunting task of encoding all possible
colorings. Here is a coloring generated by the ZChaff
solver running in under one second on a laptop computer
Check out the following
Youtube video showing how this search proceeds:
It is also possible to force the solver to generate a "balanced"
coloring, by requiring it to find a solution using two colors
(green and blue) 27
times and two colors (red and yellow) 28 times.
SAT solvers can also be used to solve optimization problems, by
performing a series of calls to the solvers to do binary search
on the objective function. If we ask the solver to find a
coloring that first minimizes the number of nodes colored green,
then minimizes the number colored blue, and then red, we get a
coloring with just 7 green nodes, 34 blue and red ones, and 35 yellow.
Based on further experiments, we can state that, up to the assignment of
colors, this solution has unique properties:
It is the only coloring where one color is used at most 7 times.
It is the only coloring where one color is used at least 35 times.
