Projection of solutions

问题:

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.

回答1:

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.

回答2:

The solution uses FlatZinc directly. Assume that we add a constraint 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;

The output of a flatzinc -a returned a correct combination of values:

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

My observation is that auxiliary variables must be:

1. declared with annotations is_defined_var and var_is_introduced
2. must be defined in some constraint defines_var

Annotation of a variable declaration only has no effect at all. The solver treats such a variable as a usual decision variable.