Tags:Chromatic Number of the Plane, Graph Coloring and SAT Solving
Abstract:
Satisfiability (SAT) solving has become an important technology in computer-aided mathematics with various successes in number and graph theory. In this paper we apply SAT solvers to color infinitely long strips in the plane with a given height and number of colors. The coloring is constrained as follows: two points that are exactly unit distance apart must be colored differently. To finitize the problem, we tile the strips and all points on a tile have the same color. We evaluated our approach using two different tile shapes: squares and hexagons. We were able to increase the lower bound for the strip height with 5 colors. The visualization of strips using 3 to 6 colors reveal patterns that are similar to the best known lower bounds.