Search code examples
constraintscardinalityanswer-set-programmingclingo

Cannot understand cardinality constraint in clingo

I have the graph coloring problem defined in Clingo as so:

node(sa;wa;nt;q;nsw;v;t).
color(r;g;b).

edge(sa,(wa;nt;q;nsw;v)).
edge(wa,nt). edge(nt,q). edge(q,nsw). edge(nsw,v).
edge(X,Y) :- edge(Y,X).

and I have the solution characterized like this:

{assign(N,C) : color(C)} = 1 :- node(N).
:- edge(X,Y), assign(X,C1), assign(Y,C2), C1 == C2.
#show assign/2.

I cannot understand what the = 1 in the generate portion of the code means. I know that it is "set cardinality", but I do not understand how, as the code must generate seven nodes in each answer. Additionally, the following generator (which generates all combos of nodes and colors choosing in a set of length 7) requires an = 7:

{assign(N,C) : color(C), node(N)} = 7.

Here is a picture of the graph coloring problem I am solving: https://i.sstatic.net/5Sucr.jpg

and clingo: https://potassco.org/clingo/run/

Solution 
  • {assign(N,C) : color(C)} = 1 :- node(N).

    This means "choose exactly one color for each node". Or, more precisely, for each node n, pick one color c such that assign(n, c) becomes true.

    To understand this better, we need to dig into the semantics of ASP. Here N occurs outside of the cardinality constraint, so it can be viewed as a "global variable" in this rule. The rule is essentially a shorthand for:

     {assign(sa,C) : color(C)} = 1 :- node(sa).
 {assign(wa,C) : color(C)} = 1 :- node(wa).
 {assign(nt,C) : color(C)} = 1 :- node(nt).
 {assign(q,C) : color(C)} = 1 :- node(q).
 {assign(nsw,C) : color(C)} = 1 :- node(nsw).
 {assign(v,C) : color(C)} = 1 :- node(v).
 {assign(t,C) : color(C)} = 1 :- node(t).

    Now, this set {assign(sa,C) : color(C)} is just a shorthand for {assign(sa,r), assign(sa,g), assign(sa,b)}. Now, {assign(sa,r), assign(sa,g), assign(sa,b)}=1 roughly speaking means pick one element from the set {assign(sa,r), assign(sa,g), assign(sa,b)}.

    If you look at clingo manual, the general syntax is {assign(sa,r), assign(sa,g), assign(sa,b)} rel EXPR, where rel is an arithmetic relation and EXPR is some expression.