Solving Graph Coloring Problems with Abstraction and Symmetry: the Ramsey Number R(4,3,3)=30

This paper introduces a methodology that applies to solve graph edge-coloring problems and in particular to prove that the Ramsey number $R(4,3,3)=30$. The number $R(4,3,3)$ is often presented as the unknown Ramsey number with the best chances of being found "soon". Yet, it has been sought after for more than 50 years. The proposed technique is based on two well-studied concepts, \emph{abstraction} and \emph{symmetry}. First, we introduce an abstraction on graph colorings, \emph{degree matrices}, that specify the degree of each vertex in each color. We compute, using a SAT solver, an over-approximation of the set of degree matrices of all solutions of the graph coloring problem. Then, for each degree matrix in the over-approximation, we compute, again using a SAT solver, the set of all solutions with matching degrees. Breaking symmetries, on degree matrices in the first step and with respect to graph isomorphism in the second, is cardinal to the success of the approach. We illustrate two applications: to prove that $R(4,3,3)=30$ and to compute the, previously unknown number, 78{,}892, of $(3,3,3;13)$ Ramsey colorings.