类似的 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

这些约束确实是等价的。但是，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小于或等于x中y的发生次数。将约束表示为：

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

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

Answer 2

如果声明var 1..5: n被删除，则没有可以在output部分中使用的全局n，这将产生错误：MiniZinc: type error: undefined identifiern''。

如果您保持var 1..5: n那么exists循环中的变量n对全局定义的变量n没有任何影响，结果(全局(n将采用任何值 1..5(如果打印所有解决方案，则会显示(。