Проектирование решений

Question

Есть ли возможность рассказать MiniZinc о проектных решениях на подмножестве множества переменных? Или есть какой-то другой способ перечислить все решения, которые являются уникальными по отношению к оценке некоторого подмножества переменных?

Я пытался использовать аннотации FlatZinc непосредственно в MiniZinc, но это не работает, поскольку в процессе выравнивания добавляются аннотации 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 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;

solve satisfy;

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

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

Данные решения (с фиксированным решателем Gecode) теперь:

х:[1, 1]

---

х:[2, 1]

---

х:[3, 1]

---

х:[1, 2]

---

х:[2, 2]

---

х: [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

Аннотация объявления переменной только не имеет никакого эффекта вообще. Решатель рассматривает такую ​​переменную как обычную переменную решения.