matrix are sorted lexicographically.

For an $n\times k$ degree matrix $M$ we denote by $lex(M)$ the smallest matrix with rows and columns in the lexicographic order (non-increasing) obtained by permuting rows and columns of $M$.

\[def:abs\] Let $A$ be a graph coloring on $n$ vertices with $k$ colors. The *abstraction* of $A$ to a degree matrix is $\alpha(A)=lex(dm(A))$. For a set ${{\cal A}}$ of graph colorings we denote $\alpha({{\cal A}}) = {\left\{~\alpha(A)  \left|
      \begin{array}{l}A\in{{\cal A}}\end{array}
    \right.     \right\}}$.

Note that if $A$ and $A'$ are weakly isomorphic, then $\alpha(A)=\alpha(A')$.

\[def:conc\] Let $M$ be an $n\times k$ degree matrix. Then, $\gamma(M) =
  {\left\{~A  \left|
      \begin{array}{l}\alpha(A)=M\end{array}
    \right.     \right\}}$ is the set of graph colorings represented by $M$. For a set ${{\cal M}}$ of degree matrices we denote $\gamma({{\cal M}}) = \cup{\left\{~\gamma(M)  \left|
      \begin{array}{l}M\in{{\cal M}}\end{array}
    \right.     \right\}}$.

Let $\varphi(A)$ be a graph coloring problem in $k$ colors on an $n\times n$ adjacency matrix, $A$. Our strategy to compute ${{\cal A}}=sol(\varphi(A))$ is to first compute an over-approximation ${{\cal M}}$ of degree matrices such that $\gamma({{\cal M}})\supseteq{{\cal A}}$ and to then use ${{\cal M}}$ to guide the computation of ${{\cal A}}$. We denote the set of solutions of the graph coloring problem, $\varphi(A)$, which have a 