Неудовлетворительное решение с `forall ограничений (i в x) (x [i] <= x [i + 1]);` - PullRequest
Новая
       4

Неудовлетворительное решение с `forall ограничений (i в x) (x [i] <= x [i + 1]);`

0 голосов
/ 12 февраля 2019

Я работаю над проблемой игрушек, чтобы изучить миницинк.Возьмите массив (в настоящее время жестко задан размер 3) значений от 0 до 9 и найдите комбинации, в которых сумма равна произведению. 

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

output["\(x)"];

Выходы 

[2, 3, 1]
----------

Этоработает, как и ожидалось, однако, следующий я пытаюсь ограничить, так что значения должны увеличиваться в порядке.

Сначала я попробовал это: 

constraint forall(i in x)( 
   x[i] <= x[i+1]
);

Это было неудовлетворительно.Я думал, что это может быть связано с тем, что индекс i+1 больше, чем размер массива для последнего элемента.Таким образом, я добавил условие для предотвращения выхода за пределы индекса последнего элемента: 

constraint forall(i in x)( 
   i < n /\ x[i] <= x[i+1]
);

Однако это также было НЕ УДОВЛЕТВОРЕНО.

Что-то не так с моим концептуальным пониманием.Что не так с моим подходом?

1 Ответ

0 голосов
/ 12 февраля 2019

ПРОБЛЕМА (ы).

В общем, ограничение в порядке.В контексте этого примера, однако, это противоречиво.Давайте посмотрим, почему это так.

Мы знаем, что решение должно включать 1, 2, 3, таким образом, мы можем сделать вывод, что ограничение 

constraint forall (i in x) (
    x[i] <= x[i+1]
);

"эквивалентно" 

constraint x[1] <= x[2];
constraint x[2] <= x[3];
constraint x[3] <= x[4];

, для которого mzn2fzn сообщает о следующей проблеме: 

  WARNING: undefined result becomes false in Boolean context
  (array access out of bounds)
  ./t.mzn:12:
  in binary '<=' operator expression
  in array access

Когда такое же ограничение записывается без жестко закодированных значений индекса, компилятор mzn2fzn не может обнаружить несоответствие дорешатель вызывается.Однако семантика access out of bounds остается неизменной (то есть false) во время выполнения, поэтому формула становится неудовлетворительной.

Ограничение 

constraint forall(i in x)( 
   i < n /\ x[i] <= x[i+1]
);

дополняет предыдущееограничение с требованием, что i должно быть меньше, чем n.Это явно неверно для i = 3, поэтому в модели есть еще одно несоответствие.Ограничение будет правильным, если вы используете символ импликации -> вместо (логического) и символа /\.

SOLUTION (s).

Во-первых, позвольте мне отложить в сторону возможное неправильное понимание языка.Понятие i in x, которое вы использовали в своей модели, относится к элементам в массиве x, а не к набору индексов x.В этом конкретном случае решение и набор индексов x содержат одинаковые значения, поэтому это не вызывает несогласованности.Однако в общем случае это не так, поэтому лучше использовать функцию index_set() следующим образом: 

constraint forall(i, j in index_set(x) where i < j)(
   x[i] <= x[j]
);

пример : 

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

constraint forall(i, j in index_set(x) where i < j)(
   x[i] <= x[j]
);

solve satisfy;

output["\(x)"];

выход 

~$ mzn2fzn test.mzn 
~$ optimathsat -input=fzn < test.fzn 
x = array1d(1..3, [1, 2, 3]);
----------

Более элегантное решение заключается в использовании следующего глобального ограничения, которое упомянуто в документации (версия 2.2.3) из MiniZinc: 

predicate increasing(array [int] of var bool: x)
predicate increasing(array [int] of var int: x)
predicate increasing(array [int] of var float: x)

Предикат допускает повторяющиеся значения в массиве, то есть он применяет нестрогий возрастающий порядок (если это необходимо, объедините increasing с distinct).

Предикат содержится в файле increasing.mzn.Однако вместо этого люди обычно включают файл globals.mzn, чтобы иметь доступ ко всем предикатам одновременно.

пример : 

include "globals.mzn";

par int: n = 3; % hardcode for now 

array[1..n] of var 0..9: x;

constraint sum(x) != 0;
constraint sum(x) == product(x);

constraint increasing(x);

solve satisfy;

output["\(x)"];

приводит к 

~$ mzn2fzn t.mzn 
~$ optimathsat -input=fzn < t.fzn 
x = array1d(1..3, [1, 2, 3]);
----------
...