Previous Up Next

7.2  Problem Modelling

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 ECLiPSe 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. ECLiPSe’s backtracking model) are largely invisible to the user, as GFD automatically maintains the Gecode computational state to match ECLiPSe’s.

7.2.1  Usage

To load the GFD library into your program, simply add the following directive at an appropriate point in your code.

:- lib(gfd).

7.2.2  Integer domain variables

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.

7.2.3  Constraints

GFD supports the (integer finite domain) constraints implemented by Gecode. Some of these constraints correspond to those in ECLiPSe’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 ECLiPSe’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:

gfd_gac
Domain consistent (Generalised Arc-Consistent), maps to ICL_DOM in Gecode.
gfd_bc
Bound consistent, maps to ICL_BND in Gecode.
gfd_vc
Value consistent, maps to ICL_VAL in Gecode.
gfd
Default consistency level, maps to ICL_DEF in Gecode.

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 ECLiPSelevel 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 ECLiPSe’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.

Constraint argument conventions

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 ECLiPSe, 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 ECLiPSe.

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 ECLiPSeway, 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].

Domain constraints

The following domain constraints are supported by GFD:

?Vars #:: ++Domain
Constrains Vars to have the domain Domain. A reified version is also available. ::/2,3 are also supported as aliases.

Arithmetic and logical expressions

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.

Relational Constraints
These specify an arithmetic relationship between two integer expressions. Constraint expressions are allowed as arguments of relational constraints, with the truth value of the expression treated as the integer value 1 (true) or 0 (false).

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).

Logical Connective constraints
Specifies a logical connection between constraint expression(s). . All logical connectives have their reified counterparts.

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
Variables. If X is not yet a domain variable, it is turned into one.
123
Integer constants.
-Expr
Sign change.
abs(Expr)
The absolute value of Expr.
E1+E2
Addition.
E1-E2
Subtraction.
E1*E2
Multiplication.
E1//E2
Integer division, truncating towards zero.
E1/E2
Division, defined only if E2 evenly divides E1 (non-inlined).
E1 rem E2
Integer remainder, same sign as E1.
Expr^N
Nth power. N is a positive integer. .
min(E1,E2)
Minimum.
max(E1,E2)
Maximum.
sqr(Expr)
Square. Logically equivalent to Expr*Expr.
rsqr(Expr)
Reverse of the sqr function. Differ from sqrt in that negative root is not excluded (non-inlined).
isqrt(Expr)
Integer square root (always positive). Truncated towards zero.
sqrt(Expr)
Square root, defined only if Expr is the square of an integer (non-inlined).
inroot(Expr,N)
Integer Nth root, N is a positive integer. Truncated to nearest smaller integer. For even N, result is the non-negative root.
rpow(Expr,N)
Reverse of exponentiation, i.e. find X in 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).
sum(ExprCol)
Sum of a collection of expressions (ExprCol non-inlined).
sum(IntCol*ExprCol)
Scalar product of a collection of integers and expressions. IntCol and ExprCol must be the same size (ExprCol non-inlined).
min(ExprCol)
Minimum of a collection of expressions (ExprCol non-inlined).
max(ExprCol)
Maximum of a collection of expressions (ExprCol non-inlined).
element(ExprIdx, Col)
Element constraint, Evaluate to the ExprIdx’th element of Col. ExprIdx can be an integer expression.
#>, #>=, #=, #=<, #<, #\=

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)).

ConLev:Expr
Post Expr at consistency level ConLev. Consistency levels are described in section 7.2.3.
eval(Expr)
Logically equivalent to Expr. Provided for compatiblity with IC
Functional/reified constraints
Reified constraints (whose last argument is a 0/1 variable) and functional constraints (whose last argument is an integer variable) can be written without their last argument within an expression context. The expression then effectively evaluates to the value of the missing (unwritten) argument. (non-inlined)

and for constraint expressions:

X
Boolean Variables. Domain variables with domain 0/1. If cariable is not yet a domain variable, it is turned into one.
1
truth value (0 for false, 1 for true).
E1 and E2
Reified constraint conjunction. e.g. X #> 3 and Y #< 8. E1 and E2 are constraint expressions.
E1 or E2
Reified constraint disjunction. e.g. X #> 3 or Y #< 8. E1 and E2 are constraint expressions.
E1 xor E2
Reified constraint exclusive disjunction/non-equivalence. e.g. X #> 3 xor Y #< 8. E1 and E2 are constraint expressions.
E1 => E2
Reified constraint implication. e.g. X #> 3 => Y #< 8. E1 and E2 are constraint expressions.
neg E
Reified constraint negation. e.g. neg X #> 3 E is a constraint expressions.
E1 <=> E2
Reified constraint equivalence. e.g. X #> 3 <=> Y #< 8. This is similar to #= used in an expression context. E1 and E2 are constraint expressions.
element(ExprIdx, BoolCol)
Element constraint, Evaluate to the ExprIdx’th element of BoolCol. ExprIdx can be an inlined integer expression. BoolCol is a collection of boolean values or domain variable.
#>, #>=, #=, #=<, #<, #\=

Reified relational constraint, both the left- and right- hand arguments are inlined integer expressions.

ConLev:Expr
Post Expr at consistency level ConLev. Consistency levels are described in section 7.2.3.
eval(Expr)
Logically equivalent to Expr. Provided for compatibility with IC.
Reified constraints
Reified constraints (whose last argument is a 0/1 variable) can be written without their last argument within an expression context. The expression then effectively evaluates to the value of the missing (unwritten) argument. (non-inlined)

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 ECLiPSe level by GFD to extract the sub-expressions and any new domain variables, and these sub-expressions (in the form of ECLiPSe 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.

Arithmetic constraints

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).

all_eq(?Collection,?Y)
Constrains each element of Collection to be equal to Y. Similar constraints for the other relations: all_ge/2) (greater than or equal to), all_gt/2 (greater than), all_le/2 (less than or equal to), all_lt/2 (less than), and all_ne/2 (not equal).
max(+Collection,?Max)
Constrains Max to be the maximum of the values in Collection. Similarly, min(+Collection,?Min) for minimum.
max_index(+Collection,?Index)
Constrains Index to be the the index(es) of the variable(s) with the maximum of the values in Collection. Similarly, min_index(+Collection,?Index)
max_index(+Collection,?Index)
Constrains Index to be the the index(es) of the variable(s) with the maximum of the values in Collection. Similarly, min_index(+Collection,?Index) for minimum.
max_first_index(+Collection,?Index)
Constrains Index to be the the index of the first variable with the maximum of the values in Collection. Similarly, min_first_index(+Collection,?Index) for minimum.
mem(+Vars,?Member [,?Bool])
Constrains Member to be the a member element in Vars. The reified version has the Bool argument.
scalar_product(++Coeffs,+Collection,+Rel,?Sum [,?Bool])
Constrains the scalar product of the elements of Coeffs and Collection to satisfy the relation sum(Coeffs*Collection) Rel P. Reified with Bool argument.
sum(+Collection,?Sum)
Constrains Sum to be the sum of the elements in Collection, or if the argument is of the form IntCollection*Collection, the scalar product of the connections.
sum(+Collection,+Rel,?Sum [,?Bool]
Constrains the sum of the elements of Collection to satisfy the relation sum(Collection) Rel Sum. Reified with Bool argument.

Ordering constraints

These constraints impose some form of ordering relation on their arguments.

lex_eq(+Collection1,+Collection2)
Constrains Collection1 to be lexicographically equal to Collection2. Constraints for the other lexicographic relations: lex_ge/2 (lexicographically greater or equal to), lex_gt/2 (lexicographically greater than), lex_le/2 (lexicographically less or equal to), lex_lt/2, (lexicographically less than), lex_neq/2 (lexicographically not equal to).
ordered(+Relation,+Collection)
Constrains Collection to be ordered according to Relation.
precede(++Values,+Collection)
Constrains each value in Values to precede its succeeding value in Collection.
precede(+S,+T,+Collection)
Constrains S to precede T in Collection.
sorted(?Unsorted, ?Sorted)
Sorted is a sorted permutation of Unsorted.
sorted(?Unsorted, ?Sorted, ?Positions)
Sorted is a sorted permutation (described by Positions) of Unsorted.

Counting and data constraints

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.

alldifferent(+Vars)
Constrains all elements of Vars are different.
alldifferent_cst(+Vars,++Offsets)
Constrains the values of each element plus corresponding offset to be pairwise different.
among(+Values, ?Vars, +Rel, ?N)
The number of occurrences (Occ) in Vars of values taken from the set of values specified in Values satisfies the relation Occ Rel N.
atleast(?N, +Vars, +V)
At least N elements of Vars have the value V. Similarly atmost(?N, +Vars, +V).
count(+Value, ?Vars, +Rel, ?N)
Constrains the number of occurrences of Value in Vars (Occ) to satisfy the relation Occ Rel N.
count_matches(+Values, ?Vars, +Rel, ?N)
The number of the elements in Vars that match their corresponding value in Values, Matches, satisfies the relation Matches Rel N.
element(?Index, +Collection, ?Value)
Constrains Value to be the Indexth element of the integer collection Collection.
gcc(+Bounds,+Vars)
Constrains the number of occurrences of each Value in Vars according to the specification in Bounds (global cardinality constraint).
nvalues(+Collection, +Rel, ?Limit)
Constrains N, the number of distinct values occurring in Collection to satisfy the relation N Rel Limit.
occurrences(+Value,+Vars,?N)
Constrains the value Value to occur N times in Vars.
sequence(+Low,+High,+K,+Vars,++Values)
The number of values taken from Values is between Low and High for all sequences of K variables in Vars. There is also a version for binary (0/1) variables: sequence(+Low,+High,+K,+ZeroOnes).

Resource and scheduling constraints

These constraints deal with scheduling and/or allocation of resources.

bin_packing(+Items,++ItemSizes,+BinLoads)
The one-dimensional bin packing constraint with loads: packing M items into N bins, each bin having a load specified in BinLoads.
bin_packing(+Items,++ItemSizes,+N,+BinSize)
The one-dimensional bin packing constraint: packing M items into N bins of size BinSize.
bin_packing_md(+Items,++ItemMDSizes,+BinMDLoads)
The multi-dimensional bin packing constraint with loads: packing M L-Dimensional items into N L-Dimensional bins, each bin having a load in each dimension. The dimension L is implicitly specified in ItemMDSizes and BinMDLoads.
bin_packing_md(+Items,++ItemMDSizes,+N,+BinMDSize)
The multi-dimensional bin packing constraint loads: packing M L-Dimensional items into N L-Dimensional bins, each bin having a size in each dimension. The dimension L is implicitly specified in ItemMDSizes and BinMDSize.
cumulative(+Starts,+Durations,+Usages,+ResourceLimit)
Single-resource cumulative task scheduling constraint. A version with optional tasks is also available: cumulative_optional(+StartTimes, +Durations, +Usages, +ResourceLimit, +Scheduled).
cumulatives(+Starts,+Durations,+Heights,+Assigned,+Capacities)
Multi-resource cumulatives constraint on specified tasks.
cumulatives_min(+Starts,+Durs,+Heights,+Assgn,+Mins)
Multi-resource cumulatives constraint on specified tasks with required minimum resource consumptions.
disjoint2(+Rectangles)
Constrains the position (and possibly size) of the rectangles in Rectangles so that none overlap. A version where placement of rectangles is optional is disjoint2_optional(+Rectangles).
disjunctive(+StartTimes, +Durations)
Constrains the tasks with specified start times and durations to not overlap in time. A version with optional tasks is also available: disjunctive_optional(+StartTimes, +Durations, +Scheduled).

Graph constraints

In these constraints, the arguments represent a graph, and the constraint imposes some form of relation on the graph.

circuit(+Succ)
Constrains elements in Succ to form a Hamiltonian circuit. A version allowing constant offsets is circuit_offset(+Succ,+Offset).
circuit(+Succ,++CostMatrix,?Cost)
Constrains elements in Succ to form a Hamiltonian circuit, with Cost being the cost of the circuit, based on the edge cost matrix CostMatrix. A version allowing constant offsets is circuit_offset(+Succ,+Offset,++CostMatrix,?Cost).
circuit(+Succ,++CostMatrix,+ArcCosts,?Cost)
Constrains elements in Succ to form a Hamiltonian circuit. ArcCosts are the costs of the individual hops, and Cost their sum, based on the edge cost matrix CostMatrix. A version with constant offsets is available as circuit_offset(+Succ,+Offset,++CostMatrix,+ArcCosts,?Cost),
ham_path(?Start,?End,+Succ)
Constrains elements in Succ to form a Hamiltonian path from Start to End. A version with constant offsets is available as ham_path_offset(?Start,?End,+Succ,+Offset).
ham_path(?Start,?End,+Succ,++CostMatrix,?Cost)
Constrains elements in Succ to form a Hamiltonian path from Start to End, with Cost being the cost of the path, based on the edge cost matrix CostMatrix. A version with constant offsets is available as ham_path_offset(?Start, ?End, +Succ, +Offset, ++CostMatrix, ?Cost).
ham_path(?Start,?End,+Succ,++CostMatrix,+ArcCosts,?Cost)
Constrains elements in Succ to form a Hamiltonian path from Start to End. ArcCosts are the costs of the individual hops, and Cost their sum, based on the edge cost matrix CostMatrix. A version with constant offsets is available as ham_path_offset(?Start, ?End, +Succ, +Offset, ++CostMatrix, +ArcCosts, ?Cost).
inverse(+Succ,+Pred)
Constrains elements of Succ to be the successors and Pred to be the predecessors of nodes in a digraph. A version with offsets is also available: inverse(+Succ,+SuccOffset,+Pred,+PredOffset).

Extensional constraints

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.

regular(+Vars, ++RegExp)
Constrains Vars’ solutions to conform to that defined in the regular expression RegExp.
table(+Vars, ++Table)
Constrain Vars’ solutions to be those defined by the tuples in Table. The variant table(+Vars, ++Table, +Option) allows the specification of the algorithm used.
extensional(+Vars, ++Transitions, +Start, +Finals)
Constrain Vars’ solutions to conform to the finite-state automaton specified by Transitions with start state Start and final states Finals.

Other constraints

Constraints that don’t fit into the other categories.

bool_channeling(?Var, +DomainBools, +Min)
Channel the domain values of Vars to the 0/1 boolean variables in DomainBools.
integers(+Vars)
Pseudo constraint (i.e. no constraint will be posted in Gecode): Vars’ domain is the integer numbers (within default bounds).

Previous Up Next