5.7 Generic Propagators

The generic propagators FD.sum, FD.sumC and FD.sumCN do interval propagation. The propagators FD.sumAC and FD.sumACN do interval propagation but may also cut holes into domains. For example,

{FD.dom 0#10 [X Y]}{FD.sumAC [1 ~1] [X Y] '>:' 8}

will reduce the domains of X and Y to . Except for propagators FD.sumCN and FD.sumACN, equality is exploited, e. g. {FD.sumC [2 3] [A A] '=:' 10} is equivalent to {FD.sumC [5] [A] '=:' 10}.

,

Let S denote the current constraint store and x a finite domain integer. denotes the largest integer such that holds. Analogously, denotes the smallest integer such that holds.

Let n denote a real number. denotes the largest integer which is equal or smaller than n. Analogously, denotes the smallest integer which is equal or larger than n.

sum

{FD.sum *Dv +A *D}

creates a propagator for

For the operational semantics see FD.sumC. For the relation symbol '\\=:', the propagator waits until at most one non-determined variable is left. Then the appropriate value is discarded from the variable's domain. For the other relations, the propagator does interval propagation.

sumC

{FD.sumC +Iv *Dv +A *D}

creates a propagator for the scalar product of the vectors Iv and Dv:

Let be D and be -1. Then, the operational semantics is defined as follows. For each product , an isolation (projection) is computed:

For the right hand side , the upper and lower limit are defined as follows.

These values are used to narrow the domain of  until a fixed point is reached. We describe the propagation for the different possible values of A.

'=<:'

Narrowing is done according to the following inequalities.

Here denotes the basic constraint and denotes the basic constraint .

The propagator ceases to exist, if the following condition holds.

As an example consider

X - Y =<: Z - V

We have the following narrowing.

The propagator ceases to exist if holds.

'>=:'

This case can be reduced to =<: due to the observation that

is equivalent to

Alternatively, can be used for the definition.

'<:'

Analogous to '=<:'

'>:'

Analogous to '>=:'

'=:'

In this case, the operational semantics is defined by conjunction of the formulas given for =<: and >=:. Furthermore, coreferences are realized in that, e. g. the propagator 3*X=:3*Y tells the basic constraint X=Y.

'\\=:'

In this case, the propagator waits until at most one non-determined variable is left, say . Then, denotes a unique integer value which is discarded from the domain of .

Additional propagation is achieved through the realization of coreferences, i. e. equality between variables. If the store S entails (without loss of generality) , the generic propagator evolves into:

sumCN

{FD.sumCN +Iv *Dvv +A *D}

creates a propagator for

Let be D, be -1, and be 1. Then, the operational semantics is defined as follows. For , an isolation (projection) is computed:

For the right hand side , the upper and lower limit are defined as follows.

These values are used to narrow the domain of  until a fixed point is reached. We describe the propagation for the different possible values of A.

'=<:'

The narrowing is done according to the following inequalities.

Here denotes the basic constraint and denotes the basic constraint .

The propagator ceases to exist, if the following condition holds.

As an example consider

3*X*Y - Z =<: A

We have the following formulas.

The propagator ceases to exist if holds.

'>=:'

This case can be reduced to '=<:' due to the observation that

is equivalent to

Alternatively, can be used for the definition.

'<:'

Analogous to '=<:'

'>:'

Analogous to '>=:'

'=:'

In this case, the operational semantics is defined by conjunction of the formulas given for '=<:' and '>=:'.

'\\=:'

In this case, the propagator waits until at most one non-determined variable is left, say . Then, denotes a unique integer, and if

denotes an integer value, this value is discarded from the domain of .

Coreferences are not exploited for nonlinear generic constraints. The only exception is the expression

X * X =: Y

which has the same operational semantics as {FD.times X X Y} (but note that the occurring variables are not automatically constrained to finite domain integers).

sumAC

{FD.sumAC +Iv *Dv +A *D}

creates a propagator for the absolute value of the scalar product of the vectors Iv and Dv:

The operational semantics is as follows. If A is '<:', '=<:' or '\\=:', the following definition holds.

If A is '>:', '>=:' or '=:', the following definition holds.

where the disjunction is realized by constructive disjunction.

sumACN

{FD.sumACN +Iv *Dvv +A *D}

creates a propagator for

The operational semantics is defined analogously to FD.sumAC.

sumD

{FD.sumD *Dv +A *D}

creates a propagator analogous to FD.sum but performs domain-consistent propagation. Note that only equality (A is '=:') and disequality (A is '\\=:') are supported, as for inequalities domain and bounds propagation are equivalent.

sumCD

{FD.sumCD +Iv *Dv +A *D}

creates a propagator analogous to FD.sumC but performs domain-consistent propagation. Note that only equality (A is '=:') and disequality (A is '\\=:') are supported, as for inequalities domain and bounds propagation are equivalent.

Denys Duchier, Leif Kornstaedt, Martin Homik, Tobias Müller, Christian Schulte and Peter Van Roy
Version 1.4.0 (20080702)