GFD provides facilities to model and solve problems over the finite integer domain, with Gecode as the solver. It supports the constraints provided by Gecode – and Gecode supports a large set of constraints. The search to solve the problem can be done at the ECL^{i}PS^{e} level (with support from Gecode for variable and value selections), or the whole search can be performed by Gecode itself using one of its search engines.
Implementation-level differences (like Gecode’s re-computation based model vs. ECL^{i}PS^{e}’s backtracking model) are largely invisible to the user, as GFD automatically maintains the Gecode computational state to match ECL^{i}PS^{e}’s.
To load the GFD library into your program, simply add the following directive at an appropriate point in your code.
:- lib(gfd).
An (integer) domain variable is a variable which can be instantiated only to a value from a given finite set of integer values.
A variable becomes a domain variable when it first appears in a (GFD) constraint. If the constraint is a domain constraint, then the variable will be given the domain specified by the constraint. Otherwise, the variable will be given a default domain, which should be large enough for most problem instances.
The default domain is an interval, and the maximum and minimum values of this interval can be changed using gfd_set_default/2 (with the options interval_max and interval_min for the maximum and minimum values, respectively). You can also obtain the current values of interval_max and interval_min using gfd_get_default/2.
The Gecode documentation suggests that domain variables should be given as small a domain as possible, and requires the user to explicitly specify a domain for all domain variables. While this is not required by GFD, following Gecode’s convention is still a good idea, since overly large domains can negatively affect performance. It is therefore recommended to make use of domain constraints, and specify the domain for variables before using them in other constraints.
A domain variable is mapped into a Gecode IntVar
.
In GFD, as in IC, booleans (such as the boolean in reified constraints) are
normal domain variables with the domain [0,1]
. However, in Gecode,
boolean domain variables are a separate class BoolVar
. Boolean
domain variables are implemented in GFD by linking the integer
domain variable representing the boolean to an internal
BoolVar
in the Gecode solver state, and the user always access the
boolean via the integer domain variable.
GFD supports the (integer finite domain) constraints implemented by Gecode. Some of these constraints correspond to those in ECL^{i}PS^{e}’s native finite domain solvers (IC and FD), but many do not. For those that are implemented in IC and/or FD, the same name and syntax is used by GFD (although details may differ, such as the types allowed for arguments). See Table of Finite domain Constraints for the constraints supported by ECL^{i}PS^{e}’s finite domain solvers. In addition to propagating constraints at a unspecified or default level, Gecode also support three propagaion consistency levels. GFD map these consistency levels to four modules:
Constraints can be posted unqalified for the default consistency level, or explicitly qualified with the module name for the desired consistency level, e.g.
gfd_gac:alldifferent(Xs)
Alternatively, constraints can also be imported from one of the modules and then posted unqualified at the imported consistency level.
The default consistency level is supported for all constraints, but posting a constraint at the other three consistency levels is supported only if that consistency level is implemented for that constraint in Gecode – see the individual documentation for the constraints for details. Note that the three consistency modules are implicitly created when GFD is loaded, and do not need to be loaded explicitly.
Even constraints that involve expressions may be posted at specific consistency levels. In fact, a consistency level can be specified for any sub-expression within the expression. However, it is possible that some of the sub-constraints and sub-expressions inside the expressions are not supported at the given consistency level. In such cases, these sub-expressions will be posted at the default consistency level. Note that any sub-expressions with its own specified consistency level will also be factored out and posted separately.
For example, the N-Queens example
can post domain consistent versions of the #\=/2
constraints:
:- lib(gfd). queens_list(N, Board) :- length(Board, N), Board :: 1..N, (fromto(Board, [Q1|Cols], Cols, []) do ( foreach(Q2, Cols), param(Q1), count(Dist,1,_) do gfd_gac: (Q2 #\= Q1), gfd_gac: (Q2 - Q1 #\= Dist), gfd_gac: (Q1 - Q2 #\= Dist) ) ), labeling(Board).
In this particular example, using the stronger propagation actually results in a reduction in performance, as there is no reduction in search space from the stronger propagation, but an increase in the cost of doing the propagation,
Gecode maintains a solver state representing the problem, with the constraints and problem variables, and performs constraint propagation within this solver state. GFD adds the constraints and problem variables to this state as they are posted in the user program. Unlike the problem variables, there are no ECL^{i}PS^{e}level representation of the constraints. One consequence is that floundering – active constraints remaining at the end of computation – can only be determined from the solver state. GFD provides solver_constraints_number/1, and solver_vars_number/1 to obtain the current number of active constraints and problem variables, respectiviely, in the current solver state.
Unlike ECL^{i}PS^{e}’s native solvers, constraint propagation in Gecode must be triggered explicitly. In GFD, triggering propagation in the Gecode solver state is implemented as a demon goal gfd_do_propagate/1 at scheduling priority 9. When a constraint is posted, it is added to the solver state, and the propagate demon goal is scheduled for execution. It is thus possible to post multiple constraints without propagation by posting the constraints at a more urgent (i.e. numerically smaller) priority than 9 (see call_priority/2). This could reduce the cost of performing the propagation.
GFD’s constraints (and other predicates) follows several conventions for the format of its arguments. These are outlined in this section.
For arguments in constraints that are domain variables, the argument
can be supplied as an
array element using array notion (e.g. Array[1]
).
Non-domain variables will be turned into domain variables with the default
interval, and an integer can be given in place of a domain variable,
representing a domain variable with a singleton domain.
For arguments that are a group of variables or values, these are supplied as a collection (as used in collection_to_list/2). In some cases, the elements in the collection are required to be ordered, and for such cases, the ordering is with respect to the flattened form of the collection, with indexing starting at 1 for the first element. Array notation can again be used to supply a part of the array as a collection.
Indexing always start at 1 for ECL^{i}PS^{e}, which is different from Gecode, where index starts from 0. GFD maps between the two index conventions in various ways, depending on the constraint, with the aim of minimising the overhead. GFD also supports versions of these constraints that uses Gecode’s native indices, i.e. starting from 0, and these have an additional _g in their name (e.g. bin_packing_g/3 is the Gecode native index version of bin_packing/3). These versions of the constraint do not have the overhead of converting the index value, but may be incompatible with the rest of ECL^{i}PS^{e}.
In general, any collection argument can be supplied as a nested collection
(e.g. nested listed or multi-dimensional arrays). In some
cases, nested collections are required and supply information required
by the constraint, e.g.
the dimension in multi-dimensional bin-packing predicates. Also,
some predicates’ argument expect a two dimensional matrix, in which
case the argument must be supplied as a two dimensional collection
(list of lists, two dimensional array). A two dimensional collection is
organised in the standard ECL^{i}PS^{e}way, i.e. row-major order, as a
collection of rows, where each row having the same number of elements, and
each of these
element representing the column elements in that row. In array notation,
the row is addressed first, followed by the column, i.e.
[Row,Column]
.
The following domain constraints are supported by GFD:
::/2,3
are also supported as aliases.GFD supports expressions as arguments for relational and logical connective constraints. Expressions can either evaluate to an integer (integer expression) or a truth value (constraint expression). Integer and constraint expressions maps to Gecode’s LinIntExpr and BoolExpr, respectively. Unlike IC’s expressions, user-defined constraints are not allowed, but unrecognised ground terms in integer expressions are treated as arithmetic functions and evaluated.
All relational constraints have their reified counterparts, which has an extra boolean argument that specify if the constraint is entailed or not. Expressions in refied constraints are restricted to inlined (i.e. Gecode native) integer expressions.
The relational constraints are: #</2,3 (less than), #=/2,3 (equal), #=</2,3 (less than or equal to), #>/2,3 (greater than), #>=/2,3 (greater than or equal to), #\=/2,3 (not equal to).
The available connectives are:
<=>/2,3 (equivalent), =>/2,3 (implies), and/2,3 (and), or/2,3 (or), xor/2,3 (exclusive or), neg/1,2 (negation).
Boolean domain variables with domain [0,1] and constraints which can be reified can occur as an argument of a logical connective, i.e. as a constraint expression, evaluating to the reified truth value.
For compatibility with IC, #=/2 can be used instead of <=>/2 and #\=/2 can be used instead of xor.
Gecode also supports half reification as well as the normal
full reification for reified constraints. Half verification
is when the propagation is in one direction only across the logical
connective (i.e. =>
), rather than bi-directional (<=>
).
In GFD, constraints can be half reified as follows:
Boolean => Constraint Constraint => Boolean
where Constraint is the half reified constraint, written without its boolean argument Boolean. The two alternatives are for the two different direction of propagation.
The syntax for the expressions closely follows that in IC. The following can be used inside integer expressions:
X
is not yet a domain variable, it is turned
into one.Expr*Expr
.E1 = X^N
..
N is a positive integer. Differ from inroot in that
the result is only defined for integral root, and negative root not
excluded (non-inlined).IntCol
and ExprCol
must be the same size
(ExprCol non-inlined).Posted as a constraint, both the left- and right- hand arguments are inlined expressions (non-inlined).
Within the expression context, the constraint evaluates to its
reified truth value. If the constraint is entailed by the
state of the constraint store then the (sub-)expression
evaluates to 1
. If it is dis-entailed by the state of
the constraint store then it evaluates to 0
. If its
reified status is unknown then it evaluates to a boolean domain
variable 0..1
.
Note: The simple cases (e.g. Bool #= (X #> 5)
) are
equivalent to directly calling the reified forms of the basic
constraints (e.g. #>(X, 5, Bool)
).
Expr
. Provided for compatiblity
with ICand for constraint expressions:
X #> 3 and Y #< 8
.
E1 and E2 are constraint expressions.X #> 3 or Y #< 8
.
E1 and E2 are constraint expressions.X #> 3 xor Y #< 8
.
E1 and E2 are constraint expressions.X #> 3 => Y #< 8
.
E1 and E2 are constraint expressions.neg X #> 3
E is a constraint expressions.X #> 3 <=> Y #< 8
.
This is similar to #= used in an expression context.
E1 and E2 are constraint expressions.Reified relational constraint, both the left- and right- hand arguments are inlined integer expressions.
Expr
. Provided for compatibility
with IC.The expressions allowed by GFD are a super-set of the expressions supported by Gecode. The components not supported by Gecode are indicated by ‘non-inlined’ in the above description. When an expression is posted, it is parsed and broken down into expressions and/or logical connectives supported by Gecode, along with any constraints). This is done to allow the user greater freedom in the code they write, and also to provide better compatibility with IC.
Note that posting of complex expressions is relatively expensive: they are first parsed at the ECL^{i}PS^{e} level by GFD to extract the sub-expressions and any new domain variables, and these sub-expressions (in the form of ECL^{i}PS^{e} structures) are then parsed again at the GFD C++ level to convert them to the appropriate Gecode data structures, which are then passed to Gecode. Gecode itself will then convert these data structures to the basic constraints that it supports.
Unlike IC, GFD domain variables must have finite upper and lower bounds, and any arithmetic expression that evaluate to values outside these bounds will fail. In particular, auxillary variables created by GFD used to represent factored out subexpressions are given the default bounds, and this may lead to unexpected failures, e.g. assuming the default bounds was not changed, the following will fail:
A :: 0..10^9, A #= 10^8/1.
because division (/) is non-inlined and is factored our, and
10^8
is outside the default bounds.
These constraints impose some form of arithmetic relation between their arguments. Some of these constraints can occur inside expressions, while others are “primitive” versions of the constraint where the arguments are domain variables (or integers).
Bool
argument.Bool
argument.
Bool
argument.These constraints impose some form of ordering relation on their arguments.
These constraints impose restrictions either on the number of values that can be taken in one or more collections of domain variables, and/or on the positions of values in the collection.
These constraints deal with scheduling and/or allocation of resources.
In these constraints, the arguments represent a graph, and the constraint imposes some form of relation on the graph.
These are “user defined constraints” (also known as ad-hoc constraints), i.e. the allowable tuples of values for a collection of domain variables is defined as part of the constraint. These predicate differs in the way the allowable values are specified.
Constraints that don’t fit into the other categories.