Minizinc程序抱怨global_cardinality中的断言失败

Question

我在Minizinc试图解决这个问题，摘自Puzzle taken from Gardner：

十个单元格编号为0，...,9铭刻一个10位数字，以便每个单元格，例如i，表示数字i在这个数字中出现的总数。找到这个号码。答案是6210001000。

我解决了它，代码在Gecode中运行得很好：

int: n=9;
set of int: N=0..n;
array[N] of var N: cell;

include "globals.mzn";
constraint global_cardinality(cell, N, cell);
solve satisfy;

output [show(cell), "\n", show(index_set(cell)), " -- ", show(index_set(N))];

Gecode的输出：

[6, 2, 1, 0, 0, 0, 1, 0, 0, 0]
0..9 -- 1..10
----------
==========

然而，G12解决者抱怨global_cardinality中的断言失败：

在调用‘断言’断言失败: global_cardinality:盖和计数必须有相同的索引集

如Gecode的输出所示，N为1..10，单元格为0.9。所以我的问题是：

• 为什么Gecode在工作？不同的实现或我的程序是错误的，但我是幸运的？
• 如何修复程序以使用G12或使其健壮/正确？

Answer 1

问题是您在0上启动了数组。虽然这样做在技术上是正确的，但最好以1(MiniZinc中的标准)启动数组。正如您所看到的，仍然有一些求解器不完全支持数组，这些数组不是从1开始的，还有一些与使用数组有关的bug，这些错误不是从0开始的。

我在g12cpx上得到了与您相同的错误，但是将数组修改为

array[1..10] of var N: cell;

给了我正确的结果。

Answer 2

您可以通过添加array1d()来修复这个问题：

 global_cardinality(cell,array1d(0..n,[i | i in N]), cell);

Gecode工作而不是G12/fd的原因是Gecode对约束有自己的MiniZinc定义，其中不包括基数检查。