问题描述
我是使用 Minizinc 进行约束编程的初学者，我需要该领域专家的帮助。
如何使用 Minizinc 计算所有可能的组合：正方形 (10x10) 内的 6 个矩形？
考虑到问题的 RESTRICTIONS 是：
1) No Rectangle Can Overlap
2) The 6 rectangles may be vertical or horizontal
输出：
0,1,. . .,6,6
1,4,4
0,5,1
0,2,0
0,0
6,0
继续组合...
解决方法
以下模型在几秒钟内找到解决方案：
% Chuffed: 1.6s
% CPLEX: 3.9s
% Gecode: 1.5s
int: noOfRectangles = 6;
int: squareLen = 10;
int: Empty = 0;
set of int: Coords = 1..squareLen;
set of int: Rectangles = 1..noOfRectangles;
% decision variables:
% The square matrix
% Every tile is either empty or belongs to one of the rectangles
array[Coords,Coords] of var Empty .. noOfRectangles: s;
% the edges of the rectangles
array[Rectangles] of var Coords: top;
array[Rectangles] of var Coords: bottom;
array[Rectangles] of var Coords: left;
array[Rectangles] of var Coords: right;
% function
function var Coords: getCoord(Coords: row,Coords: col,Rectangles: r,Coords: coord,Coords: defCoord) =
if s[row,col] == r then coord else defCoord endif;
% ----------------------< constraints >-----------------------------
% Determine rectangle limits as minima/maxima of the rows and columns for the rectangles.
% Note: A non-existing rectangle would have top=squareLen,bottom=1,left=squareLen,right=1
% This leads to a negative size and is thus ruled-out.
constraint forall(r in Rectangles) (
top[r] == min([ getCoord(row,col,r,row,squareLen) | row in Coords,col in Coords])
);
constraint forall(r in Rectangles) (
bottom[r] == max([ getCoord(row,1) | row in Coords,col in Coords])
);
constraint forall(r in Rectangles) (
left[r] == min([ getCoord(row,col in Coords])
);
constraint forall(r in Rectangles) (
right[r] == max([ getCoord(row,col in Coords])
);
% all tiles within the limits must belong to the rectangle
constraint forall(r in Rectangles) (
forall(row in top[r]..bottom[r],col in left[r]..right[r])
(s[row,col] == r)
);
% enforce a minimum size per rectangle
constraint forall(r in Rectangles) (
(bottom[r] - top[r] + 1) * (right[r] - left[r] + 1) in 2 .. 9
);
% symmetry breaking:
% order rectangles according to their top/left corners
constraint forall(r1 in Rectangles,r2 in Rectangles where r2 > r1) (
(top[r1]*squareLen + left[r1]) < (top[r2]*squareLen + left[r2])
);
% output solution
output [ if col == 1 then "\n" else "" endif ++
if "\(s[row,col])" == "0" then " " else "\(s[row,col]) " endif
| row in Coords,col in Coords];
正方形中的网格位置可以为空或采用六个值之一。该模型确定所有矩形的顶行和底行。与左右列一起，确保这些范围内的所有图块都属于同一个矩形。
要进行实验，最好从较小的正方形尺寸和/或较少数量的矩形开始。界定矩形的大小也可能有意义。否则，矩形往往会变得太小 (1x1) 或太大。
破坏对称性以强制执行一定的矩形排序，确实加快了求解过程。
,这是另一个使用 MiniZincs Geost 约束的解决方案。该解决方案很大程度上基于 Patrick Trentins 的优秀答案 here。如果这对您有帮助，请务必给他一些荣誉。还要确保看到他对模型的解释。
我假设使用 geost 约束会稍微加快这个过程。正如 Axel Kemper 所建议的那样，对称破坏可能会进一步加快速度。
include "geost.mzn";
int: k;
int: nObjects;
int: nRectangles;
int: nShapes;
set of int: DIMENSIONS = 1..k;
set of int: OBJECTS = 1..nObjects;
set of int: RECTANGLES = 1..nRectangles;
set of int: SHAPES = 1..nShapes;
array[DIMENSIONS] of int: l;
array[DIMENSIONS] of int: u;
array[RECTANGLES,DIMENSIONS] of int: rect_size;
array[RECTANGLES,DIMENSIONS] of int: rect_offset;
array[SHAPES] of set of RECTANGLES: shape;
array[OBJECTS,DIMENSIONS] of var int: x;
array[OBJECTS] of var SHAPES: kind;
array[OBJECTS] of set of SHAPES: valid_shapes;
constraint forall (obj in OBJECTS) (
kind[obj] in valid_shapes[obj]
);
constraint geost_bb(k,rect_size,rect_offset,shape,x,kind,l,u);
以及对应的数据：
k = 2; % Number of dimensions
nObjects = 6; % Number of objects
nRectangles = 4; % Number of rectangles
nShapes = 4; % Number of shapes
l = [0,0]; % Lower bound of our bounding box
u = [10,10]; % Upper bound of our bounding box
rect_size = [|
2,3|
3,2|
3,5|
5,3|];
rect_offset = [|
0,0|
0,0|
0,0|];
shape = [{1},{2},{3},{4}];
valid_shapes = [{1,2},{1,{3,4}];
输出读数略有不同。举个例子：
x = array2d(1..6,1..2,[7,2,5,3,0]);
kind = array1d(1..6,[1,1,3]);
这意味着矩形 1 被放置在 [7,0] 并采用形状 [2,3]，如下图所示：
基于@Phonolog 的答案，获得所需输出格式的一种方法是使用通过约束映射到 m 的二维数组 x（此处 size 是边界框大小）：
% mapping to a 2d-array output format
set of int: SIDE = 0..size-1;
array[SIDE,SIDE] of var 0..nObjects: m;
constraint forall (i,j in SIDE) ( m[i,j] = sum(o in OBJECTS)(o *
(i >= x[o,1] /\
i <= x[o,1] + rect_size[kind[o],1]-1 /\
j >= x[o,2] /\
j <= x[o,2] + rect_size[kind[o],2]-1)) );
% symmetry breaking between equal objects
array[OBJECTS] of var int: pos = [ size*x[o,1] + x[o,2] | o in OBJECTS ];
constraint increasing([pos[o] | o in 1..nObjects-1]);
solve satisfy;
output ["kind=\(kind)\n"] ++
["x=\(x)\n"] ++
["m="] ++ [show2d(m)]
编辑：这里是完整的代码：
include "globals.mzn";
int: k = 2;
int: nObjects = 6;
int: nRectangles = 4;
int: nShapes = 4;
int: size = 10;
set of int: DIMENSIONS = 1..k;
set of int: OBJECTS = 1..nObjects;
set of int: RECTANGLES = 1..nRectangles;
set of int: SHAPES = 1..nShapes;
array[DIMENSIONS] of int: l = [0,0];
array[DIMENSIONS] of int: u = [size,size];
array[OBJECTS,DIMENSIONS] of var int: x;
array[OBJECTS] of var SHAPES: kind;
array[RECTANGLES,DIMENSIONS] of int: rect_size = [|
3,2|
2,3|
5,3|
3,5|];
array[RECTANGLES,DIMENSIONS] of int: rect_offset = [|
0,0|
0,0|];
array[SHAPES] of set of SHAPES: shape = [
{1},{4}];
array[OBJECTS] of set of SHAPES: valid_shapes =
[{1,4}];
constraint forall (obj in OBJECTS) (
kind[obj] in valid_shapes[obj]
);
constraint
geost_bb(
k,u
);
% mapping to a 2d-array output format
set of int: SIDE = 0..size-1;
array[SIDE,SIDE] of var 0..nObjects: m;
constraint forall (i,2]-1)) );
% symmetry breaking between equal objects
array[OBJECTS] of var int: pos = [ size*x[o,2] | o in OBJECTS ];
constraint increasing([pos[o] | o in 1..nObjects-1]);
solve satisfy;
output ["kind=\(kind)\n"] ++
["x=\(x)\n"] ++
["m="] ++ [show2d(m)]