Graph coloring

Given an undirected graph G=(V,E), where V is a set of vertices, and E is a set of edges, and given a set of colors, the goal of the graph coloring problem is to assign a color to each vertex in V, such that no two adjacent vertices share the same color.

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 K cannot be assigned to both vertex I and vertex J.

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).