无法理解 clingo 中的基数约束

Question

我在 Clingo 中定义了图形着色问题：

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

我有这样的解决方案：

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

我无法理解代码生成部分中的 = 1 是什么意思。我知道它是 "set cardinality"，但我不明白怎么做，因为代码必须在每个答案中生成七个节点。此外，以下生成器（生成一组长度为 7 的节点和颜色选择的所有组合）需要 = 7:

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

这是我正在解决的图形着色问题的图片：https://imgur.com/a/tX7qtkJ

和 clingo：https://potassco.org/clingo/run/

Answer 1

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

这意味着 "choose exactly one color for each node"。或者，更准确地说，对于每个节点 n，选择一种颜色 c，使 assign(n, c) 变为真。

为了更好地理解这一点，我们需要深入研究 ASP 的语义。这里 N 出现在基数约束之外，因此可以查看作为此规则中的 "global variable"。该规则本质上是一个 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).

现在，这个集合 {assign(sa,C) : color(C)} 只是一个 shorthand {assign(sa,r), assign(sa,g), assign(sa,b)}。现在，{assign(sa,r), assign(sa,g), assign(sa,b)}=1 粗略地说意味着从集合 {assign(sa,r), assign(sa,g), assign(sa,b)}.

中选择一个元素

如果你看一下 clingo 手册，一般的语法是 {assign(sa,r), assign(sa,g), assign(sa,b)} rel EXPR，其中 rel 是一个算术关系，EXPR 是一些表达式。

无法理解 clingo 中的基数约束

Cannot understand cardinality constraint in clingo

constraints

cardinality

answer-set-programming

clingo