given degree matrix, $M$, by $sol_M(\varphi(A))$. Then $$\begin{aligned}
\label{eq:approx}   
       sol(\varphi(A)) &=&  \bigcup_{M\in{{\cal M}}} sol_M(\varphi(A))\\
\label{eq:solM}
    sol_M(\varphi(A)) & = & sol(\varphi(A)\wedge\alpha(A){=}M)\end{aligned}$$ Equation (\[eq:approx\]) implies that, we can compute the solutions to a graph coloring problem $\varphi(A)$ by computing the independent sets $sol_M(\varphi(A))$ for any over approximation ${{\cal M}}$ of the degree matrices of the solutions of $\varphi(A)$. This facilitates the computation for two reasons: (1) The problem is now broken into a set of independent sub-problems for each $M\in{{\cal M}}$ which can be solved in parallel, and (2) The computation of each individual $sol_M(\varphi(A))$ is now directed using $M$.

The constraint $\alpha(A){=}M$ in the right side of Equation (\[eq:solM\]) is encoded to SAT by introducing (encodings of) cardinality constraints. For each row of the matrix $A$ the corresponding row in $M$ specifies the number of elements with value $c$ (for $1\leq c\leq k$) that must be in that row. We omit the precise details of the encoding to CNF. In our implementation this is performed by the finite domain constraint compiler  and details can be found in [@jair2013].

When computing $sol_M(\varphi(A))$ for a given degree matrix we can no longer apply the symmetry breaking Constraint (\[eq:symbreak\]) as it might constrain the 