G12: From Solver Independent Models to Efficient Solutions Peter J. Stuckey NICTA Victoria Laboratory University of Melbourne Outline G12 Project Overview Developing Constraint Solutions Solver Independent Modelling Zinc example and features Mapping models to algorithms Cadmium mapping tentative examples Efficient Solutions Mercury discussion Concluding Remarks May 4-5 2005

Copyright 2005 National ICT Australia Limited 2 Underpants Gnomes Business Plan Phase 1: Collect underpants Phase 2: ?????? Phase 3: Profit May 4-5 2005 Copyright 2005 National ICT Australia Limited 3 G12 Project Plan Phase 1: Solver Independent

Modelling Phase 2: ????? Phase 3: Efficient Solutions May 4-5 2005 Copyright 2005 National ICT Australia Limited 4 G12 Overview G12: a software platform for solving large scale industrial combinatorial optimisation problems. ZINC: A language to specify solver independent models CADMIUM: A mapping language from solver independent models to solvers A language for specifying search MERCURY: (For our purposes)

May 4-5 2005 A language to interface to external solvers A language to write solvers A language to combine solvers Providing debugging support Copyright 2005 National ICT Australia Limited 5 Group 12 of the Periodic Table May 4-5 2005 Copyright 2005 National ICT Australia Limited

6 G12 Participants Peter Stuckey, NICTA Victoria Maria Garcia de la Banda, Monash University Michael Maher, NICTA Kensington (NSW) Kim Marriott, Monash University John Slaney, NICTA Canberra Zoltan Somogyi, NICTA Victoria Mark Wallace, Monash University

Toby Walsh, NICTA Kensington (NSW) and others May 4-5 2005 Copyright 2005 National ICT Australia Limited 7 Outline G12 Project Overview Developing Constraint Solutions Solver Independent Modelling Zinc example and features Mapping models to algorithms Cadmium mapping tentative examples Efficient Solutions Mercury discussion

Concluding Remarks May 4-5 2005 Copyright 2005 National ICT Australia Limited 8 The Problem Solving Process Find four different integers between 1 and 5 which sum to 14 Conceptual Model User-oriented declarative problem statement S. S {1..5} |S| = 4 S|S| = 4 = 4 sum(S) = 14. Design Model Correct efficient algorithm [W,X,Y,Z] :: 1..5, alldifferent([W,X,Y,Z]), W + X + Y + Z #= 14, labeling([W,X,Y,Z]).

Solution W=2X=3Y=4Z=5 May 4-5 2005 Copyright 2005 National ICT Australia Limited S = {2,3,4,5} 9 From Conceptual Model to Design Model Conceptual Model: logical specification S {W,X,Y,Z} Logical Transformation Mapping the logical constraints to behaviour |S| = 4 {W,X,Y,Z}|S| = 4 = 4 alldifferent([W,X,Y,

Z]) Adding a specification of search labeling([W,X,Y,Z]) Design model: algorithmic specification May 4-5 2005 Copyright 2005 National ICT Australia Limited 11 Behaviour: Choosing a Solving Technology Mixed Integer Programming (MIP) strong optimization, lower bounding limited expressiveness for constraints (linear only) able to handle huge problems 1,000s of vars and constraints Finite Domain Propagation (FD) strong satisfaction, poor optimization highly expressive constraints

specialized algorithms for important sub-constraints DPLL Boolean Satisfaction (SAT) satisfaction principally, limited expressiveness (clauses or Boolean formulae) effective conflict learning, highly efficient propagation Local Search: SA, GSAT, DLM, Comet, genetic algorithms good optimization, poorer satisfaction (cant detect unsatisfiability) highly expressive constraints (arbitrary functions?) scale to large problems May 4-5 2005 Copyright 2005 National ICT Australia Limited 12 Behaviour: Hybrid Solving Approaches Design model using two or more solving approaches Only need partially model the problem in each part

pass constraints from one model to another values of variables W = 2 bounds of variables W 3 cuts 2X + 3Y + 4Z 15 pass upper or lower bounds from one technique to another Decompose the problem into two or more parts using different solving techniques Dantzig-Wolfe decomposition, Column generation, ... May 4-5 2005 Copyright 2005 National ICT Australia Limited 15 Search: Generic search strategy: limited discrepancy search, first fail, maximum regret symmetry breaking,

learn parameters Specific search strategy (programmed) Solving technology may restrict search Hybrid search: Support the search of one method with another Define heuristic function with one method support limited discrepancy search of other method Wide area local search, repair based methods May 4-5 2005 Copyright 2005 National ICT Australia Limited 16 Environment The worst answer to a constraint problem? No

An even worse answer to a constraint problem execution does not terminate in days! (Performance) Debugging the Design Model visualization of the active constraints visualization of the solver state (e.g. domains of variables) visualization of the search (preferably) mapped back to Conceptual Model Hybrid approaches complicate this! May 4-5 2005 Copyright 2005 National ICT Australia Limited 17 G12 Project Diagram May 4-5 2005

Copyright 2005 National ICT Australia Limited 19 G12 Goals Richer Modelling Separate conceptual modelling from design modelling using solver independent conceptual models mapping from conceptual to design models Richer Mapping extensible user defined mappings hybridization of solvers Richer Solving hybridization of search Richer Environment visualization of search and constraint solving May 4-5 2005

Copyright 2005 National ICT Australia Limited 21 Advantages of G12 model Checking the conceptual model trusted default mappings give basic design model test conceptual model on small examples this way Checking the design model check optimized mapping versus trusted default mapping Remembering good modelling approaches reuse of model independent mappings transformations/optimizations of design models Support for algorithmic debugging reverse mapping to visualize in terms of the conceptual

model May 4-5 2005 Copyright 2005 National ICT Australia Limited 22 Outline G12 Project Overview Developing Constraint Solutions Solver Independent Modelling Zinc example and features Mapping models to algorithms Cadmium mapping tentative examples Efficient Solutions Mercury discussion Concluding Remarks

May 4-5 2005 Copyright 2005 National ICT Australia Limited 23 What is Solver Independent Modelling A model independent of the solver to be used Examples .cnf format for SAT AMPL for linear and quadratic programming HAL program using solver classes (?) ECLiPSe program (for eplex, ic, fd,etc solvers) (?) OPL (although it essentially connects to one solver)

All the above fix the form of the constraints by the model All except .cnf fix the solving paradigm More independent ESRA [Uppsala] Essence and Conjure [York] model and transformation rules May 4-5 2005 Copyright 2005 National ICT Australia Limited 24 Zinc: a solver independent modelling language mathematical notation like syntax (coercion, overloading, iteration, sets, arrays) expressive constraints (FD, set, linear arithmetic, integer) different kinds of problems (satisfaction, explicit optimisation, preference (soft constraints)) separation of data from model high-level data structures and data encapsulation (lists,

sets, arrays, records, constrained types) extensibility (user defined functions, constraints) reliability (type checking, assertions) simple, declarative semantics Zinc extends OPL and moves closer to CLP language such as ECLiPSe May 4-5 2005 Copyright 2005 National ICT Australia Limited 25 Example Zinc model Social Golfers Given a set of players, a number of weeks and a size of playing groups. Devise a playing schedule so that each player plays each week no pairs play together twice

Many symmetries (ignore for now) May 4-5 2005 order of groups order of weeks order of players ... Copyright 2005 National ICT Australia Limited 26 Social Golfers in Zinc 0.1 Type Declarations (to be read from data file) enum Players = {...};

Parameter Declarations (first 2 from data file) int: Weeks; int: GroupSize; int: Groups = |Players| div GroupSize; Assertions on Parameters assert(Players must be divisible by GroupSize) Groups * GroupSize == |Players|; Variable Declarations array[1..Weeks,1..Groups] of var set of Player: group; May 4-5 2005 Copyright 2005 National ICT Australia Limited 27 Social Golfers in Zinc 0.1 Predicate (and Function) Declarations predicate maxOverlap(var set of $E: x,y, int: m) =

|x inter y| =< m; predicate partition(list of var set of $E:sets, set of $E: univ) = forall (i,j in 1..length(sets) where i < j) maxOverlap(sets[i],sets[j],0) /\ unionlist(sets) == univ; May 4-5 2005 Copyright 2005 National ICT Australia Limited 28 Social Golfers in Zinc 0.1 Constraints constraint forall (i in 1..Weeks)( partition([group[i,j] | j in 1..Groups], Players) /\ forall (j in 1.. Groups) ( |group[i,j]| == Groupsize /\ forall (k in i+1..Weeks; l in 1..Groups) maxOverlap(group[i,j],group[k,l],1)

)); class(redundant):: constraint forall (a,b in Players where a < b) sum (i in 1..Weeks; j in 1..Groups) holds({a,b} subset group[i,j]) =< 1; May 4-5 2005 Copyright 2005 National ICT Australia Limited 29 Zinc Features Types: float, int, bool, string,

tuples, records (with named fields), discriminated unions sets, lists, arrays (multidimensional = array of array of ...) var type arrays and lists of var types: array [1..12] of var int set var type of nonvar type: var set of bool coercion nonvar type to var type: float -> var float (x + 3.0) ground sets to lists: length({1,2,3,5,8}) lists to one-dimensional arrays: constrained types (assertions) record Task = (int: Duration, var int: Start, Finish) where Finish == Start + Duration; May 4-5 2005 Copyright 2005 National ICT Australia Limited 31

Zinc Features Comparisons ==, !=, >, <, >= , =< generated automatically for all types (lexicographic) Reification predicates are functions to var bool Boolean operations: /\ (and), \/ (or), ~ (not), xor, =>, <=, <=> ZeroOne = 0..1; function holds(var bool:b):var ZeroOne:h h is the integer coercion of the bool b Anything can be reified problem for solvers? May 4-5 2005 Copyright 2005 National ICT Australia Limited

32 Zinc Features List and Set comprehensions generators + tests must be independent of vars list of int: b = [2*i | i in 1..100 where ~(kind[i] in S)] shorthand sum (i in 1..Weeks; j in 1..Groups) holds(c) =< 1; sum([ holds(c) | i in 1..Weeks; j in 1..Groups ]) =< 1; Functions and predicates local variables (non-recursive) but foldl, foldr, zip function unionlist(list of var set of $E: sets): var set of $E = foldl(union,{},sets) starting point for mapping language Cadmium May 4-5 2005

Copyright 2005 National ICT Australia Limited 33 Zinc Features Annotations classification constraints: class(string) (possible multiple) classifications for constraints used for guiding rewriting, debugging class(linear) :: constraint x + 3*y + 4*z =< q; soft constraints: level(int) and strength(float) lower levels are preferential strength gives relative priority over levels int: strong = 1; level(strong) strength(2.0):: constraint x < 2 /\ y < 9; map to objective function if not supported by solver Objectives

minimize/maximize May 4-5 2005 Copyright 2005 National ICT Australia Limited 34 Zinc Status and Challenges Status Initial language design Type checker Compiler in progress Challenges Easy to use for mathematical programmers Error messages, syntax Symmetry specification Multi parameter objective and/or robustness objective specification

Recursion? Pattern matching May 4-5 2005 Copyright 2005 National ICT Australia Limited 35 Outline G12 Project Overview Developing Constraint Solutions Solver Independent Modelling Zinc example and features Mapping models to algorithms Cadmium mapping tentative examples Efficient Solutions Mercury discussion

Concluding Remarks May 4-5 2005 Copyright 2005 National ICT Australia Limited 37 Cadmium Maps solver independent models to solvers extension of Zinc term rewriting/constraint handling rules like features Model independent transformations! (as far as possible) Trying to extract some of the internal transformations performed by solvers, to make them visible reusable replaceable

Also adds search strategy to model not really discussed here May 4-5 2005 Copyright 2005 National ICT Australia Limited 38 Cadmium Examples (VAPOR) Simple Defaults map = bdd_sets.map; Overriding Defaults map = bdd_sets.map; predicate partition(list of var set of $E: sets, set of $E: univ) = bdd_partition(sets, univ, [prop = cardinality]); Using Classes class(redundant) :: c <=> delay(vars(c), c);

Merging Constraints map = bdd_sets.map; partition(sets, univ), sorted(sets) <=> list of var set of $E: sets, set of $E: univ | bdd_and_prop(bdd_partition(sets,univ),bdd_sorted(sets)); May 4-5 2005 Copyright 2005 National ICT Australia Limited 39 Cadmium Examples (VAPOR) Variable Conversion creates mapping sat from original variables to new variables var set of $E: s <=> array[$E] of var bool: sat(s); Mapping of Functions and Predicates function ||(array[$E] of var bool:s): var int = sum (e in $E) holds(s[e]); function inter(array[$E] of var bool:s,t):

array[$E] of var bool = [ s[e] /\ t[e] | e in $E ]; function {}: array[$E] of bool = [false | e in $E]; (?????) Refinement and Specialization of Constraints s subset t <=> set forall (e in maxOverlap(s,t,c1) int: c1, int May 4-5 2005 of $E:s, var set of $E:t | s) e in t; \ maxOverlap(s,t,c2) <=> :c2, c1 =< c2 | true. Copyright 2005 National ICT Australia Limited 40

Cadmium Examples (VAPOR) Multiple Solvers m1 = bdd_sets.map; m2 = sat_sets.map; m2::|_| = _ <=> true; channeling { forall (var set of $E:s; $E:e) m1::e in bdds(s) ==> m2::sat(s)[e] == true /\ m1::e notin bdds(s) ==> m2::sat(s)[e] == false /\ m2::sat(s)[e] == true ==> m1::e in bdd(s) /\ m2::sat(s)[e] == false ==> m1::e notin bdd(s) /\ } May 4-5 2005 Copyright 2005 National ICT Australia Limited 42 Mapping to Local Search (VAPOR)

Variable and Parameter mapping var set of $E:s, |s| == c <=> int:c | array [1..c] of var $E:lcl(s); set of $E: s <=> int:c= |s| | array [1..c] of $E: lcl(s); Predicate mapping predicate subset(array[$R1] of var $E: s, t) = forall (i in $R1) exists (j in $R2) s[i] == t[j]; predicate partition(list of var array[$R] of $E: sets, set of $E: univ) = forall (e in univ) sum (i in 1..length(sets); j in $R) holds(sets[i][j]==e) == 1; maxOverlap(_,_,1) <=> true May 4-5 2005 Copyright 2005 National ICT Australia Limited 44 Mapping to Local Search (VAPOR) Defining Penalty Functions

violation(a =< b) <=> var int: a,b | max(0,a - b); var int:f = sum [violation(c) | class(redundant) :: c ]; var int:p = sum [holds(c) | c = partition(_,_) ]; Defining the algorithm .. .. .. .. move definition .. tabu list definition .. search (using f) .. debugging check (using p) .. May 4-5 2005 Copyright 2005 National ICT Australia Limited 45

Cadmium Status and Challenges Status many discussions Challenges Specification: model independent mappings (polymorphism) solver communication full hybridization Rewriting: control, confluence?, interaction with subtypes Search: Salsa, Comet, CLP

Error messages: unmapped constraints, etc Reverse mappings? The last step outputing the format required by an external solver May 4-5 2005 Copyright 2005 National ICT Australia Limited 47 Outline G12 Project Overview Developing Constraint Solutions Solver Independent Modelling Zinc example and features Mapping models to algorithms Cadmium mapping tentative examples Efficient Solutions

Mercury discussion and hybrid example Concluding Remarks May 4-5 2005 Copyright 2005 National ICT Australia Limited 48 Mercury Purely declarative functional/logic programming language developed since October 1993 at University of Melbourne designed for programming in the large strong static typing: Hindley/Milner + type classes with functional dependencies + existential types strong static moding (tracking instantiation of arguments) strong static determinism (number of answers for predicates/functions) strong module system

highly efficient, sophisticated compile-time optimizations May 4-5 2005 Copyright 2005 National ICT Australia Limited 49 Extending Mercury No constraint solving (not even Herbrand) added solver types to Mercury Dual view of a type External view: pure declarative solver variable Internal view: data structure representing solver information adding solvers to Mercury herbrand, bdd_sets, sat (MiniSat), lp (cplex, clpr), fd Hybridization facilities (currently complete methods only) essentially attach arbitrary code to solver events

variable is fixed bounds changes new cut/nogood generated May 4-5 2005 Copyright 2005 National ICT Australia Limited 50 Mercury hybridization experiment bdd FD solver (JAIR 24) DPLL based SAT solver (MiniSAT) May 4-5 2005 Copyright 2005 National ICT Australia Limited 51 Hybridizing BDD and MiniSAT

Variable to variable propagation fixed variables in BDD <-> fixed variables in MiniSAT Scheduling Unit propagation in MiniSAT is one propagator higher priority than any BDD propagators Modelling all constraints represented in BDD solver NO constraints represented in MiniSAT! May 4-5 2005 Copyright 2005 National ICT Australia Limited 54 Dynamic clause generation Propagation in the BDD solver represents inferences Initially D(S) = {{} .. {1,2,3,4}}, D(x) = {0,1,2,3}

D(S) = {{1,2} .. {1,2,4}}, D(x) = {0,1,2}, |S| = 4 S|S| = 4 = x gives D(S) = {{1,2}}, D(x) = {2} Simple inference 1 S 2 S (3 S) (x = 3) (x = 0) Minimal inference 1 S (x = 0) Pass the inferences made to the SAT solver (1 S) (x = 0) May 4-5 2005 Copyright 2005 National ICT Australia Limited 57 Experiments Social Golfers Problems Versus bounds propagation bdd set solver using a

sequential smallest element is set search strategy (18/20) simple inferences (18/20): fails 1/2 - 1 (0.70), time 4/5 2 (1.22) minimal inferences: just inferring (18/20): time 1 - 3 (1.76) (surprisingly low !) using inferences in implication graph only (19/20): fails 1/35 - 1 (0.29), time 1/10 - 2 (0.78) adding clauses (20/20): fails 1/157 - 1 (0.10), time 1/62 - 2 (0.30) May 4-5 2005 Copyright 2005 National ICT Australia Limited 59 What does it mean? Conflict directed backjumping in another guise? Related work PalM, E-constraints: uses decision cuts not 1-UIP Katsirelos and Bacchus CP2003: only forward checking,

(appear to) only use FC inferences in implication graph finite domain propagation = clausal cut generation? May 4-5 2005 Copyright 2005 National ICT Australia Limited 61 Outline G12 Project Overview Developing Constraint Solutions Solver Independent Modelling Zinc example and features Mapping models to algorithms Cadmium mapping tentative examples Efficient Solutions

Mercury discussion Concluding Remarks May 4-5 2005 Copyright 2005 National ICT Australia Limited 62 G12 Progress Zinc Language design Type checker Starting compiler Cadmium Mercury building new solvers: fd, generic propagation structures, value propagation integrate solvers: bdd_sets, minisat, CPLEX

solver types May 4-5 2005 Copyright 2005 National ICT Australia Limited 63 Other Aspects of the G12 Project Logical Transformations (Zinc2Zinc): dualization, etc Robust solutions: insensitive to change in parameters

Search Master-subproblem decompositions: Benders, Lagrangian relaxation, column generation Population search: evolutionary algorithms Solver visualization Default mappings Online optimization Scripting May 4-5 2005 Copyright 2005 National ICT Australia Limited 64 Conclusion G12 is an ambitious project aiming to provide Solver independent modelling Model independent mappings from conceptual to design models Easy experimentation of hybrid approaches

A good environment for exploring design models We have only just begun! The holy grail Default mappings are good enough: only conceptual model May 4-5 2005 Copyright 2005 National ICT Australia Limited 65 Advertisement Constraint Programming positions available see http://nicta.com.au/jobs.html positions in Melbourne (Network Information Processing) and Sydney (Knowledge Representation and Reasoning) G12 postgraduates needed apply to University of Melbourne or University of New

South Wales G12 visitors welcome are you interested in some of the things discussed here? May 4-5 2005 Copyright 2005 National ICT Australia Limited 66 End END May 4-5 2005 Copyright 2005 National ICT Australia Limited 68