Решение minizinc lazyfd игнорирует ограничение

Проблема состоит в том, чтобы найти расписание, по которому некоторые люди будут играть в гольф (или что-то еще) в группах фиксированного размера. Мы должны гарантировать, что каждый игрок одновременно находится только в одной группе.

Вот мой код:

int: gr;             % number of groups
int: sz;             % size of groups
int: we;             % number of weeks

int: n=gr*sz;        % number of players

set of int: G=1..gr; % set of group indices
set of int: P=1..n;  % set of players
set of int: W=1..we; % set of weeks

% test instance
gr = 2;
sz = 2;
we = 2;

array[G,W] of var set of P: X;
   %X[g,w] is the set of people that form group with index g in week w


% forall group x, |x| = sz
constraint forall (g in G, w in W) 
  (card (X[g,w]) = sz);

% one person cannot play in two groups simultaneously
constraint forall (g in G, w in W, p in X[g,w], g2 in (g+1..gr))
  (not(p in X[g2,w]));

solve satisfy;

Моя проблема теперь в том, что если я использую lazyfd-решатель G12, т.е.

$ minizinc -b lazy this.mzn

я получил

X = array2d(1..2 ,1..2 ,[1..2, 1..2, 1..2, 1..2]);
----------

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

$ minizinc this.mzn

дает

X = array2d(1..2 ,1..2 ,[1..2, 1..2, 3..4, 3..4]);
----------

что правильно. G12 MIP и Gecode также дают правильный результат.

Как это возможно? И как я могу использовать ленивый решатель, чтобы на него положиться? Или это просто моя установка как-то испорчена?


person JTSkywalker    schedule 10.11.2017    source источник
comment
выглядит как bug, сообщите об этом здесь; по какой причине вы бы не использовали другой движок, кроме lazy?   -  person Patrick Trentin    schedule 11.11.2017
comment
Производительность была моей причиной, но я предполагаю, что производительность связана с ошибкой ... У меня был более сложный пример, где только ленивый решатель смог решить его за разумное время - сначала я не понял, что это был неправильное решение!   -  person JTSkywalker    schedule 11.11.2017
comment
В этом примере механизм fd находит 36 различные расположения массивов менее чем за 1 секунду, тогда как механизм lazy находит 777 разные расположения. Итак, да, это связано с ошибкой или некоторыми другими внутренними ограничениями самого движка, о которых я не знаю.   -  person Patrick Trentin    schedule 11.11.2017
comment
Хорошо, это означает, что я вообще не могу доверять движку lazy, так как я действительно не понимаю, в чем заключается ошибка. Спасибо!   -  person JTSkywalker    schedule 11.11.2017


Ответы (1)


Известно, что G12 / lazyFD не работает в разных местах. Проблема в том, что решатели G12 больше не разрабатываются и, скорее всего, скоро будут удалены из дистрибутивов.

В качестве альтернативы я бы предложил Chuffed. Chuffed - решатель FD, написанный на C ++ с генерацией ленивых предложений. Он должен быть правильным и работать лучше, чем решатель G12 (по крайней мере, когда решения верны).

Chuffed и другие решатели MiniZinc можно найти на странице программного обеспечения веб-сайта MiniZinc.

person Dekker1    schedule 11.11.2017