Minizinc 建模:Vars 作为坐标集
Minizinc modelling: Vars as coordinate sets
我正在 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,而且使用通用大小的集来建模整数三元组似乎不太自然。
我的问题是:什么是易于处理且 'correct' 对坐标集和完全不同的约束进行建模的方法?
我正在使用 minizinc IDE 包中的地理编码求解器。该模型如下所示。求解时间为 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|];
注意:我 运行 您的模型使用 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|];
我正在 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,而且使用通用大小的集来建模整数三元组似乎不太自然。
我的问题是:什么是易于处理且 'correct' 对坐标集和完全不同的约束进行建模的方法?
我正在使用 minizinc IDE 包中的地理编码求解器。该模型如下所示。求解时间为 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|];
注意:我 运行 您的模型使用 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|];