by “time” indicate the time (in seconds) to find all colorings iterating with a SAT solver. The timeout assumed here is 24 hours. The column headed by “\#” specifies the number of colorings found by iterated SAT solving.

In the first four rows, notice the impact of symmetry breaking which reduces the number of solutions by 1–3 orders of magnitude. In the next three rows the reduction is more acute. Without symmetry breaking the colorings cannot be computed within the 24 hour timeout. The sets of colorings obtained with symmetry breaking have been verified to reduce, using `nauty` [@nauty], to the known number of colorings modulo weak isomorphism indicated in the second column.

Abstraction: Degree Matrices for Graph Colorings {#sec:abs}
================================================

This section introduces an abstraction on graph colorings defined in terms of *degree matrices*. The motivation is to solve a hard graph coloring problem by first searching for its degree matrices. Degree matrices are to graph coloring problems as degree sequences [@ErdosGallai1960] are to graph search problems. A degree sequence is a monotonic nonincreasing sequence of the vertex degrees of a graph. A graphic sequence is a sequence which can be the degree sequence of some graph.

The idea 