Home

FaCiLe - La Recherche

Contents

1. Cstr t gt Cstr t gt Cstr t val xor Cstr t gt Cstr t gt Cstr t val not Cstr t gt Cstr t Logical reification operators on constraints namely and or implies equivalent exclusive or not 4 13 Module SetDomain Integer Set Domain Operations module S sig type t Domain t val empty t val is_empty t gt bool val mem int gt t gt bool val add int gt t gt t val singleton int gt t val remove int gt t gt t val union t gt t gt t val inter t gt t gt t val diff t gt t gt t val compare t gt t gt int val equal t gt t gt bool val subset t gt t gt bool val iter int gt unit gt t gt unit val cardinal t gt int val elements t gt int list val min_elt t gt int val max_elt t gt int val choose t gt int val remove_up int gt t gt t val remove_low int gt t gt t end Implementation of sets of integers The signature is freely inspired by the Set module of the standard OCaml library type elt S t Type of elements of set domains They are sets themselves type t 62 Modules Type of finite domains of integer sets a domain is a powerset lattice of sets bounded by definite elements or glb Greater Lower Bound and possible elements or lub Lower Upper Bounds The glb is a subset of the lub Note that the empty domain cannot be represented 4 13 1 Creation val elt_of_list int
2. nb_wakings n must be passed to Cstr create Finally two other optional arguments may be specified e priority should be passed to the create function to precise the priority of the new con straint in the constraints queue Constraints with lower priority are waken only when there is no more constraint of higher priority in the waking queue Time costly constraints should get a later while quick elementary constraints should be immediate and standard constraints normal default value 3That is unreifiable and without the use of waking identities 32 Advanced Usage e init is executed as soon as the post function is called on the constraint to perform ini tialization of inner data structures needed by update thus not called when dealing with a reified constraint The default and intended behaviours of init are a bit intricate when using waking identities Its detailed use is explained in the next paragraphs with the help of two examples The default behaviours of init is to call update 0 and ignores its result when nb_wakings is equal to 1 which is its default value to do nothing fun gt O when nb_wakings is greater than 1 If this is not the desired behaviour the init argument must 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 funct
3. a list gt Facile Goals t lt fun gt let gprint_int x Goals atomic fun gt print_int x val gprint_int int gt Facile Goals t lt fun gt let gprint_list iter_disj gprint_int val gprint_list int list gt Facile Goals t lt fun gt if Goals solve gprint_list 1 7 2 9 amp amp Goals fail Goals success then print_newline 1729 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 gt Goals success self val repeat Facile Goals t lt abstr gt 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 gt match Fd value var with Val _ gt Goals success Unk attr gt let dom Var Attr dom attr in let remove_min HHH 3 5 Backtrackable Invariant References BIRs 37 Goals atomic fun gt Fd refine var Domain remove_min dom and min Domain min dom in Goals unify var min
4. gt Cstr t mem x v states that x belongs to v val inf_min Var SetFd t gt Var SetFd t gt Cstr t inf min vi v2 ensures that the minimal element of v1 is less than or equal to the minimal element of v2 The empty set is smaller than any other set Useful to break permutation symmetries for a set of set variables Not reifiable val order Var SetFd t gt Var SetFd t gt Cstr t order v1 v2 ensures that v1 is less than or equal to v2 according to Domain compare see 4 6 3 Caution order builds the cardinal variables of v1 and v2 if they are already available please use order_with_card Not reifiable val order_with_card Var SetFd t gt Var Fd t gt Var SetFd t gt Var Fd t gt Cstr t order_with_card vi cardi v2 card2 is equivalent to order but the cardinals of the variables must be provided too Useful to sort a set of variables val member Var SetFd t gt SetDomain elt list gt Cstr t member v 1 ensures that v will have a value in 1 Not reifiable val sum_weight Var SetFd t gt int int list gt Var Fd t sum_ weight v weights returns an integer variable equal to the sum of the weights associated with the value in v weights must be a list of pairs value weight that associates a unique weight to each value possibly in v All the weights must be positive integers 4 4 Module Cstr Posting Constraints and Building New Ones 47 4 4 Module Cstr Posting Constraints and Building New Ones
5. gt t Intersection resp union on domains difference t gt t gt t difference big small returns big small small must be included in big otherwise the behaviour is unspecified incorrect return value or exception raised diff t gt t gt t diff di d2 returns di d2 i e domain of elements in di which are not in d2 minus t gt t minus d returns the domain of opposite values of d plus t gt elt gt t plus d n translates a domain by n times t gt elt gt t times d k expands a domain by factor k compare t gt t gt elt compare di d2 is a comparison function working first on the cardinal then if d1 and d2 have the same size on the lexicographic order of the domains expressed in extension compare_elt elt gt elt gt elt compare_elt el e2 is a comparison function on elements of domains Convenient to use the Domain module as a functor argument as in module Var disjoint t gt t gt bool disjoint d1 d2 tests whether d1 and d2 are disjoint 4 7 Module FdArray Constraints over Arrays of Variables 53 4 7 Module FdArray Constraints over Arrays of Variables val min Var Fd t array gt Var Fd t val max Var Fd t array gt Var Fd t min vars resp max vars returns a variable constrained to be equal to the variable that will be instantiated to the minimal resp maximal value among all the variables in the array vars Raises Invalid_argument if v
6. val name a b t gt string name r returns the name specified or generated of BIR r val fprint Pervasives out_channel gt printer Pervasives out_channel gt a gt unit gt Ca b t gt unit fprint c printer fun _ _ gt r prints BIR r on channel c An optional custom printer can be given to display the value of r 4 11 Module Invariant Backtrackable Invariant References 59 4 11 2 Operations generic arithmetic arrays val unary name string gt Ca gt b gt Ca c t gt b unsetable_t unary name Invariant unary f wraps the unary function f into an operator on BIRs An optional string can be given to name the operator val binary name string gt Ca gt b gt c gt Ca d t gt b e t gt c unsetable_t binary name Invariant binary f wraps the binary function f into an operator on BIRs An optional string can be given to name the operator val ternary name string gt Ca gt b gt c gt d gt Ca e t gt Ob f t gt Cc g t gt d unsetable_t ternary name Invariant ternary f wraps the ternary function f into an operator on BIRs An optional string can be given to name the operator val sum int a t array gt int unsetable_t sum a returns a BIR equal to the sum of elements of a val prod int a t array gt int unsetable_t sum a returns a BIR equal to the product
7. 4 9 3 Operators and Built in Goals 4 9 4 Operations on Array of Variables 4 9 5 Operations on List of Variables 22222220 4 9 6 Optimization oa 4 9 7 Search Strategy eee eee 4 9 8 SOWING as es bo sen au na nun naar 4 10 Module Interval Variable Membership to an Interval 4 11 Module Invariant Backtrackable Invariant References 4 11 1 Creation and access 2 2 2 cn ae 4 11 3 From domain variables to BIRS 4 12 Module Reify Constraints Reification 412 1 Operators ers 4 4 2 eon SERRE DEG Eee eae ee 4 13 Module SetDomain Integer Set Domain Operations Pae be o ca ANS a ip anang ee ee ee eee eee eer 4 15 Module Stak Global Stack of Goals Backtrackable Operations 4 15 1 Access Na 4 15 2 Gamo 4 15 3 Backtrackable References 4 16 Module Var Constrained Attributed Finite Domain Variables be cee di dn ee es 410 2 ACCESS 5 a a eae cack oh A a ak ee 4 16 3 Refinement 2 2 2 0 2 2 000 4 16 4 Events and suspending lt ooo 4 17 Module Easy 2 2 aai onen 41 CONTENTS xi 71 xii CONTENTS Part I User s Manual 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 faciliti
8. 64 inter 44 59 intersection Domain 10 Interval interval 48 60 64 SetDomain 24 Var SetFa 24 Domain 9 Var Fa 6 10 interval_iter Invariant invariants is_bound is_empty is_member 55 is_solved 47 INDEX 73 is_var 58 64 is_empty Domain 9 is_var iter 7 49 59 60 66 Var Fd 12 labeling labeling B4 Goals Array 6 Goals List largest_hole_around 49 later 45 lds 22 55 level Level_not_found levels 61 List 54 lub max ES 51 58 60 63 67 Domain 9 FdArray Var Attr Var Fa 12 max_cstr 51 max_elt 59 max_of_expr 43 nen 12 87 PO 59 00 member Domain 9 Var Attr 11 Var Fd 3555 00 65 Domain 9 FdArray 18 Var Attr 11 Var Fa 12 min_cstr ES BI min_elt min_max 49 60 64 min_max_of_expr 43 min_of_expr 14 43 minimize B3 minus name 177 52 59 55 Var Fd nb_choice_points nb_wakings 31 33 normal not 19 7 59 not_instantiated_fd older 61 on_ e Faa once 52 one 16 optimization order 44 order_with_card 44 outside 44 plus 50 post El 15 46 priority 45 47 prod 15 42 57 prod_fd 15 42 ref 62 refine 12 65 refine_low 65 refine_low_up 65 refine_up STO reification 19 20 81 33 Reify 53 remove remove_closed_inter remove
9. For example the standard min size strategy will be implemented as follows 3 2 Constraints Control 29 let min_size_order Goals Array choose_index fun al a2 gt Var Attr size al lt Var Attr size a2 val min_size_order Facile Var Fd t array gt int lt fun gt let min_size_strategy Goals Array forall select min_size_order val min_size_strategy Facile Var Fd t gt Facile Goals t gt Facile Var Fd t array gt Facile Goals t lt fun gt let min_size_labeling min_size_strategy Goals indomain val min_size_labeling Facile Var Fd t array gt Facile Goals t lt fun gt 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 accordi
10. Overview This module defines the type t of constraints and functions to create and post constraints mainly a create function which allows to build new constraints from scratch this function is not needed when using standard FaCiLe predefined constraints and the mostly useful post function which must be called to actually add a constraint to the constraint store 4 4 1 Basic exception DontKnow Exception raised by the check function of a reified constraint when it is not known whether the constraint is satisfied or violated type priority Type of waking priority val immediate priority val normal priority val later priority Available priorities e immediate as soon as possible for quick updates e normal standard priority e later for time consuming constraints e g Gcc cstr Alldiff cstr type t The type of constraints val create name string gt nb_wakings int gt fprint Pervasives out_channel gt unit gt priority priority gt init unit gt unit gt check unit gt bool gt not unit gt t gt int gt bool gt t gt unit gt t create name nb_wakings fprint priority init check not update delay builds a new constraint e name is a describing string for the constraint Default value is anonymous e nb_wakings is the number of calls to Var delay with distinct waking_id arguments see 4 16 4 within the constraint own delay funct
11. 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 opt 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 Getting Started Chapter 2 Building Blocks FaCiLe offers variables and constraints on integer and set finite domains This chapter first describes how to build a constraint program on standard integer variables while explaining the basics underlying concepts of FaCiLe Then section 2 7 extends the scheme to set variables which work in a similar fashion 2 1 Domains Finite domains of integers are created accessed and handled with functions of module Domain ex haustively described in section 4 6 Domains basically are sets of elements of type Domain elt here integers or sets of integers for the set domains described in section 2 7 1 They are repre sented as functional objects of abstract type Domain t and can therefore be shared Domains are built with different functions according to the domain properties e Domain empty is the empty domain e Domain create is the most general constructor and builds a domain from a list of integers possibly unsorted and
12. min_max t gt elt elt min max d returns both the lower and upper bound of d If d is empty the behaviour is unspecified incorrect return value or exception raised iter elt gt unit gt t gt unit iter f d successively applies function to all element of d in increasing order interval_iter elt gt elt gt unit gt t gt unit interval_iter f d successively applies function f to the bounds of all the disjoint intervals of d in increasing order E g a suitable function to print a domain can be defined as fun mini maxi gt Printf printf d d mini maxi mem elt gt t gt bool member elt gt t gt bool member n d tests if n belongs to d values t gt elt list value d returns the list of values of the domain d fprint_elt Pervasives out_channel gt elt gt unit fprint Pervasives out_channel gt t gt unit Pretty printing of elements and domains sprint t gt string sprint d returns a string representation of d included t gt t gt bool included di d2 tests whether domain d1 is included in domain d2 smallest_geq t gt elt gt elt greatest_leq t gt elt gt elt smallest_geq dom val resp greatest_leq dom val returns the smallest resp greatest value in dom greater resp smaller than or equal to val Raises Not_found if max dom lt val resp min dom gt val largest_hole_around t gt elt gt elt elt largest_hole_aro
13. remove_min amp amp self val indomain Facile Easy Fd t gt Facile Goals t lt fun gt 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 9 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 e a constant e or a mutable value e or the result of a function applied to other invariants e or an attribute of any dynamic data structure e g the maximal value of a finite domain variable 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 n the change of the value of one of 71 will be taken into account in constant time to update 7 The main original use of invariants proposed in 9 is within local search algorithms In our con text it can be used also to compute a heuristic criterion used during se
14. 1_40 6 10 _41 0 5 _42 6 10 unit 3Not infix 2 5 Search 21 2 5 Search Most constraint models are not tight enough to yield directly a single solution so that search and or optimization is necessary to find appropriate ones FaCiLe uses goals to search for solutions All built in goals and functions to create and combine goals are gathered in module Goals see 4 9 This section only introduces ready to use goals intended to implement basic search strategies but more experienced users shall refer to sections 3 1 2Jand 3 4 where combining goals with iterators and building goals from scratch are explained FaCiLe s most standard labeling goals is Goals indomain which instantiates non determini stically a single variable by disjunctively trying each value still in its domain in increasing order To be executed a goal must then be passed as argument to function Goals solve which returns true if the goal succeeds or false if it fails let x Fd create Domain create 4 2 12 val x Facile Var Fd t lt abstr gt Goals solve Goals indomain x bool true Fd fprint stdout x 4 unit So the first attempt to instantiate x to 4 obviously succeeds The values of the domain of x can be enumerated with a slightly more sophisticated goal which fails just after Goals indomain Module Goals provides Goals fail which is a goal that always fails and conjunction and disjunction operators
15. 4 7 unit match Fd value vd with Val n gt Do nothing Unk attr gt Remove every value gt 2 let new_dom Domain remove_up 2 Var Attr dom attr in Fd refine vd new_dom unit Fd fprint stdout vd vd 1 2 unit O Whenever the domain of a variable becomes empty a failure occurs see 2 5 for more explanations about failure match Fd value vd with Val n gt Do nothing Unk attr gt Remove every value lt 4 let new_dom Domain remove_low 4 Var Attr dom attr in Fd refine vd new_dom Exception Fcl_stak Fail Var XxxFd refine Access Besides Fd value and Fd is_var which access the state of a variable module Fd provides the mapping of module Domain functions like Fd size Fd min Fd max Fd values Fd iter and Fd member and they return meaningful values whatever the state bound or unbound of the variable may be let vr Fd interval 5 8 val vr Facile Var Fd t lt abstr gt Fd size vr int 4 let vi2 Fd int 12 val vi2 Facile Var Fd t lt abstr gt Fd member vi2 12 bool true Contrarily function Fd id which returns the unique identifier associated with a variable or function Fd name which returns its specified string name only work if the variable is still unin stantiated otherwise an exception is raised 2 3 Arithmetic Expressions 13 An order based on the integer identifiers is
16. 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
17. defined by function Fd compard as well as an equality function Fd equal observing the following two rules 1 bound variables are smaller than unbound variables 2 unbound variables are compared according to their identifiers Fd id vr int 2 Fd id v12 Exception Failure Fatal error Var XxxFd id bound variable Fd compare v12 Fd int 11 int 1 Fd compare vr v12 int 1 Fd id vd int 0 Fd compare vd vr int 1 Eventually function Fd elt_value returns the integer value of a bound variable If the variable is not instantiated an exception is raised Fd elt_value Fd int 1 Facile Var Fd elt 1 Fd elt_value Fd interval 0 1 Exception Failure Fatal error Var XxxFd elt_value unbound variable _3 2 3 Arithmetic Expressions Arithmetic expressions and constraints over finite domain variables are built with functions and operators of module Arith see 4 2 Creation and Access Arithmetic expressions are objects of abstract type Arith t which contain a representation of an arithmetic term over finite domain variables An expression is ground when all the variables used to build it are bound in such a state an expression can be evaluated with function Arith eval which returns its unique integral value A call to Arith eval with an expression that is not ground raises the exception Invalid_argument However any expression can be printed on an output ch
18. e g Gcc cstr Standard or label mode of the OCaml compiler option labels may be used with the library FaCiLe makes use of labels labelled arguments as less as possible only optional arguments are labelled Compilation with FaCiLe FaCiLe is provided as bytecode and native codd libraries Bytecode version is compiled with debugging information g option of ocamlc and then can be used with the source level replay debugger ocamldebug A lot of checks are done in this mode 1f supported by your architecture See http caml inria fr ocaml portability html vi and exceptions may be raised revealing bad usage of the system fatal errors or bugs in the system itself internal errors In the second case diligent users should send a bug report to the developers In the native code version these redundant checks are not done and this mode should be used only on well tried code The Makefile in the examples directory of the distribution provides generic rules to compile with FaCiLe in both modes producing out bytecode or opt native code executables The library may also be used through linked toplevel produced with the following command after installation ocamlmktop o facile 1 facile facile cma This is the toplevel used in the inlined examples of this documentation and invoked with the command line facile I facile Availability The FaCiLe distribution and documentation are available from
19. e one variable for each area l c r and m e all variables have the same domain 0 1 0 being red and 1 white e one difference constraint for each adjacency l c c r m cand the maple leaf is forced to be red m 0 The following piece of code solves this problem 3 4 Getting Started Figure 1 1 The problem of the Canadian flag maple ml open Facile open Easy let _ Variables let red 0 and white 1 in let dom Domain create red white in let 1 Fd create dom and c Fd create dom and r Fd create dom and m Fd create dom in Constraints Cstr post fd2e 1 lt gt fd2e c Cstr post fd2e c lt gt fd2e r Cstr post fd2e m lt gt 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 1 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 unix ocamlc I facile facile cma maple ml unix a out 1 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 e The user interface to the library is provided by module Facile which gathers several spe cialized submodules We thus advise
20. gt Goals t gt a list gt Goals t exists select g x1 x2 xn isg x1 Il g x2 II Il gxm ie returns the disjunctive iteration of goal g on list a val member Var Fd t gt int list gt Goals t member v 1 returns the disjunctive iteration of the instantiation of the variable v to the values in the integer list 1 Defined by fun v 1 gt exists fun x gt create fun O gt Fd unify v x 1 val labeling Var Fd t list gt Goals t Standard labeling i e conjunctive non deterministic instantiation of a list of variables Defined as forall indomain end 4 10 Module Interval Variable Membership to an Interval 57 4 9 6 Optimization type bb_mode Restart Continue Branch and bound mode val minimize step int gt mode bb_mode gt t gt Var Fd t gt int gt unit gt t minimize step 1 mode Continue goal cost solution runs a Branch and Bound algorithm on goal for bound cost with an improvement of at least step between each solution found With mode equal to Restart the search restarts from the beginning for every step whereas with mode Continue default the search simply carries on with an update of the cost constraint solution is called with the instantiation value of cost which must be instantiated by goal as argument each time a solution is found this function can therefore be used to store e g in a reference the current solution Default step is 1 mini
21. in case of failure unify may be called either on unbound variables or on instantiated variables refine t gt domain gt unit refine v d reduces the domain of v with domain d d must be included in the domain of v otherwise the behaviour is unspecified corrupted system or exception raised refine_low t gt elt gt unit refine_low v inf reduces the domain of v by cutting all values strictly less than inf refine_up t gt elt gt unit refine_up v sup reduces the domain of v by cutting all values strictly greater than sup refine_low_up t gt elt gt elt gt unit refine_low_up v inf sup reduces the domain of v by cutting all values strictly less than inf and greater than sup Robust even if v is already bound checks that inf lt v lt sup otherwise fails 68 Modules 4 16 4 Events and suspending val val val val val end on_refine event Event occuring when a variable is changed i e its domain modified on_subst event Event occuring when a variable is instantiated on_min event on_max event Event occuring when the lower resp upper bound of a variable decreases delay event list gt t gt waking_id int gt Cstr t gt unit delay event_list v waking_id id c suspends constraint c on all the events in event_list occurring on v An optional integer id may be associated to the wakening it must be unique and range from 0 to nb wakings 1 nb_wa
22. let x Fd interval 2 6 and y Fd interval 4 12 let xe fd2e x and ye fd2e y let ineql i2e 3 ye i2e 2 xe ye ile 5 xe ye gt i2e 4300 val ineq1 Facile Cstr t lt abstr gt Cstr fprint stdout ineql 6 4 _18 4 12 10 _20 0 432 lt 4300 unit 2 4 Constraints 17 which ensures 3y 2xy x 5x y gt 4300 i e 10x y 4y gt 4300 is equivalent to ineq2 let ineq2 i2e 10 xe 2 ye i2e 4 ye gt i2e 4300 val ineq2 Facile Cstr t lt abstr gt Cstr fprint stdout ineq 2 9 4 _18 4 12 10 _22 0 432 lt 4300 unit Once posted ineq1 or ineq2 incidentally yield a single solution Printf printf x a y a n Fd fprint x Fd fprint y x _17 2 6 y _18 4 12 unit Cstr post ineql unit Printf printf x a y a n Fd fprint x Fd fprint y x 6 y 12 unit It is also worth mentioning that arithmetic constraints involving large enough sums of boolean variables are automatically detected by FaCiLe and handled internally by a specific efficient mech anism The user may thus be willing to benefit from these features by choosing a suitable problem modeling This automatic behaviour can be tuned by specifying the minimum size from which the constraint is optimized see 4 2 6 Note on Overflows Users should be carefull when expecting the arithmetic solver to compute bounds from variables wi
23. list gt elt Creates a set from a list of integers val interval elt gt elt gt t interval glb lub builds the domain of sets greater than glb and smaller than lub An Invalid_argument exception is raised if glb is not a subset of lub 4 13 2 Access and Operations val size t gt int size d returns glb d lub d 1 i e the height of the lattice not its number of elements val min t gt elt val max t gt elt val min_max t gt elt elt Access to glb and lub val fprint_elt Pervasives out_channel gt elt gt unit val fprint Pervasives out_channel gt t gt unit Pretty printing of elements and domains val mem elt gt t gt bool mem x d tests whether x belongs to the domain d val included t gt t gt bool included di d2 tests whether the domain d1 is included in d2 i e glb d2 included in elb d1 and lub d1 included in lub d2 val iter elt gt a gt t gt a Iteration on values of the domain Exponential with the size of the domain val values t gt elt list Returns values of a domain Exponential with the size of the domain 4 14 Module Sorting Sorting Constraint val sort Var Fd t array gt Var Fd t array sort a returns an array of variables constrained to be the variables in a sorted in increasing order val sortp Var Fd t array gt Var Fd t array Var Fd t array 4 15 Module Stak Global Stack of Goals Backtrackable Opera
24. min_of_expr e max_of_expr e 4 2 4 Arithmetic Constraints on Expressions FaCiLe processes arithmetic constraints to try to simplify and factorize common subexpressions Furthermore auxilliary variables are created to handle non linear expressions and substituted to the original terms So printing an arithmetic constraint may produce something quite different from the user s input val lt 7 t gt t gt Cstr t val lt t gt t gt Cstr t val 7 t gt t gt Cstr t val gt 7 t gt t gt Cstr t val gt 7 t gt t gt Cstr t val lt gt 7 t gt t gt Cstr t Strictly less less or equal equal greater or equal strictly greater and different constraints on expressions val shift Var Fd t gt int gt Var Fd t shift x d returns a finite domain variable constrained to be equal to x d 4 2 5 Reification The following operators are shortcuts to lighten the writing of reified expressions They replace the corresponding constraint by an expression equal to a boolean variable that is instantiated to 1 when the constraint is satisfied and to 0 if it is violated See module Reify val lt 77 t gt t gt t el op e2 is equivalent to fd2e Reify boolean el op e2 val lt t gt t gt t val t gt t gt t val gt 7 t gt t gt t val gt 77 t gt t gt t val lt gt t gt t gt t Reified strictly less less or equal equal grea
25. of a variable by labeling its domain in increasing order val instantiate Domain t gt int gt Var Fd t gt t instantiate choose var Non deterministic instantiation of a variable by labeling its domain using the value returned by the choose function val dichotomic Var Fd t gt t Non deterministic instantiation of a variable by dichotomic recursive exploration of its domain Instantiation of Set Variables module Conjunto sig val indomain Var SetFd t gt Goals t Non deterministic instantiation of set variables refine of Gervet s Conjunto 3 end 4 9 4 Operations on Array of Variables module Array sig val foralli select a array gt int gt int gt a gt Goals t gt a array gt Goals t foralli select g a returns the conjunctive iteration of the application of goal g on the elements of array a and on their indices The order is computed by the heuristic select which must raise Not_found to terminate Default heuristic is increasing order over indices val forall select a array gt int gt a gt Goals t gt a array gt Goals t forall select g a defined by foralli select fun i x gt g x a ie indices of selected elements are not passed to goal g val existsi select a array gt int gt int gt a gt Goals t gt a array gt Goals t existsi select g a returns the disjunctive iteration of the application of goal g on th
26. 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 B 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 Cstr id Cstr name 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 precis
27. rec name create_rec f returns a goal calling f f takes the goal itself as argument and should return a goal success to stop Useful to write recursive goals name default value is create_rec 4 9 3 Operators and Built in Goals val 887 t gt t gt t val t gt t gt t Conjunction and disjunction over goals Note that these two operators do have the same priority Goals expressions must therefore be carefully parenthesized to produce the expected result val forto int gt int gt int gt t gt t val fordownto int gt int gt int gt t gt t forto min max g resp fordownto min max g returns the conjunctive iteration of goal g on increasing resp decreasing integers from min resp max to max resp min val once t gt t once g cuts choice points left on goal g val sigma domain Domain t gt Var Fd t gt t gt t sigma domain Domain int fgoal creates the goal fgoal v where v is a new variable of domain domain Default domain is the largest one It can be considered as an existential quantification hence the concrete notation sigma of this function because existential quantification can be seen as a generalized disjunction 4 9 Module Goals Building and Solving Goals 55 Instantiation of Finite Domain Variables val unify Var Fd t gt int gt t unify var x instantiates variable var to x val indomain Var Fd t gt t Non deterministic instantiation
28. ss aa asa ow a aka Ae ee aa BH Ge en HG 3 3 User s Constraints 24 4 4 44 4 48 daa eee we ey Re es 34 Users Goals 544625 4004 66 BARGE Ewa a Ja an ban a Ss i donde e Ug be Aad OR ee eh heya E Go E NN ese etch ccs len Shae ara ete ok a 3 5 Backtrackable Invariant References B RS 2 22 22 2 222 nn 3 5 1 Type creation access and modification 2222 3 0 2 Operations 22 ssia 4 4 waa dae as ee a 3 5 3 Domain access ix 10 13 15 15 16 17 19 21 23 24 24 24 25 25 CONTENTS II Reference Manual 4 1 Module Alldiff The All Different Constraint 4 2 Module Arith Arithmetic Expressions and Constraints 4 21 B sic lie is 2 2 5 6 4 8 4 SR RR ee Oa ge ee PEFFE 423 ACCESS o e e 2 in an ae ee o a ja a a a a A 4 2 4 Arithmetic Constraints on Expressions EE E O 4 2 6 Boolean sums setting 4 3 Module Conjunto Constraints on Finite Sets MAA Basic sea e a eee eRe eed a A AAD ACCESS we 44 24 04 2 ew eee a RA eG 4 5 Module Data Bactrackable Data Structures oe eee 4 6 1 Building New Domains 22 2 2 2 2 nenn 4 6 2 ACCeSS i ea a Re adden 4 6 3 Operations 0 2 0 2 o SR 4 8 Module Gce Global Cardinality Constraint 4 9 Module Goals Building and Solving Goals 4 9 1 ACCESS o wa una A ad 4 9 2 Creation 6 6 4 2 044445 24 4 6 pee ee oR wd
29. the web site where general infor mation can be found http www recherche enac fr opti facile Questions bug reports can be mailed to facile recherche enac fr Installation Installation of FaCiLe is described in the README file of the distribution Below is a copy of the corresponding part INSTALLATION All you need is the Objective Caml 3 02 or greater compiler and standard Unix tools make 0 Configure the library The single option of configuration is the directory you want to put the library files in facile cma facile cmxa facile a facile cmi Default is the subdirectory facile of the Ocaml library directory returned by ocamlc where configure faciledir lt target directory gt 1 First compile the library with a simple make 2 Check the result make check You should get a solution for the 8 queens problem vii 3 Then install the library with a usually as root make install Examples The directory examples of the distribution contains some examples and a generic Makefile to compile files with FaCiLe Examples are taken from the classic litterature Coins Give back change for any amount Golf Organize a golf tournament for 8 teams of 4 players Golomb Find optimal Golomb rulers Jobshop Solve the famous mt10 scheduling problem Edge Finding inside Magic To count and to be counted Marriage Stabilize preferences among spouses Prolog Use FaCiLe as a Prolog interpreter on
30. v with Val n gt f_bound n Unk attr gt f_unbound attr An alternative boolean function Fd is_var returns the current state of a variable sparing the match construct let vi Fd create Domain create 1 equivalent to Fd int 1 val vi Facile Var Fd t lt abstr gt Fd is_var v1 bool false Fd fprint stdout vi 1 unit Domain Reduction Module Fd provides two functions to perform backtrackable domain reductions on variables typ ically used within instantiation goals and filtering of user defined constraints e unify v n instantiates variable v to integer n or fails whenever n does not belong to the domain of v unify may be called on instantiated variables let vr Fd interval 2 6 val vr Facile Var Fd t lt abstr gt Fd unify vr 7 Exception Fcl_stak Fail Var XxxFd subst Fd unify vr 5 unit I Type Var concrete_fd constructors Unk and Val stand respectively for Unknown unbound and Value bound 12 Building Blocks Fd fprint stdout vr 5 unit Fd unify vi 2 Exception Fcl_stak Fail Var XxxFd unify Fd unify vi 1 unit e refine v dom reduces the domain of v to dom dom must be included in the current domain of v otherwise an assert failure is raised with the byte code library facile cma or the system will be corrupted with the optimized native code library facile cmxa Fd fprint stdout vd vd 1 2
31. 09 and o and r Fd interval 09 and y Fd interval 09 in Constraints Cstr post fd2e m gt i2e 0 Cstr post fd2e s gt i2e 0 let digits ls e n d m o r yl in Cstr post Alldiff cstr digits let c Fd array 3 0 1 in Carry array Fd interval 0 9 Fd interval 0 9 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 d d 4d dWn value s value e value n value d Printf printf d 4d 4d dWn value m value o value r value e Printf printf d 4d d 4d 4dWn value m value o value n value e value y end else prerr_endline No solution unix ocamlc I facile facile cma smm ml unix a out 9567 1085 10652 We detail each step of the above example e 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 e Disequations M 4 0 and S 0 are then expressed by arithmetic inequality constraints and we assert that all digits must be distinct with the global Alldiff
32. 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 Stak fail 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 gt unit Goals Array and Goals List modules of FaCiLe allows to construct conjunction with a amp amp and di
33. 17 ES 652 56 63 Invariant 37 Domain 5 9 Var Fa 5 10 create_rec Cstr estr 1 51 55 55 E1 Alldiff 6 NI als BEE 72 INDEX delay 30 66 depth 61 dichotomic 53 diff 50 59 difference 50 Domain 10 disjoint 44 50 Conjunto 25 don 11 62 Domain 48 domain 02 63 domaine FE DontKnow 45 e2fd Easy module element constraint see get elements et 28 68 69 61 61 elt_of_list elt_value elt_value 13 empty 928 59 SetDomain S 24 equal 12 59 eval 13 42 event 80 62 63 events 15 29 30 exists existsi 53 Fail fail Goals FD 57 60 Fa 55 60 fd fd2e FdArray find floundering fold forall Goals Array 28 Goals List 29 foralli 53 fordownto 82 forto Sprint BS 2 87 85 52 50 160 EA 5 Domain 9 Invariant 88 SetDomain 24 Var SetFd 24 25 Arith 19 Cstr 16 Var Attr E Var Fa 5 10 fprint_array 65 fprint_elt 49 60 Gcc get PT ET ET BO ETE FdArray 18 get_boolsum_threshold 43 get_cstr glb Goals goals user s defined arbitrary atomic recursive greatest_leq Hashtb1 47 120 5 E sa 101150 65 E Var Attr 11 Var Fa 12 immediate 45 included 49 60 indomain 21 53 Goals Conjunto 25 inf_min 44 inside Conjunto instantiate int Domain 9 Var Fa 10 int_value
34. All the modules are extensively described in part Hof this documentation We do not recommend to users to open modules in Facile but to use prefixed notations e g function post of Cstr is written Cstr post The pseudo module named Easy is the exception and should be opened it provides several aliases to the most frequently used values see 4 17 and functions To avoid interferences with other modules of the user all the modules are aliased in the Facile module and implementation module files are all prefixed by fcl_ except of course Facile itself For example implementation of module Gcc is in file fcl_gec ml and alias module Gcc Fcl_gcc is defined in Facile facile ml This alias mechanism is entirely transparent to the user of FaCiLe except for the one interested by the implementation of the library The only possible visibility of Fcl_ prefix is given by the uncaught exceptions printer e g Fcl_stak Fail instead of Stak fail The reference part of this documentation is automatically generated from module interfaces mli Some available functions types or modules are intentionally not documented or even hidden in Facile module They are not intented to the casual user Values and types names try to benefit as much as possible from the modularity For example most of the types are named t type of constraints is Cstr t type of domains is Domain t In the same way printing functions are named fprint constraints are named cstr
35. Bin_matching evt uses a more sophisticated algorithm namely a bin matching 6 which is called whenever the event evt see 3 2 1 occurs on one of the variables to globally check the satisfiability of the constraint 18 Building Blocks let vars Fd array 5 0 4 val vars Facile Var Fd t array l lt abstr gt lt abstr gt lt abstr gt lt abstr gt lt abstr gt let ct Alldiff cstr vars val ct Facile Cstr t lt abstr gt Fd fprint_array stdout vars 1_23 0 4 _24 0 4 _25 0 4 _26 0 4 _27 0 4 unit Cstr post ct Fd unify vars 0 3 unit Fd fprint_array stdout vars 13 _24 0 2 4 _25 0 2 4 _26 0 2 4 _27 0 2 4 unit Module FdArray provides the element constraint named FdArray get which allows to index an array of variables by a variable and the min resp max constraint which returns a variable constrained to be equal to the variable that will instantiate to the minimal resp maximal value among the variables of an array let vars Fd interval 7 12 Fd interval 2 5 Fd interval 4 81 val vars Facile Var Fd t array lt abstr gt lt abstr gt lt abstr gt let index Fd interval 10 10 val index Facile Var Fd t lt abstr gt let vars_index FdArray get vars index val vars_index Facile Var Fd t lt abstr gt Fd fprint stdout index _31 0 2 unit Fd fprint stdout vars_index _32 2 12 uni
36. FaCiLe A Functional Constraint Library Release 1 1 N BARNIER P BRISSET October 6 2004 er er Preface FaCiLe is a constraint programming library over integer finite domains written in OCaml 8 It offers all usual constraints system facilities to create and handle finite domain variables arith metic expressions and constraints possibly non linear built in global constraints and search goals FaCiLe allows to easily build user defined constraints and goals including recursive ones from scratch or by combining simple primitives making pervasive use of OCaml higher order func tionals to provide a simple and flexible user interface As FaCiLe is an OCaml library and not yet another language the user benefits from type inference and strong typing discipline high level of abstraction modules and objects system as well as native code compilation efficiency garbage collection and replay debugger All these features of OCaml among many others allow to prototype and experiment quickly modeling data processing and interface are implemented with the same powerful and efficient language This manual is not a document about constraint programming techniques but only a tool description Users should be familiar with other constraint systems to easily apprehend FaCiLe through the reading of this manual Beginners can easily find comprehensive information on the Web e g http www cs unh edu ccc archive This manual is neither
37. _low remove_low_up remove_max remove_min 50 remove_up 10 50 59 replace E s 211159 scalprod 15 42 scalprod_fd 15 15 42 search 21 2 select Goals Array 28 Goals List sr B7 EN BT E set variables 2 Conjunto 25 constraints domains labeling glb lub set_boolsum_threshold setable setable_t SetAttr SetDomain 59 SetDomain S 24 74 INDEX SetFa 58 66 shift 43 sigma 52 singleton size 48 58 60 61 63 64 Var Attr 11 Var Fa 12 smallest 44 smallest_geq 49 solve 5 21 55 sort 60 Sorting sortp sprint Stak subset success 21 sun 7 BEAJET sum_fd 42 sum_weight 44 4 ET ES E ES EA lee t type Arith 19 Cstr 115 Domain 5 p Var Attr 11 Var Fa 10 ternary 57 times 50 toplevel unary 38 57 58 unify 53 65 Var SetFa 24 Goals 22 Var Fd union 44 50 Conjunto 25 Domain 10 unsafe_create unsetable unsetable_t update value 11 64 values 49 60 66 Domain 9 Var Fd Var variables 5 6 access ehem creation domain reduction waking identity waking_id 83 xor 19 59 zero 46 Bibliography 1 Nicolas Barnier Application de la programmation par contraintes des probl mes de gestion 10 du trafic a rien PhD thesis Institut National Polytechnique
38. a course about func tional programming and users should refer to the official Caml Web site at http caml inria fr and the OCaml manual 8 to obtain introductory as well as advanced material about the host language of FaCiLe Hurried readers may also take a look at a short overview appearing in the ALP Newsletter 2 Thorough ones may find deeper insights on FaCiLe implementation details unveiled in the second part of one of the author PhD thesis 1 Since OCaml forbids overloading FaCiLe unusual looking operators might be a little discon certing at first sight Moreover there is no implicit casting so explicit conversions between vari ables or integer and arithmetic expressions are compulsory These features lead to less concise expressions than with poorly typed languages however the user precisely knows which operation is executed by the system and cannot erratically mix values of different types Furthermore ML style higher order functionals and powerful type system ease the design and processing of complex data structures without the need of syntactic sugar iterators mapping and folding are native in OCaml So FaCiLe does not endlessly provide more and more ad hoc functions for each particular case to exhibit the smallest possible code for toy examples but rather aims at featuring simple building blocks and operators to combine them efficiently This manual is structured in two main parts 1 The user s manual which star
39. a family tree problem Queens Place queens on a chessboard Seven eleven My grocer s favorite arithmetic puzzle Tiles Tile a big square with small squares Contents I User s Manual 1 Getting Started ll Basicslia sr isa eS Ng Sete eee AeA ET OA ee ee ee nag 1 2 A Classic Examplel o se et e caasa aan aie a ee 2 Building Blocks 21 DOMAINS eons 2 4 4 ee ar aa aa ES SE AR RA da eaaa 2 9 Va abl s se sess 2 20 5 4 m au Ho ad eee a ala deta edd a da a 4 2 3 Arithmetic Expressions ee 2A Constraints x 2 a e wh aa Ae aE Ee HR Ae A A de as DAT Creation and Usel a sa s a 2 uns ea hee RRR 2 4 2 Arithmetic Constraints 2 a 2 4 3 Global Constraints NG paria Bs ANAS GG he ae es ee oes AE AS A AA aid a haw a ae en NN Bd Be de TR gece tna Se ea arc E op ese cae Gee Ge Gees as a 2 7 Constraint Programs on Finite Sets 2 2 en 271 Set Domains p aats a eed ae PE aS eee Ee E a 2 1 2 Sek Variables s 24 a amp dose a aa arte de ev dr RS ni 2 7 3 Constraints 2 2 2 2m nn 2 7 4 Labeling 2 24 sa rs near 3 Advanced Usage 3d Search Control 2 222 a an OE eee anne 3 1 1 Basic Mechanismsl lt ooo aa a a ne ee NG NG oe oe ee ee 3 2 Constraints Control sra wi A kana nerd a ee a ee aa AA a ead 4 4 Bk OU ee add ewes ee eek Ob bw boa eh BS 3 2 2 Suspending to Events Waking Identity 2 22 222 be ke ee iv lato tal a Gh ae Be BE E e ehh HO Deere 3 24 Constraint Store s
40. all g x let sol ref in let store Goals atomic fun gt sol Fd elt_value x sol in let goal g x amp amp store amp amp Goals fail in ignore Goals solve goal Isol val findall Facile Easy Fd t gt Facile Goals t gt Facile Easy Fd t gt Facile Easy Fd elt list lt fun gt RHHXHXHHXH 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 4 16 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 gt Facile Goals t lt fun gt 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 latte
41. annel with function Arith fprint A variable of type Fd t or an OCaml integer of type int are not arithmetic expressions and therefore cannot be mixed up with the latter Conversion functions are provided by module Arith to build an expression from variables and integers e Arith i2e n returns an expression which evaluates to integer n e Arith fd2e v returns an expression which evaluates to n when v is bound to n 2Comparison functions return 0 if both arguments are equal a positive integer if the first is greater than the second and a negative one otherwise as specified in the OCaml standard library 14 Building Blocks Handily enough opening module Easy allows direct access to most useful functions and operators of module Arith including i2e and fd2e let vi Fd interval 2 5 val vi Facile Var Fd t lt abstr gt let expi fd2e vi val exp1 Facile Arith t lt abstr gt Arith fprint stdout expl _4 2 5 unit Arith eval expl Exception Failure Fatal error Expr eval variable _4 unknown Fd unify vi 4 unit Arith eval expl int 4 Arith fprint stdout i2e 2 2 unit Maximal and minimal values of expressions can be accessed by functions Arith max_of_expr and Arith min_of_expr let exp2 fd2e Fd interval 3 12 val exp2 Facile Arith t lt abstr gt Arith min_of_expr exp2 int 3 Arith max_of_expr exp2 int 12 Conver
42. arch 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 e a mutable integer BIR has type int setable Inv t e whereas a non mutable float BIR has type float notsetable Inv t 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 lt abstr gt val y float Facile Invariant unsetable_t lt abstr gt Invariant get x Invariant get y int float 1729 3 14 Invariant set x 1730 unit Invariant get x int 1730 38 Advanced Usage Like finite domain variables BIRs can be named thanks to an optional string argument name and feature a unique integer identity accessible with function Invariant id 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 g
43. ars is empty Not reifiable val min_cstr Var Fd t array gt Var Fd t gt Cstr t val max_cstr Var Fd t array gt Var Fd t gt Cstr t min cstr vars mini resp max_cstr vars maxi returns the constraint fd2e min vars fd2e mini resp fd2e max vars fd2e maxi Raises Invalid_argument if vars is empty Not reifiable val get Var Fd t array gt Var Fd t gt Var Fd t get vars index returns a variable constrained to be equal to vars index Variable index is constrained within the range of the valid indices of the array 0 Array length vars 1 Raises Invalid_argument if vars is empty Not reifiable val get_cstr Var Fd t array gt Var Fd t gt Var Fd t gt Cstr t get_cstr vars index v returns the constraint fd2e vars index fd2e v Variable index is constrained within the range of the valid indices of the array 0 Array length vars 1 Raises Invalid_argument if vars is empty Not reifiable 4 8 Module Gcc Global Cardinality Constraint type level Basic Medium High val cstr level level gt Var Fd t array gt Var Fd t int array gt Cstr t cstr level High vars distribution returns a constraint ensuring that for each pair c v of cardinal variable c and integer value v in the list distribution c variables in the array vars will be instantiated to v i e card vi v vi in vars c All values v in distribution must be different otherwise the exception Invalid_ar
44. cardinality constraint In Pro ceedings of the Thirteenth National Conference on Artificial Intelligence 1996 75
45. cile Var Fd t lt abstr gt let xor cti ct2 Reify not ct1 lt gt ct2 in let xor_cstr xor fd2e x i2e 5 fd2e y i2e 5 in Cstr post xor_cstr Cstr post fd2e x lt i2e 4 Printf printf x a y a n Fd fprint x Fd fprint y x _38 3 4 y 5 unit Furthermore module Arith contains convenient shortcuts to reify its basic arithmetic con straints These operators stand for the reification and transformation into arithmetic expression of their basic counterparts i e they take two arithmetic expressions as operands and yield a new arithmetic expression being the boolean variable related to the truth value of the arithmetic constraint el e2 is therefore equivalent to fd2e Reify boolean el e2 These operators can also be directly accessed through the opening of module Easy In the following example the constraint stating that at least two of the three variables contained in array vs must be greater than 5 is expressed with the reified greater or equal gt let vs Fd array 30 10 val vs Facile Var Fd t array lt abstr gt lt abstr gt lt abstr gt Cstr post Arith sum Array map fun v gt fd2e v gt i2e 5 vs gt i2e 2 Fd fprint_array stdout vs 1_40 0 10 _41 0 10 _42 0 10 1 unit If vs 1 is forced to be less than 5 the two other variables become greater than 5 Cstr post fd2e vs 1 lt i2e 5 Fd fprint_array stdout vs
46. cstr constraint which takes an array of variables as argument see 4 1 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 4 14 embedded in separate module and called with function cstr e 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 func tions 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 e 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 1 2 A Classic Example 7 We could of course have used a different but equivalent model constraining the addition to be exact without auxilliary carry variables let opi i2e 1000 fd2e s i2e 100 fd2e e i2e 10
47. 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 gt a lt gt b Val a Unk attr_y when not Var Attr member attr_y a gt true Unk attr_x Val b when not Var Attr member attr_x b gt true Unk attr_x Unk attr_y when 3 3 User s Constraints 33 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 gt true _ gt 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 diff ml 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 lt abstr gt val y Facile Easy Fd t lt abstr gt let diseq Diff cstr x y val diseq Facile Cstr t lt abstr gt Cstr post diseg unit let goal Goals indomain x amp amp Goals indomain y amp am
48. de Toulouse December 2002 www recherche enac fr opti papers thesis Nicolas Barnier and Pascal Brisset FaCiLe a Functional Constraint Library ALP Newsletter 14 2 May 2001 Carmen Gervet Interval propagation to reason about sets Definition and implementation of a practical language Constraints 1 3 191 244 1997 www icparc ic ac uk cg6 Noelle Bleuzen Guernalec and Alain Colmerauer Narrowing a 2n block of sorting in O nlogn In Principles and Practice of Constraint Programming Springer Verlag 1997 William D Harvey and Matthew L Ginsberg Limited discrepancy search In Chris Mellish editor Fourteenth International Joint Conference on Artificial Intelligence IJCAI 95 volume 1 pages 607 615 Montral Qubec Canada August 1995 Morgan Kaufmann J Hopcroft and R Karp An n algorithm for maximum matching in bipartite graphs SIAM Journal of Computing 2 4 225 231 1973 Serge Le Huitouze A new data structure for implementing extensions to Prolog In P De ransart and J Matuszy ski editors PLILP 90 LNCS 456 pages 136 150 Springer Verlag 1990 10 Xavier Leroy The Objective Caml System User s and reference manual http caml inria fr 2000 Laurent Michel and Pascal Van Hentenryck Localizer A modelling language for local search In Proceedings of the Third Conference on Principles and Practice of Constraint Programming 1997 Jean Charles R gin Generalized arc consistency for global
49. e Backtrackable Invariant Refer ences noted BIR in the sequel BIRs are single valued variables whose values are restored upon backtracks and which are linked by one way constraints They maintain functional dependencies between source setable BIRs initialized with their creation value and unsetable BIRs built upon them BIRs may be convenient to automatically handle heuristic criteria or the data structures of local search algorithms 9 Note that circular dependencies are not allowed by the typing policy type Ca b t type setable type unsetable type a setable_t a setable t type a unsetable_t a unsetable t Type of BIRs Parameter a stands for the type of the value of the BIR Parameter b is setable if the BIR can be assigned unsetable if not setable_t and unsetable_t are shortcuts 4 11 1 Creation and access val create name string gt a gt a setable_t create name v returns a setable BIR with initial content v An optional string can be given to name the BIR val constant name string gt a gt a unsetable_t constant name cst returns an unsetable BIR with initial content cst An optional string can be given to name the BIR val set a setable_t gt a gt unit Assignment of a setable BIR val get a b t gt a Access to the content of a BIR val id Ca b t gt int id r returns a unique integer associated to BIR r
50. e elements of array a and on their indices The order is computed by the heuristic select which must raise Not_found to terminate Default heuristic is increasing order over indices val exists select a array gt int gt a gt Goals t gt a array gt Goals t 56 Modules exists select g a defined by existsi select fun ix gt g x a ie indices of selected elements are not passed to goal g val choose_index Var Attr t gt Var Attr t gt bool gt Var Fd t array gt int choose_index order fds returns the index of the best minimun free not instantiated variable in the array fds for the criterion order Raises Not_found if all variables are bound instantiated val not_instantiated_fd Var Fd t array gt int not_instantiated_fd fds returns the index of one element in fds which is not instantiated Raises Not_found if all variables in array fds are bound val labeling Var Fd t array gt Goals t Standard labeling i e conjunctive non deterministic instantiation of an array of variables Defined as forall indomain end 4 9 5 Operations on List of Variables module List sig val forall select a list gt a a list gt a gt Goals t gt a list gt Goals t forall select g x1 x2 xn isg x1 487 g x2 48 amp amp g xn Le returns the conjunctive iteration of goal g on list a val exists select a list gt a a list gt a
51. e is Goals Continue 2 7 Constraint Programs on Finite Sets CP can be parameterized by the mathematical structure on which to express variables and con straints In almost the same way FaCiLe uses the generic mechanism of functors to provide variables either on integers domain or on finite sets of integers domain Hence the interface of type BASICFD see on which variables are built is the same for both types and then further extended for integer ones once parameterized by the Domain module and once by the SetDomain one So the few previous sections are relevant to document set variables and constraints Specific issues are discussed below 2 7 1 Set Domains The standard Domain module builds domain of type Domain t from its basic elements integers whose type is aliased as Domain elt Similarly the SetDomain module builds domain of type SetDomain t from basic elements set of integers with type SetDomain elt The latter type simply is an alias for type SetDomain S t of module SetDomain S which provides values and functions to build and handle elements of SetDomain see 4 13 Set domains represent sets of integers sets They are described as powerset lattices of sets bounded by its definite elements the glb Greater Lower Bound and possible elements lub Lower Upper Bound So the glb corresponds to the min value of an integer domain while the lub corresponds to its max Figure 2 1 illustrates the representation of the follow
52. e of v if it is instantiated and raises a Failure exception otherwise val int_value t gt elt val size t gt int size v returns the number of integer values in the domain of v 1 if v is instantiated 4 16 Module Var Constrained Attributed Finite Domain Variables 67 val val val val val val val member t gt elt gt bool member v n returns true if n belongs to the domain of v and false otherwise id t gt int id v returns a unique integer identifying the attribute associated with v Must be called only on non ground variable raise Failure otherwise name t gt string name v returns the name of variable v the empty string if it was not provided while created Must be called only on non ground variable raise Failure otherwise compare t gt t gt int Compares two variables Values bound variables are smaller than unknowns unbound variables Unknowns are sorted according to their attribute id equal t gt t gt bool Tests if two variables are equal with respect to compare fprint Pervasives out_channel gt t gt unit fprint chan v prints variable v on channel chan fprint_array Pervasives out_channel gt t array gt unit fprint_array chan vs prints array of variables vs on channel chan 4 16 3 Refinement val val val val val unify t gt elt gt unit unify v n instantiates variable v with integer value n Raises Stak Fail
53. ed otherwise i e it is not yet known if the constraint is satisfied or violated and the boolean variable is not instantiated the reification of a constraint does not perform any domain reduction on the variables involved In the following example the boolean variable x_less_than_y is constrained to the truth value of the inequation constraint x lt y let x Fd interval 3 6 and y Fd interval 5 8 val x Facile Var Fd t lt abstr gt val y Facile Var Fd t lt abstr gt let x_less_than_y Reify boolean fd2e x lt fd2e y val x_less_than_y Facile Var Fd t lt abstr gt Fd fprint stdout x_less_than_y _36 0 1 unit Cstr post fd2e y gt i2e 7 unit Fd fprint stdout x_less_than_y 1 unit Fd fprint stdout Reify boolean fd2e x fd2e y 0 unit When posted the reification of a constraint calls the check function see 3 3 of the constraint which verifies whether it is satisfied or violated without performing domain reduction If it is violated the negation of the constraint is posted with a call to another function of the constraint dedicated to reification namely not see 3 3 Both functions are always defined for all constraints but their default behaviour is merely exception raising Failure Fatal error which means that the constraint is actually not reifiable as specified in the documentation of the relevant constraints in the reference manual R
54. eification functions and operators only work on reifiable constraints i e constraints endowed with a check function and a not function or built in constraints for which the doc umentation does not mention Not reifiable Otherwise a Failure fatal error exception is raised val boolean delay_on_negation bool gt Cstr t gt Var Fd t boolean delay_on negation true c returns a boolean 0 1 variable associated to the constraint c The constraint is satisfied iff the boolean variable is instantiated to 1 Conversely its negation is satisfied iff it is instantiated to 0 The waking conditions of the contraint relating c and the boolean variable are the ones set by the delay function of c set by the delay argument of Cstr create If the optional argument delay_on_negation is set to true the new constraint is also attached to the events that awake the negation of c i e the constraint returned by the not function of c otherwise it is not delay_on_negation default value is true val cstr delay_on_negation bool gt Cstr t gt Var Fd t gt Cstr t cstr delay_on_negation true c b is equivalent to the constraint boolean delay_on negation c b delay_on negation default value is true 4 13 Module SetDomain Integer Set Domain Operations 61 4 12 1 Operators val 4877 Cstr t gt Cstr t gt Cstr t val 77 Cstr t gt Cstr t gt Cstr t val gt Cstr t gt Cstr t gt Cstr t val lt gt
55. ely control the behaviour of the resulting constraint Cstr create name string gt nb_wakings int gt fprint out_channel gt unit gt 3 3 User s Constraints 31 priority Facile Cstr priority gt init unit gt unit gt check unit gt bool gt not unit gt Facile Cstr t gt int gt bool gt Facile Cstr t gt unit gt Facile Cstr t lt fun gt However to define a new simpld 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 e update should perform propagation domains filtering and consistency checks Tt must return true iff the constraint is consistent raise Stak Fail whenever an inconsistency is detected and return false otherwise Its integer parameter should be ignored as in the first example below if waking ids are not used as 0 will consistently be fed as argument e delay schedules the awakening of the constraint i e the execution of its update function The delay argument takes only one argument ct which is the constraint itself To specify on which events the constraint is to be woken this function must call Var XxxFd delay once or several times as shown in the example below This latter function takes an events list a variable and the constra
56. ented at each choice point Useful to implement search strategies such as Limited Discrepancy Search 5 4 15 2 Control exception Level_not_found of level Raised by cut val cut level gt unit cut 1 cuts the choice points left on the stack until level 1 Raise Level_not_found if level is not reached and stack is empty 64 Modules exception Fail of string Raised during solving whenever a failure occurs The string argument is informative val fail string gt a fail x equivalent to raise Fail x 4 15 3 Backtrackable References type a ref Backtrackable reference of type a Le type of mutable data structures restored on backtracking val ref a gt a ref Returns a reference whose modifications will be trailed during the solving of a goal val set a ref gt a gt unit Sets a backtrackable reference val get a ref gt a Dereference 4 16 Module Var Constrained Attributed Finite Domain Variables module type ATTR sig type t Type of attributes type domain Type of domains stored in attributes type elt Type of element of domains type event Type of events modifications on variables on which to suspend val dom t gt domain dom a returns the integer domain of an attribute val on_refine event Event occuring when a variable is changed i e its domain modified val on_subst event Event occuring when a variable is insta
57. eption is raised not must be specified if the constraint is reifiable as well as check not should return a constraint which is the negation of the constraint being defined When the constraint is reified it is called to post the negation of the constraint whenever check O return false i e the negation is entailed by the constraint store Default Failure exception is raised update is a mandatory argument which propagates the constraint i e filters domains and checks consistency This function takes an integer as its unique parameter according to the optional waking_id argument given to the Var delay calls featured in the constraint own delay function see below When a waking event occurs this function is called with the corresponding integer waking_id and must return true when the constraint is partially satisfied for this event false if further propagations have to be performed and raise Stak Fail whenever an inconsistency is detected The whole constraint is solved when update 0 update nb_wakings 1 have all returned true E g a global constraint on an array of variables can be aware of which variable has triggered the awakening by providing the integer index of the variable as its waking_id to the Var delay function update is called with 0 by default when the nb_wakings argument has been omitted in this case the constraint is solved as soon as update returns true delay schedules the awakening of the con
58. es 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 vii 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 1 facile facile cma and invoked with facile 1 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
59. estored as before its execution by Goals solve The following example solves the minimization of x y while x y 10 let x Fd interval 0 10 and y Fd interval O 10 in Cstr post fd2e x fd2e y i2e 10 let c Arith e2fd fd2e x 2 fd2e y 2 in let store ref None in let solution cc store Some cc Fd elt_value x Fd elt_value y Printf printf Found d n cc in let g Goals minimize Goals indomain x amp amp Goals indomain y c solution in if Goals solve g Goals success then match store with None gt Printf printf No solution n Some best_c best_x best_y gt Printf printf Optimal solution cost d x d y d n best_c best_x best_y Found 100 Found 82 Found 68 Found 58 Found 52 Found 50 Optimal solution cost 50 x 5 y 5 unit Additionally Goals minimize has two optional arguments e step the improvement between two consecutive solutions must be greater than step i e the constraint posted each time a solution is found is c lt cc step step default value is obviously 1 24 Building Blocks e mode may be either Goals Restart or Goals Continue of type bb_mode with mode Restart the search restarts from the beginning at each step i e the system backtracks until the very state prior to the execution of minimize whereas with mode Continue the search simply carries on with an update of the cost constraint Default mod
60. eturn an integer candidate for instantiation Labeling of variable x in decreasing order is then merely let label_and_print labeling v labeling v amp amp gprint_fd v amp amp Goals fail Goals success 22 Building Blocks val label_and_print Facile Var Fd t gt Facile Goals t gt Facile Var Fd t gt Facile Goals t lt fun gt Goals solve label_and_print Goals instantiate Domain max x 12 2 4 bool true Function label_and_print is defined here to lighten the writing of enumeration goals it takes only the instantiation goal and the variable as arguments In the example below variable x is labelled in increasing order of the absolute value of its values Function Domain choose allows to only specify the relevant order let goal label_and_print Goals instantiate Domain choose fun vi v2 gt abs vi lt abs v2 x val goal Facile Goals t lt abstr gt Goals solve goal 2 4 12 bool true Beside non deterministic instantiation FaCiLe provides also Goals unify to enforce the in stantiation of a variable which might be already bound to a given integer value Goals solve Goals unify x 2 bool true Fd fprint stdout x 2 unit Goals solve Goals unify x 12 bool false Goals solve Goals unify Fd int 0 0 bool true Search strategy Like most CP system FaCiLe default standard strategy is Depth First Search Howe
61. goal is to use the Goals atomic function which soalifies any unit function i e of type unit gt unit Let s write the goal which writes a variable on the standard output let gprint_fd x Goals atomic fun gt Printf printf a n Fd fprint x val gprint_fd Facile Easy Fd t gt Facile Goals t lt fun gt To instantiate a variable inside a goal we may write the following definition let unify_goal x v Goals atomic fun gt Fd unify x v val unify_goal Facile Easy Fd t gt Facile Easy Fd elt gt Facile Goals t lt fun gt let v Fd interval 0 3 in if Goals solve unify_goal v 2 then Fd fprint stdout v 2 unit 3 4 User s Goals 35 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 gt print_int x val gprint_int int gt Facile Goals t lt fun gt 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 find
62. gument is raised Three levels of propagation are provided Basic is the quickest High performs the highest amount of propagation level default value is High The constraint posts the redundant constraint stating that the sum of the cardinals is equal to the number of variables This constraint is also known as the distribute constraint Not reifiable 4 9 Module Goals Building and Solving Goals This module provides functions and operators to build goals that will control the search i e mainly choose and instantiate variables 54 Modules 4 9 1 Access type t The type of goals val name t gt string name g returns the name of the goal g val fprint Pervasives out_channel gt t gt unit fprint chan g prints the name of goal g on channel chan 4 9 2 Creation val fail t val success t Failure resp success Neutral element for the disjunction resp conjunction over goals Could be implemented as create fun gt Stak fail fail resp create fun O gt O val atomic name string gt unit gt unit gt t atomic name atomic f returns a goal calling function f f must take as argument and return name default value is atomic val create name string gt a gt t gt a gt t create name create f a returns a goal calling f a f should return a goal success to stop name default value is create val create_rec name string gt t gt t gt t create
63. inality or membership The following example defines a fixed set super and its 2 partition as sets sub1 and sub2 It uses the union disjoint and cardinal constraints of module Conjunto fflet lub SetDomain elt_of_list 1 2 val lub Facile SetDomain elt lt abstr gt let super Var SetFd interval lub lub val super Facile Var SetFd t lt abstr gt let subl Var SetFd interval SetDomain S empty lub and sub2 Var SetFd interval SetDomain S empty lub val subi Facile Var SetFd t lt abstr gt val sub2 Facile Var SetFd t lt abstr gt let card Conjunto cardinal Conjunto union sub1 sub2 val card Facile Var Fd t lt abstr gt Cstr post Conjunto disjoint subl sub2 unit Cstr post fd2e card i2e SetDomain S cardinal lub unit 2 7 4 Labeling A specific goal is provided within module Goals Conjunto to non deterministically instantiate set variables The following example enumerates and prints the 2 partitions of set super 26 Building Blocks let print Printf printf subi a sub2 a n Var SetFd fprint subi Var SetFd fprint sub2 in let g Goals Conjunto indomain subi amp amp Goals Conjunto indomain sub2 88 Goals atomic print amp amp Goals fail in ignore Goals solve g sub1 sub2 1 2 subi 2 sub2 1 subi 1 sub2 2 subl 1 1 2 sub2 unit Chapter 3 Advanced Usage 3 1 Search Control 3 1
64. ing domain let glb SetDomain elt_of_list 1 2 val glb Facile SetDomain elt lt abstr gt fflet lub SetDomain elt_of_list 1 2 3 4 5 val lub Facile SetDomain elt lt abstr gt let sd SetDomain interval glb lub val sd Facile SetDomain t lt abstr gt SetDomain fprint stdout sd 12 12345 unit Note that the glb must be included in the lub and that holes cannot be represented at the domain level 2 7 2 Set Variables The module defining set variables SetFd shares its interface with module of integer variables Fd let sv Var SetFd interval name sv glb lub val sv Facile Var SetFd t lt abstr gt Var SetFd fprint stdout sv sv 12 112345 unit Var SetFd unify sv SetDomain S empty Exception Fcl_stak Fail Var XxxFd subst 2 7 Constraint Programs on Finite Sets 25 1 2 elb we 1 2 3 1 2 4 1 2 5 gt a A inclusion 12 34 1 2 3 5 1 2 4 5 bi TE ii y 1 2 3 4 5 lub Figure 2 1 Lattice of a set domain However specific convenient set operations and constraints are located in module Conjunto Conjunto inside 5 sv unit Var SetFd fprint stdout sv sv 125 112345 unit 2 7 3 Constraints Constraints on set variables can be found in module Conjunto see 4 3 Set operators like union intersection subset are provided as well as operators involving integer variables like card
65. int ct as parameters and returns unit However we recommend to name new constraints and precise their printing facilities which may obviously help debugging by specifying the following two optional arguments e name should be a relevant string describing the purpose of the constraint e fprint to print more accurate information on the constraint state variables domains maintained data structures values To define a reifiable constraint two additional optional arguments must also be specified e check should return true if the constraint is entailed false if its negation is entailed and raise the exception DontKnow otherwise check is called when the constraint is reified and should not therefore perform any domain modification e not should return the negation of the constraint which is a constraint itself It is called when the negation of a reified constraint is entailed and to access the waking conditions of the negation of a constraint when its reification is posted and the optional argument delay_on_negation of Reify boolean is set to true which is its default value Logical operators of module Reify also call the not function for the same purpose see 2 4 4 To be able to use waking identities their number must be specified e nb_wakings default value is 1 This optional argument is used in conjonction with waking identities specified in the delay argument If contiguous waking ids 0 to n 1 are used
66. ints on them 4 2 1 Basics type t Type of arithmetic expressions over variables of type Var Fd t and integers val i2e int gt t i2e n returns an expression which evaluates to n val fd2e Var Fd t gt t fd2e v returns an expression which evaluates to n if the variable v is instantiated to n val e2fd t gt Var Fd t e2fd e creates and returns a new variable v and posts the constraint fd2e v e 43 44 Modules 4 2 2 Construction of Arithmetic Expressions Only if compiled in bytecode using facile cma the arithmetic operators check whether any integer overflow i e the result of an arithmetic operation on integers is less than min_int or greater than max_int occurs during constraints internal computations and raise an assert failure Arithmetic operations are taken modulo 2 otherwise or 263 on 64 bit processors see the OCaml reference manual 8 thus incomplete failures may happen with native code compiled programs val val val val val val val val val val val val val 7 t o gt tot ttt 70D t gt to t Addition substraction multiplication on expressions 7 t gt int gt t Exponentiation of an expression to an integer value 7 t gt t gt t 47 t gt t gt t Division and modulo on expressions The exception Division_by_zero is raised whenever the second argument evaluates to 0 abs t gt t Absolute value on ex
67. ion 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 diff ml open Facile open Easy let cstr x y let name different in let fprint c Printf fprintf c 4s fa lt gt 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
68. ion see below Default value is 1 Beware that if nb wakings is greater than 1 and the optional init argument is not provided init default behaviour is to do nothing i e the update function will not be called e fprint should print the constraint on an output channel taken as its only argument Default value is to print the name string 48 Modules val post val one val zero priority is either immediate normal or later Time costly constraints should be waken after quick ones Default value is normal init is useful to perform initialization of auxiliary data structures needed and maintained by the update function init is called as soon as the constraint is posted Default value is to call update 0 if nb_wakings is equal to 1 to perform an initial propagation if nb_wakings is greater than 1 default value is fun gt O i e it does nothing Hence an init argument must be provided if this is not the desired behaviour check must be specified if the constraint is to be reifiable as well as the not function When the constraint is reified check is called to verify whether the constraint is satisfied or violated i e the constraint itself or its negation is entailed by the constraint store It should return true if the constraint is satisfied false if it is violated and raise DontKnow when it is not known check must not change the domains of the variables involved in the constraint Default Failure exc
69. ives the time and space complexity of the basic invariants Invariant Time Memory s ti O 1 od p hiz ti O 1 1 O 1 m mMinsep1m ti Ologn O n i argminjen mi Ollogn O n let a Array map Invariant create 1 2 3 41 val a int Facile Invariant setable_t array l lt abstr gt lt abstr gt lt abstr gt lt abstr gt let s Invariant sum a val s int Facile Invariant unsetable_t lt abstr gt 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 lt abstr gt let y Invariant unary name log log x val y float Facile Invariant unsetable_t lt abstr gt 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 sub
70. kings being the argument of Cstr create specifying the number of calls to delay with distinct waking_id arguments These integers are arguments to the update function of constraints and aim at discriminating waking events to fire the appropriate propagation rule waking_id default value is 0 This function has no effect on instantiated variables as no event could occur on a ground variable Common variables module signature module type FD sig include Var BASICFD val remove t gt elt gt unit remove v a removes a from the domain of v Leaves the domain unchanged if a does not belong to it val values t gt elt list val end values v returns the list of all integers in the domain of v If v is instantiated to n returns the singleton list containing n iter elt gt unit gt t gt unit iter f v iterates f on each integer in the domain of v Extended signature for finite domain variable with added functions irrelevant to set variables module Fd FD with type domain Domain t and type elt Domain elt and type attr Attr t and type event Attr event Concrete finite domain variable module module SetFd BASICFD with type domain SetDomain t and type elt SetDomain S t and type attr SetAttr t and type event SetAttr event Concrete integer set variable module 4 17 Module Easy 69 4 17 Module Easy Easy is a module that the user is strongly advised to open in o
71. labeling of submodule List embedded in module Goals see 4 9 The goal is thereafter solved by a call to solve which returns false if a failure occurred and true otherwise e 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 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 4 0 and S 40 zw 206 E a lt a M 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 6 Getting Started let s Fd interval 0 9 and e Fd interval O 9 and n and d Fd interval O 9 and m Fd interval
72. lobally consistent When a constraint is posted it is attached to the involved variables and activated propagation occurs as soon as the constraint is posted Consequently if an inconsistency is detected prior to the search i e before the call to Goals solve see 2 5 a Stak Fail exception is raised However inconsistencies generally occur during the search so that failures are caught by the goal solving mechanism of FaCiLe which will backtrack until the last choice point 16 Building Blocks Constraints basically perform domain reductions on their involved variables first when posted and then each time that a particular event occurs on their variables An event corresponds to a domain reduction on a variable the minimal or maximal value has changed the size of the domain has decreased or the variable has been bound All these kinds reduction cause different events to trigger the awakening of the appropriate constraints See 3 2 1 for a more precise description of this event driven mechanism Constraints can also be printed on an output channel with function Cstr fprint which usually yields useful information about the variables involved and or the name of the constraint 2 4 2 Arithmetic Constraints The simplest and standard constraints are relations on arithmetic expressions c f 2 3 e equality e strict and non strict inequality lt gt lt gt e disequality lt gt FaCiLe provides them as infi
73. ments of domains Type of domain reduction events 66 Modules 4 16 1 Creation val create name string gt domain gt t create name d returns a new variable with domain d If provided name will be used by the pretty printer val interval name string gt elt gt elt gt t interval name inf sup returns a new variable with domain inf sup If provided name will be used by the pretty printer val array name string gt int gt elt gt elt gt t array array n inf sup returns an array of n new variables with domain inf sup If provided name suffixed with the index of the element will be used by the pretty printer val elt elt gt t elt e returns a new variable instantiated to value e 4 16 2 Access val is_var t gt bool is_var v returns true if v is not instantiated and false otherwise val is_bound t gt bool is_bound v returns true if v is instantiated and false otherwise val value t gt attr elt Var concrete value v returns Val nif v is instantiated to n Unk a otherwise where a is the attribute of v Should always be used in a matching match value v with Val n gt Unk a gt val min t gt elt min v returns the lower bound of v val max t gt elt max v returns the upper bound of v val min_max t gt elt elt min_max v returns both the lower and upper bounds of v val elt_value t gt elt int_value v returns the valu
74. mize always fails 4 9 7 Search Strategy val lds step int gt t gt t lds step 1 g returns a goal which will iteratively search g with increasing limited discrepancy see 5 by increment step step default value is 1 4 9 8 Solving val solve control int gt unit gt t gt bool solve control fun _ gt g solves the goal g and returns a success true or a failure false The execution can be precisely controlled with the control argument whose single argument is the number of bactracks since the beginning of the search This function is called after every local failure e it can raise Stak Fail to force a failure of the search in the current branch i e backtrack e it can raise any other user exception to stop the search process e it must return unit to continue the search this is the default behavior 4 10 Module Interval Variable Membership to an Interval val is_member Var Fd t gt int gt int gt Var Fd t is_member v inf sup returns a boolean variable which will be instantiated to 1 if v is in inf sup and to 0 otherwise val cstr Var Fd t gt int gt int gt Var Fd t gt Cstr t cstr v inf sup b returns a constraint ensuring that the boolean variable b is instantiated to 1 if v is in inf sup and to 0 otherwise Not reifiable 58 Modules 4 11 Module Invariant Backtrackable Invariant Refer ences This module provides types and functions to create and handl
75. modules Invariant Fd and Invariant SetFd For example the heuristic criterion which selects the variable with the smallest domain is easily computed as follows 3 5 Backtrackable Invariant References BIRs 39 let best fun vars gt Invariant Array argmin Array map Invariant Fd size vars val best Facile Invariant Fd fd array gt int gt a gt int Facile Invariant unsetable_t lt fun gt 40 Advanced Usage Part II Reference Manual 41 Chapter 4 Modules The following sections are extracted from mli module interfaces of FaCiLe and sorted by alpha betic order A comprehensive index of these sections can be found at the end of this document 4 1 Module Alldiff The All Different Constraint type algo Lazy Bin_matching of Var Fd event val cstr algo algo gt Var Fd t array gt Cstr t alldiff algo Lazy vars States that the variables of vars are different from each other The optional argument algo specifies the level of propagation Lazy waits for instantiation and removes the corresponding value from other domains Bin_matching c waits for event c e g Var Fd on_refine and uses a bin matching algorithm to ensure the constraint is consistent algo default value is Lazy Not reifiable 4 2 Module Arith Arithmetic Expressions and Constraints Overview This module provides functions and operators to build arithmetic expressions and state in dis equation constra
76. ms 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 diffid ml 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 gt Fd remove y Fd elt_value x 1 gt Fd remove x Fd elt_value y _ gt failwith Diff_if cstr unexpected waking id end 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
77. n val create elt list gt t create 1 builds a new domain containing the values of 1 Removes duplicates and sorts values Returns empty if 1 is empty val unsafe_create elt list gt t unsafe_ create 1 builds a new domain containing the values of 1 1 must be sorted and must not contain duplicate values otherwise the behaviour is unspecified Returns empty if 1 is empty It is a more efficient variant of create val interval elt gt elt gt t interval inf sup returns the domain of all integers in the closed interval inf sup Raise Invalid_argument if inf gt sup val int t The largest representable domain Handy to create variables for which bounds cannot be previously known It is actually much smaller than interval min int max_int which really is the biggest one to try to prevent overflows while computing bounds of expressions involving such variables val boolean t The domain containing 0 and 1 4 6 2 Access val is_empty t gt bool is_empty d tests whether the domain d is empty or not val size t gt elt size d returns the number of integers in d val min t gt elt val max t gt elt min d resp max d returns the lower resp upper bound of d If d is empty the behaviour is unspecified incorrect return value or exception raised 4 6 Module Domain Domain Operations 51 val val val val val val val val val val val val val val
78. n fprint stdout Domain union discontinuous range 73 1 2 12 unit Domain fprint stdout Domain remove_up 3 discontinuous 1 2 3 unit Domain fprint stdout Domain remove_closed_inter 7 10 range 4 6 11 12 unit 2 2 Variables FaCiLe variables are attributed objects 7 which maintain their current domain and can be back tracked during the execution of search goals Creation FaCiLe finite domain constrained variables are build and handled by functions of module Var Fd described exhaustively in section 4 16 Variables are objects of type Fd t created by a call to one of the following functions of module Var Fd e create d takes a domain d as argument e interval inf sup yields a variable whose domain ranges the interval inf sup It is equivalent to create Domain interval inf sup e array n inf sup creates an array of n interval variables Equivalent to Array init n fun _ gt Fd interval inf sup e int n returns a variable already bound to n Note that the submodule Fd can be reached by opening module Easy in all the toplevel examples modules Facile and Easy are supposed open therefore a function of module Fd is called with Fd f instead of Facile Var Fd f The first three creation functions actually have an optional argument labelled name which allows to associate a string identifier to a variable The ubiquitous fprint function writes a variable on an output channel and
79. ng 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 e Modification of the domain on_refine e Substitution of the variable i e reduction of the domain to a singleton on_subst e Modification of the minimum value of the domain on_min e Modification of the maximum value of the domain on_max Note that these events are not independant and constitute a lattice which top is on_subst and bottom is on_refine e on_subst implies all other eventd e on_min and on_max imply on_refine Constraints are attached to the variables through these events thanks to the Var Fd delay 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 lIt means that e g the event on_min occurs even if a variable is instantiated to its minimum value 20r Var SetFd delay for set variables 30 Advanced Usage 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
80. ntiated 4 16 Module Var Constrained Attributed Finite Domain Variables 65 val val val val val val val val val end on_min event on_max event Event occuring when the lower resp upper bound of a variable decreases fprint Pervasives out_channel gt t gt unit fprint chan a prints attribute a on channel chan min t gt elt max t gt elt min a resp max a returns the lower resp upper bound of a member t gt elt gt bool member a n tests if n belongs to dom a id t gt int id a returns a unique integer identifying the attribute a constraints_number t gt int constraints_number a returns the number of different constraints attached to a size t gt int size a returns the number of integer values in the domain of a Signature of the Attribute of a Domain Variable A module endowed with this type is required to build finite domain variables Domain and SetDomain are suitable domain modules module Attr ATTR with type domain Domain t and type elt Domain elt module SetAttr ATTR with type domain SetDomain t and type elt SetDomain S t type a b concrete Unk of a Val of b Concrete type of the value of finite domain variables module type BASICFD sig type t type attr type domain type elt type event Type of finite domain variable Type of attributes Type of domains Type of ele
81. of elements of a module Array sig val get Ca b Invariant t array gt int c Invariant t gt a Invariant unsetable_t get a i returns the BIR element number i of array a val argmin Ca b Invariant t array gt a gt c gt int Invariant unsetable_t argmin a c returns the BIR index of the minimum BIR value of a for criterion c val min Ca b Invariant t array gt a gt c gt a Invariant unsetable_t min a c returns the minimum BIR value of a for criterion c end 4 11 3 From domain variables to BIRs module type FD sig type fd Type of a finite domain variable 60 Modules type elt Type of elements in the domain val min fd gt elt Invariant unsetable_t val max fd gt elt Invariant unsetable_t val size fd gt int Invariant unsetable_t val is_var fd gt bool Invariant unsetable_t BIR variants of Fd Var access functions val unary name string gt fd gt a gt fd gt a Invariant unsetable_t unary name Invariant XxxFd unary f v Wrapper of any access function over fd type end Generic signature module Fd FD with type fd Var Fd t and type elt Var Fd elt Module for accessing finite integer domain variables with BIRs module SetFd FD with type fd Var SetFd t and type elt Var SetFd elt Module for accessing set domain variables with BIRs 4 12 Module Reify Constraints Reification All the r
82. oughly arithmetic constraints are reifiable as well as the interval constraint of module Interval see 4 10 while others global ones are not Reified constraint are by default woken up with the events triggering its standard awakening i e as if it were directly posted and those of its negation This behaviour might possibly be too time costly for some specific problem and the call to Reify boolean with its optional argument delay_on_negation see 4 12 set to false disables it i e the events associated with the negation of the constraint are ignored Module Reify also provides standard logical most of them infix operators over constraints e 227 conjunction e 77 disjunction e gt implication e lt gt equivalence 20 Building Blocks xof exclusive or not negation These operators can be directly accessed through the opening of module Easy except Reify not for obvious reasons and Reify xor which are not infix Note that unlike Reify boolean these operators do not have a delay_on_negation optional argument so that the constraints they return will be woken by both the events of their arguments and those of the negations of their arguments These operators can be combined to yield complex logical operators For example the exclu sive or may be redefined in the following way let x Fd interval 3 5 and y Fd interval 5 7 val x Facile Var Fd t lt abstr gt val y Fa
83. p Goals atomic fun gt Cstr fprint stdout diseq amp amp Goals fail in while Goals solve goal do done 2 different 1 lt gt 2 2 different 1 lt gt 3 2 different 2 lt gt 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 lt abstr gt val y Facile Easy Fd t lt abstr gt let reified_diseq Reify boolean Diff cstr x y val reified_diseq Facile Var Fd t lt abstr gt Fd fprint stdout reified_diseg 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 func tion 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 argumend The 4 As correctly guessed by the reader these ids are used to access an internal array 34 Advanced Usage update function now makes use of this information argument id and perfor
84. pressions sum t array gt t sum_fd Var Fd t array gt t sum exps resp sum fd vars returns the sum of all the elements of an array of expressions resp variables Returns an expression that evaluates to 0 if the array is empty scalprod int array gt t array gt t scalprod_fd int array gt Var Fd t array gt t scalprod coeffs exps resp scalprod_fd coeffs vars returns the scalar product of an array of integers and an array of expressions resp variables Returns an expression that evaluates to 0 if both arrays are empty Raises Invalid_argument if the arrays don t have the same length prod t array gt t prod_fd Var Fd t array gt t prod exps resp prod_fd vars returns the product of all the elements of an array of expressions resp variables Returns an expression that evaluates to 1 if the array is empty 4 2 3 Access val val fprint Pervasives out_channel gt t gt unit fprint chan e prints expression e on channel chan eval t gt int eval e returns the integer numerical value of a fully instantiated expression e Raises Invalid_argument if e is not instantiated 4 2 Module Arith Arithmetic Expressions and Constraints 45 val min_of_expr t gt int val max_of_expr t gt int min_of_expr e resp max_of_expr e returns the minimal resp maximal possible value of expression e val min_max_of_expr t gt int int min_max_of_expr e is equivalent to
85. r 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 maxi mum 36 Advanced Usage let min_or_max v Goals create fun gt let min Fd min v and max Fd max v in Goals unify v min Goals unify v max e 08 val min_or_max Facile Easy Fd t gt Facile Goals t lt fun gt 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 create function gt Goals success x xs gt fgoal x iter_disj fgoal xs list val iter_disj a gt Facile Goals t gt
86. rder to facilitate access to FaCiLe unless names clash with other open modules It simply defines aliases to values and types of other modules e All the infix operators from Arith Goals and Reify e Frequently used mapping functions of Arith i2e and fd2e e Type of finite domain variables from Var concrete_fd Unk of Fd attr Val of Fd elt e Module Fd from Var Note that the user of FaCiLe can extend this mechanism with its own Easier module aliasing any value or type of the library 70 Modules gt BO MGI lt gt 20 lt 10 E lt PO CD 14 22 47 Ta 22 EA 22 1 14 22 e 14 22 co TD abs active_store add algo A algo type 17 all_disjoint 44 Alldiff MI argmin 38 Arith arithmetic expressions 6 access 13 creation operators 14 Array array 6 atomic ATTR Attr 63 attr 63 backtrackable invariant reference BASICFD 24 63 71 bb_mode bb_mode type 23 binary BIR boolean 48 Domain p Reify cardinal Conjunto SetDomain S choose choose_index compare 12 50 59 65 compare_elt 50 concrete 63 concrete_fd type L Conjunto 44 53 constant 37 56 constraints arithmetic overflow control creation events global post 5 priority reification store user s defined constraints_number 63 create 30 87 75
87. respectively amp amp and which can be directly accessed when module Easy is open to combine simple goals Hence such an enumeration goal would look like Goals indomain x amp amp Goals fail But the result of such a goal will be a failure and the state of the system variable x not instan tiated will not be restored A simple disjunction of this goal with the goal that always succeeds Goals success yields the desirable behaviour Goals indomain x amp amp Goals fail Goals success In order to display the execution of this goal a printing goal gprint_fd which prints a variable on the standard output but will not be detailed in this section see 3 4 1 can eventually be inserted conjunctively between indomain and fail let x Fd create Domain create 4 2 12 val x Facile Var Fd t lt abstr gt let goal Goals indomain x amp amp gprint_fd x amp amp Goals fail Goals success val goal Facile Goals t lt abstr gt Goals solve goal 4 2 12 bool true Note that unfortunately the logical operators do have the same priority Hence goals expressions must be carefully parenthesized to produce the expected result Module Goals also provides the function Goals instantiate that allows to specify the or dering strategy of the labeling Goals instantiate takes as first argument a function to which is given the current domain of the variable as single argument and should r
88. rgument if the two arrays have not the same length e Arith prod exps builds the product of all the elements of the array of expressions exps Their variable counterparts where the array of expressions is replaced by an array of variables are defined as well Arith sum_fd Arith scalprod_fd Arith prod_fd Note that Arith sum_fd a for example is simply defined as Arith sum Array map fd2e a let size 5 val size int 5 let coefs Array init size fun i gt it1 val coefs int array l1 2 3 4 51 let vars Fd array size 0 9 val vars Facile Var Fd t array l lt abstr gt lt abstr gt lt abstr gt lt abstr gt lt abstr gt let pscal_exp Arith scalprod_fd coefs vars val pscal_exp Facile Arith t lt abstr gt Arith fprint stdout pscal_exp 1 _8 0 9 2 _9 0 9 3 _10 0 9 4 _11 0 9 5 _12 0 9 unit 0 Arith min_of_expr pscal_exp int 0 Arith max_of_expr pscal_exp int 135 2 4 Constraints 2 4 1 Creation and Use A constraint in FaCiLe is a value of type Cstr t It can be created by a built in function arith metic global constraints or user defined see 3 3 A constraint must be posted with the function Cstr post to be taken into account i e added to the constraint store The state of the system can then be accessed by a call to the function Cstr active_store which returns the list of all constraints still unsolved i e not yet g
89. rix Goals Array forall labeling_array val labeling_matrix Facile Var Fd t array array gt Facile Goals t lt fun gt 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 lt n then match Fd value array i with Unk _ gt i Val _ gt loop i 1 else raise Not_found in loop 0 val first_unbound Facile Easy Fd t array gt int lt fun gt let forall_unbounds Goals Array forall select first_unbound val forall_unbounds Facile Easy Fd t gt Facile Goals t gt Facile Easy Fd t array gt Facile Goals t lt fun gt 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
90. sely an arithmetic expression can be transformed into a variable thanks to function Arith e2fd which creates a new variable constrained to be equal to its argument see 2 4 2 Operators Module Arith provides classic linear and non linear arithmetic operators to build complex expres sions Most frequently used ones can be directly accessed through the opening of module Easy which considerably ligthen the writing of equations especially for binary infix operators e 7 x addition substraction multiplication and division the exception Division_by_zero is raised whenever its second argument evaluates to 0 e e n raises e to the nth power where n is an integer e x y modulo The exception Division_by_zero is raised whenever y evaluates to 0 Arith abs absolute value let vx Fd interval name x 3 6 and vy Fd interval name y 4 12 let expl i2e 2 fd2e vx fd2e vy i2e 3 val exp1 Facile Arith t lt abstr gt Arith fprint stdout expl 3 y 4 12 2 x 3 6 unit 2 4 Constraints 15 Arith min_of_expr expl int 3 Arith max_of_expr expl int 11 Global arithmetic operators working on array of expressions are provided as well e Arith sum exps builds the sum of all the elements of the array of expressions exps e Arith scalprod ints exps builds the scalar products of an array of integers by an array of expressions Arith scalprod raises Invalid_a
91. sjunction 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 kk g 4 amp amp ue g 7 Of course iterators may be composed as is illustrated below where the cartesian product 1 3 x 4 5 is deterministically enumerated let enum_couples Goals forto 1 3 fun i gt Goals forto 4 5 fun j gt Goals atomic fun gt Printf printf Yd d n i j in Goals solve enum_couples 1 4 27 28 Advanced Usage 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 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 amp amp Goals Array forall g le1 e2 enl g ei amp amp g e2 amp amp ee 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 gt Facile Goals t lt fun gt 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_mat
92. straint ct which is taken as its unique argument i e the execution of its update function If update id should be called because it may propagates when one of the events contained in the events see list es occurred on variable v then Var delay es v waking_id id ct should be called within the body of the delay function Beware that all the waking_ids must be contiguous integers ranging from 0 to nb_wakings 1 otherwise the behaviour is unspecified delay is a mandatory argument t gt unit post c posts the constraint c to the constraint store t t The constraint which succeeds resp fails immediately 4 4 2 Access val id t gt int 4 5 Module Data Bactrackable Data Structures 49 val val val val val val id c returns a unique integer identifying the constraint c name t gt string name c returns the name of the constraint c priority t gt priority priority c returns the priority of the constraint c fprint Pervasives out_channel gt t gt unit fprint chan c prints the constraint c on channel chan Calls the fprint function passed to create is_solved t gt bool is_solved c returns true if c is satisfied and false otherwise active_store unit gt t list active_store returns the list of all active constraints i e whose update functions have returned false not t gt t not c returns the negation of c 4 5 Module Data Bactrackable Data Struct
93. t let mini FdArray min vars val mini Facile Var Fd t lt abstr gt Fd fprint stdout mini _33 2 5 unit FdArray get and FdArray min which produce a new variable and thus hide an underlying constraint also have their constraint counterpart FdArray get_cstr and FdArray min_cstr which take an extra variable as argument and return a constraint of type Cstr t that must be posted to be effective FdArray min_cstr vars mini is therefore equivalent to the constraint fd2e FdArray min vars fd2e mini and FdArray get_cstr vars index v to fd2e FdArray get vars index fd2e v More sophisticated global constraints are available as well as FaCiLe built in constraints e the global cardinality constraint 10 a k a distribute constraint Gcc cstr see 4 8 e the sorting constraint 4 Sorting cstr see 4 14 2 4 Constraints 19 2 4 4 Reification FaCiLe constraints can be reified thanks to the Reify module and its function Reify boolean see which takes an argument of type Cstr t and returns a new boolean variable This boolean variable is interpreted as the truth value of the relation expressed by the constraint and the following equivalences hold e the boolean variable is bound to 1 iff the constraint is satisfied and the constraint is there after posted e the boolean variable is bound to 0 iff the constraint is violated and the negation of the constraint is thereafter post
94. t 2 6 Optimization 23 Early Backtrack With FaCiLe as in Prolog systems any dynamic modification performed within goals may be undone backtracked to restore the state of the system However no choice point is associated to the root of the constraint program so that variables modifications oc curring before the call to Goals solve can never be undone As the standard way of adding constraints with FaCiLe is to post them prior to the solving i e statically outside goals the domain reductions initially made by these constraints are not backtrackable 2 6 Optimization Classic Branch amp Bound search is provided by the function minimize of module Goals It allows to solve a specified goal g while minimizing a cost defined by a finite domain variable c 1 Goal g is solved and the cost must then be bound to a value cc i e the current cost of the current solution 2 Backtracking is performed to restore the state of the system as before the execution of g and a new constraint stating c lt cc is added to the constraint store 3 The process loops until goal fails The third argument of Goals minimize is a function solution int gt unit called each time a solution is found The argument of solution is the current value of the cost cc which must be instantiated by g This function is handy to store the last solution and cost in references because Goals minimize always fails so that the decision and cost variables are r
95. ter or equal strictly greater and different 4 2 6 Boolean sums setting FaCiLe tries to automatically optimize the processing of boolean 0 1 variables sums whenever their sizes are large enough val get_boolsum_threshold unit gt int Returns the minimum size for boolean sums optimization Default 5 val set_boolsum_threshold int gt unit Set the minimum size for boolean sums optimization boolsum_threshold max_int disables it 46 Modules 4 3 Module Conjunto Constraints on Finite Sets val subset Var SetFd t gt Var SetFd t gt Cstr t subset vi v2 ensures that v1 is a subset of v2 Not reifiable val cardinal Var SetFd t gt Var Fd t cardinal v returns the cardinal an integer variable of the set v Not reifiable val smallest Var SetFd t gt Var Fd t smallest v returns the smallest element an integer variable of v val union Var SetFd t gt Var SetFd t gt Var SetFd t val inter Var SetFd t gt Var SetFd t gt Var SetFd t Operations on sets val all_disjoint Var SetFd t array gt Cstr t all disjoint vars ensures that all the set variables of array vars are pairwise disjoint Not reifiable val disjoint Var SetFd t gt Var SetFd t gt Cstr t disjoint vi v2 defined by all disjoint lv1 v21 Not reifiable val inside int gt Var SetFd t gt unit val outside int gt Var SetFd t gt unit Basic refinements for labeling val mem Var Fd t gt Var SetFd t
96. th very large domain that means with values close to max_int or min_int depending on the system and architecture Especially with exponentiation and multiplication an integer overflow may occur which will yield an error message Fatal error integer overflow on stderr and an exception Assert_failure if the program is compiled in byte code A spurious calculation probably leading to a failure during propagation will happen if it is compiled in native code An unexpected behaviour when performing such operations in native code should thus always be checked against the safer byte code version 2 4 3 Global Constraints Beside arithmetic constraints FaCiLe provides so called global constraints which express a re lation on a set of variables They are defined in separate modules in which a function and possibly several variants usually named cstr yields the constraint these functions takes an array of variables as their main argument The most famous one is probably the all different constraint which expresses that all the elements of an array of variables must take different values This constraint is invoked by the function Alldiff cstr algo vars where vars is an array of variables and algo an optional argument of type Alldiff algo that controls the efficiency of the constraint see 4 1 e Lazy waits for the instantiation of a variable and then removes the chosen value from the domains of the remaining variables e
97. tions 63 sortp a same as sort but returns a couple sorted perm where sorted is the array of sorted variables and perm is an array of variables constrained to be the permutation between a and sorted i e a i sorted perm i val cstr Var Fd t array gt p Var Fd t array option gt Var Fd t array gt Cstr t cstr a perm None sorted returns the constraint ensuring that sorted is the result of sorting array a according to the permutation perm perm default value is None meaning the argument is irrelevant Raises Invalid_argument if arrays have incompatible length Not reifiable 4 15 Module Stak Global Stack of Goals Backtrackable Operations This module provides functions to control the execution of the goal stack as well as backtrackable references i e mutable data structures restored on backtracking Nota the module name Stak lacks a c because of a possible clash with the OCaml standard library module Stack 4 15 1 Access type level Type of a level in the stack val older level gt level gt bool older 11 12 true if level 11 precedes 12 val size unit gt int Size of the stack i e number of trailings val depth unit gt int Depth of the stack i e number of active levels val level unit gt level Returns the current level val levels unit gt level list Returns the current active levels val nb_choice_points unit gt int Access to a global counter increm
98. 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 1 2 A Classic Example 5 e 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 4 6 like Domain create 1 which creates a domain containing all integers of list 1 e 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 4 2 e 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 e Here the search goal is a simple labeling of the list of all the problem variables 1 c r m obtained by a call to function
99. ts with basic examples to give a taste of FaCiLe then details the main concepts and eventually discusses more advanced subjects like the design of constraints and goals from scratch 2 The reference manual which describes module by module all the functionalities of FaCiLe This part of the documentation is automatically generated from the source code interface files mli which may be directly consulted Numerous examples are provided all along the user s manual and more complete ones are available within the standard distribution in the examples directory as well as a generic Makefile do build FaCiLe OCaml softwares iii Eventually we would like to thank our early known beta testers Mattias Waldau and Pal Kristian Engstad whose suggestions helped us to improve FaCiLe Good reading Foreword Portability FaCiLe requires only the OCaml system release 3 02 or greater and should work in any environ ment supporting this system It is developed in a Linux environment on PC architecture but does not use any specificities of Unix It should work on other operating systems i e MS Windows Mac OS provided that the installation process is customised to the environment FaCiLe Structure and Naming Conventions The library is split into numerous modules and submodules They are all included possibly with a limited user oriented interface into the main module Facile which should be opened by any other modules using FaCiLe
100. und dom val returns the largest hole interval in dom centred around val Returns val val if val belongs to dom and raises Not_found if val is outside dom bounds Equivalent to greatest_leq dom val smallest_geq dom val but faster choose elt gt elt gt bool gt t gt elt choose ord d returns the mininum value of d for order ord Raises Not_found if d is empty 4 6 3 Operations val val add elt gt t gt t add n d returns d U n remove elt gt t gt t remove n d returns d n Returns d if n is not in d 52 Modules val val val val val val val val val val val val val val val val remove_up elt gt t gt t remove_low elt gt t gt t remove_up n d resp remove_low n d returns d n 1 max_int resp d min_int n 1 i e removes values stricly greater resp less than n remove_low_up elt gt elt gt t gt t remove_low_up low up disa shortcut for remove_up up remove_low low d remove_closed_inter elt gt elt gt t gt t remove_closed inter inf sup d returns d inf supl i e removes values greater than or equal to inf and less or equal to sup in d Returns d if inf gt sup remove_min t gt t remove_max t gt t remove min d resp remove_max d returns d without its lower resp upper bound Raises Invalid argument if d is empty intersection t gt t gt t union t gt t
101. ures This module provides efficient backtrackable data structures i e with incremental setting and trailing module Array sig val set a array gt int gt a gt unit set t i x Bactrackable assignment of t i with x end Bactrackable arrays module Hashtbl sig type Ca b t val create int gt a b t val get a b t gt a b Hashtbl t val add a b t gt a gt b gt unit val find a b t gt a gt b val mem a b t gt a gt bool val remove a b t gt a gt unit val replace a b t gt a gt b gt unit val iter a gt b gt unit gt a b t gt unit val fold a gt b gt c gt c gt Ca b t gt c gt c end Bactrackable hashtables This module provides a subset of the hashtable interface of the OCaml standard library module Hashtbl see 8 50 Modules 4 6 Module Domain Domain Operations This module provides functions to create and handle domains which are useful to build variables and perform propagation i e domain filtering type elt int Type of element of domains for generic interface see 4 16 type t Type of finite domains of integers functional no in place modifications domains can be shared Standard equality and comparison can be used on domains 4 6 1 Building New Domains val empty t The empty domai
102. uses this string name if provided or an internal identifier if not let vd Fd create name vd discontinuous val vd Facile Var Fd t lt abstr gt Fd fprint stdout vd vd 1 2 4 7 unit 2 2 Variables 11 Attribute A FaCiLe variable can be regarded as either in one of the following two states e uninstantiated or unbound such that an attribute containing the current domain of size strictly greater than one is attached to the variable e instantiated or bound such that merely an integer is attached to the variable So an unbound variable is associated with an attribute of type Var Attr t holding its current domain its string name a unique integer identifier and various internal data irrelevant to the end user Functions to access attributes data are gathered in module Var Attr e dom returns the current domain of an attribute e the mapping of fprint min max size member of module Domain applied on the embedded domain of an attribute e g min a is equivalent to Domain min dom a e id to get the identifier of an attribute e constraints_number returns the number of active constraints still attached to a variable Although variables are of abstract type Fd t function Fd value v returns a concrete view of type Var concrete_fd Unk of Attr t Val of int Elof a variable v so that a control structure that depends on the instantiation of a variable will typically look like match Fd value
103. ver FaCiLe now offers Limited Discrepancy Search 5 as well see 4 9 7 and even ifa general mechanism to change the search strategy is not provided skilled users are encouraged to plunder and hack the source code of module Goals to devise new custom strategies themselves Floundering If the search goal does not instantiate all the variables involved in the posted constraints some of the constraints may still be unsolved when a solution is found so that this solution may be incorrect To be sure that all the constraints have been solved the user can use the function Cstr active_store and checks that the returned constraints list is empty This checking may be done after the completion of the search i e after Goals solve or better embedded within the search goal The latter allows to cleanly integrate this verification in optimization and findall goals A non floundering check goal could be implemented in the following way function Goals atomic used here to build a new atomic goal is explained in section 3 4 1 let check_floundering Goals atomic fun gt if Cstr active_store lt gt then failwith Some constraints are still unsolved val check_floundering Facile Goals t lt abstr gt A simple conjunction with check_floundering at the end of the labeling goal will do the job Information about the alive constraints may be extracted as well thanks to module Cstr access functions id name fprin
104. with duplicates e Domain interval is a shorthand when domains are continuous e Domain boolean is a shorthand for create 0 1 e Domain int is the largest well at least very large domain Domains can be conveniently printed on an output channel with Domain fprint and are dis played as lists of non overlapping intervals and single integers inf sup val2 inf3 sup3 in increasing order let discontinuous Domain create 4 7 2 4 1 3 val discontinuous Facile Domain t lt abstr gt Domain fprint stdout discontinuous 1 2 4 7 unit let range Domain interval 4 12 val range Facile Domain t lt abstr gt Domain fprint stdout range 4 12 unit Various functions allow access to properties of domains like among others see 4 6 Domain is_empty Domain min Domain max whose names are self explanatory 9 10 Building Blocks Domain is_empty range bool false Domain max range Facile Domain elt 12 Domain member 3 discontinuous bool true Domain values range Facile Domain elt list 4 5 6 7 8 9 10 11 12 Operators are provided as well to handle domains and easily perform set operations like Domain intersection Domain union Domain difference and domain reduction like Domain remove Domain remove_up Domain remove_low etc see 14 6 Domain fprint stdout Domain intersection discontinuous range 4 7 unit Domai
105. x operators suffixed with the character similarly to expression operators These operators are declared in the Easy module and don t need module prefix notation whenever Easy is opened The small example below uses the equality operator and points out the effect on the variables domains of posting the constraint equation O lt x lt 10 O lt y lt 10 0 lt z lt 10 let x Fd interval O 10 and y Fd interval O 10 and z Fd interval O 10 let equation x y 2 z gt 90 fd2e x fd2e y i2e 2 fd2e z gt i2e 90 val equation Facile Cstr t lt abstr gt before propagation has occurred Cstr fprint stdout equation 3 2 _15 0 10 1 _16 0 100 lt 90 unit Cstr post equation unit after propagation has occurred Cstr fprint stdout equation 3 2 _15 0 5 1 _16 90 100 lt 90 unit Notice that the output of the Cstr fprint function does not look exactly like the stated inequation but gives a hint about how the two operands of the main sum are internally reduced into new single variables constrained to be equal to the latters This mechanism is of course hidden to the user and is only unfolded when using the pretty printer FaCiLe compiles and simplifies normalizes arithmetic constraints as much as possible so that variables and integers may be scattered inside an expression with no loss of efficiency There fore the constraint ineql

Download Pdf Manuals

Related Search

Related Contents

Gaggia-Syncrony-cod 165892000 rev.01.PMD  Extron electronic Scan Rate Indicator SRI 200 User's Manual  User manual  Assessment Manager  Sima SFX-10 video mixer  Vol.11_no 3 – mai 2010  comment se personnalise la communication en ligne  InFocus 65V User's Manual  

Copyright © All rights reserved. Failed to retrieve file