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

last modified 2007/Mar/30 17:10

alice library manual.

The FD structure

________ Synopsis ____________________________________________________

________ Import ______________________________________________________