One model is to use one variable for each vertex, whose value is the color that is assigned to the vertex. The following program encodes this model. The predicate `color(NV,NC)` colors a graph with `NV` vertices and `NC` colors. It is assumed that the vertices are numbered from 1 to `NV`, the colors are numbered from 1 to `NC`, and the edges are given as a predicate named `edge/2`,

color(NV,NC):- new_array(A,[NV]), term_variables(A,Vars), Vars :: 1..NC, foreach(I in 1..NV-1, J in I+1..NV, ((edge(I,J);edge(J,I)) -> A[I] $\= A[J] ; true) ), sat_solve(Vars), writeln(Vars).

Another model is to use `NC` Boolean variables for each vertex, where each variable corresponds to a color. The following program encodes this model. The first `foreach` loop ensures that, for each vertex, only one of its Boolean variables can take the value 1. The next `foreach` loop ensures that no two adjacent vertices can have the same color. The formula

$\ A[I,K] $\/ $\ A[J,K]ensures that the color

color(NV,NC):- new_array(A,[NV,NC]), term_variables(A,Vars), Vars :: [0,1], foreach(I in 1..NV, sum([A[I,K] : K in 1..NC]) $= 1 ), foreach(I in 1..NV-1, J in I+1..NV, ((edge(I,J);edge(J,I)) -> foreach(K in 1..NC, $\ A[I,K] $\/ $\ A[J,K]); true) ), sat_solve(Vars), writeln(A).

Neng-Fa Zhou 2013-01-25