Functions and Predicates

◀predicate bin_packing(int: c,
array [int] of var int: bin,
array [int] of int: w) =

assert(index_set(bin)==index_set(w),
"bin_packing: the bin and weight arrays must have identical index sets",
assert(lb_array(w)>=0,
"bin_packing: the weights must be non-negative", assert(c>=0,
"bin_packing: capacity must be non-negative", forall ( b in
lb_array(bin)..ub_array(bin) ) ( c>=sum ( i in
index_set(bin) ) ( w[i]*
bool2int(bin[i]==b) ) ))))

(standard decomposition from bin_packing.mzn:10)Requires that each item i with weight w[i], be put into bin[i] such that the sum of the weights of the items in each bin does not exceed the capacity c.

Assumptions:

- forall i, w[i] >=0
- c >=0

◀predicate bin_packing_capa(array [int] of int: c,
array [int] of var int: bin,
array [int] of int: w) =

assert(index_set(bin)==index_set(w),
"bin_packing_capa: the bin and weight arrays must have identical index sets",
assert(lb_array(w)>=0,
"bin_packing_capa: the weights must be non-negative",
assert(lb_array(c)>=0,
"bin_packing_capa: the capacities must be non-negative", forall (
i in index_set(bin) ) (
min(index_set(c))<=bin[i] /\ bin
[i]<=max(index_set(c)) ) /\ forall (
b in index_set(c) ) ( c
[b]>=sum ( i in index_set(bin) ) ( w[i]*bool2int(bin[i]==b) ) ))))

(standard decomposition from bin_packing_capa.mzn:10)Requires that each item i with weight w[i], be put into bin[i] such that the sum of the weights of the items in each bin b does not exceed the capacity c[b].

Assumptions:

- forall i, w[i] >=0
- forall b, c[b] >=0

◀function array [int] of var int: bin_packing_load(array [int] of var int: bin,
array [int] of int: w) =

let {
array [dom_bounds_array(bin)] of var 0..sum(w): load,
constraint bin_packing_load(load, bin, w),
} in (load)

(standard decomposition from bin_packing_load_fn.mzn:11)Returns the load of each bin resulting from packing each item i with weight w[i] into bin[i], where the load is defined as the sum of the weights of the items in each bin.

Assumptions:

- forall i, w[i] >=0

◀predicate bin_packing_load(array [int] of var int: load,
array [int] of var int: bin,
array [int] of int: w) =

assert(index_set(bin)==index_set(w),
"bin_packing_load: the bin and weight arrays must have identical index sets",
assert(lb_array(w)>=0,
"bin_packing_load: the weights must be non-negative", sum(load)==
sum(w) /\ forall ( i
in index_set(bin) ) (
min(index_set(load))<=bin[i] /\ bin[i]<=
max(index_set(load)) ) /\ forall ( b
in index_set(load) ) ( load
[b]==sum ( i in index_set(bin) ) ( w[i]*bool2int(bin[i]==b) ) )))

(standard decomposition from bin_packing_load.mzn:9)Requires that each item i with weight w[i], be put into bin[i] such that the sum of the weights of the items in each bin b is equal to load[b].

Assumptions:

- forall i, w[i] >=0

◀predicate diffn(array [int] of var int: x,
array [int] of var int: y,
array [int] of var int: dx,
array [int] of var int: dy) =

assert(index_set(x)==index_set(y) /\ index_set(x)==index_set(dx) /\
index_set(x)==index_set(dy), "diffn: index set mismatch", forall ( i,
j
in index_set(x) where i < j ) ( x[i]+dx
[i]<=x[j] \/ y[i]+dy
[i]<=y[j] \/ x[j]+dx
[j]<=x[i] \/ y[j]+dy
[j]<=y[i]
))

(standard decomposition from diffn.mzn:6)Constrains rectangles i, given by their origins (x[i], y[i]) and sizes (dx[i], dy[i]), to be non-overlapping. Zero-width rectangles can still not overlap with any other rectangle.

◀predicate diffn_k(array [int,int] of var int: box_posn,
array [int,int] of var int: box_size) =

let {
set of int: DIMS = index_set_2of2(box_posn),
} in (
assert(index_set_2of2(box_size)==DIMS /\
index_set_1of2(box_posn)==index_set_1of2(box_size),
"diffn: index sets of arguments are incorrect", forall ( b1, b2
in
index_set_1of2(box_posn) where b1 < b2 ) (
diffn_nonoverlap_k([ box_posn[b1, j] | j in DIMS ], [ box_size
[b1, j] | j in DIMS ], [ box_posn[b2, j] | j in DIMS ], [ box_size
[b2, j] | j in DIMS ])
)))

(standard decomposition from diffn_k.mzn:7)Constrains k-dimensional boxes to be non-overlapping. For each box i and dimension j, box_posn[i, j] is the base position of the box in dimension j, and box_size[i, j] is the size in that dimension. Boxes whose size is 0 in any dimension still cannot overlap with any other box.

◀predicate diffn_nonstrict(array [int] of var int: x,
array [int] of var int: y,
array [int] of var int: dx,
array [int] of var int: dy) =

assert(index_set(x)==index_set(y) /\ index_set(x)==index_set(dx) /\
index_set(x)==index_set(dy), "diffn: index set mismatch", forall ( i,
j
in index_set(x) where i < j ) ( dx[i]==
0 \/ dx[j]==
0 \/ dy[i]==
0 \/ dy[j]==
0 \/ x[i]+dx
[i]<=x[j] \/ y[i]+dy
[i]<=y[j] \/ x[j]+dx
[j]<=x[i] \/ y[j]+dy
[j]<=y[i]
))

(standard decomposition from diffn_nonstrict.mzn:6)Constrains rectangles i, given by their origins (x[i], y[i]) and sizes (dx[i], dy[i]), to be non-overlapping. Zero-width rectangles can be packed anywhere.

◀predicate diffn_nonstrict_k(array [int,int] of var int: box_posn,
array [int,int] of var int: box_size) =

let {
set of int: DIMS = index_set_2of2(box_posn),
} in (
assert(index_set_2of2(box_size)==DIMS /\
index_set_1of2(box_posn)==index_set_1of2(box_size),
"diffn: index sets of arguments are incorrect", forall ( b1, b2
in
index_set_1of2(box_posn) where b1 < b2 ) (
diffn_nonstrict_nonoverlap_k([ box_posn[b1, j] | j in DIMS ],
[ box_size[b1, j] | j in DIMS ], [ box_posn[b2, j] | j in DIMS ],
[ box_size[b2, j] | j in DIMS ])
)))

(standard decomposition from diffn_nonstrict_k.mzn:7)Constrains k-dimensional boxes to be non-overlapping. For each box i and dimension j, box_posn[i, j] is the base position of the box in dimension j, and box_size[i, j] is the size in that dimension. Boxes whose size is 0 in at least one dimension can be packed anywhere.

◀predicate geost(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind) =

assert(index_set_1of2(rect_size)==index_set_1of2(rect_offset) /\
index_set_2of2(rect_size)==1..k /\
index_set_2of2(rect_offset)==1..k /\
index_set(shape)==1..length(shape) /\
index_set_1of2(x)==index_set(kind) /\
index_set_2of2(x)==1..k /\
forall ( i in index_set(shape) ) (
shape[i] subset index_set_1of2(rect_size)
), "geost: index sets of arguments are incorrect", assert(forall ( i
in index_set(shape) ) (
card(shape
[i]) > 0
),
"geost: sets in shape must be non-empty", let {
set of int: DIMS =
1..k,
set of int: SHAPES
= 1..
length(shape),
set of int: OBJECTS
= index_set(kind),
} in (
forall ( s in
SHAPES ) (
forall ( r1, r2
in
shape[s] where r1 < r2 ) (
assert(geost_nonoverlap_k([ rect_offset[r1, j] | j in DIMS ],
[ rect_size[r1, j] | j in DIMS ], [ rect_offset[r2, j] | j in
DIMS ], [ rect_size[r2, j] | j in DIMS ]),
((((("geost: rectangles "++show(r1))++" and ")++show(r2))++
" in shape ")++
show(s))++
" overlap!")
)
) /\
forall ( o1, o2 in
OBJECTS where o1 < o2 ) (
forall ( s1 in
dom(kind[o1]), s2 in dom(kind[o2]) ) (
kind[o1]==
s1 /\
kind[o2]==
s2 -> forall ( r1 in shape[s1], r2 in shape[s2] ) (
geost_nonoverlap_k([ x[o1, j]+rect_offset[r1, j] | j in
DIMS ], [ rect_size[r1, j] | j in DIMS ], [ x[o2, j]+rect_offset
[r2, j] | j in DIMS ], [ rect_size[r2, j] | j in DIMS ])
)
)
))))

(standard decomposition from geost.mzn:14)A global non-overlap constraint for k dimensional objects. It enforces that no two objects overlap.

Parameters

- k: the number of dimensions
- rect_size: the size of each box in k dimensios
- rect_offset: the offset of each box from the base position in k dimensions
- shape: the set of rectangles defining the i-th shape. Assumption: Each pair of boxes in a shape must not overlap.
- x: the base position of each object. x[i,j] is the position of object i in. dimension j.
- kind: the shape used by each object.

◀predicate geost_bb(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind,
array [int] of var int: l,
array [int] of var int: u) =

assert(index_set(l)==1..k /\
index_set(u)==1..k,
"geost_bb: index set of bounds arrays is not 1.."++
show(k), let {
set of int: DIMS = 1..k,
set of int: OBJECTS =
index_set(kind),
} in (
geost(k, rect_size, rect_offset,
shape, x, kind) /\
forall ( o in OBJECTS ) (
forall ( s in dom(kind[o]) ) (
kind[o]==s -> forall ( r in
shape[s], j in DIMS ) ( x[o, j]+
rect_offset[r, j]>=l[j] /\ x[o, j]+
rect_offset[r, j]+rect_size[r, j]<=u[j] )
)
)))

(standard decomposition from geost.mzn:96)A global non-overlap constraint for k dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global k dimensional bounding box.

Parameters

- k: the number of dimensions
- rect_size: the size of each box in k dimensios
- rect_offset: the offset of each box from the base position in k dimensions
- shape: the set of rectangles defining the i-th shape. Assumption: Each pair of boxes in a shape must not overlap.
- x: the base position of each object. x[i,j] is the position of object i in dimension j.
- kind: the shape used by each object.
- l: is an array of lower bounds, l[i] is the minimum bounding box for all objects in dimension i.
- u: is an array of upper bounds, u[i] is the maximum bounding box for all objects in dimension i.

◀predicate geost_smallest_bb(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind,
array [int] of var int: l,
array [int] of var int: u) =

let {
set of int: DIMS = 1..k,
set of int: OBJECTS = index_set(kind),
} in (
geost_bb(k, rect_size, rect_offset, shape, x, kind, l, u) /\
forall ( j in DIMS ) (
exists ( o in OBJECTS, s in dom(kind[o]) ) (
kind[o]==s /\
exists ( r in shape[s] ) (
x[o, j]+rect_offset[r, j]==l[j]
)
) /\
exists ( o in OBJECTS, s in dom(kind[o]) ) (
kind[o]==s /\
exists ( r in shape[s] ) (
x[o, j]+rect_offset[r, j]+rect_size[r, j]==u[j]
)
)
))

(standard decomposition from geost.mzn:147)A global non-overlap constraint for k dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global k dimensional bounding box. In addition, it enforces that the bounding box is the smallest one containing all objects, i.e., each of the 2k boundaries is touched by at least by one object.

Parameters

- k: the number of dimensions
- rect_size: the size of each box in k dimensios
- rect_offset: the offset of each box from the base position in k dimensions
- shape: the set of rectangles defining the i-th shape. Assumption: Each pair of boxes in a shape must not overlap.
- x: the base position of each object. x[i,j] is the position of object i in dimension j.
- kind: the shape used by each object.
- l: is an array of lower bounds, l[i] is the minimum bounding box for all objects in dimension i.
- u: is an array of upper bounds, u[i] is the maximum bounding box for all objects in dimension i.

◀predicate knapsack(array [int] of int: w,
array [int] of int: p,
array [int] of var int: x,
var int: W,
var int: P) =

assert(index_set(w)==index_set(p) /\ index_set(w)==index_set(x),
"index set of weights must be equal to index set of profits and index set of items",
assert(lb_array(w)>=0, "weights must be non-negative",
assert(lb_array(p)>=0, "profits must be non-negative", forall ( i
in index_set(x) ) ( x[i]>=
0 ) /\ W>=0 /\ P>=0 /\ P==sum ( i
in index_set(p) ) ( x
[i]*p[i] ) /\ W==sum ( i
in index_set(w) ) ( x
[i]*w[i] ))))

(standard decomposition from knapsack.mzn:15)Requires that items are packed in a knapsack with certain weight and profit restrictions. Assumptions:

- Weights w and profits p must be non-negative
- w, p and x must have the same index sets

Parameters

- w: weight of each type of item
- p: profit of each type of item
- x: number of items of each type that are packed
- W: sum of sizes of all items in the knapsack
- P: sum of profits of all items in the knapsack