minizinc - 类似 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);

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