Previous Up Next

Chapter 1  Getting Started

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:


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: This piece of code illustrates a typical FaCiLe CSP solving with the following pervasive ordered structure:
  1. data and variables declaration
  2. constraints statements
  3. search goal specification
  4. 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: 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.


Previous Up Next