# How to check this now famous graph has chromatic number 5?

Just read this paper from Aubrey de Grey, who used Mathematica to find a unit distance graph of chromatic number 5.

Here's the graph he discovered:

g = CloudGet@"https://www.wolframcloud.com/objects/d44eaba1-37f3-4f82-8d27-a547da117f8d";


How can we check this graph does indeed have chromatic number 5?

• I implemented a basic minimum colouring function for IGraph/M (will be in the next version due in 1-2 weeks) based on SatisfiabilityInstances. With this approach, checking 4-colourability of this particular graph is already too slow. I just wanted to mention this in case someone tries things in the same direction (SatisfiableQ, etc.). – Szabolcs Apr 19 '18 at 16:01
• There was a post about this on W|C too: community.wolfram.com/groups/-/m/t/1320004 – Szabolcs Apr 19 '18 at 16:31
• (For 5-colouring, the IGraph/M implementation manages fine and quickly. The problem is with proving that a 4-colouring does not exist, which is extremely slow.) – Szabolcs Apr 20 '18 at 13:41
• With the symmetry breaking heuristic described in the same paper, the timing comes down to 3-4 seconds. Will update when I get the time. – Szabolcs Apr 20 '18 at 16:19

Update: With IGraph/M 0.3.98 and later, you can now simply use

IGChromaticNumber[g]


or use

IGMinimumVertexColoring[g] // Timing
(* {14.6513, ...} *)


to find a minimum colouring.

IGMinimumVertexColoring transforms the colouring problem into Boolean satisfiability, and has an option to force a distinct set of colours onto a set of vertices. Usually one would pass a clique, as the colours of a clique must be all distinct. Doing this can significantly speed up the function (in particular the part that verifies that the graph is not $\chi-1$-colourable). However, the SAT solver's performance seems to also depend on the ordering of clauses.

For this graph, the default heuristic finds the clique {2, 1, 7}, and imposes distinct colours on it. But giving the vertices of the clique in a different order (and thus imposing different colours on its vertices) results in different performance.

IGMinimumVertexColoring[g, "ForcedColoring" -> {1, 2, 7}]; // Timing
(* {3.89746, Null} *)


Thus, if you have hard colouring problems, it is worth experimenting with passing different constraints throught he "ForcedColoring" option.

If anyone here can see some pattern in which constraints give generally the best performance, please let me know.

I have recently implemented minimum vertex colouring for IGraph/M. It is based on encoding the $k$-colouring problem into a satisfiability one and using SatisfiabilityInstances. This is based on the suggestions of user @Juho. The current implementation uses the "Traditional" encoding described e.g. in https://doi.org/10.1016/j.dam.2006.07.016

The version of IGraph/M that includes this function is not yet released, but if you want to play with it, you can contact me privately. Alternatively, you can look at the implementation of IGKVertexColoring here:

https://github.com/szhorvat/IGraphM/blob/master/IGraphM/IGraphM.m#L4369

Simply replace IGIndexEdgeList[g] with List @@@ EdgeList@IndexGraph[g] to make it work without the rest of the package.

With this function, finding a 5-colouring of this graph is easy:

sol = IGKVertexColoring[g, 5]; // Timing
(* {0.116768, Null} *)

Graph[g, GraphStyle -> "BasicBlack",
EdgeStyle -> Opacity[0.1],
VertexStyle -> Thread[VertexList[g] -> ColorData[97] /@ First[sol]],
ImageSize -> Large, VertexSize -> {"Scaled", 0.01}]


However, proving that the chromatic number is 5 requires showing that there is no 4-colouring. This is possible, but not at all fast.

sol = IGKVertexColoring[g, 4]; // Timing
(* {1726.04, Null} *)

sol
(* {} *)


As an experiment, I tried the same with the glucose 4.0 SAT solver, and it took 470 seconds—faster, but not dramatically so.

Suggestions for improving on these functions are most welcome.

Update:

I just updated the implementation in IGraph/M by implementing a heuristic similar to those described in the section "Breaking symmetry" of the mentioned paper. This means that the GitHub link above now points to a more complex implementation. But the performance is much better:

Max@IGMinimumVertexColoring[g] // Timing
(* {3.96151, 5} *)


Verifying the chromatic number takes only 4 seconds now.

• Do I understand correctly that using the updateIGraphM[]  install script also installs the needed igraph files? Or do I separately need to install some version of igraph? And if the latter, which? At igraph.org I find R/igraph, C/igraph, and python-igraph; and for macOS, which I'm using, I also find a MacPorts port called simply igraph. – murray Apr 20 '18 at 18:28
• @murray You do not need to download anything from igraph.org. Everything is in the IGraph/M paclet. However, the current version does not include the minimum vertex colouring functionality. If you are interested in playing with this, drop me an email and I'll send you a work-in-progress version. – Szabolcs Apr 20 '18 at 19:36