投影解决方案 [英] Projection of solutions
问题描述
是否有可能告诉MiniZinc在变量集的子集上项目解决方案？或者是否有任何其他方法来枚举所有的解决方案是唯一的wrt到一些变量的子集的评估？
我试图在MiniZinc中直接使用FlatZinc注释，但它不工作，因为平展过程添加了更多的definitions_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;
解决满足;
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 x1和x2每个x3值重复打印。
更新：
但是，如果x3涉及任何约束（以任何有趣的方式），它似乎是与版本1.6相同的行为。这可能不是你想要的...
Update2：
我问过Gecode的开发人员关于这一点，他回答说：
关于投影语义，这确实取决于求解器。 Gecode实例不应该产生重复的解决方案（基于输出语句中提到的），而g12fd确实，AFAIK。因此，答案是投影由输出项定义，但只有一些解算器保证唯一性。
当我们测试这个，发现Gecode中的一个错误，不符合答案。这是现在固定的（在SVN版本）。
以下模型如何给x1和x2的独特的答案（使用固定Gecode版本）：
int：n = 5;
var 1..n：x1;
var 1..n：x2;
var 1..n：x3;
解决满足;
约束
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。
Is there a possibility to tell MiniZinc to project solutions on a subset of the set of variables? Or is there any other way to enumerate all solutions that are unique wrt to evaluation of some subset of variables?
I have tried to use FlatZinc annotations directly in MiniZinc, but it does not work, since the flattening process adds more defines_var annotations and my annotations are ignored.
I tried the following model in MiniZinc 2.0 (https://www.minizinc.org/2.0/index.html) and this seems to work as you expect, i.e. that just x1 and x2 are projected (printed) in the result.
int: n = 3;
var 1..n: x1;
var 1..n: x2;
var 1..n: x3;
solve satisfy;
constraint
x3 > 1
;
output [ show([x1,x2])];
The result is:
[1, 1]
----------
[2, 1]
----------
[3, 1]
----------
[1, 2]
----------
[2, 2]
----------
[3, 2]
----------
[1, 3]
----------
[2, 3]
----------
[3, 3]
----------
==========
In MiniZinc v 1.6 x1 and x2 are printed repeatedly for each x3 value.
Update:
However, if x3 is involved in any constraints (in any interesting way) it seems to be the same behaviour as in version 1.6. And that's probably not what you want...
Update2:
I asked one of the developers of Gecode about this and he answered:
Regarding the projection semantics, this really depends on the solver. Gecode for instance should not produce duplicate solutions (based on what is mentioned in the output statement), whereas g12fd does, AFAIK. So the answer would be that projection is defined by the output item, but only some solvers guarantee uniqueness.
When we tested this, we found a bug in Gecode that didn't comply with the answer. This is now fixed (in the SVN version).
The following model how just give distinct answers for x1 and x2 (using the fixed Gecode version):
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])];
The solutions given (with the fixed Gecode solver) are now:
x:[1, 1]
x:[2, 1]
x:[3, 1]
x:[1, 2]
x:[2, 2]
x:[1, 3]
==========
This works both for MiniZinc 1.6 and MiniZinc 2.0.
这篇关于投影解决方案的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
