Tags:graph coloring, maximum clique and satisfiability
Abstract:
We present an exact algorithm for graph coloring and maximum clique problems based on SAT technology. It relies on four sub-algorithms that alternatingly compute cliques of larger size and colorings with fewer colors. We show how these techniques can mutually help each other: larger cliques facilitate finding smaller colorings, which in turn can boost finding larger cliques. We evaluate our approach on the DIMACS graph coloring suite, and first show that our algorithm can improve the state-of-the-art MaxSAT-based solver IncMaxCLQ for finding maximum cliques. For the graph coloring problem, we close two open instances, decrease two upper bounds, and increase one lower bound.