3

我正在研究一个玩具问题来学习 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]
);

然而，这也是不令人满意的。

我的概念理解有些不对劲。我的方法有什么问题？

4

1 回答 1

4

问题）。

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

我们知道解决方案必须包括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]);
----------

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

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]);
----------
于 2019-02-12T12:11:20.700 回答