Another look at graph coloring via propositional satisfiability

This paper studies the solution of graph coloring problems by encoding into propositional satisfiability problems. The study covers three kinds of satisfiability solvers, based on postorder reasoning (e.g., grasp, chaff), preorder reasoning (e.g., 2cl, 2clsEq), and back-chaining (modoc). The study evaluates three encodings, one of them believed to be new. Some new symmetry-breaking methods, specific to coloring, are used to reduce the redundancy of solutions. A by-product of this research is an implemented lower-bound technique that has shown improved lower bounds for the chromatic numbers of the long-standing unsolved random graphs known as DSJC125.5 and DSJC125.9. Independent-set analysis shows that the chromatic numbers of DSJC125.5 and DSJC125.9 are at least 18 and 40, respectively, but satisfiability encoding was able to demonstrate only that the chromatic numbers are at least 13 and 38, respectively, within available time and space.