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.)
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: