类似 MiniZinc 约束之间的区别答案

【问题标题】：Difference between similar MiniZinc constraints类似 MiniZinc 约束之间的区别
【发布时间】：2020-07-04 17:58:58
【问题描述】：

在斑马谜题 (http://rosettacode.org/wiki/Zebra_puzzle#MiniZinc) 的解决方案中，有一个约束条件是其中一只宠物必须是斑马：

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

下面的表达式有不同的含义吗？它们产生不同的结果。

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

【问题讨论】：

标签： minizinc

【解决方案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 小于或等于y 在x 中的出现次数。将约束表示为：

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

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

【讨论】：

感谢您的回答。我仍在研究为什么第二版约束会产生不同的结果。 hakank 的回答似乎对此有所启发。
@AttilaKaroly，它们可能会导致不同的答案，因为有多个答案，因为可能有多个答案。当求解器获得不同（等效）模型时，它可能不会以相同的顺序给出解决方案，因为它的搜索决策可能不会以相同的顺序。查看所有解决方案 (-a) 时，解决方案应该是相同的。
在 IDE 中将“用户定义的行为/在这么多解决方案后停止”的值设置为零与使用 -a 选项相同吗？令人惊讶的是，我用上述设置得到了 5 种不同的解决方案。
是的，这将导致相同的行为

【解决方案2】：

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

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

【讨论】：

当从模型中删除n时，仍然可以使用[i | i in index_set(Gz) where fix(Gz[i]) = Zebra][1]之类的方法在输出模型中找到n的值
@Dekker1 好点。然后就不需要原来的约束或存在的变体了。
感谢您非常有用的回答，hakank。似乎n 的使用是在使用Gz[n]=Zebra 约束的第二版时打印出不同的输出。