Previous Up Next

Chapter 3  Advanced Usage

3.1  Search Control

3.1.1  Basic Mechanisms

FaCiLe implements a standard depth-first search with backtracking. OR control is handled with a stack (module Stak), while AND control is handled with continuations.

OR control can be modified with a cut la Prolog: a level is associated to each choice-point (node in the search tree) and choice-points created since a specified level can be removed, i.e. cut (functions Stak.level and Stak.cut).

OR and AND controls are implemented by the Goals.solve function. AND is operationally mapped on the imperative sequence. OR is based on the exception mechanism: backtrack is caused by the exception which is raised by failing constraints. Note that this exception is caught and handled by the Goals.solve function only.

3.1.2  Combining Goals with Iterators

Functional programming allows the programmer to compose higher-order functions using iterators. An iterator is associated to a datatype and is the default control structure to process a value in the datatype. There is a strong isomorphism between the datatypes and the corresponding iterators and this isomorphism is a simple guideline to use them.

Imitating the iterators of the standard OCaml library, FaCiLe provides iterators for arrays and lists. While standard Array and List modules allows to construct sequences (with a ';') of imperative functions (type 'a -> unit), Goals.Array and Goals.List modules of FaCiLe allows to construct conjunction (with a &&~) and disjunction (with a ||~) of goals (type Goals.t).

The simplest iterator operates on integers and provides a standard for-to loop by applying a goal to consecutive integers:
Goals.forto 3 7 g = (g 3) &&~ (g 4) &&~ ... &&~ (g 7)
Of course, iterators may be composed, as is illustrated below, where the cartesian product [1..3] [4..5] is deterministically enumerated:
let enum_couples =
 Goals.forto 1 3
 (fun i ->
 Goals.forto 4 5
 (fun j ->
 Goals.atomic (fun () -> Printf.printf "Goals.solve enum_couples;;
 - : bool = true
Function Goals.atomic (used in the previous example), which builds an ``atomic'' goal (i.e. a goal which returns nothing), is detailed in section 3.4.1.

Arrays: module Goals.Array

Standard Loop
The polymorphic Goals.Array.forall function applies uniformally a goal to every element of an array, connecting them with a conjunction (&&~).
Goals.Array.forall g [|e1; e2; ...; en|] = (g e1) &&~ (g e2) &&~ ... &&~ (g en)
Labeling of an array of variables is the iteration of the instantiation of one variable (Goals.indomain):
let labeling_array = Goals.Array.forall Goals.indomain;;
 val labeling_array : Facile.Var.Fd.t array -> Facile.Goals.t = <fun>

A matrix is an array of arrays; following the isomorphism, labeling of a matrix must be simply a composition of the array iterator:
let labeling_matrix = Goals.Array.forall labeling_array;;
 val labeling_matrix : Facile.Var.Fd.t array array -> Facile.Goals.t = <fun>

Changing the Order
An optional argument of Goals.Array.forall, labelled ?select, gives the user the possibility to choose the order in which the elements are considered. ?select is a function which is applied to the array by the iterator and which must return the index of one element on which the goal is applied. This function must raise the exception Not_found to stop the loop.

For example, if we want to apply the goal only on the unbound variables of an array, we may write:
let first_unbound array =
 let n = Array.length array in
 let rec loop i = (* loop until free variable found *)
 if i < n then
 match Fd.value array.(i) with
 Unk _ -> i
 | Val _ -> loop (i+1)
 raise Not_found in
 loop 0;;
 val first_unbound : Facile.Easy.Fd.t array -> int = <fun>
let forall_unbounds = Goals.Array.forall  select:first_unbound;;
 val forall_unbounds :
  (Facile.Easy.Fd.t -> Facile.Goals.t) ->
  Facile.Easy.Fd.t array -> Facile.Goals.t = <fun>
Note that the function forall is polymorphic and can be used for an array of any type.

The function Goals.Array.choose_index facilitates the construction of heuristic functions that may be provided to the forall ?select argument. It constructs such a function from an ordering function on variable attributes (free variables are ignored). For example, the standard ``min size'' strategy will be implemented as follows:
let min_size_order = 
 Goals.Array.choose_index (fun a1 a2 -> Var.Attr.size a1 < Var.Attr.size a2);;
 val min_size_order : Facile.Var.Fd.t array -> int = <fun>
let min_size_strategy = Goals.Array.forall  select:min_size_order;;
 val min_size_strategy :
  (Facile.Var.Fd.t -> Facile.Goals.t) ->
  Facile.Var.Fd.t array -> Facile.Goals.t = <fun>
let min_size_labeling = min_size_strategy Goals.indomain;;
 val min_size_labeling : Facile.Var.Fd.t array -> Facile.Goals.t = <fun>

Note that module Goals.Array also provides a disjunctive iterator, exists, which has the same profile than forall. Variants Goals.Array.foralli and Goals.Array.existsi allow to specify goals which take the index of the relevant variable as an extra argument (like the OCaml standard library iterator Array.iteri).

Lists: module Goals.List

FaCiLe Goals.List module provides similar iterators for lists except of course iterators which involve index of elements.

3.2  Constraints Control

Constraints may be seen operationally as ``reactive objects''. They are attached to variables, more precisely to events related to variable modifications. A constraint mainly is an update function (responsible for performing propagations) which is called when the constraint is woken because a specific event occured. Events are queued according to the priority of the constraint, and the search control is resumed as soon as all queues are emptied.

3.2.1  Events

An event (of type Var.Fd.event) is a modification of the domain of a variable. FaCiLe currently provides four specific events: Note that these events are not independant and constitute a lattice which top is on_subst and bottom is on_refine: Constraints are attached to the variables through these events, thanks to the Var.Fd.delay2 function. In concrete terms, lists of constraints (one per event) are put in the attribute of the variable. Note that this attachement occurs only when the constraint is posted.

3.2.2  Suspending to Events, Waking Identity

Constraints are suspended to events by invoking the delay function wich takes an events list and an optional integer waking identity as parameters (in addition to the constraint itself and to the variable triggering the events of course). When posted, the constraint will be registered to all the events appearing in the events list, along with the waking identity. This integer will be passed to the update function whenever one of the events in the list occurs. It allows to dicriminate the event and/or the variable responsible for the wakening, so as to fire a specific rule without having to inspect all the variables to find out the culprit.

A typical use of waking identities is in global constraints that takes an array of variables as parameter. The index of the variable can be associated to the event(s) on which the constraint is suspended and the update function may avoid traversing the entire array to compute the propagation.

The use of a waking identity is optional and 0 is assumed (default value) if the parameter is omitted. However, if this feature is used, the identities must be consecutive integers ranging from 0 to n-1, and n, the number of distinct wakings, must be passed as an optional parameter (labelled nb_wakings) to the Cstr.create function. Actually, an array of size n is internally build to record the result of the calls to update with each identity. The constraint is solved when all such calls have returned true (see 3.3).

3.2.3  Wakening, Queuing, Priorities

When an event occurs, related constraints are woken and put in a queue. The queue is processed after each sequence of waking. This processing is protected against reentrance. Constraints are considered one after the other and each update function is called to perform propagation. Propagation may fail by raising an exception or succeed. The propagation of one constraint is also protected against being woken again by itself.

When a constraint is triggered, the update function does not know by which event, nor gets information about the variable responsible of it.

A constraint is woken only once by two distinct events. Note also that the waking queue contains constraints and not variables.

FaCiLe implements three ordered queues and ensures that a constraint in a lower queue is not propagated before a constraint present in a higher queue. The queue is chosen according to the priority of a constraint (abstract type Cstr.priority). The priority is specified when the constraint is defined (see 3.3). It can be changed neither when the constraint is posted nor later. Priorities are defined in module Cstr: immediate, normal or later.

3.2.4  Constraint Store

FaCiLe handles the constraint store of all the posted and active constraints (a constraint becomes inactive if it is solved, i.e. if its update function returns true, see 3.3). For debugging purpose, this store can be consulted using the function Cstr.active_store and the returned constraints list may be processed using constraints (of type Cstr.t) access functions (, and Cstr.fprint).

3.3  User's Constraints

The Cstr.create function allows the user to build new constraints from scratch. This function may take up to eight arguments to precisely control the behaviour of the resulting constraint :
 - : ?name:string ->
  ?nb_wakings:int ->
  ?fprint:(out_channel -> unit) ->
  ?priority:Facile.Cstr.priority ->
  ?init:(unit -> unit) ->
  ?check:(unit -> bool) ->
  ?not:(unit -> Facile.Cstr.t) ->
  (int -> bool) -> (Facile.Cstr.t -> unit) -> Facile.Cstr.t
 = <fun>

However, to define a new simple3 constraint, very few arguments must be passed to the create function as numbers of them are optional (thus labelled) and have default values. Merely the two following arguments are actually needed to build a new constraint by evaluating Cstr.create update delay: However we recommend to name new constraints and precise their printing facilities, which may obviously help debugging, by specifying the following two optional arguments: To define a reifiable constraint, two additional optional arguments must also be specified: To be able to use waking identities, their number must be specified: Finally two other optional arguments may be specified:
Example of reifiable constraints
The example below defines a new constraint stating that variable x should be different from variable y. This constraint specifies an optional name and an optional printing function. It suspends itself to instantiation events of its two variables (without using any waking identity). Its update function ignores its integer argument (update _ = ...) and withdraws the instantiation value of one of its variable in the domain of the other. This constraint is reifiable as the check and not functions are specified.

Note that no optional init function is provided, neither any nb_wakings argument: in this case, the default behaviour of init will be to call update 0. The init function is the first function to be called as soon as the constraint is posted, and its usual intended role is to perform an initial propagation and possibly initialize internal data structures of the constraint. This is what happens in this first example. However, if the constraint is suspended on an instantiation event (XxxFd.on_subst), and the update function relies on the fact that it will only be called when the variable is instantiatied (e.g. without testing that the variable is effectively bound), then the default init behaviour is not appropriate. Use a specific init function instead by providing this optional argument to Cstr.create, as shown in the second example (that uses waking ids). 
open Facile
open Easy

let cstr x y =
  let name = "different" in
  let fprint c =
    Printf.fprintf c "%s: %a <> %a\n" name Fd.fprint x Fd.fprint y
  and delay ct =
    (* The constraint is suspended on the instantiation of x or y. *)
    Fd.delay [Fd.on_subst] x ct;
    Fd.delay [Fd.on_subst] y ct
  and update _ =
    (* If one of the two variables is instantiated, its value is
       removed in the domain of the other variable. *)
    if Fd.is_bound x then
      begin Fd.remove y (Fd.elt_value x); true end
    else if Fd.is_bound y then
      begin Fd.remove x (Fd.elt_value y); true end
    else false
  and check () = (* Consistency check for reified constraints. *)
    match (Fd.value x, Fd.value y) with
      (Val a, Val b) -> a <> b
    | (Val a, Unk attr_y) when not (Var.Attr.member attr_y a) -> true
    | (Unk attr_x, Val b) when not (Var.Attr.member attr_x b) -> true
    | (Unk attr_x, Unk attr_y) when
    (* If the intersection of domains is empty, the constraint is satisfied. *)
        let dom_x = Var.Attr.dom attr_x and dom_y = Var.Attr.dom attr_y in
        Domain.is_empty (Domain.intersection dom_x dom_y) -> true
    | _ -> raise Cstr.DontKnow
  and not () = fd2e x =~ fd2e y in (* Negation for reification. *)
  (* Creation of the constraint. *)
  Cstr.create ~name ~fprint ~check ~not update delay

Let's compile the file:
ocamlc -c -I +facile
and use the produced object:
#load "diff.cmo";;
let x = Fd.interval 1 2 and y = Fd.interval 2 3;;
 val x : Facile.Easy.Fd.t = <abstr>
 val y : Facile.Easy.Fd.t = <abstr>
let diseq = Diff.cstr x y;;
 val diseq : Facile.Cstr.t = <abstr> diseq;;
 - : unit = ()
let goal =
 Goals.indomain x  Goals.indomain y
  Goals.atomic (fun () -> Cstr.fprint stdout diseq) in
while (Goals.solve goal) do () done;;
 2: different: 1 <> 2
 2: different: 1 <> 3
 2: different: 2 <> 3
 - : unit = ()
Another example to test the reification function check:
let x = Fd.create (Domain.create [1;3;5])
and y = Fd.create (Domain.create [2;4;6]);;
 val x : Facile.Easy.Fd.t = <abstr>
 val y : Facile.Easy.Fd.t = <abstr>
let reified_diseq = Reify.boolean (Diff.cstr x y);;
 val reified_diseq : Facile.Var.Fd.t = <abstr>
Fd.fprint stdout reified_diseq;;
 1- : unit = ()
Variables x and y have disjoint domains, so the boolean variable reified_diseq is instantiated to 1 as expected.

Example of constraints using waking identities
The above example could benefit from the use of waking ids, avoiding the cost of testing which variable has been instantiated within the update function. The next example features such a disequality constraint. The delay function must now specify a waking id (argument waking_id) along with its associated events list and variable. These ids must form an interval ranging from 0 to a given n-1, and its size n must be provided to the Cstr.create function through its optional nb_wakings argument4. The update function now makes use of this information (argument id) and performs the appropriate propagation depending on which waking event has occurred. This function must return true if the constraint is satisfied for this particular event and false otherwise. The constraint will be satisfied only when all the calls to update 0, ..., update (n-1) have returned true.

In this example, we must provide an init function as well, because the nb_wakings argument is greater than 1 and the default behaviour of init is then to do nothing. But the constraint should propagate at post time, so an appropriate init function (which incidentally calls the update one) is provided. 
open Facile
open Easy

let cstr x y =
  let delay ct = (* Ids are associated with waking events. *)
    Fd.delay [Fd.on_subst] x ~waking_id:0 ct;
    Fd.delay [Fd.on_subst] y ~waking_id:1 ct
  and update id =
    begin (* Update function using waking ids. *)
      match id with
        0 -> Fd.remove y (Fd.elt_value x)
      | 1 -> Fd.remove x (Fd.elt_value y)
      | _ -> failwith "Diff_if.cstr: unexpected waking id"
    true in
  let init () =
  (* Update should be called if x or y is already bound when posting
     the constraint. This is the job of the init function. *)
    if not (Fd.is_var x) then ignore (update 0)
    else if not (Fd.is_var y) then ignore (update 1) in
  (* Creation of the constraint with 2 waking ids. *)
  Cstr.create ~nb_wakings:2 ~init update delay

3.4  User's Goals

3.4.1  Atomic Goal: Goals.atomic

The simplest way to create a deterministic atomic goal is to use the Goals.atomic function which ``goalifies'' any unit function (i.e. of type unit -> unit).

Let's write the goal which writes a variable on the standard output:
let gprint_fd x = Goals.atomic (fun () -> Printf.printf " val gprint_fd : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
To instantiate a variable inside a goal, we may write the following definition:
let unify_goal x v = Goals.atomic (fun () -> Fd.unify x v);;
 val unify_goal : Facile.Easy.Fd.t -> Facile.Easy.Fd.elt -> Facile.Goals.t =
let v = Fd.interval 0 3 in
if Goals.solve (unify_goal v 2) then Fd.fprint stdout v;;
 2- : unit = ()
Note that this goal is the built-in goal Goals.unify.

This goal creation can be used to pack any side effect function:
let gprint_int x = Goals.atomic (fun () -> print_int x);;
 val gprint_int : int -> Facile.Goals.t = <fun>
Goals.solve (Goals.forto 0 5 gprint_int);;
 012345- : bool = true

The FaCiLe implementation of the classic ``findall'' of Prolog also illustrates the use of Goals.atomic to perform side effects: in this case to store all the solutions found in a list. The function findall in this example takes a ``functional goal'' g as argument which itself takes the very variable x from which we want to find all the possible values for which g succeeds; it could correspond to the Prolog term:
findall(X, g(X), Sol)
let findall g x =
 let sol = ref [] in
 let store = Goals.atomic (fun () -> sol := Fd.elt_value x :: !sol) in
 let goal = g x  store in
 ignore (Goals.solve goal);
 val findall :
  (Facile.Easy.Fd.t -> Facile.Goals.t) ->
  Facile.Easy.Fd.t -> Facile.Easy.Fd.elt list = <fun>
We first declare a reference sol on an empty list to store all the solutions. Then the simple goal store is defined to push any new solution on the head of sol -- note that we here use Fd.elt_value v (see ??) for conciseness but it is quite unsafe unless we are sure that v is bound. The main goal is the conjunction of g, store and a failure. This goal obviously always fails, so we ``ignore'' the boolean returned by Goals.solve, and the solutions list is eventually returned.

The main point when creating goals is to precisely distinguish the time of creation of the goal from the time of its execution. For example, the following goal does not produce what might be expected:
let wrong_min_or_max var =
 let min = Fd.min var and max = Fd.max var in
 (Goals.unify var min ||  Goals.unify var max);;
 val wrong_min_or_max : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
The min and max of the variable var are processed when the goal is created and may be different from the min and max of the variable when the goal will be called. To fix the problem, min and max must be computed within the goal. Then the latter must return the disjunction, which cannot be done with a simple call to Goals.atomic; function Goals.create (described in the next section) must be used instead.

3.4.2  Arbitrary Goal: Goals.create

The function Goals.atomic does not allow to construct goals which themselves construct new goals (similar to Prolog clauses). The Goals.create function ``goalifies'' a function which must return another goal, possibly Goals.success to terminate.

Let's write the goal which tries to instantiate a variable to its minimum value or to its maximum:
let min_or_max v =
 (fun () ->
 let min = Fd.min v and max = Fd.max v in
 Goals.unify v min ||  Goals.unify v max)
 val min_or_max : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
The other difference between Goals.create and Goals.atomic is the argument of the goalified function which may be of any type ('a) and which must be passed as the second argument to Goals.create. In the previous example, we use ().

Goals.create allows the user to define recursive goals by a mapping on a recursive function. In the next example, we iterate a goal non-deterministically on a list. Note that this goal is equivalent to the built-in goal Goals.List.exists.

let rec iter_disj fgoal list =
 [] -> Goals.success
 | x::xs -> fgoal x ||  iter_disj fgoal xs)
 val iter_disj : ('a -> Facile.Goals.t) -> 'a list -> Facile.Goals.t = <fun>
let gprint_int x = Goals.atomic (fun () -> print_int x);;
 val gprint_int : int -> Facile.Goals.t = <fun>
let gprint_list = iter_disj gprint_int;;
 val gprint_list : int list -> Facile.Goals.t = <fun>
if Goals.solve (gprint_list [1;7;2;9] ||  Goals.success) then
 print_newline ();;
 - : unit = ()

3.4.3  Recursive Goals: Goals.create_rec

FaCiLe provides also a constructor for intrinsically recursive goals. Expression Goals.create_rec f is similar to Goals.create f except that the argument of the function f is the created goal itself.

The simplest example using this feature is the classic repeat predicate of Prolog implementing a non-deterministic loop:
let repeat = Goals.create_rec (fun self -> Goals.success ||  self);;
 val repeat : Facile.Goals.t = <abstr>
The goalified function simply returned the disjunction of a success and itself.

The Goals.indomain function which non-deterministically instantiates a variable is written using Goals.create_rec:
let indomain var =
 Goals.create_rec  name:"indomain"
 (fun self ->
 match Fd.value var with
 Val _ -> Goals.success
 | Unk attr ->
 let dom = Var.Attr.dom attr in
 let remove_min =
 Goals.atomic (fun () -> Fd.refine var (Domain.remove_min dom))
 and min = Domain.min dom in
 Goals.unify var min ||  (remove_min  self));;
 val indomain : Facile.Easy.Fd.t -> Facile.Goals.t = <fun>
The goal first checks if the variable is already bound and does nothing in this case. If it is an unknown, it returns a goal trying to instantiate the variable to its minimum or to remove it before continuing with the remaining domain.

3.5  Backtrackable Invariant References -- BIRs

FaCiLe provides through the module Invariant some features to handle data-structures which are functionnally dependant between each other. These invariants are directly derived from the work of [8], although they are meant to be used within CP search goals. So they'll be called backtrackable invariant references or BIRS in the sequel, as their values are restored upon backtracks.

An invariant is either: FaCiLe can provide efficient handling of the dependencies between BIRs in order to keep them updated. For example, if an integer (or floating point) BIR i is defined as the sum of n others i1, ..., in, the change of the value of one of i1, ... in will be taken into account in constant time to update i.

The main original use of invariants proposed in [8] is within local search algorithms. In our context, it can be used also to compute a heuristic criterion used during search. The implementation of BIRs in FaCiLe is fully compatible with backtrack.

In the following, we call BIR a mutable value and invariant the relation (a functional equation) between BIRs.

3.5.1  Type, creation, access and modification

BIRs of FaCiLe are polymorphic so you can handle any data-structures with them. A BIR may be mutable or not and this property is handled by the typing: However, shortcuts with only one type parameter are defined in module Invariant to simplify the writting of BIRS: 'a setable_t and 'a unsetable_t.

We show in the following example how to create, access and modify a BIR:
let x = Invariant.create 1729 and y = Invariant.constant 3.14;;
 val x : int Facile.Invariant.setable_t = <abstr>
 val y : float Facile.Invariant.unsetable_t = <abstr>
(Invariant.get x, Invariant.get y);;
 - : int * float = (1729, 3.14)
Invariant.set x 1730;;
 - : unit = ()
Invariant.get x;;
 - : int = 1730

Like finite domain variables, BIRs can be named thanks to an optional string argument (?name) and feature a unique integer identity (accessible with function

3.5.2  Operations

FaCiLe provides basic arithmetic operators on integer BIRs. These functions are completed by primitives working on array of BIRs (submodule Invariant.Array).

The following table gives the time and space complexity of the basic invariants :
Invariant Time Memory
s =
O(1) O(1)
p =
O(1) O(1)
m =
i [1,n]
O(logn) O(n)
i = argmini [1,n] xi O(logn) O(n)

let a = Invariant.create [|1;2;3;4|];;
 val a : int Facile.Invariant.setable_t array =
  [|<abstr>; <abstr>; <abstr>; <abstr>|]
let s = Invariant.sum a;;
 val s : int Facile.Invariant.unsetable_t = <abstr>
Invariant.get s;;
 - : int = 10
Invariant.set a.(3) 8;;
 - : unit = ()
Invariant.get s;;
 - : int = 14

The library also provides generic wrappers (unary, binary and ternary, for functions with arity up to tree) for BIRs which allow the user to transform any function working on the type a into a function working on an a BIR:
let x = Invariant.create  name:"x" 2.71;;
 val x : float Facile.Invariant.setable_t = <abstr>
let y = Invariant.unary  name:"log" log x;;
 val y : float Facile.Invariant.unsetable_t = <abstr>
Invariant.fprint stdout y; Invariant.get y;;
 log(x)- : float = 0.996948634891609564
Invariant.set x 8.0; Invariant.get y;;
 - : float = 2.07944154167983575
These wrapped functions can be named with an optional string argument.

3.5.3  Domain access

In order to implement computation of heuristic criterion, it is required to be able to translate attributes of finite domain variables (of type Fd.t or SetFd.t) into invariant references. These functionalities are listed in submodules Invariant.Fd and Invariant.SetFd.

For example, the heuristic criterion which selects the variable with the smallest domain is easily computed as follows :
let best = fun vars ->
 Invariant.Array.argmin ( Invariant.Fd.size vars);;
 val best :
  Facile.Invariant.Fd.fd array ->
  (int -> 'a) -> int Facile.Invariant.unsetable_t = <fun>

It means that, e.g. the event on_min occurs even if a variable is instantiated to its minimum value.
Or Var.SetFd.delay for set variables.
That is unreifiable and without the use of waking identities.
As correctly guessed by the reader, these ids are used to access an internal array.

Previous Up Next