constraints - 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 和其他求解器报告说这不能令人满意。

我在看什么？

score 2 · Accepted Answer

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

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

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

constraint bool_eq(false,true);
solve  satisfy;

这就是为什么 FlatZinc 求解器会产生 UNSATISFIABLE 的原因。

有趣的是，以下模型使用临时决策变量有效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：

变量 0..9：T = A_1_1；

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

constraint A_3_1 + A_2_1 + A_1_1 = 2 * A_1_1;

score -1 · Accepted Answer

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

2 回答 2