
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.
Abstract:This paper introduces a methodology that can be applied to solve graph edgecoloring 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 wellstudied 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 overapproximation of the set of degree matrices of all solutions of the graph coloring problem. % Then, for each degree matrix in the overapproximation, 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: eprint from arXiv.org Michael Codish The Department of Computer Science BenGurion University of the Negev PoB 653, BeerSheva, 84105, Israel mcodish@cs.bgu.ac.il
