constraints - 解决方案的投影

是否可以告诉MiniZinc在一组变量的子集中投影解决方案？还是有其他方法可以枚举所有对某些变量子集求值的唯一解决方案？

我试图直接在MiniZinc中使用FlatZinc批注，但是它不起作用，因为扁平化过程会添加更多define_var批注，而我的批注将被忽略。

最佳答案

我在MiniZinc 2.0(https://www.minizinc.org/2.0/index.html)中尝试了以下模型，这似乎可以按您的预期工作，即，仅将x1和x2投影(打印)在结果中。

int: n = 3;
var 1..n: x1;
var 1..n: x2;
var 1..n: x3;

solve satisfy;
constraint
  x3 > 1
;

output [  show([x1,x2])];

结果是:

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

在MiniZinc v 1.6中，对于每个x3值重复打印x1和x2。

更新:

但是，如果x3涉及任何约束(以任何有趣的方式)，则其行为似乎与版本1.6中的行为相同。那可能不是你想要的...

更新2:

我向Gecode的一位开发人员询问了这一点，他回答:

关于投影语义，这实际上取决于求解器。例如，Gecode不应产生重复的解决方案(基于输出语句中提到的内容)，而g12fd可以产生AFAIK。因此答案是投影由输出项定义，但是只有一些求解器可以保证唯一性。

当我们对此进行测试时，我们发现Gecode中的错误与答案不符。现在，此问题已修复(在SVN版本中)。

以下模型仅给出x1和x2的不同答案(使用固定的Gecode版本):

int: n = 5;

var 1..n: x1;
var 1..n: x2;
var 1..n: x3;

solve satisfy;

constraint
   x2 + x1 < 5 /\
   x2 +x3 > x1
;

output [  "x:", show([x1,x2])];

现在给出的解决方案(使用固定的Gecode求解器)是:

x:[1，1]

x:[2，1]

x:[3，​​1]

x:[1、2]

x:[2，2]

x:[1，3]

==========

这适用于MiniZinc 1.6和MiniZinc 2.0。

关于constraints - 解决方案的投影，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/24942148/