# The FD structure

## ________ Synopsis ____________________________________________________

```    signature FD
structure FD : FD```

Finite domain variables are variables whose values are integers.

If a propagator is invoked, it tries to narrow the domains of the variables it is posted on. The amount of narrowing of domains depends on the operational semantics of the propagator. There are two main schemes for the operational semantics of a propagator. Domain propagation means that the propagator narrows the domains such that all values are discarded, which are not contained in a solution of the modeled constraint. But due to efficiency reasons, most propagators provide only interval propagation, i. e. only the bounds of domains are narrowed. Even faster to perform, but even less strict is value propagation, which is performed only when one of the variables is determined. Some propagators take a "consistency level" argument to determine the desired mode of operation.

## ________ Import ______________________________________________________

```    import signature FD from "x-alice:/lib/gecode/FD-sig"
import structure FD from "x-alice:/lib/gecode/FD"```

## ________ Interface ___________________________________________________

```signature FD =
sig
type space
type intvar
type boolvar
exception NotAssigned
type domain = (int*int) vector
exception InvalidDomain
val domainFromList : int list -> domain
val domainToList : domain -> int list
val intvar :  space * domain -> intvar
val intvarVec :  space * int * domain -> intvar vector
val range :  space * (int * int) -> intvar
val rangeVec :  space * int * (int * int) -> intvar vector
val boolvar :  space -> boolvar
val boolvarVec :  space * int -> boolvar vector
val intvar2boolvar : space * intvar -> boolvar
val boolvar2intvar : boolvar -> intvar
datatype avalsel = AVAL_MIN | AVAL_MED | AVAL_MAX
val assign : space * intvar vector * avalsel -> unit
val dom :  space * intvar * (int * int) vector -> unit
datatype relation =
EQ (* Equality         == *)
| NQ (* Disequality      != *)
| LQ (* Less or equal    <= *)
| LE (* Less             <  *)
| GQ (* Greater or equal >= *)
| GR (* Greater          >  *)
datatype conlevel =
BND | DEF | DOM | VAL
val rel  :  space * intvar * relation * intvar -> unit
val relI :  space * intvar * relation * int -> unit
val equal  : space * intvar * intvar * conlevel -> unit
val equalV : space * intvar vector * conlevel -> unit
val distinct : space * intvar vector * conlevel -> unit
val distinctOffset : space * (int * intvar) vector *
conlevel -> unit
val sortedness : space * intvar vector * intvar vector * conlevel -> unit
val permsort : space * intvar vector * intvar vector * intvar vector * conlevel -> unit
val gcc1 : space * intvar vector * int vector * int * int * int * int *
conlevel -> unit
val gcc2 : space * intvar vector * int vector * int * int * int * int *
int * conlevel -> unit
val gcc3 : space * intvar vector * int * conlevel -> unit
val gcc4 : space * intvar vector * int * int * conlevel -> unit
val gcc5 : space * intvar vector * intvar vector * int * int *
conlevel -> unit
val gcc6 : space * intvar vector * int vector * intvar vector * int *
int * bool * int * int * conlevel -> unit
val gcc7 : space * intvar vector * int vector * intvar vector * int *
int * int * bool * int * int * conlevel -> unit
val countII : space * intvar vector *
int * relation * int -> unit
val countVI : space * intvar vector *
intvar * relation * int -> unit
val countIV : space * intvar vector *
int * relation * intvar -> unit
val countVV : space * intvar vector *
intvar * relation * intvar -> unit
val element : space * intvar vector * intvar *
intvar -> unit
val elementI : space * int vector * intvar *
intvar -> unit
val lex : space * intvar vector * relation *
intvar vector -> unit
val nega  : space * boolvar * boolvar -> unit
val conj  : space * boolvar * boolvar * boolvar -> unit
val disj  : space * boolvar * boolvar * boolvar -> unit
val impl  : space * boolvar * boolvar * boolvar -> unit
val equi  : space * boolvar * boolvar * boolvar -> unit
val exor  : space * boolvar * boolvar * boolvar -> unit
val conjV : space * boolvar vector * boolvar -> unit
val disjV : space * boolvar vector * boolvar -> unit
val linear : space * (int * intvar) vector * relation *
int * conlevel -> unit
val min : space * intvar vector * intvar -> unit
val max : space * intvar vector * intvar -> unit
val abs : space * intvar * intvar * conlevel -> unit
val mult: space * intvar * intvar * intvar * conlevel -> unit
structure Reified :
sig
val intvar : space * domain * boolvar -> intvar
val intvarVec : space * int * domain * boolvar ->
intvar vector
val dom : space * intvar * (int * int) vector *
boolvar -> unit
val rel : space * intvar * relation * intvar *
boolvar -> unit
val relI : space * intvar * relation * int *
boolvar -> unit
val linear : space * (int * intvar) vector * relation *
int * boolvar * conlevel -> unit
end
structure Reflect :
sig
val min : space * intvar -> int
val max : space * intvar -> int
val med : space * intvar -> int
val value : space * intvar -> int (* NotAssigned *)
val boolVal : space * boolvar -> bool (* NotAssigned *)
val size : space * intvar -> int
val dom : space * intvar -> domain
val assigned : space * intvar -> bool
val range : space * intvar -> bool
end
datatype b_var_sel =
B_DEGREE_MAX
| B_DEGREE_MIN
| B_MAX_MAX
| B_MAX_MIN
| B_MIN_MAX
| B_MIN_MIN
| B_NONE
| B_REGRET_MAX_MAX
| B_REGRET_MAX_MIN
| B_REGRET_MIN_MAX
| B_REGRET_MIN_MIN
| B_SIZE_MAX
| B_SIZE_MIN
datatype b_val_sel =
B_MAX
| B_MED
| B_MIN
| B_SPLIT_MAX
| B_SPLIT_MIN
val branch : space * intvar vector * b_var_sel *
b_val_sel -> unit
end
```

## ________ Description _________________________________________________

type space

The type of first class comutational spaces. Usually equal to SPACE.space.

type intvar

The type of finite domain variables.

type boolvar

The type of boolean constraint variables. Fundamentally, they are FD variables constrained to the 0-1 domain.

exception NotAssigned

is raised when a reflection operation intended for determined values only is performed on a variable in a space where its domain is not yet narrowed to a single value.

type domain = (int*int) vector

The type of domain descriptions. Used to define variable bounds at variable creation or later, in value declaration, and reflection. It is an ordered, non-overlapping, non-contingous vector of ordered integer pairs. For example the set of all primes between 1 and 10 is #[(2,3),(5,5),(7,7)]
Observe that #[(1,2),(3,4)] is an invalid domain: contigous ranges, use #[(1,4)] instead
#[(1,3),(3,4)] is even more so.
#[(3,2)] is also invalid, the range is ill-defined.
#[(4,5),(1,2)] is nonconformant in pair ordering, #[(1,2),(4,5)] is fine.

exception InvalidDomain

Exception thrown by all variable creation and domain tell operations on receipt of a domain description not conforming to the above rules.

domainFromList l

Returns a valid domain description containing the same integers as l does.

domainToList d

Returns the list of integers that correspond to domain description d.

intvar (s, d)

Returns a fresh FD variable valid in s and all its descendents not originating from a child created earlier than the introduction of the variable.
The fresh variable is already constrained to be in d.

intvarVec (s, n, d)

Returns n FD variables freshly created in s. They are already constrained to be in d.

range (s, (min, max))

Returns an FD variable freshly created in s. It is already constrained to be between min and max, inclusive.

rangeVec (s, n, (min, max))

Returns n FD variables freshly created in s. They are already constrained to be between min and max, inclusive.

boolvar s

Returns true-false domain variable freshly created in s.

boolvarVec (s, n)

Returns n true-false domain variables freshly created in s.

intvar2boolvar (s, x)

Constrains x to the (0,1) range, and returns a boolvar tied to it with the obvious mapping 0:false, 1:true.

boolvar2intvar b

Returns an intvar in the 0-1 range tied to b with the mapping 0:false, 1:true.

datatype avalsel

Type to identify a value assignments strategy.
AVAL_MIN: Pick the smallest possible value.
AVAL_MAX: Pick the largest possible value.
AVAL_MED: Pick the median of the available values.

assign (s, v, strategy)

Determines all elements of v in s following the strategy provided.

dom (s, x, d)

Constrains x in s to the domain d.

datatype relation

Type to identify an arithmetic relation in constraints.
EQ: Equal.
NQ: Not equal.
LQ: Less or equal.
LE: Less.
GQ: Greater or equal.
GR: Greater.

datatype conlevel

Type to identify the eagerness of propagation. When the required level is not implemented for a propagator, the closest, stricter version is used.
DOM: Domain Proagatin. Strictest.
BND: Bounds Propagation.
VAL: Value Propagation. Most loose.

DEF: The default for the propagator.

rel (s, x, relation, y)

Creates a propagator to constrain x and y in s to be in the given relation.

relI (s, x, relation, n)

Constrains x in s to be in the given relation with the integer n.

equal (s, x, y, level)

Creates a propagator to constrain x and y in s to be equal.

equalV (s, v, level)

Creates a propagator to constrain all elements of v in s to be equal.

distinct (s, v, level)

Creates a propagator to constrain all elements of v in s to be different, pairwise non-equal.

distinctOffset (s, v, level)

Creates a propagator in s for the following: For all (ci,xi) and (cj,xj), xi+ci != xj+cj.

sortedness (s, xs, ys, level)

Creates a propagator in s that states that the ys are the sorted xs.

permsort (s, xs, ys, zs, level)

Creates a propagator in s that states that the ys are the sorted xs, and the zs are the corresponding permutation.

gcc1 (s,x,c,m,u,min,max,level)
gcc2 (s,x,c,m,ulow,uup,min,max,level)
gcc3 (s,x,u,level)
gcc4 (s,x,min,max,level)
gcc5 (s,x,c,min,max,level)
gcc6 (s,x,v,c,m,u,all,min,max,level)
gcc7 (s,x,v,c,m,ulow,uup,all,min,max,level)

Creates a propagator in s for the global cardinality constraint. This constraint generalises the distinct constraint in that it gives lower and upper bounds on the number of times a certain value may occur in x.

This constraint comes with seven different ways to specify its arguments.

countII (s, v, rel1, n, rel2, m level)
countVI (s, v, rel1, x, rel2, m level)
countIV (s, v, rel1, n, rel2, y level)
countVV (s, v, rel1, x, rel2, y level)

Creates a propagator in s for the following: The number of elements in v in rel1 with n (or x) is in rel2 with m (or y).
For example, There are exactly 5 non-zero elements of v:
countII (s, v, NQ, 0, EQ, 5 DEF)

element (s, v, x, y)
elementI (s, v, x, y)

Creates a propagator in s for the following: The xth element of v is y

lex (s, v1, rel, v2)

Creates a propagator in s for the following: v1 and v2 taken as strings of integers are lexographically oredered according to rel.

nega (s, b1, b2)

Creates a propagator in s ensuring b1 is the negation of b2. Observe that all consistency levels would result in the same algorithm for propagators operating on booleans only.

conj (s, b1, b2, b3)

Creates a propagator in s ensuring b3 is the conjunction of b1 and b2

disj (s, b1, b2, b3)

Creates a propagator in s ensuring b3 is the disjunction of b1 and b2

impl (s, b1, b2, b3)

Creates a propagator in s ensuring b3 is the implication from b1 to b2

equi (s, b1, b2, b3)

Creates a propagator in s ensuring b3 is the equivalence of b1 and b2

exor (s, b1, b2, b3)

Creates a propagator in s ensuring b3 is the non-equality of b1 and b2

conjV (s, v, b1)

Creates a propagator in s ensuring b1 is the conjunction of all elements in v.

disjV (s, v, b1)

Creates a propagator in s ensuring b1 is the disjunction of all elements in v.

linear (s, v, rel, n, level)

Creates a propagator in s for the following: Regard the elements of v as two-tier multiplications. The sum of all these multiplicants is in rel with n

min (s, v, x)

Creates a propagator in s ensuring x is equal to the smallest element of v.

max (s, v, x)

Creates a propagator in s ensuring x is equal to the largest element of v.

abs (s, x, y, level)

Creates a propagator in s ensuring y is equal to the absolute value of x.

mult (s, x, y, z, level)

Creates a propagator in s ensuring z is equal to x times y.

Reified.intvar (s, dom, b)

Returns an FD variable freshly created in s. Also, a propagator is created to ensure b is true if and only if the intvar returned is in dom.

Reified.intvarVec (s, n, dom, b)

Returns a vector of FD variables freshly created in s. Also, a propagator is created to ensure b is true if and only if all the intvars returned are in dom.

Reified.dom (s, x, dom, b)

Creates a propagator in s to ensure b is true if and only if x is in dom.

Reified.rel (s, x, rel, y, b) Reified.relI (s, x, rel, n, b)

Creates a propagator in s to ensure b is true if and only if x is in rel with y (or n).

Reified.linear (s, v, rel, n, b, level)

Creates a propagator in s to ensure b is true if and only if the regular linear constraint holds for the arguments.

Reflect.min (s, x)

Returns the smallest possible value in the current domain of x in s.

Reflect.max (s, x)

Returns the largest possible value in the current domain of x in s.

Reflect.med (s, x)

Returns the median of the possible values x may take in s.

Reflect.value (s, x)

Returns the value x takes in s. Throws NotAssigned if x is not determined.

Reflect.boolVal (s, b)

Returns the value b takes in s. Throws NotAssigned if b is not determined.

Reflect.size (s, x)

Returns the number of possible values x may take in s.

Reflect.dom (s, x)

Returns the current domain of x in s.

Reflect.assigned (s, x)

Returns true if x is determined to be a single value in s, false if not yet.

Reflect.range (s, x)

Returns true if the possible values x may take in s form a single, continuous range.

datatype b_var_sel

Identifies the variable selection strategy in branching.
B_DEGREE_MAX : Pick the variable involved in the most propagators.
B_DEGREE_MIN : Pick the variable involved in the fewest propagators.
B_MAX_MAX : Pick the variable with the largest upper bound.
B_MAX_MIN : Pick the variable with the smallest upper bound.
B_MIN_MAX : Pick the variable with the largest lower bound.
B_MIN_MIN : Pick the variable with the smallest lower bound.
B_NONE : Pick the leftmost undetermined variable.
B_REGRET_MAX_MAX : Pick the variable with largest max-regret. The max-regret of a variable is the difference between the largest and second-largest value still in the domain.
B_REGRET_MAX_MIN : Pick the variable with smallest max-regret. The max-regret of a variable is the difference between the largest and second-largest value still in the domain.
B_REGRET_MIN_MAX : Pick the variable with largest min-regret. The min-regret of a variable is the difference between the smallest and second-smallest value still in the domain.
B_REGRET_MIN_MIN : Pick the variable with smallest min-regret. The min-regret of a variable is the difference between the smallest and second-smallest value still in the domain.
B_SIZE_MAX : Pick the variable with the most possible values.
B_SIZE_MIN : Pick the variable with the fewest possible values. Also known as First Fail strategy.

datatype b_val_sel

Identifies the value selection strategy in branching.
B_MAX : Pick the largest possible value of the variable.
B_MIN : Pick the smallest possible value of the variable.
B_MED : Pick the median of all possible values of the variable.
B_SPLIT_MIN : Pick the lower half of the domain.
B_SPLIT_MAX : Pick the upper half of the domain.

branch (s, v, varStrategy, valStrategy)

Creates a new branching (aka distributor or labeling) in s over the variables in v following the given strategy.