类似 MiniZinc 约束之间的差异

Question

在斑马拼图 (http://rosettacode.org/wiki/Zebra_puzzle#MiniZinc) 的解决方案中，有一个限制说明其中一只宠物必须是斑马：

var 1..5: n;
constraint Gz[n]=Zebra;

下面的表达有不同的意思吗？他们产生不同的结果。

constraint exists(n in 1..5)(Gz[n]=Zebra);

Answer 1

如果删除了声明var 1..5: n，那么output部分就没有可以使用的全局n，这会产生错误：MiniZinc: type error: undefined identifier n'`.

如果你保留 var 1..5: n 那么 exists 循环中的变量 n 对全局定义的变量 n 没有任何影响，结果是（全局）n 将取值 1..5 中的任何一个（如果打印所有解决方案，则会显示）。

Answer 2

这些约束确实是等价的。然而，MiniZinc 为求解器转换这些约束的方式有所不同。

第一个选项将被翻译为元素约束：

var 1..5: n;
constraint array_int_element(n, Gz, Zebra);

而第二个会导致大子句约束：

constraint bool_clause([Gz[1]=Zebra, Gz[2]=Zebra, Gz[3]=Zebra, Gz[3]=Zebra, Gz[5]=Zebra], [])

虽然约束是等效的，但它可能取决于求解器在求解过程中哪种形式更有效。

更好的方法是使用全局 count_leq(array [int] of var int: x, int: y, int: c)，它强制 c 小于或等于 y 在 x 中出现的次数。表示约束为：

include "count_leq.mzn";
constraint count_leq(Gz, Zebra, 1);

直接传达约束的含义并允许求解器使用最适合其求解机制的约束形式

Difference between similar MiniZinc constraints