set V; # nodes
param q default card(V); # number of colors to try
# we definitely won't need more colors than there are vertices
set C = 1..q; # set of potential colors
set E within V cross V; # edges
var x {V cross C} binary;
# x[v,c] = 1 if vertex v is colored using color c, and x[v,c] = 0 otherwise
var y {C} <= 1;
# encodes whether color c i used (1 = used)
# x binary => y binary, so we don't need to declare that here
# <= 1 is important with the current variant of the Conflict constraints,
# as otherwise y[c] >= 2 nullifies this condition for color c.
# objective function: minimize the number of colors used
minimize NumOfUsedCols:
sum {c in C} y[c];
# each vertex has exactly one color
s.t. AssignColor {v in V}:
sum {c in C} x[v,c] = 1;
# adjacent vertices must not have the same color
s.t. Conflict {(u,v) in E, c in C}:
x[u,c] + x[v,c] <= y[c];
# we can use y[c] as the right-hand side, since
# y[c] = 0 indeed implies x[u,c] = 0 = x[v,c]
# and y[c] = 1 gives the Conflict constraint from the our coloring model
# if vertex v has color c, then color c is used
s.t. SetIndicator {v in V, c in C}:
x[v,c] <= y[c];
# we can safely require that no node is colored by a color number
# greater than the number of v (formulation requires v and c to be numbers).
# This constraint removes symmetric solutions and thus reduces
# the search space for the solution algorithm.
s.t. EnforceColNum {v in V, c in C: v < c}:
x[v,c] = 0;