Searching for Monochromatic-Square-Free Ramsey Grid Colorings via SAT Solvers

Monochromatic-square-free Ramsey grid coloring is a challenging problem to solve computationally. It relates to Ramsey-theoretic combinatorics and multiple party communication protocol complexity. Recently, using a parallel search algorithm on cluster based super computers, a 2-color 14×14 solution was found in 2.5 hours. In this paper, we report on another approach to solve the monochromatic-square-free Ramsey grid coloring problem. The approach first reduces monochromatic-square-free Ramsey grid coloring to satisfiability, and then applies an existing SAT solver to solve it. Using a SAT solver on a sequential machine, we found another 2-color 14×14 solution in about two seconds, which is more than four thousand times faster that the parallel algorithm using 288 cores. We also showed that no 2-color 15×15 solution exists, which answered the open question whether a 15×15 grid graph was monochromatic-square-free 2-colorable or not.