Minizinc：平凡的平等无法满足

Question

我有以下 minizinc 模型：

include "globals.mzn";
var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
constraint (A_3_1+A_2_1+A_1_1) = A_1_1;
solve satisfy;

模型应具有平凡解 0=A_1_1=A_2_1=A_3_1。但是，Gecode 和其他求解器将此报告为无法满足。

我忽略了什么？

Answer 1

这似乎是 MiniZinc 将模型转换为 FlatZinc 格式时的错误。给出的消息来自 MiniZinc：

WARNING: model inconsistency detected
test66.mzn:6:
in binary '=' operator expression

生成的 FlatZinc 文件仅包含以下内容：

constraint bool_eq(false,true);
solve  satisfy;

这就是 FlatZinc 求解器产生不满足的原因。

有趣的是，以下模型有效，使用临时决策变量，T:

var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
var 0..9: T;

constraint
    T = A_3_1 + A_2_1 + A_1_1 /\
    T = A_1_1
; 
solve satisfy;

模型然后产生所有 10 个解决方案，A_1_1 被分配了 0 到 9 的值，A_2_1 = A_3_1 = 0，T 被分配给相同的值值为 A_1_1。

但是，如果 T 是用 A_1_1 初始化的，那么会再次抛出 UNSAT：

var 0..9: T = A_1_1;

更新：可以注意到以下约束有效，即右侧的 2 * A_1_1：

constraint A_3_1 + A_2_1 + A_1_1 = 2 * A_1_1;

Answer 2

您的约束似乎试图使用赋值运算符，但该操作可能无效。您可以尝试 a = b+ c 但 b+c=a 可能不允许。或者，您可以尝试使用相等 == 运算符来定义应该起作用的约束。我没有安装程序来验证，但希望它能让您更深入地了解这个问题。如果也有错误，我不会感到惊讶，我很想知道。

Minizinc: Trivial equality unsatisfiable