alice
library
manual.

The `FD` structure

^Synopsis^{____________________________________________}

    signature FD
    structure FD : FD

The FD structure provides access to finite domain variables and propagators.

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 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_MAX | AVAL_MED | AVAL_MIN
      val assign : space * intvar vector * avalsel -> unit
      val dom : space * intvar * domain -> unit
      datatype relation = EQ | GQ | GR | LE | LQ | NQ
      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 gcc :
         space * intvar vector * int vector * int vector * conlevel -> unit
      val countII :
         space * intvar vector * relation * int * relation * int -> unit
      val countVI :
         space * intvar vector * relation * intvar * relation * int -> unit
      val countIV :
         space * intvar vector * relation * int * relation * intvar -> unit
      val countVV :
         space * intvar vector * relation * 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
      val power : 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 * domain * 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
            val boolVal : space * boolvar -> bool
            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_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.
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.
gcc (s, xs, ls, us, 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. The ls give the lower bounds, so e.g. ls=#[1,3,1,0] says that the 0 must occur at least once, the 1 at least 3 times, the 2 at least once, and the 3 may not occur at all. The us are the corresponding upper bounds.
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.
power (s, x, y, z, level): Creates a propagator in s ensuring z is equal to x to the power of 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_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.

last modified 2005/Aug/03 09:17

alice library manual.

The FD structure

________ Synopsis ____________________________________________________

________ Import ______________________________________________________