带有`constraint forall(i in x)( x[i] <= x[i+1] );` 的不可满足的解决方案

Question

我正在解决一个学习 minizinc 的玩具问题。取一个值在 0 到 9 之间的数组（目前硬编码为大小 3），并找到总和等于乘积的组合。

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

output["\(x)"];

产出

[2, 3, 1]
----------

这按预期工作，但是，接下来我尝试进行约束，以便值必须按顺序增加。

首先我尝试了这个：

constraint forall(i in x)( 
   x[i] <= x[i+1]
);

这是无法满足的。我在想这可能是由于 i+1 索引大于最后一项的数组大小。所以我给forall加了一个条件，防止最后一项的index越界：

constraint forall(i in x)( 
   i < n /\ x[i] <= x[i+1]
);

然而，这也是无法满足的。

我的概念理解有问题。我的方法有什么问题？

Answer 1

问题。

总的来说，约束没问题。然而，在这个例子的上下文中，它是不一致的。让我们看看为什么会这样。

我们知道解决方案必须包含1, 2, 3，因此，我们可以推断出约束条件

constraint forall (i in x) (
    x[i] <= x[i+1]
);

是"equivalent"到

constraint x[1] <= x[2];
constraint x[2] <= x[3];
constraint x[3] <= x[4];

mzn2fzn 报告了以下问题：

  WARNING: undefined result becomes false in Boolean context
  (array access out of bounds)
  ./t.mzn:12:
  in binary '<=' operator expression
  in array access

在没有硬编码索引值的情况下编写相同的约束时，mzn2fzn 编译器无法在调用求解器之前检测到不一致。但是，access out of bounds 的语义在运行时仍然相同（即 false），因此公式变得不可满足。

约束条件

constraint forall(i in x)( 
   i < n /\ x[i] <= x[i+1]
);

增加了先前的约束，要求 i 必须小于 n。这对于 i = 3 显然是错误的，因此模型中又存在一处不一致。如果您使用蕴涵符号 -> 而不是（逻辑）和符号 /\.

，则约束将是正确的

解决方案。

首先，让我抛开对语言的可能误解。您在模型中使用的理解 i in x 指的是数组 x 内的元素，而不是 x 的索引集。在这种特殊情况下，解决方案和 x 的索引集包含相同的值，因此不会导致不一致。然而，一般情况下并非如此，所以最好使用函数 index_set() 如下：

constraint forall(i, j in index_set(x) where i < j)(
   x[i] <= x[j]
);

例子:

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

constraint forall(i, j in index_set(x) where i < j)(
   x[i] <= x[j]
);

solve satisfy;

output["\(x)"];

产量

~$ mzn2fzn test.mzn 
~$ optimathsat -input=fzn < test.fzn 
x = array1d(1..3, [1, 2, 3]);
----------

一个更优雅的解决方案是使用下面的全局约束，在MiniZinc的documentation (v. 2.2.3)中提到：

predicate increasing(array [int] of var bool: x)
predicate increasing(array [int] of var int: x)
predicate increasing(array [int] of var float: x)

谓词在数组中允许重复值，也就是说，它强制执行非严格递增顺序（如果需要，请将 increasing 与 distinct 组合）。

谓词包含在文件 increasing.mzn 中。但是，人们通常会包含文件 globals.mzn，以便一次访问所有谓词。

例子:

include "globals.mzn";

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

constraint increasing(x);

solve satisfy;

output["\(x)"];

产量

~$ mzn2fzn t.mzn 
~$ optimathsat -input=fzn < t.fzn 
x = array1d(1..3, [1, 2, 3]);
----------

带有`constraint forall(i in x)( x[i] <= x[i+1] );` 的不可满足的解决方案

Unsatisfiable solution with `constraint forall(i in x)( x[i] <= x[i+1] );`

minizinc

optimathsat