constraints - 解决方案的投影

Question

是否有可能告诉 MiniZinc 在一组变量的子集上投影解决方案？或者有没有其他方法可以枚举所有对评估某些变量子集唯一的解决方案？

我曾尝试在 MiniZinc 中直接使用 FlatZinc 注释，但它不起作用，因为扁平化过程添加了更多的 define_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 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。

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;

flatzinc -a 的输出返回了正确的值组合：

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

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

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

变量声明的注释根本没有任何作用。求解器将此类变量视为通常的决策变量。