Minizinc：if-then-else 语句中的数组赋值问题

Question

var 1..5: k=1;
array[1..2] of var 1..48: key2;
constraint forall(i in 1..4,j in 1..48 where k= ceil(j/24))(if 
                 table[i,j]!=0 then key2[k]=j else true endif);

我试图在我的 minizinc 中应用这个约束 program.Objective 是为了最大化成本函数，这是约束之一但是当我运行这段代码显示

Finished in 203msec
Compiling first.mzn with data empdata2.dzn
Running first.mzn
=====UNSATISFIABLE=====
Finished in 189msec

如果我将 key2[k]=j 替换为 true，那么它会编译并且运行没有任何错误。我在 program.I 中的其他任何地方都没有使用 key2 数组，我正在使用数据文件提供输入，并且我已将 key2 数组初始化为 key2=[1,1]。我是 minizinc 的初学者，我不明白为什么在这种情况下将数字分配给数组会出现问题？

Answer 1

我运行以下模型，它为 Gecode 和 G12fd 求解器提供了很多解决方案（使用 "solve satisfy"）。您使用哪个 MiniZinc 版本？我使用最新的 Git 版本 MiniZinc 2.0，它与 v2.0.2 大致相同。

var 1..5: k=1;
array[1..2] of var 1..48: key2;
array[1..4,1..48] of var 0..1: table;

solve satisfy;

constraint forall(i in 1..4,j in 1..48 where k= ceil(j/24))(if 
              table[i,j]!=0 then key2[k]=j else true endif);

output [
    "key2:", show(key2), "\n",
    "table: ", show(table), "\n",
];

模型中是否还有此处未显示的其他约束？

Minizinc：if-then-else 语句中的数组赋值问题

Minizinc: Issue in array assignment in if-then-else statement

constraint-programming

minizinc