Computing Small Unit-Distance Graphs with Chromatic Number 5

Abstract

We present a new method for reducing the size of graphs with a given property. Our method, which is based on clausal proof minimization, allowed us to compute several 553-vertex unit-distance graphs with chromatic number 5, while the smallest published unit-distance graph with chromatic number 5 has 1581 vertices. The latter graph was constructed by Aubrey de Grey to show that the chromatic number of the plane is at least 5. The lack of a 4-coloring of our graphs is due to a clear pattern enforced on some vertices. Also, our graphs can be mechanically validated in a second, which suggests that the pattern is based on a reasonably short argument.

To appear in Geombinatorics XXVIII(1) in July-2018, a special issue dedicated to 5-chromatic unit-distance graphs

References in corpus (1)

• Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

Cited by in corpus (6)

• Constructing 5-chromatic unit distance graphs embedded in the Euclidean plane and two-dimensional spheres
• Graph minimization, focusing on the example of 5-chromatic unit-distance graphs in the plane
• The chromatic number of the Minkowski plane -- the regular polygon case
• A $6$-chromatic two-distance graph in the plane
• On the support of a non-autocorrelated function on a hyperbolic surface
• Small unit-distance graphs in the plane