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

Michael Codish, Michael Frank, Avraham Itzhakov and Alice Miller   

Technical Report (unpublished); September 2014.


This paper introduces a methodology that can be applied to solve graph edge-coloring problems and in particular has been used 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 remained an open problem for more than 50 years. % The proposed technique is based on two well-studied concepts, mph{abstraction} and mph{symmetry}. First, we introduce an abstraction on graph colorings, mph{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 the approach via two applications: proving that $R(4,3,3)=30$ and computing the previously unknown number of $(3,3,3;13)$ Ramsey colorings (78{,}892).

Available:    bibtex entry

Related sites:   e-print from

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel

© copyright notice