增量Minizinc中的变量数组元素

Question

我想对特定的数组元素执行简单的递增操作:

最小的不工作示例:

array[1..2] of var 0..1: a = [0, 0];

constraint forall (i in 1..2) (
    a[i] = a[i] + 1
);

output ["\(a)"];

solve satisfy;

这会产生minizinc输出

  WARNING: model inconsistency detected
  stack.mzn:3:
  in call 'forall'
  in array comprehension expression
    with i = 1
  stack.mzn:4:
  in binary '=' operator expression
=====UNSATISFIABLE=====
% stack.fzn:1: warning: model inconsistency detected before search.

为什么这是模型中的不一致 - 为什么我不能引用当前数组元素的旧值？还有其他方法可以将当前数组元素增加1吗？

我是限制性解决的新手,所以我希望这不是一个非常愚蠢的问题.

Answer 1

重要的是要知道MiniZinc是一种声明性语言.在一个约束条件中,你没有说明一条指令,但你正在向解算器说明"真相".

这意味着类似的指令a = a + 1将无效,因为您声明我们正在寻找一个值,a这是它自己的价值+ 1.由于不存在这样的值,我们称模型不一致,因为找不到解.

约束项的思想是表达不同变量和参数之间的关系.你可以写一下:constraint forall(i in N) (a[i] = a[i-1] + 1).这意味着我们将寻找a[i]比a[i-1]所有人多1 的价值i in N.(注意,我们应该添加一个if语句以确保i-1保持在给定的范围内)

作为一般规则:如果在等号的一侧有文字,则在另一侧使用该文字将创建不一致的模型.

如果您仍想创建一个将给定数组的值增加1的MiniZinc模型,则可以使用以下模型:

set of int: N = 1..2
array[N] of int: a = [0,1];
array[N] of var int: b;

constraint forall(i in N) (
    b[i] = a[i] + 1
);

由于变量a现在用表达式表示b,这不违反我们的规则.