This first chapter introduces the overall framework of FaCiLe and gives
a preliminary insight about its programming environment and functionalities.
OCaml code using FaCiLe facilities (file csp.ml in the
following example) must be compiled with the
library of object byte code facile.cma when batch compiling
with ocamlc:
ocamlc -I +facile facile.cma csp.ml
and with the library of object code facile.cmxa for native
compilation with ocamlopt:
ocamlopt -I +facile facile.cmxa csp.ml
provided that the standard installation of FaCiLe (and previously of
the OCaml system of course) has been performed (see p. ??) and
that the facile.cm[x]a files have been successfully
created in the OCaml standard library directory. For larger programs,
a generic Makefile can be found in directory examples
(see p. ??).
It may however be convenient to use an OCaml custom toplevel to
experiment toy examples or check small piece of serious (thus larger)
code. A FaCiLe toplevel (i.e. in which facile.cma is pre-loaded)
is easily built with the following command:
ocamlmktop -o facile -I +facile facile.cma
and invoked with:
./facile -I +facile
The two following sections give a quick overview of the main basic
concepts of FaCiLe with the help of two very simple examples which
are explained step by step.
1.1 Basics
We first give a slight taste of FaCiLe with the recurrent trivial
problem of the Canadian flag: one has to repaint the Canadian flag
(shown in figure 1.1) with its two original colors,
red and white, so that two neighbouring areas don't have the same
color and the maple leaf is... red, of course. The CSP model is
desperately straightforward:
-
one variable for each area l, c, r and m;
- all variables have the same domain [0..1], 0 being red and 1, white;
- one difference constraint for each adjacency l ¹ c,
c ¹ r, m ¹ c and the maple leaf is forced to be red m = 0.
Figure 1.1:
The problem of the Canadian flag
The following piece of code solves this problem:
maple.ml
open Facile
open Easy
let _ =
(* Variables *)
let red = 0 and white = 1 in
let dom = Domain.create [red; white] in
let l = Fd.create dom and c = Fd.create dom
and r = Fd.create dom and m = Fd.create dom in
(* Constraints *)
Cstr.post (fd2e l <> fd2e c);
Cstr.post (fd2e c <> fd2e r);
Cstr.post (fd2e m <> fd2e c);
Cstr.post (fd2e m = i2e red);
(* Goal *)
let var_list = [l;c;r;m] in
let goal = Goals.List.labeling var_list in
(* Search *)
if Goals.solve goal then begin
Printf.printf "l="; Fd.fprint stdout l;
Printf.printf " c="; Fd.fprint stdout c;
Printf.printf " r="; Fd.fprint stdout r;
Printf.printf " m="; Fd.fprint stdout m;
print_newline () end
else
prerr_endline "No solution"
ocamlc -I +facile facile.cma maple.ml
./a.out
l=0 c=1 r=0 m=0
Surprisingly enough, the new flag is a faithful copy of
the genuine one.
This small example introduces the following features of FaCiLe:
-
The user interface to the library is provided by module
Facile
which gathers several specialized ``submodules''. We thus advise to
open module Facile systematically to lighten FaCiLe functions
calls. Most frequently used functions and submodules can then be
directly accessed by opening module Easy (open Easy).
Functions and modules names have been carefully chosen to avoid
name clashes as much as possible with OCaml standard library when
opening these two modules, but the ``dot prefix'' notation
can still be used in case of a fortuitous overlapping.
- The problem variables are created by a call to function
create of module Fd (for Finite domain,
see ??) which takes a domain of type Domain.t as
only argument. Domains are built and handled by functions of
module Domain (see ??) like
Domain.create l which creates a domain containing all integers
of list l.
-
fd2e and i2e
constructs an expression respectively
from a variable and an integer. More complex arithmetic expressions
and constraints are built with infix operators (obtained by adding the
suffix ~ to their integer counterparts) taking two expressions
as arguments. Most usual arithmetic operators (not necessarily infix)
are provided in module Arith (see ??).
- Function
post from module
Cstr adds a constraint to the
constraint ``store'', which means that the constraint is taken into account
and domain reduction is performed (as well as propagation on other variables).
- Here the search goal is a simple labeling of the list of all the
problem variables
[l;c;r;m] obtained by a call to function
labeling of submodule List embedded in module
Goals (see ??). The goal is thereafter solved by
a call to solve which returns false if a failure occurred
and true otherwise.
- The solution is then printed using function
fprint from
module Fd, which prints a variable on an output channel, i.e. its
domain if the variable is not instantiated and its value otherwise.
This piece of code illustrates a typical FaCiLe CSP solving with the
following pervasive ordered structure:
-
data and variables declaration
- constraints statements
- search goal specification
- goal solving, i.e. searching solution(s)
In the next section, a more sophisticated example will help to
precisely describe how these features can be easily implemented with
FaCiLe.
1.2 A Classic Example
We solve now the even more recurrent cryptarithmetic problem
SEND+MORE=MONEY (see figure 1.2) where each letter stands for
a distinct digit (with M¹ 0 and S¹ 0).
|
|
| |
S |
E |
N |
D |
| + |
M |
O |
R |
E |
|
| M |
O |
N |
E |
Y |
|
Figure 1.2:
The
SEND+
MORE=
MONEY problem
We model this problem with one variable for each digit plus three auxilliary
variables to carry over, and the subsequent four arithmetic constraints
specifying the result of the addition as we would do by hand. The following
program implement this model:
smm.ml
open Facile
open Easy
let _ =
(* Variables *)
let s = Fd.interval 0 9 and e = Fd.interval 0 9 and n = Fd.interval 0 9
and d = Fd.interval 0 9 and m = Fd.interval 0 9 and o = Fd.interval 0 9
and r = Fd.interval 0 9 and y = Fd.interval 0 9 in
(* Constraints *)
Cstr.post (fd2e m > i2e 0);
Cstr.post (fd2e s > i2e 0);
let digits = [|s;e;n;d;m;o;r;y|] in
Cstr.post (Alldiff.cstr digits);
let c = Fd.array 3 0 1 in (* Carry array *)
let one x = fd2e x and ten x = i2e 10 * fd2e x in
Cstr.post ( one d + one e = one y + ten c.(0));
Cstr.post (one c.(0) + one n + one r = one e + ten c.(1));
Cstr.post (one c.(1) + one e + one o = one n + ten c.(2));
Cstr.post (one c.(2) + one s + one m = one o + ten m);
(* Search goal solving *)
if Goals.solve (Goals.Array.labeling digits) then begin
let value = Fd.elt_value in
Printf.printf " Printf.printf "+ Printf.printf "= y)
end else
prerr_endline "No solution"
ocamlc -I +facile facile.cma smm.ml
./a.out
9567
+ 1085
=10652
We detail each step of the above example:
-
Variables whose domains range integer intervals are created
with function Fd.interval inf sup which creates a variable whose
domain contains all integers between
inf and sup (inclusive).
-
Disequations M¹ 0 and S¹ 0 are then expressed by arithmetic
inequality constraints and we assert that all digits must be distinct
with the global
Alldiff.cstr constraint which takes an array of
variables as argument (see ??). FaCiLe provides
some other global constraints as well, such as the global cardinality
constraint (a.k.a. the ``distribute'' constraint) or the ``sorting''
constraint (see ?? and ??),
embedded in separate module and called with function cstr.
- The three auxilliary carry variables are then created with
Fd.array n inf sup which builds an array of n variables
whose domains range the interval [inf..sup], and two
auxilliary functions one x and ten x are defined which
return an arithmetic expression being respectively equal to x
and ten times x to lighten the main constraints statements.
- The equations reproducing the way we would compute the addition of
figure 1.2 by hand are then straightforwardly stated and posted
to the constraint store. The problem is finally solved as in the
first example by a simple labeling of the decision variables,
i.e. the ``digits'', using function
labeling of module
Goals.Array (which is the counterpart of Goals.List
over arrays of variables). The solution is then printed with
function Fd.elt_value which returns the integer value
of an instantiated variable (or raises an exception whenever
it is still unbound).
We could of course have used a different but equivalent model
constraining the addition to be exact without auxilliary carry
variables:
...
let op1 =
i2e 1000 *~ fd2e s +~ i2e 100 *~ fd2e e +~ i2e 10 *~ fd2e n +~ fd2e d
and op2 =
i2e 1000 *~ fd2e m +~ i2e 100 *~ fd2e o +~ i2e 10 *~ fd2e r +~ fd2e e in
let result =
i2e 10000 *~ fd2e m +~
i2e 1000 *~ fd2e o +~ i2e 100 *~ fd2e n +~ i2e 10 *~ fd2e e +~ fd2e y in
Cstr.post (op1 +~ op2 =~ op3);
...
This alternative model would undoubtedly produce the same result.
The next chapter will explore in a more formal way how to handle
the main concepts of FaCiLe introduced in the two previous examples.