如何在 minizinc 中正确迭代约束中的二维数组？

Question

我想解决图表着色的问题。当一个图形应该用最少数量的颜色着色时，问题就是没有相邻顶点被着色为相同的颜色。 这是我的带有玩具图的代码。

int: N_Vertices=4;
int: N_Edges=3;
array[1..N_Edges, 1..2] of int: Adjacency;
Adjacency = [| 0, 1
             | 1, 2
             | 1, 3|];
array [1..N_Vertices] of var int: coloring;

constraint forall(e in 1..N_Edges)(coloring[Adjacency[e, 1]] != coloring[Adjacency[e, 2]]);
constraint forall(c in coloring)(c >= 0);

solve minimize (max(coloring));

但它给了

 WARNING: undefined result becomes false in Boolean context
  (array access out of bounds)
Playground:11:
  in call 'forall'
  in array comprehension expression
    with e = 1
  in binary '!=' operator expression
  in array access

  WARNING: model inconsistency detected
Playground:11:
  in call 'forall'
  in array comprehension expression
    with e = 1
  in binary '!=' operator expression
  in array access
=====UNSATISFIABLE=====

我想我在第一个约束中对 Adjacency 迭代做错了。应该怎么做呢？

Answer 1

问题在于Adjacency：这些值以 0 为基数，但 coloring 以 1 为基数 (array[1..N_Vertices])。 MiniZinc 默认使用 base 1 索引。

最简单的方法是将 Adjacency 中的索引改为以 1 为底：

Adjacency = [| 1, 2
             | 2, 3
             | 2, 4|];

那么解决办法是：

coloring = array1d(1..4, [1, 0, 1, 1]);
----------
==========

如果您想在Adjacency 中保留基数为0 的索引，则必须通过将1..N_Edges 替换为0..N_Edges-1 来进行一些其他调整：

int: N_Vertices=4;
int: N_Edges=3;
array[0..N_Edges-1, 1..2] of int: Adjacency;        

Adjacency = array2d(0..N_Edges-1,1..2,[| 0, 1
             | 1, 2
             | 1, 3|]);

array[0..N_Vertices-1] of var int: coloring;
constraint forall(e in 0..N_Edges-1)(coloring[Adjacency[e, 1]] != coloring[Adjacency[e, 2]]);
constraint forall(c in coloring)(c >= 0);

答案：

coloring = array1d(1..4, [1, 0, 1, 1]);

另外，我建议您给coloring 一个适当的域而不是var int，例如：

array[0..N_Vertices-1] of 0..4: coloring; % recommended
% ....
% Then this is not needed:
% constraint forall(c in coloring)(c >= 0);