Minizinc 建模：变量作为坐标集

Question

我正在对 minizinc 中的约束满足程序进行建模，其中解决方案是在 3D 网格上分配点。限制之一是只有一个点可以占据任何给定位置，因此这些点必须在至少一个坐标上成对不同。

我的点变量被建模为 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

这样我就可以使用内置函数了

all_different

然后我看到了如何强制集合具有基数 3，而且使用通用大小的集合来建模三元组似乎不太自然。

我的问题是：什么是对坐标集和完全不同的约束进行建模的易处理且“正确”的方法？

我正在使用 minizinc IDE 包中的 gecode 求解器。模型如下所示。求解时间为 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|];  

Answer 1

注意：我使用 Gecode 和 Git 的最新 MiniZinc 版本在 60 毫秒（不是 24 分钟）内运行了您的模型，获得了第一个解决方案。所以下面的东西可能对你没有帮助......

另外，我回答了您最初的问题，即如何将all_different 与 3D 数组 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 谓词更快。

请注意，如果生成的整数非常大（例如对于大 N），这种 all_different 方法可能会很糟糕。

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|];