Abstract
Graph coloring is a major component of numerous
allocation and scheduling problems.
We introduce a hybrid CP/SAT approach to graph
coloring based on exploring Zykov’s tree: for two
non-neighbors, either they take a different color
and there might as well be an edge between them,
or they take the same color and we might as well
merge them. Branching on whether two neighbors get the same color yields a symmetry-free tree
with complete graphs as leaves, which correspond
to colorings of the original graph.
We introduce a new lower bound for this problem
based on Mycielskian graphs; a method to produce
a clausal explanation of this bound for use in a
CDCL algorithm; and a branching heuristic emulating Brelaz on the Zykov tree.
The combination of these techniques in a branchand-bound search outperforms Dsatur and other
SAT-based approaches on standard benchmarks
both for finding upper bounds and for proving
lower bounds