`constraint forall(i in x)( x[i] <= x[i+1] );` 无法满足的解决方案

Posted 2023-02-22

【中文标题】`constraint forall(i in x)( x[i] <= x[i+1] );` 无法满足的解决方案

【英文标题】：Unsatisfiable solution with `constraint forall(i in x)( x[i] <= x[i+1] );`

【发布时间】：2019-02-12 11:00:30

【问题描述】：

我正在研究一个玩具问题来学习 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加了一个条件，防止最后一项的索引越界：

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

但是，这也是不令人满意的。

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

【参考方案1】：

问题。

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

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

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

“等价于”

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]);
----------