Моделирование Minizinc: переменные как наборы координат

avatar
Tall Man
30 марта 2017 в 09:26
238
1
0

Я моделирую программу удовлетворения ограничений в minizinc, где решением является назначение точек на трехмерной сетке. Одно из ограничений заключается в том, что только одна точка может занимать любую заданную позицию, поэтому точки должны попарно отличаться хотя бы по одной из своих координат.

Мои точечные переменные смоделированы как массив N X 3 координат:

array[1..N,1..3] of var -N..N: X;

И ограничение разницы

constraint forall(i in 1..N-1)(forall(j in i+1..N)(not X_eq(i,j))); %extremely slow
predicate X_eq(int: a, int: b)=
 (X[a,1]=X[b,1]/\X[a,2]=X[b,2]/\X[a,3]=X[b,3]);

Но время решения проблемы резко возрастает, когда я формулирую ограничение таким образом. У меня есть много других ограничений, которые нужно добавить, и это уже слишком медленно, чтобы просто найти точки, которые отличаются.

Вместо этого я попытался смоделировать точки как

array[1..N] var set of -N..N

Чтобы я мог использовать встроенную функцию

все_разные

Но затем я вижу, как заставить наборы иметь кардинальность 3, а также кажется менее естественным использовать наборы общего размера для моделирования триплета целых чисел.

Мой вопрос: каков удобный и "правильный" способ моделирования набора координат и различных ограничений?

Я использую решатель gecode, который входит в комплект IDE minizinc. Модель показана ниже. Время решения — 24 минуты.

array[1..N] of 0..1:  seq=[1,1,0,0,0,0,0,1,1,0,0,0,1,0,0,0,1,0];    
int: N=18;
int: H=6;

array[1..N,1..3] of var -N..N: X;

array [1..H,1..3] of 0..N:c;     


%H are in core
constraint forall(i in 1..N)(  if (seq[i]=1) then exists(j in 1..H)([i,1]=c[j,1] /\ X[i,2]=c[j,2] /\ X[i,3]=c[j,3]   ) else true endif);
%All points different
constraint forall(i in 1..N-1)(forall(j in i+1..N)(not X_eq(i,j))); %extremely slow
predicate X_eq(int: a, int: b)=
 (X[a,1]=X[b,1]/\X[a,2]=X[b,2]/\X[a,3]=X[b,3]);


solve satisfy;
output[show(X[i,j]) ++ " "|i in 1..N,j in 1..3]++["\n"];

c=[|0,0,0|
0,0,1|
0,0,2|
0,1,0|
0,1,1|
0,1,2|];  
Источник

Ответы (1)

avatar
hakank
30 марта 2017 в 18:36
1

Примечание. Я запустил вашу модель, поскольку получил первое решение за 60 мс (а не 24 минуты), используя Gecode и последнюю версию MiniZinc из Git. Так что приведенные ниже вещи могут вам не помочь...

Кроме того, я отвечаю на вашу первоначальную проблему, т.е. как использовать all_different с трехмерным массивом X (array[1..N, 1..3]). Я мог что-то упустить в вашей модели, но вот модель, которая решает проблему выполнимости за 9 мс.

Идея создать массив, преобразующий точку в целое число: (X[I,1]-1)*N*N + (X[I,2]-1)*N + X[I,3] (ср. десятичное число 523 равно 5*10*10 + 2*10 + 3). Возможно, это надо подкорректировать, но общее представление вы поняли. Кроме того, я добавил - в комментарии - другой подход, который сравнивает каждую пару точек, которые должны быть быстрее, чем ваш предикат X_eq.

Обратите внимание, что этот all_different подход может быть плохим, если сгенерированные целые числа будут очень большими (например, для больших N).

include "globals.mzn"; 

array[1..N] of 0..1:  seq=[1,1,0,0,0,0,0,1,1,0,0,0,1,0,0,0,1,0];    
int: N=18;
int: H=6;
array [1..H,1..3] of 0..N:c;     
array[1..N,1..3] of var -N..N: X;

solve satisfy;

% hakank: here's my approach of all_different
constraint
   all_different([(X[i,1]-1)*N*N + (X[i,2]-1)*N + X[i,3] | i in 1..N])

   %% another approach (slower than all_different)
   %% for each pair: ensure that there is at least one coordinate differ
   % forall(I in 1..N, J in 1..N where I < J) (
   %   sum([X[I,K] != X[J,K] | K in 1..3]) > 0
   % )

  ;

  % from original model
  constraint
     %H are in core
     forall(i in 1..N)(  
        if (seq[i]=1) then exists(j in 1..H) (
              X[i,1]=c[j,1] /\ X[i,2]=c[j,2] /\ X[i,3]=c[j,3]   
        ) 
        else true endif
    )
  ;

  output 
  [
     show([X[I,J]  | J in 1..3]) ++ "\n"
     | I in 1..N
  ] 
  ;

  c=[|0,0,0|
      0,0,1|
      0,0,2|
      0,1,0|
      0,1,1|
      0,1,2|];
Tall Man
31 марта 2017 в 09:10
0

Спасибо, я тоже делал что-то подобное. На вопрос дан ответ, но ваша модель все еще работала медленно в моей системе. Он компилируется в 30-мегабайтный файл flatzinc с помощью minizinc 2.1.4 из комплекта, но гораздо более короткая и быстрая версия с использованием автономного компилятора minizinc. Не уверен, почему