alice
library
manual.

Alice Project

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 non-negative 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. For some propagators, there is an operational semantics in between both schemes.

A propagator ceases to exist if all the variables it is posted on are determined. In the following sections, only exceptions from this rule are mentioned, i. e. if the propagator ceases to exist earlier. For example, FD.lessEq(x, y) ceases to exist if the current upper bound of x is smaller than or equal to the current lower bound of y.

Note that every propagator creation can raise a Tell exception if it is performed on toplevel and the constraint is inconsistent with other constraints.

See also: FS, Linear


________ Import ______________________________________________________

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

________ Interface ___________________________________________________

     signature FD =
     sig
	type fd
	type bin = fd

	exception Tell of {cause : exn}
	    
	datatype domain_element =
	    SINGLE of int
	  | RANGE  of int * int
	    
	type domain = domain_element vector
	    
	datatype relation =
	    LESS
	  | LESSEQ
	  | EQUAL
	  | NOTEQUAL
	  | GREATER
	  | GREATEREQ

	datatype dist_mode =
	    NAIVE
	  | FIRSTFAIL
	  | SPLIT_MIN
	  | SPLIT_MAX
	  | NBSUSPS

	datatype assign =
	    MIN
	  | MID
	  | MAX
	    
	(* Implementation dependent fd limits *)
	val inf : int
	val sup : int

	(* Allocation Functions *)
	val fd : domain option -> fd (* Domain, Overflow *)
	val fdVec : int * domain -> fd vector (* Domain, Overflow *)
	val range : int * int -> fd (* Domain, Overflow *)
	val rangeVec : int * (int * int) -> fd vector (* Domain, Overflow *)
	val bin : unit -> bin
	val binVec : int -> bin
	    
	(* Assignment *)
	val assign : assign * fd vector -> unit

	(* Conversion *)
	val toInt : fd -> int
	val future : fd -> int
	val fromInt : int -> fd
	val isBin : fd -> bool

	(* Standards Sums *)
	val sum : fd vector * relation * fd -> unit
	val sumC : (int * fd) vector * relation * fd -> unit
	val sumAC : (int * fd) vector * relation * fd -> unit
	val sumCN : (int * fd vector) vector * relation * fd -> unit
	val sumACN : (int * fd vector) vector * relation * fd -> unit
	val sumD : fd vector * relation * fd -> unit
	val sumCD : (int * fd) vector * relation * fd -> unit

	(* Standard Propagators; Interval propagation *)
	val plus : fd * fd * fd -> unit (* X + Y =: Z *)
	val minus : fd * fd * fd -> unit (* X - Y =: Z *)
	val times : fd * fd * fd -> unit (* X * Y =: Z *)
	val power : fd * int * fd -> unit (* pow(X, I) =: Z *)
	val divI : fd * int * fd -> unit (* X divI I =: Z *)
	val modI : fd * int * fd -> unit (* X modI I =: Z *)

	(* Standard Propagators; Domain propagation *)
	val plusD : fd * fd * fd -> unit (* X + Y =: Z *)
	val minusD : fd * fd * fd -> unit (* X - Y =: Z *)
	val timesD : fd * fd * fd -> unit (* X * Y =: Z *)
	val divD : fd * int * fd -> unit (* X divD I =: Z *)
	val modD : fd * int * fd -> unit (* X modD I =: Z *)

	val min : fd * fd * fd -> unit (* min(X, Y) =: Z *)
	val max : fd * fd * fd -> unit (* max(X, Y) =: Z *)

	val equal : fd * fd -> unit (* X =: Y *)
	val notequal : fd * fd -> unit (* X \=: Y *)
	val distance : fd * fd * relation * fd -> unit
	val less : fd * fd -> unit (* X <: Y *)
	val lessEq : fd * fd -> unit (* X <=: Y *)
	val greater : fd * fd -> unit (* X >: Y *)
	val greaterEq : fd * fd -> unit (* X >=: Y *)
	val disjoint : fd * int * fd * int -> unit
	val disjointC : fd * int * fd * int * bin -> unit
	val tasksOverlap : fd * int * fd * int * bin -> unit

	(* Non-Linear Propagators *)
	val distinct : fd vector -> unit
	val distinctOffset : (fd * int) vector -> unit
	val distinct2 : ((fd * int) * (fd * int)) vector -> unit
	val atMost : fd * fd vector * int -> unit
	val atLeast : fd * fd vector * int -> unit
	val exactly : fd * fd vector * int -> unit
	val element : fd * int vector * fd -> unit

	(* 0/1 Propagators *)
	val conj : bin * bin * bin -> unit
	val disj : bin * bin * bin -> unit
	val exor : bin * bin * bin -> unit
	val nega : bin * bin -> unit
	val impl : bin * bin * bin -> unit
	val equi : bin * bin * bin -> unit

	(* Reified Constraints *)
	structure Reified :
	    sig
		(* Reified Variable is returned *)
		val fd : domain * bin -> fd (* Domain, Overflow *)
		(* Reified Vector of Variables is returned *)
		val fdVec : int * domain * bin -> fd vector (* Domain, Overflow *)
		(* Same as in Oz *)
		val card : int * bin vector * int * bin -> unit
		val distance : fd * fd * relation * fd * bin -> unit
		val sum : fd vector * relation * fd * bin -> unit
		val sumC : (int * fd) vector * relation * fd * bin -> unit
		val sumAC : (int * fd) vector * relation * fd * bin -> unit
		val sumCN : (int * fd vector) vector * relation * fd * bin -> unit
		val sumACN : (int * fd vector) vector * relation * fd * bin -> unit
	    end

	(* Reflection *)
	structure Reflect :
	    sig
		val min : fd -> int
		val max : fd -> int
		val mid : fd -> int
		val nextLarger : fd * int -> int
		val nextSmaller : fd * int -> int
		val size : fd -> int
		val dom : fd -> domain
		val domList : fd -> int list
		val nbSusps : fd -> int
		val eq : fd * fd -> bool (* token eq *)
	    end

	(* Watching *)
	structure Watch :
	    sig
		val min : fd * int -> bool
		val max : fd * int -> bool
		val size : fd * int -> bool
	    end

	(* Distribution *)
	val distribute : dist_mode * fd vector -> unit
	val choose : dist_mode * fd vector -> fd * domain

	(* Scheduling Stuff *)
	structure Schedule :
	    sig
		type tasks  = (string * string list) vector
		type starts = (string * fd) vector
		type specs  = (string * int) vector

		val cumulative : tasks * starts * specs * specs * specs -> unit
		val cumulativeEF : tasks * starts * specs * specs * specs -> unit
		val cumulativeTI : tasks * starts * specs * specs * specs -> unit
		val cumulativeUp : tasks * starts * specs * specs * specs -> unit
		val disjoint : fd * int * fd * int -> unit
		val firstsDist : tasks * starts * specs -> unit
		val lastsDist : tasks * starts * specs -> unit
		val firstsLastsDist : tasks * starts * specs -> unit
		val taskIntervalsDistP : tasks * starts * specs -> unit
		val taskIntervalsDistO : tasks * starts * specs -> unit
		val serializedDisj : tasks * starts * specs -> unit
		val serialized : tasks * starts * specs -> unit
		val taskIntervals : tasks * starts * specs -> unit
	    end
     end

________ Description _________________________________________________

type fd
type bin = fd

The type of finite domain variables. The type bin is used to indicate boolean 0/1 variables.

exception Tell

is raised when a propagator is created on toplevel and is inconsistent with other constraints.

datatype domain_element = SINGLE of int | RANGE of int * int
type domain = domain_element vector

The type of finite domains. Use SINGLE i to specify a single integer i and RANGE(il, ih) to specify a value domain [il, il + 1, ..., ih], presuming that ih is greater than or equal to il.

For example, the value #[SINGLE(5), RANGE(7, 10)] specifies the domain [5,7,8,9,10].

datatype relation = LESS | LESSEQ | EQUAL | NOTEQUAL | GREATER | GREATEREQ

This is the datatype to denote a arithmetic relation which is given to generic propagators as an argument.

datatype dist_mode = NAIVE | FIRSTFAIL | SPLIT_MIN | SPLIT_MAX | NBSUSPS

This datatype is used to denote the distribution stragety which is given to the FD.distribute function.

datatype assign = MIN | MID | MAX

This datatype is used to assign implementation dependent values to finite domain variables. MIN denotes the minimal integer value, MAX denotes the maximal integer value and MID the medium value.

inf

denotes the implementation dependent lower bound of a fd variable.

sup

denotes the implementation dependent upper bound of a fd variable.

fd dom

returns a freshly created finite domain variable initialized with the given domain dom. In case dom equals to NONE, the maximal domain [MIN, MIN + 1, ..., MAX] is used.

fdVec (n, dom)

returns a vector of freshly created finite domain variables. The vector has size n and all variables are initialized with the domain denoted by dom.

range (il, ih)

convenience abbreviation for fd (SOME (#[RANGE(il, ih)])).

rangeVec (n, il, ih)

convenience abbreviation for fdVec (n,#[RANGE(il, ih)]).

bin ()

convenience abbreviation for fd (SOME (#[RANGE(0, 1)])).

binVec n

convenience abbreviation for fdVec (n,#[RANGE(0, 1)]).

assign (as, v)

Every finite domain variable contained in vector v is assigned the value denoted by as, that is, either the minimal, medium or maximal value possible.

toInt f

returns the integer value i denoted by the finite domain variable is returned, presuming that f has a singleton domain.

future f

returns the integer value i denoted by the finite domain variable is returned, presuming that f has a singleton domain.

fromInt i

returns a freshly created finite domain variable initialized with the singleton domain #[SINGLE i].

isBin f

returns true iff f is 0/1 variable, false otherwise.

sum (v, rel, r)

creates a propagator for

        v1 + ... + vn - r rel 0

For the precise operational semantics, see here.

In case, rel denotes NOTEQUAL, 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 (v, rel, r)

creates a propagator for

        i1 * v1 + ... + in * vn - r rel 0

For the precise operational semantics, see here.

sumAC (v, rel, r)

creates a propagator for the absolute value of the scalar product

        |iv * v| = |i1 * v1 + ... + in * vn| rel r

For the precise operational semantics, see here.

sumCN (v, rel, r)

creates a propagator for

        i1 * v1 * ... * v1m1 + ... + in * vn1 * ... *vnmn - r rel 0

For the precise operational semantics, see here.

sumACN (v, rel, r)

creates a propagator for

        |i1 * v1 * ... * v1m1 + ... + in * vn1 * ... *vnmn| rel r

For the precise operational semantics, see here.

sumD (v, rel, r)

creates a propagator analogous to sum but performs domain propagation. Note that only equality (EQUAL) and non-equality are supported (NOTEQUAL), as for inequalities domain and bounds propagation are equivalent

sumCD (v, rel, r)

creates a propagator analogous to sumC but performs domain propagation. Note that only equality (EQUAL) and non-equality are supported (NOTEQUAL), as for inequalities domain and bounds propagation are equivalent

plus (x, y, z)

z is the sum of x and y. The propagator constraints its arguments as X + Y = Z.

minus (x, y, z)

z is the difference of x and y. The propagator constraints its arguments as X - Y = Z.

times (x, y, z)

z is the product of x and y. Coreferences are exploited. If the store entails X = Z, the propagator ceases to exist and the constraint Y = 1 is imposed. If the store entails Y = Z, the propagator ceases to exist and the constraint X = 1 is imposed. If the store entails X = Y, the propagator ceases to exist and a propagator is imposed instead, which constrains the variables X and Y as described here.

power (x, i, z)

z is the result of x raised to the power of i. The propagator constrains the variables X and Y as described here.

divI (x, i, z)

z is the result of the integer division of x by i.

A domain bound is discarded from the domain of one variable, if there is no value between the lower and upper bound of the domain of the other variable, such that the constraint holds. Additionally, if x = z, the propagator is replaced by I = 1.

modI (x, i, z)

z is the result of x modulus i.

A domain bound is discarded from the domain of one variable, if there is no value between the lower and upper bound of the domain of the other variable, such that the constraint holds. Additionally, if x = z, the propagator is replaced by x < i. If the current upper bound of x is less than i, the propagator is replaced by x=z.

plusD (x, y, z)

z is the sum of x and y. The propagator constraints its arguments as X + Y = Z.

Does domain propagation, which can be very expensive.

minusD (x, y, z)

z is the difference of x and y. The propagator constraints its arguments as X - Y = Z.

Does domain propagation, which can be very expensive.

timesD (x, y, z)

z is the product of x and y.

Does domain propagation, which can be very expensive.

divD (x, i, z)

z is the result of the integer division of x by i.

Does domain propagation, which can be very expensive.

modD (x, i, z)

z is the result of x modulus i.

Does domain propagation, which can be very expensive.

min (x, y, z)

z is the minimum of x modulus y.

For precise operational semantics, see here.

max (x, y, z)

z is the maximum of x and y.

For precise operational semantics, see here.

equal (x, y)

Post the constraint that x equals y.

notequal (x, y)

Post the constraint that x does not equal y.

distance (x, y, rel, z)

creates a propagator for

        |x - y| rel z

May cut holes into domains.

This propagator is equivalent to sumAC(#[(1, x), (~1, y)], rel, z) but is more efficient.

less (x, y)

Post the constraint that x is less than y.

lessEq (x, y)

Post the constraint that x is less than or equal to y.

greater (x, y)

Post the constraint that x is greater than y.

greaterEq (x, y)

Post the constraint that x is greater than or equal to y.

disjoint (x, i1, y, i2)

creates a propagator for

        x + i1 <= y or y + i2 <= x

May cut holes into the domains.

For precise operational semantics, see here.

disjointC (x, i1, y, i2, c)

creates a propagator for

        ((x + i1 <= y) and (c = 0)) or ((y + i2 <= x) and (c = 1))

May cut holes into the domains.

For precise operational semantics, see here.

tasksOverlap (x, i1, y, i2, c)

For operational semantics, see here.

distinct v

All elements in v are pairwise distinct. If one element becomes determined, the remaining elements are constrained to be different from it. If two variables become equal, the propagator fails, e. g. FD.distinct #[a,a, b] will fail even if a is not determined.

distinctOffset v

All sums di + ii are pairwise distinct. If one becomes determined, the remaining elements dj are constrained to be different from di + ii - ij.

distinct2 v

For operational semantics, see here.

atMost (x, v, i)

Post the constraint that at most x elements of v are equal to i.

For precise operational semantics, see here.

atLeast (x, v, i)

Post the constraint that at least x elements of v are equal to i.

For precise operational semantics, see here.

exactly (x, v, i)

Post the constraint that exactly x elements of v are equal to i.

For precise operational semantics, see here.

element (x, v, z)

Post the constraint that the xth element of v is z.

It propagates as follows. For each integer i in the domain of x, the i-th element of v is in the domain of z; and no other values. For each value j in the domain of z, all positions where j occurs in v are in the domain of x; and no other values.

conj (x, y, z)

z is the conjunction of x and y.

For operational semantics, see here.

disj (x, y, z)

z is the disjunction of x and y.

exor (x, y, z)

z is the exclusive disjunction of x and y.

nega (x, y)

y is the negation of x.

impl (x, y, z)

z is the implication of x by y (x -> y).

equi (x, y, z)

z is the equivalence of x by y (x <-> y).

Reified.fd (dom, c)

returns a freshly created finite domain variable which is initialized with dom and reified into c.

Reified.fdVec (n, dom, c)

returns a vector of size n of finite domain variables. Each variable is initialized with dom and reified into c.

Reified.card (i1, v, i2, c)

For detailed documentation, see here.

Reified.sum (v, rel, r, c)

Reifies sum(v, rel, r) into c.

Reified.sumC (v, rel, r, c)

Reifies sumC(v, rel, r) into c.

Reified.sumAC (v, rel, r, c)

Reifies sumAC(v, rel, r) into c.

Reified.sumCN (v, rel, r, c)

Reifies sumCN(v, rel, r) into c.

Reflect.min x

returns the current lower bound of x.

Reflect.max x

returns the current upper bound of x.

Reflect.mid x

returns the integer which is closest to the middle of the current domain (the arithmetical means of the lower and upper bound of x). In case of ties, the smaller element is selected.

Reflect.nextLarger (x, i)

returns the smallest integer in the domain of x which is larger than i.

Reflect.nextSmaller (x, i)

returns the largest integer in the domain of x which is smaller than i.

Reflect.size x

returns the size of the current domain of x.

Reflect.dom x

returns the the current domain of x.

Reflect.domList x

returns the the current domain of x as an ordered list of integers.

Reflect.nbSusps x

returns the the current number of suspensions on x.

Reflect.eq (x, y)

returns true iff x and y denote the same variable, false otherwise.

distribute (spec, v)

v is distributed according to the distribution spec spec:

choose (spec, v)

selects a element e from v according to the distribution spec spec and returns a tuple consisting of e and its specification according to spec.



last modified 1970/01/01 01:00