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 \{0,1,9,10\}. 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}.

\underline{x},\overline{x}

Let S denote the current constraint store and x a finite domain integer.\underline{x} denotes the largest integer such that S \models x \geq \underline{x} holds. Analogously, \overline{x} denotes the smallest integer such that S \models x \leq \overline{x} holds.

\lfloor n \rfloor$, $\lceil n \rceil

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

sum

{FD.sum *Dv +A *D}

creates a propagator for

1*{\tt D}_1+\ldots+1*{\tt D}_n+(-1)*{\tt D}\;\sim_{{\tt A}}\;0

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:

{\tt I}_1*{\tt D}_1+\ldots+{\tt I}_n*{\tt D}_n+(-1)*{\tt D}\;\sim_{{\tt A}}\;0

Let {\tt D}_{n+1} be D and {\tt I}_{n+1} be -1. Then, the operational semantics is defined as follows. For each product {\tt I}_k*{\tt D}_k, an isolation (projection) is computed:

 {\tt I}_k*{\tt D}_k \;\sim_{{\tt A}}\; \underbrace{- \sum_{i = 1, i \neq k}^{n+1}
{\tt I}_i * {\tt D}_i}_{{\mbox{\sl RHS}}_k}.

For the right hand side {\mbox{\sl RHS}}_k, the upper \overline{\mbox{\mbox{\sl RHS}}_k} and lower limit \underline{\mbox{\mbox{\sl RHS}}_k} are defined as follows.

 ~$~
\begin{eqnarray*}
\overline{\mbox{\mbox{\sl RHS}}_k} \ =\
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\underline{{\tt D}}_i \;-\; 
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\overline{{\tt D}}_i 
\\
\underline{\mbox{\mbox{\sl RHS}}_k} \ = \
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\overline{{\tt D}}_i \;-\; 
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\underline{{\tt D}}_i
\end{eqnarray*}
~$~

These values are used to narrow the domain of {\tt D}_k 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.

{\tt D}_k \leq \left \lfloor  \frac{\overline{{\mbox{\sl RHS}}_k}}{{\tt I}_k}
\right \rfloor \quad 
\mbox{ if\ } {\tt I}_k > 0

{\tt D}_k \geq \left \lceil  \frac{\overline{{\mbox{\sl RHS}}_k}}{{\tt I}_k} \right \rceil \quad
\mbox{ if\ } {\tt I}_k < 0

Here x\leq n denotes the basic constraint x \in
\{0,\ldots,n\} and x \geq n denotes the basic constraint x \in
\{n,\ldots,\codeinline{oz}{FD.sup}\}.

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

\sum_{i =1, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\overline{{\tt D}}_i \;+\;
\sum_{i =1, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\underline{{\tt D}}_i 
\leq 0

As an example consider

- Y =<: Z - V

We have the following narrowing.

\codeinline{oz}{X} \leq \overline{\codeinline{oz}{Z}} - \underline{\codeinline{oz}{V}} + \overline{\codeinline{oz}{Y}}
\quad \quad
\codeinline{oz}{Y} \geq \underline{\codeinline{oz}{X}} - \overline{\codeinline{oz}{Z}} + \overline{\codeinline{oz}{V}}
\quad \quad
\codeinline{oz}{Z} \geq \underline{\codeinline{oz}{X}} - \overline{\codeinline{oz}{Y}} + \underline{\codeinline{oz}{V}}
\quad\quad
\codeinline{oz}{V} \leq \overline{\codeinline{oz}{Z}} - \underline{\codeinline{oz}{X}} + \overline{\codeinline{oz}{Y}}

The propagator ceases to exist if \overline{\codeinline{oz}{X}} - \underline{\codeinline{oz}{Y}}
\leq \underline{\codeinline{oz}{Z}} - \overline{\codeinline{oz}{V}} holds.

'>=:'

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

{\tt I}_1*{\tt D}_1+\ldots+{\tt I}_n*{\tt D}_n+(-1)*{\tt D}\;\geq\;0

is equivalent to

(-{\tt I}_1)*{\tt D}_1+\ldots+(-{\tt I}_n)*{\tt D}_n+1*{\tt D}\;\leq\;0

Alternatively, \underline{\mbox{\mbox{\sl RHS}}_k} 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 {\tt D}_k. Then, {\mbox{\sl RHS}}_k denotes a unique integer value which is discarded from the domain of {\tt D}_k.

Additional propagation is achieved through the realization of coreferences, i. e. equality between variables. If the store S entails (without loss of generality) {\tt D}_1 = {\tt D}_2, the generic propagator evolves into:

({\tt I}_1 + {\tt I}_2) * {\tt D}_2 + \ldots +
{\tt I}_n*{\tt D}_n+(-1)*{\tt D}\;\sim_{{\tt A}}\;0

sumCN

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

creates a propagator for

{\tt I}_1*{\tt D}_{11}*\ldots*{\tt D}_{1m_1}+\ldots+{\tt I}_n*{\tt D}_{n1}*\ldots*{\tt D}_{nm_n}+
(-1)*{\tt D}\;\sim_{{\tt A}}\;0

Let {\tt D}_{(n+1)1} be D, {\tt I}_{n+1} be -1, and m_{n+1} be 1. Then, the operational semantics is defined as follows. For k, 1
\leq k \leq n+1, an isolation (projection) is computed:

{\tt I}_{k}*{\tt D}_{k1}*\ldots*{\tt D}_{km_k} \;\sim_{{\tt A}}\; \underbrace{- {\sum_{i = 1, i \neq k}^{n+1}
{\tt I}_i * \prod_{j=1}^{m_i}{\tt D}_{ij}}}_{{\mbox{\sl RHS}}_k}

For the right hand side {\mbox{\sl RHS}}_k, the upper \overline{\mbox{\mbox{\sl RHS}}_k} and lower limit \underline{\mbox{\mbox{\sl RHS}}_k} are defined as follows.

~$~
\begin{eqnarray*}
\overline{\mbox{\mbox{\sl RHS}}_k} \ =\
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\underline{{\tt D}}_{ij} \;-\;
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\overline{{\tt D}}_{ij}
\\
\underline{\mbox{\mbox{\sl RHS}}_k} \ = \ 
-\sum_{i =1, i\neq k, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\overline{{\tt D}}_{ij} \;-\;
\sum_{i =1, i\neq k, {\tt I}_i < 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\underline{{\tt D}}_{ij}
\end{eqnarray*}
~$~

These values are used to narrow the domain of {\tt D}_{kl}, 1 \leq l
\leq m_k, 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.

{\tt D}_{kl} \leq \left \lfloor  \frac{\overline{\mbox{\sl RHS}}_k}{{\tt I}_k * \prod_{j=1,
j\neq l}^{m_k} \underline{{\tt D}}_{kj}} \right \rfloor \quad
\mbox{ if\ } {\tt I}_k > 0

{\tt D}_{kl} \geq \left \lceil  \frac{\overline{\mbox{\sl RHS}}_k}{{\tt I}_k * \prod_{j=0,
j\neq l}^{m_k} \overline{{\tt D}}_{kj}} \right \rceil \quad
\mbox{ if\ } {\tt I}_k < 0

Here x\leq n denotes the basic constraint x \in
\{0,\ldots,n\} and x \geq n denotes the basic constraint x \in
\{n,\ldots,\codeinline{oz}{FD.sup}\}.

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

\sum_{i =1, {\tt I}_i > 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\overline{{\tt D}}_{ij} + 
\sum_{i =1, {\tt I}_{i} < 0}^{n+1} {\tt I}_i *
\prod_{j=1}^{m_i}\underline{{\tt D}}_i 
\leq 0

As an example consider

3*X*- Z =<: A

We have the following formulas.

\codeinline{oz}{X} \leq \left\lfloor \frac{\overline{\codeinline{oz}{A}} +
\overline{\codeinline{oz}{Z}}}{3*\underline{\codeinline{oz}{Y}}} \right\rfloor 
\quad \quad
\codeinline{oz}{Y} \leq \left\lfloor \frac{\overline{\codeinline{oz}{A}} +
\overline{\codeinline{oz}{Z}}}{3*\underline{\codeinline{oz}{X}}} \right\rfloor
\quad \quad
\codeinline{oz}{Z} \geq \underline{\codeinline{oz}{X}} *\overline{\codeinline{oz}{Y}} - \overline{\codeinline{oz}{A}}
\quad \quad
\codeinline{oz}{A} \geq \underline{\codeinline{oz}{X}} *\overline{\codeinline{oz}{Y}} - \overline{\codeinline{oz}{Z}}

The propagator ceases to exist if 3*\overline{\codeinline{oz}{X}}*\overline{\codeinline{oz}{Y}} -
\underline{\codeinline{oz}{Z}} \leq \underline{\codeinline{oz}{A}} holds.

'>=:'

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

{\tt I}_1*{\tt D}_{11}*\ldots*{\tt D}_{1k_1}+\ldots+{\tt I}_n*{\tt D}_{n1}*\ldots*{\tt D}_{nk_n}+(-1)*{\tt D}_{(n+1)1}\;\leq\;0

is equivalent to

(-{\tt I}_1)*{\tt D}_{11}*\ldots*{\tt D}_{1k_1}+\ldots+(-{\tt I}_n)*{\tt D}_{n1}*\ldots*{\tt D}_{nk_n}+1*{\tt D}_{(n+1)1}\;\geq\;0

Alternatively, \underline{\mbox{\mbox{\sl RHS}}_k} 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 D_{kl}. Then, {\mbox{\sl RHS}}_k denotes a unique integer, and if

\frac{{\mbox{\sl RHS}}_k}{{\tt I}_k * \prod_{j=1,
j\neq l}^{m_k} {{\tt D}}_{kj}}

denotes an integer value, this value is discarded from the domain of {\tt D}_{kl}.

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

* 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:

|{\tt Iv} * {\tt Dv}| = |{\tt I}_1*{\tt D}_1 + \ldots +
{\tt I}_n*{\tt D}_n|\;\sim_{{\tt A}}\;{\tt D}

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

 {\tt Iv} * {\tt Dv} \sim_{{\tt A}} D \;\wedge\; (-{\tt Iv})*{\tt Dv}
\sim_{{\tt A}} D

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

{\tt Iv} * {\tt Dv} \sim_{{\tt A}} D \;\vee\; (-{\tt Iv})*{\tt Dv}
\sim_{{\tt A}} D

where the disjunction is realized by constructive disjunction.

sumACN

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

creates a propagator for

|{\tt I}_1*{\tt D}_{11}*\ldots*{\tt D}_{1k_1}+\ldots+{\tt I}_n*{\tt D}_{n1}*\ldots*{\tt D}_{nk_n}|\;\sim_{{\tt A}}\;{\tt D}

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)