解的投影

Question

是否有可能告诉MiniZinc对变量集的子集进行项目解决方案？或者是否有其他方法来枚举所有唯一的wrt解决方案来计算变量的子集？

我曾尝试在FlatZinc中直接使用MiniZinc注释，但它不起作用，因为扁平化过程添加了更多的defines_var注释，而我的注释被忽略了。

Answer 1

我在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 v1.6中，对每个x3值重复打印x1和x2。

更新：

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

Update2：

我问了一位Gecode的开发人员，他回答说：

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

当我们对此进行测试时，我们在Gecode中发现了一个不符合答案的bug。现在这是固定的(在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都是有效的。

Answer 2

该解决方案直接使用FlatZinc。假设我们添加了一个约束x3=x1+x2

var 1..3: x1 :: output_var;
var 1..3: x2 :: output_var;
var 1..3: x3 :: is_defined_var :: var_is_introduced;

constraint int_plus(x1, x2, x3) :: defines_var(x3);
constraint int_le_reif(1, x3, true);

solve satisfy;

平面锌-a的输出返回值的正确组合：

x1 = 1;
x2 = 1;
----------
x1 = 2;
x2 = 1;
----------
x1 = 1;
x2 = 2;
----------
==========

我的观察是，辅助变量必须是：

1. 用注释is_defined_var和var_is_introduced声明
2. 必须在某些约束defines_var中定义

变量声明的注释完全不起作用。求解者将这样的变量视为通常的决策变量。