The following constraints model a set of lines or rectangles, respectively, so that no pair of objects overlap:
disjoint1(+Lines)
disjoint1(+Lines,+Options)
where Lines is a list of terms F(Sj,Dj) or F(Sj,Dj,Tj), Sj and Dj are domain variables with finite bounds denoting the origin and length of line j respectively, F is any functor, and the optional Tj is an atomic term denoting the type of the line. Tj defaults to 0 (zero).
Options is a list of zero or more of the following, where
Boolean must be true
or false
(false
is the
default):
decomposition(Boolean)
if true
, an attempt is made to decompose the constraint each time
it is resumed.
global(Boolean)
if true
, a redundant algorithm using global reasoning is used to
achieve more complete pruning.
wrap(Min,Max)
If used, the space in which the lines are placed should be thought of as a circle where positions Min and Max coincide, where Min and Max should be integers. That is, the space wraps around. Furthermore, this option forces the domains of the origin variables to be inside [Min,Max-1].
margin(T1,T2,D)
This option imposes a minimal distance D between the end point of
any line of type T1 and the origin of any line of type T2.
D should be a positive integer or sup
. If sup
is
used, all lines of type T2 must be placed before any line of type
T1.
This option interacts with the wrap/2
option in the sense that
distances are counted with possible wrap-around, and the distance
between any end point and origin is always finite.
The file library('clpfd/examples/bridge.pl')
contains an example
where disjoint1/2
is used for scheduling non-overlapping tasks.
disjoint2(+Rectangles)
disjoint2(+Rectangles,+Options)
where Rectangles is a list of terms F(Xj,Lj,Yj,Hj) or F(Xj,Lj,Yj,Hj,Tj), Xj and Lj are domain variables with finite bounds denoting the origin and size of rectangle j in the X dimension, Yj and Hj are the values for the Y dimension, F is any functor, and the optional Tj is an atomic term denoting the type of the rectangle. Tj defaults to 0 (zero).
Corresponds to diffn/4
in MiniZinc.
Options is a list of zero or more of the following, where
Boolean must be true
or false
(false
is the
default):
decomposition(Boolean)
If true
, an attempt is made to decompose the constraint each time
it is resumed.
global(Boolean)
If true
, a redundant algorithm using global reasoning is used
to achieve more complete pruning.
wrap(Min1,Max1,Min2,Max2)
Min1 and Max1 should be either integers or the atoms
inf
and sup
respectively. If they are integers, the space
in which the rectangles are placed should be thought of as a cylinder
wrapping around the X dimension where positions Min1 and
Max1 coincide. Furthermore, this option forces the domains of the
Xj variables to be inside [Min1,Max1-1].
Min2 and Max2 should be either integers or the atoms
inf
and sup
respectively. If they are integers, the space
in which the rectangles are placed should be thought of as a cylinder
wrapping around the Y dimension where positions Min2 and
Max2 coincide. Furthermore, this option forces the domains of the
Yj variables to be inside [Min2,Max2-1].
If all four are integers, the space is a toroid wrapping around both dimensions.
margin(T1,T2,D1,D2)
This option imposes minimal distances D1 in the X dimension and
D2 in the Y dimension between the end point of any rectangle of
type T1 and the origin of any rectangle of type T2.
D1 and D2 should be positive integers or sup
. If
sup
is used, all rectangles of type T2 must be placed
before any rectangle of type T1 in the relevant dimension.
This option interacts with the wrap/4
option in the sense that
distances are counted with possible wrap-around, and the distance
between any end point and origin is always finite.
synchronization(Boolean)
Let the assignment dimension and the temporal dimension
denote the two dimensions, no matter which is the X and which is the Y
dimension. If Boolean is true
, a redundant algorithm is
used to achieve more complete pruning for the following case:
The following example shows an artificial placement problem involving 25
rectangles including four groups of rectangles whose left and right
borders must be aligned. If Synch
is true
, it can be
solved with first-fail labeling in 23 backtracks. If Synch
is
false
, 60 million backtracks don’t suffice to solve it.
ex([O1,Y1a,Y1b,Y1c, O2,Y2a,Y2b,Y2c,Y2d, O3,Y3a,Y3b,Y3c,Y3d, O4,Y4a,Y4b,Y4c], Synch) :- domain([Y1a,Y1b,Y1c, Y2a,Y2b,Y2c,Y2d, Y3a,Y3b,Y3c,Y3d, Y4a,Y4b,Y4c], 1, 5), O1 in 1..28, O2 in 1..26, O3 in 1..22, O4 in 1..25, disjoint2([t(1,1,5,1), t(20,4,5,1), t(1,1,4,1), t(14,4,4,1), t(1,2,3,1), t(24,2,3,1), t(1,2,2,1), t(21,1,2,1), t(1,3,1,1), t(14,2,1,1), t(O1,3,Y1a,1), t(O1,3,Y1b,1), t(O1,3,Y1c,1), t(O2,5,Y2a,1), t(O2,5,Y2b,1), t(O2,5,Y2c,1), t(O2,5,Y2d,1), t(O3,9,Y3a,1), t(O3,9,Y3b,1), t(O3,9,Y3c,1), t(O3,9,Y3d,1), t(O4,6,Y4a,1), t(O4,6,Y4b,1), t(O4,6,Y4c,1)], [synchronization(Synch)]).
geost(+Objects,+Shapes) since release 4.1
geost(+Objects,+Shapes,+Options) since release 4.1
geost(+Objects,+Shapes,+Options,+Rules) since release 4.1
constrains the location in space of non-overlapping multi-dimensional Objects, each of which taking a shape among a set of Shapes.
Each shape is defined as a finite set of shifted boxes, where each
shifted box is described by a box in a k-dimensional space at the
given offset with the given sizes. A shifted box is described by a
ground term sbox(Sid,Offset,Size)
where
Sid, an integer, is the shape id; Offset, a list of k
integers, denotes the offset of the shifted box from the origin of the
object; and Size, a list of k integers greater than zero,
denotes the size of the shifted box. Then, a shape is a
collection of shifted boxes all sharing the same shape id. The shifted
boxes associated with a given shape must not overlap. Shapes is
thus the list of such sbox/3
terms.
Each object is described by a term
object(Oid,Sid,Origin
where Oid, an
integer, is the unique object id; Sid, a domain variable, is the
shape id; and Origin, a list of domain variables, is the origin
coordinate of the object. If Sid is nonground, the object is said
to be polymorphic. The possible values for Sid are the shape
ids that occur in Shapes. Objects is thus the list of such
object/3
terms.
If given, Options is a list of zero or more of the following,
where Boolean must be true
or false
(false
is
the default):
lex(ListOfOid)
where ListOfOid should be a list of distinct object ids, denotes
that the origin vectors of the objects according to ListOfOid
should be in ascending lexicographic order. Multiple lex/1
options can be given, but should mention disjoint sets of objects.
cumulative(Boolean)
If true
, redundant reasoning methods are enabled, based on
projecting the objects onto each dimension.
disjunctive(Boolean)
If true
, cliques of objects are detected that clash in one
dimension and so must be separated in the other dimension. This method
only applies in the 2D case.
longest_hole(Value,Maxbacks)
This method only applies in the 2D case and in the absence of
polymorphic objects. Value can be all
, true
or
false
. If true
, the filtering algorithm computes and uses
information about holes that can be tolerated without necessarily
failing the constraint. If all
, more precise information is
computed. If false
, no such information is computed.
Maxbacks should be an integer >= -1
and gives a bound on
the effort spent tightening the longest hole information. Experiments
suggest that 1000 may be a reasonable compromise value.
parconflict(Boolean)
If true
, redundant reasoning methods are enabled, based on
computing the number of items that can be put in parallel in the
different dimensions.
visavis_init(Boolean)
If true
, a redundant method is enabled that statically detects
placements that would cause too large holes. This method can be quite
effective.
visavis_floating(Boolean)
If true
, a redundant method is enabled that dynamically detects
placements that would cause too large holes. It’s more general than the
following option, but only applies in the 2D case and in the absence of
polymorphic objects. This method has been shown to pay off only in rare
cases.
visavis(Boolean)
If true
, a redundant method is enabled that dynamically detects
placements that would cause too large holes. This method has not been
shown to pay off experimentally.
corners(Boolean)
If true
, a redundant method is enabled that reasons in terms on
borders that impinge on the corners of objects. This method only
applies in the 2D case. It has not been shown to pay off
experimentally.
task_intervals(Boolean)
If true
, a redundant reasoning method is enabled that detects
overcrowded and undercrowded regions of the placement space. This
method has not been shown to pay off experimentally.
dynamic_programming(Boolean)
If true
, a redundant reasoning method is enabled that solves a 2D
knapsack problem for every two adjacent columns of the projection of the
objects onto each dimension. This method has pseudo-polynomial
complexity but can be quite powerful.
polymorphism(Boolean)
If true
, a reasoning method is enabled that is relevant in the
context of polymorphic objects and no slack. The method detects parts
of the placement space that cannot be filled and thus fails the
constraint. This method has not been shown to pay off experimentally.
pallet_loading(Boolean)
If true
, and if all objects consist of a single shifted box of
the same shape, modulo rotations, a redundant method is enabled that
recognizes necessary conditions for this special case.
overlap(Boolean)
If true
, the constraint that objects be non-overlapping is
lifted. This option is useful mainly in conjunction with the
Rules argument, in case the placement of objects should be
restricted by the Rules only.
volume(Total)
If given, Total is constrained to be the total volume of Objects.
bounding_box(Lower,Upper)
Lower=[L1,...,Lk] and Upper=[U1,...,Uk] should be lists of domain variables. The following conditions are imposed:
fixall(Flag,Patterns)
If given, Flag is a domain variable in 0..1
. If Flag
equals 1, either initially or by binding Flag during search, the
constraint switches behavior into greedy assignment mode. The greedy
assignment will either succeed and assign all shape ids and origin
coordinates to values that satisfy the constraint, or merely fail.
Flag is never bound by the constraint; its sole function is to
control the behavior of the constraint.
Greedy assignment is done one object at a time, in the order of
Objects. The assignment per object is controlled by
Patterns, which should be a list of one or more pattern terms of
the form object(_,SidSpec,OriginSpec)
, where SidSpec is a
term min(I)
or max(I)
, OriginSpec is a
list of k such terms, and I is a unique integer between 1
and k+1.
The meaning of the pattern is as follows. The variable in the position
of min(1)
or max(1)
is fixed first; the variable in the
position of min(2)
or max(2)
is fixed second; and so on.
min(I)
means trying values in ascending order;
max(I)
means descending order.
If Patterns contains m pattern, then object 1 is fixed according to pattern 1, …, object m is fixed according to pattern m, object m+1 is fixed according to pattern 1, and so on. For example, suppose that the following option is given:
fixall(F, [object(_,min(1),[min(3),max(2)]), object(_,max(1),[min(2),max(3)])])
Then, if the program binds F
to 1, the constraint enters greedy
assignment mode and endeavors to fix all objects as follows.
If given, Rules is a list of zero or more terms of the form shown
below, and impose extra constraints on the placement of the objects.
For the time being, the details are described in [Carlsson, Beldiceanu &
Martin 08]. Please note: the rules require that all shapes of
a polymorphic objects consist of the same number of shifted boxes. For
example, Shapes =
[sbox(1,[0,0],[3,1]),sbox(1,[0,1],[2,4]),sbox(2,[0,0],[3,1])]
will not
work.
sentence | ::= | macro | fol | |
macro | ::= | head ---> body | |
head | ::= | term | { to be substituted by a body } |
body | ::= | term | { to substitute for a head } |
fol | ::= | #\ fol | { negation } |
| | fol #/\ fol | { conjunction } | |
| | fol #\/ fol | { disjunction } | |
| | fol #=> fol | { implication } | |
| | fol #<=> fol | { equivalence } | |
| | exists(var,collection,fol) | { existential quantification } | |
| | forall(var,collection,fol) | { universal quantification } | |
| | card(var,collection,integer,integer,fol) | { cardinality } | |
| | true | ||
| | false | ||
| | expr relop expr | { rational arithmetic } | |
| | head | { macro application } | |
expr | ::= | expr + expr | |
| | - expr | ||
| | expr - expr | ||
| | min(expr,expr) | ||
| | max(expr,expr) | ||
| | expr * groundexpr | ||
| | groundexpr * expr | ||
| | expr / groundexpr | ||
| | attref | ||
| | integer | ||
| | fold(var,collection,fop,expr,expr) | ||
| | variable | { quantified variable } | |
| | head | { macro application } | |
groundexpr | ::= | expr | { where expr is ground } |
attref | ::= | entity ^ attr | |
attr | ::= | term | { attribute name } |
| | variable | { quantified variable } | |
relop | ::= | #< | #= | #> | #\= | #=< | #>= | |
fop | ::= | + | min | max | |
collection | ::= | list | |
| | objects(list) | { list of oids } | |
| | sboxes(list) | { list of sids } |
The following example shows geost/2
modeling three
non-overlapping objects. The first object has four possible shapes, and
the other two have two possible shapes each.
| ?- domain([X1,X2,X3,Y1,Y2,Y3], 1, 4), S1 in 1..4, S2 in 5..6, S3 in 7..8, geost([object(1,S1,[X1,Y1]), object(2,S2,[X2,Y2]), object(3,S3,[X3,Y3])], [sbox(1,[0,0],[2,1]), sbox(1,[0,1],[1,2]), sbox(1,[1,2],[3,1]), sbox(2,[0,0],[3,1]), sbox(2,[0,1],[1,3]), sbox(2,[2,1],[1,1]), sbox(3,[0,0],[2,1]), sbox(3,[1,1],[1,2]), sbox(3,[-2,2],[3,1]), sbox(4,[0,0],[3,1]), sbox(4,[0,1],[1,1]), sbox(4,[2,1],[1,3]), sbox(5,[0,0],[2,1]), sbox(5,[1,1],[1,1]), sbox(5,[0,2],[2,1]), sbox(6,[0,0],[3,1]), sbox(6,[0,1],[1,1]), sbox(6,[2,1],[1,1]), sbox(7,[0,0],[3,2]), sbox(8,[0,0],[2,3])]).
The shapes are illustrated in the following picture:
geost/2
: three objects and eight shapes
A ground solution is shown in the following picture:
geost/2
: a ground solution
The following example shows how to encode in Rules “objects with oid 1, 2 and 3 must all be at least 2 units apart from objects with oid 4, 5 and 6”.
[ (origin(O1,S1,D) ---> O1^x(D)+S1^t(D)), (end(O1,S1,D) ---> O1^x(D)+S1^t(D)+S1^l(D)), (tooclose(O1,O2,S1,S2,D) ---> end(O1,S1,D)+2 #> origin(O2,S2,D) #/\ end(O2,S2,D)+2 #> origin(O1,S1,D)), (apart(O1,O2) ---> forall(S1,sboxes([O1^sid]), forall(S2,sboxes([O2^sid]), #\ tooclose(O1,O2,S1,S2,1) #\/ #\ tooclose(O1,O2,S1,S2,2)))), (forall(O1,objects([1,2,3]), forall(O2,objects([4,5,6]), apart(O1,O2))))].
The following example shows how to encode in Rules “objects 3 and 7 model rooms that must be adjacent and have a common border at least 1 unit long”.
[ (origin(O1,S1,D) ---> O1^x(D)+S1^t(D)), (end(O1,S1,D) ---> O1^x(D)+S1^t(D)+S1^l(D)), (overlap(O1,S1,O2,S2,D) ---> end(O1,S1,D) #> origin(O2,S2,D) #/\ end(O2,S2,D) #> origin(O1,S1,D)), (abut(O1,O2) ---> forall(S1,sboxes([O1^sid]), forall(S2,sboxes([O2^sid]), ((origin(O1,S1,1) #= end(O2,S2,1) #\/ origin(O2,S2,1) #= end(O1,S1,1)) #/\ overlap(O1,S1,O2,S2,2)) #\/ ((origin(O1,S1,2) #= end(O2,S2,2) #\/ origin(O2,S2,2) #= end(O1,S1,2)) #/\ overlap(O1,S1,O2,S2,1))))), (forall(O1,objects([3]), forall(O2,objects([7]), abut(O1,O2))))].