Home
choco3 user manual - School of Computing Science
Contents
1. The solutions of the problem are L R 1 T 0 e L 1 R 0 T 1 L 0 R 1 T 1 e L 0 R 0 T 0 22 11 addBoolLe Add a clause to the SAT constraint which states that the boolean variable LEFT is less or equal than the boolean variable RIGHT API boolean addBoolLe BoolVar LEFT BoolVar RIGHT Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver SatFactory addBoolLe L R solver findAllSolutions The solutions of the problem are e L 1 R 1 e L 0 R 1 e L 0 R 0 22 12 addBoolLt Add a clause to the SAT constraint which states that the boolean variable LEFT is less than the boolean variable RIGHT API 132 Chapter 22 Sat solver N N Choco3 Documentation Release 3 3 1 boolean addBoolLt BoolVar LEFT BoolVar RIGHT Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver solver findAllSolutions The solutions of the problem are L 0R 1 22 13 addBoolNot Add a clause to the SAT constraint which states that the two boolean variables LEFT and RIGHT are not equal API boolean addBoolNot BoolVar LEFT BoolVar RIGHT Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver solver findAllSolutions The solutions of the pro
2. Some solutions of the problem are e N 2 XS 0 0 XS 1 0 XS 2 1 XS 3 1 e N 2 XS 0 0 XS 1 1 XS 2 3 XS 3 6 e N 3 XS 0 1 XS 1 1 XS 2 2 XS 3 4 e N 3 XS 0 3 XS 1 2 XS 2 1 XS 3 0 18 6 arithm The constraint arithm involves either e a integer variable VAR an operator OP and a constant CST It holds VAR OP CSTE where CSTE must be chosen in mp US MEM MS Mo e or two variables VAR and VAR2 and an operator OP It ensures that VARI OP VAR2 where OP must be chosen in Mele WSU Wow Woe Neat R e or two variables VAR and VAR2 two operators OP1 and OP2 and an constant CSTE The operators must be different taken from gt lt gt lt or 4 the constarint ensures that VARI OPI VAR2 OP2 CSTE API Constraint arithm IntVar VAR String OP int CSTE Constraint arithm IntVar VAR1 String OP IntVar VAR2 Constraint arithm IntVar VAR1 String OP1 IntVar VAR2 String OP2 int CSTE Example 1 Solver solver new Solver IntVar X VF enumerated X 1 4 solver solver post ICF arithm X gt 2 solver findAllSolutions The solutions of the problem are e X 3 e X 4 Example 2 Solver solver new Solver IntVar X VF enumerated X 0 2 solver IntVar Y VF enumerated X 6 1 solver Ww n we 82 Chapter 18 Constraints over i
3. Return the internal environment of the solver essential to manage backtracking ObjectiveManager getObjectiveManager Return the objective manager of the solver needed when an objective has to be optimized ExplanationEngine getExplainer Return the explanation engine declared default is NONE IPropagationEngine getEngine Return the propagation engine of the solver which orchestrate the propagation of constraints ISearchLoop getSearchLoop Return the search loop of the solver which guide the search process 3 1 Getters 21 Choco3 Documentation Release 3 3 1 3 2 Setters Method Definition set Settings settings Set the settings to use while modelling and solving strategies set AbstractStrategy Set a strategy to explore the search space In case many strategies are given they will be called in sequence set ISolutionRecorder sr Set a solution recorder and erase the previous declared one by default LastSolutionRecorder is declared it only stores the last solution found set ISearchLoop searchLoop Set the search loop to use during resolution The default one is a binary search loop set IPropagationEngine propagationEngine Set the propagation engine to use during resolution The default one is SevenQueuesPropagatorEngine set ExplanationEngi
4. Available search monitors Search Monitors 66 Chapter 14 Search monitor CHAPTER 15 Defining its own search strategy One key component of the resolution is the exploration of the search space induced by the domains and constraints It happens that built in search strategies are not enough to tackle the problem Or one may want to define its own strategy This can be done in three steps selecting the variable selecting the value then making a decision The following instructions are based on IntVar but can be easily adapted to other types of variables 15 1 Selecting the variable An implementation of the VariableSelector lt V extends Variable gt interface is needed A variable se lector specifies which variable should be selected at a fix point It is based specifications ex smallest domain most constrained etc Although it is not required the selected variable should not be already instantiated to a singleton This interface forces to define only one method V getVariable V variables One variable has to be selected from variables to create a decision on If no valid variable exists the method is expected to return nul 1 An implementation of the VariableEvaluator lt V extends Variable gt is strongly recommended It en ables breaking ties It forces to define only one method double evaluate V variable An evaluation of the given variable is done wrt the evaluator The variable with the smalles
5. solver findAllSolutions The solutions of the problem are e CS 0 1 CS 1 3 CS 2 3 CS 3 4 18 38 regular 105 o u e uv N Choco3 Documentation Release 3 3 1 e CS 0 1 CS 1 3 CS 2 3 CS 3 5 e CS 0 2 CS 1 3 CS 2 3 CS 3 4 e CS 0 2 CS 1 3 CS 2 3 CS 3 5 18 39 scalar The scalar constraint involves e an array of integer variables VARS e an array of integer COEFFS e an optional operator OPERATOR and e an integer variable SCALAR It ensures that sum VARS i COEFFS i OPERATOR SCALAR where OPERATOR must be chosen from I gt lt gt lt The scalar constraint filters on bounds only The constraint suppress variables with coefficients set to 0 recognizes sum when all coefficients are equal to or all equal to and enables under certain conditions to reformulate the constraint with a table constraint providint AC filtering algorithm See also scalar_product in the Global Constraint Catalog Implementation based on HS02 API Constraint scalar IntVar VARS int COEFFS IntVar SCALAR Constraint scalar IntVar VARS int COEFFS String OPERATOR IntVar SCALAR Example Solver solver new Solver IntVar CS VF enumeratedArray CS 4 1 4 solver int coeffs new int 1 2 3 4 IntVar R VF bounded R 0 20 solver solver post ICF scalar CS co
6. A complete list is available in the documentation of IBEX rvars is the list of involved real variables option is enable to state the propagation option default is Ibex COMPO Example Solver solver new Solver double PREC 0 01d precision RealVar x VariableFactory real x 1 0d 1 0d PREC solver RealVar y VariableFactory real y 1 0d 1 0d PREC solver RealConstraint rc new RealConstraint my Pew WCCO EEL ein 10 1 08 Tn 10 10 1 0 1 2 2 6 Tbex HC4 x Y solver post rc solver findSolution 123 Choco3 Documentation Release 3 3 1 124 Chapter 20 Constraints over real variables CHAPTER 21 Logical constraints The LogicalConstraintFactory or LCF provides various interesting constraints to manipulate other con straints These constraints are based on the concept of reification We say a constraint C is reified with a boolean variable b when we maintain the equivalence betwen b being equal to true and C being satisfied This means the C constraint may be not satisfied hence it should not be posted to the solver 21 1 not Creates the opposite constraint of the input constraint While this works for any kind of constraint including globals it might be a bit naive and slow 21 2 ifThen Creates and automatically post a constraint ensuring that if the IF statement is true then the THEN statement must be true as well A s
7. 23 4 maxDomainSize var selector A built in variable selector which chooses the non instantiated integer variable with the largest domain to branch on Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API VariableSelector lt IntVar gt maxDomainSize_var_selector 23 5 maxRegret_var_selector A built in variable selector which chooses the non instantiated integer variable with the largest difference between the two smallest values in its domain to branch on Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API VariableSelector lt IntVar gt maxRegret_var_selector 142 Chapter 23 Variable selectors CHAPTER 24 Value selectors 24 1 min_value_ selector A built in value selector which selects the variable lower bound Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntValueSelector min _ value selector 24 2 mid_value_ selector A built in value selector which selects the value in the variable domain closest to the mean of its current bounds It computes the middle value of the domain Then checks if the mean is contained in the domain If not the clos est value to the middle is chosen Rounding policy is floor It could be override by creating a new instance of IntDomainMiddle with false as parameter Important mid_value_selector should not be used with a
8. Constraint maximum IntVar MAX IntVar VAR1 IntVar VAR2 Constraint maximum IntVar MAX IntVar VARS Constraint maximum BoolVar MAX BoolVar VARS Example Solver solver new Solver IntVar MAX VF enumerated MAX IntVar Y VF enumerated Y 1 IntVar Z VF enumerated Z 2 3 solver post ICF maximum MAX Y Z solver findAllSolutions 3 solver solver solver The solutions of the problem are e MAX 2 Y 1 Z 2 e MAX 2 Y 0 Z 2 e MAX 2 Y 1 Z 2 e MAX 3 Y 1 Z 3 e MAX 3 Y 0 Z 3 e MAX 3 Y 1 Z 3 18 30 mddc A constraint which restricts the values a variable can be assigned to the solutions encoded with a multi valued decision diagram Implementation based on CY08 API Constraint mddc IntVar VARS MultivaluedDecisionDiagram MDD Example 18 29 maximum 99 Choco3 Documentation Release 3 3 1 Solver solver new Solver IntVar vars VF enumeratedArray X 2 2 2 solver Tuples tuples new Tuples tuples add 0 1 tuples add 1 1 tuples add 0 1 solver post ICF mddc vars new MultivaluedDecisionDiagram vars tuples solver findAllSolutions The solutions of the problem are e X 0 0 X 1 1 e X 0 0 X 1 1 e X 0 1 X 1 1 18 31 member A constraint which restricts the values a variable can be assigned to with respect to either e a given list of value
9. See solver search strategy selectors values SetDomainMin For real variables See solver search strategy selectors values RealDomainMiddle solver search strategy selectors values RealDomainMin solver search strategy selectors values RealDomainMax 8 2 3 Available decision operators assign remove split reverse_split 8 2 4 Available strategies For integer variables custom sequencer lexico_LB lexico_Neq_LB lexico_Split lexico_UB minDom_LB minDom_MidValue maxDom_Split minDom_UB maxReg_LB random_bound random_value domOverWDeg activity impact lastConflict generateAndTest For set variables custom sequencer force_first force_maxDelta_first force_minDelta_first remove_first lastConflict Important Black box search strategies There are many ways of choosing a variable and computing a decision on it Designing specific search strategies can be a very tough task to do The concept of Black box search heuristic or adaptive search strategy has naturally emerged from this statement Most common black box search strategies observe aspects of the CSP resolution in order to drive the variable selection and eventually the decision computation presumably a value assignment Three main families of heuristic stemming from the concepts of variable impact conflict and variable activity can be found in Chocolreleasel Black box strategies can be augmented with restarts 8 3 Default search stra
10. 2 IntVar X VF enumerated X 0 5 solver 3 IntVar Y VF enumerated Y 1 3 solver 4 Tuples tuples new Tuples true 5 tuples add 1 2 6 tuples add 1 1 7 tuples add 4 2 8 tuples add 1 4 9 solver post ICF table X Y tuples AC2001 10 solver findAllSolutions The solutions of the problem are e X 1 Y 1 e X 4 Y 2 18 46 times The times constraints involves either e three variables X Y and Z It ensures that X x Y Z e or two variables X and Z and a constant y It ensures that X x y Z The propagator of the times constraint filters on bounds only If the option is enabled and under certain condition the times constraint may be redefined with a table constraint providing a better filtering algorithm The API are Constraint times IntVar X IntVar Y IntVar Z Constraint times IntVar X int Y IntVar Z Example 1 Solver solver new Solver 2 IntVar X VF enumerated X 1 2 solver 3 IntVar Y VF enumerated Y 2 4 solver 4 IntVar Z VF enumerated Z 5 7 solver 5 solver post ICF times X Y Z 6 solver findAllSolutions The solution of the problem is e X 2Y 3Z 6 18 47 tree The tree constraint involves e an array of integer variables SUCCS e an integer variable NBTREES and 18 46 times Choco3 Documentation Release 3 3 1 e an integer OFFSET It partitions the SUCCS variables int
11. 6 solver findAllSolutions The solutions of the problem are e VAR 1 EVARS O 1 EVARS 1 0 EVARS 2 0 LVARS O 1 LVARS 1 1 LVARS 2 1 e VAR 2 EVARS O 0 EVARS 1 1 EVARS 2 0 LVARS O 0 LVARS 1 1 LVARS 2 1 e VAR 3 EVARS O 0 EVARS 1 0 EVARS 2 1 LVARS O 0 LVARS 1 0 LVARS 2 1 18 13 circuit The circuit constraint involves e an array of integer variables VARS e an integer OFFSET and e a configuration CONF It ensures that the elements of VARS define a covering circuit where VARS i OFFSET j means that j is the successor of i The filtering algorithms are the subtour elimination of CL97 constant time per propagation and the alldifferent GAC filtering of Regin94 In addition depending on CONF the dominator filtering of the tree GAC constraint FL11 and the strongly connected components filtering of the path constraint CB04 FL12 may be added through a dynamical circuit path transformation The CONF is a defined by an enum e CircuitConf LIGHT no circuit path transformation e CircuitConf FIRST circuit path transformation by duplicating the first node e CircuitConf RbD circuit path transformation by duplicating a random node e CircuitConf ALL circuit path transformation by duplicating every node 18 12 clause_channeling 87 Choco3 Documentation Release 3 3 1 This implementation is detailed in Fag14 See also circuit
12. A built in strategy which chooses the first non instantiated variable with the largest difference between the two smallest values of its domain and assigns it to its lower bound Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy maxReg_LB IntVar VARS 26 14 random_bound A built in strategy which randomly chooses a non instantiated variable and assigns it to one of its bounds randomly selected Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy random_bound IntVar VARS IntStrategy random_bound IntVar VARS long SEED 150 Chapier 26 Built in strategies Choco3 Documentation Release 3 3 1 26 15 random_value A built in strategy which randomly chooses a non instantiated variable and assigns it to a randomly selected value from its domain Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy random_value IntVar VARS IntStrategy random_value IntVar VARS long SEED 26 16 remove first A built in strategy which chooses the first unfixed variable and removes its smallest unfixed value from the envelope Scope SetVar Factory org chocosolver solver search strategy SetStrategyFactory API SetStrategy remove_first SetVar sets 26 17 sequencer A meta strategy which applies seq
13. API Constraint square IntVar VAR1 IntVar VAR2 Example 1 Solver solver new Solver 2 IntVar X VF enumerated X 0 5 solver 3 IntVar Y VF enumerated Y 1 3 solver 4 solver post ICF square X Y 5 solver findAllSolutions The solutions of the problem are X 1 Y 1 X 0 Y 0 X 1 Y 1 X 4Y 2 18 41 square 107 Choco3 Documentation Release 3 3 1 18 42 subcircuit The subcircuit constraint involves e an array of integer variables VARS e an integer OFFSET and e an integer variable SUBCIRCUIT_SIZE It ensures that the elements of VARS define a single circuit of SUBCIRCUIT_SIZE nodes where e VARS i OF FSET j means that j is the successor of i e VARS i OFFSET i means that i is not part of the circuit It also ensures that VARS i 4 OF FSET i SUBCIRCUIT_SIZE Implementation based on circuit API Constraint subcircuit IntVar VARS int OFFSET IntVar SUBCIRCUIT_SIZE Example 1 Solver solver new Solver 2 IntVar NODES VF enumeratedArray NS 5 0 4 solver 3 IntVar SI VF enumerated SI 2 3 solver 4 solver post ICF subcircuit NODES 0 SI 5 solver findAllSolutions Some solutions of the problem are e NS O 0 NS 1 1 NS 2 2 NS 3 4 NS 4 3 SI 2 e NS O 4 NS 1 1 NS 2 2 NS 3 3 NS 4 0 SI 2 e NS O 1 NS 1 2 NS 2 0 NS 3 3
14. Choco3 Documentation Release 3 3 1 Charles Prud homme Jean Guillaume Fages Xavier Lorca May 11 2015 Contents I 1 Il Preliminaries Main concepts 1 1 What is Constraint Programming 1 2 Whatis Choco so s carem 42 22584 eo Ae BaD 1 3 Technical Overview o eo rta ala Ek SR ew BR L4 Pastoty oe ak ea be ea ee be ee be bee 1 5 How to getsupport se ee ee eS Be eee 16 How to cite Choco sesde O44 28 24 a ate eee Y 1 7 Who contributes to Choco 2 0200000 2 1 Installing Choca ses garara Fw a RISD SR E EN Bee 22 MOVERVIEW of CAICOS aaa A BS 2 3 Choco 3 quick documentation 24 Choco 3 E changes ss oc oscedo deede be eae ea Soll o ciate ea bee BS Be we Aw ee ee wy Od Se BAe a Bea OIL sa oa doc a e a Eee ee Re B A Ya at ok Ae 3 3 SOME 2ie458 pee eben bh eee Sei baw Getting started Modelling problems The solver Declaring variables Aa Bemciple te a Dl Be Bog Ae yee Hs ote de Aes 4 2 Integer Variable ooo mess eo bP eRe RE 43 Constant S s so 6 6254 54 4 be eee eG he Pewee 44 Variable ViWS 2 044 4 Ae Se ee EY Re Re ee Re 45 Setvafiable 34 cetro 4 oY EGS ESE EH SG 4 6 Realvanable haras argh a eB we BR ce Bl wh Bes Constraints and propagators Dil Principle se eae eww eee eet bee ee kad eae ee 3 2 Postings comstraimts ss Ap eet py Bee ele ed Hae ais 33 Rerfymg constraints sgae em pe oe Hoe aoe oA SAT CONStHaIN
15. For Int Var represents an upper bound modification X lt 3 The refutation of the decision will be a lower bound modification int_reverse_split For Int Var represents a lower bound modification X gt 3 The refutation of the decision will be an upper bound modification set_force For SetVar represents a kernel addition 3 S The refutation of the decision will be an envelop removal set_remove For Set Var represents an envelop removal 3 S The refutation of the decision will be a kernel addition Attention A particular attention should be made while using Int Var s and their type of domain Indeed bounded variables does not support making holes in their domain Thus removing a value which is not a current bound will be missed and can lead to an infinite loop One can define its own operator by extending DecisionOperator void apply V var int value ICause cause Operations to execute when the decision is applied left branch It can throw an ContradictionException if the application is not possible void unapply V var int value ICause cause Operations to execute when the decision is refuted right branch It can throw an ContradictionException if the application is not possible DecisionOperator opposite Opposite of the decision operator Currently useless String toString A pretty print of the decision for logging Most of the time extending Abst ractStrategy is not nece
16. 0 T 0 22 16 addBoolOrEqVar Add a clause to the SAT constraint which states that LEFT V RIGTH lt gt TARGET API boolean addBoolOrEqVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver BoolVar T VF bool T solver 134 Chapter 22 Sat solver N o u a v Choco3 Documentation Release 3 3 1 SatFactory addBoolOrEqVar L R T solver findAllSolutions The solutions of the problem are L R 1 T 1 e L 1 R 0 T 1 e L 0 R 1 T 1 e L 0R 0 T 0 22 17 addBoolXorEqVar Add a clause to the SAT constraint which states that LEFT RIGTH lt gt TARGET API boolean addBoolXorEqVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver BoolVar T VF bool T solver SatFactory addBoolXorEqVar L R solver findAllSolutions T The solutions of the problem are L R 1 T 0 L 1 R 0 T 1 e L 0 R 1 T 1 e L 0R 0 T 0 22 18 addClauses Adding a clause involved either e a logical operator TREE and an instance of the solver e or two arrays of boolean variables The two methods add a clause to the SAT constraint e The first method adds one or more clauses defined by a LogOp LopOp aims at simplif
17. Factory org chocosolver solver search loop monitors SearchMonitorFactory API void restartAfterEachSolution Solver solver 27 10 nogoodRecordingOnSolution Record nogoods from solution that is anytime a solution is found a nogood is produced to prevent from finding the same solution later during the search An array of variables presumably decision ones is given as input to reduce the size of the generated nogoods Factory org chocosolver solver search loop monitors SearchMonitorFactory API void nogoodRecordingOnSolution IntVar vars 27 11 nogoodRecordingFromRestarts Record nogoods from restarts that is anytime the search restarts one or more nogoods are produced based on the decision path to prevent from scanning the same sub search tree 27 7 limitFail 157 Choco3 Documentation Release 3 3 1 Factory org chocosolver solver search loop monitors SearchMonitorFactory API void nogoodRecordingFromRestarts Solver solver 158 Chapter 27 Search Monitors Part VI Extensions of Choco 159 CHAPTER 28 IO extensions 28 1 choco parsers choco parsers is an extension of Choco 3 It provides a parser for the FlatZinc language a low level solver input language that is the target language for MiniZinc This module follows the flatzinc standards that are used for the annual MiniZinc challenge It only supports integer variables You will find it at
18. It attempts to find all solutions of the problem It returns the number of solutions found in the given limit if any 6 2 Optimization problems Choco 3 enables to solve optimization problems that is in which a variable must be optimized Tip For functions one should declare an objective variable and declare it as the result of the function Function to maximize 3X 4Y IntVar OBJ VF bounded objective 0 999 solver solver post ICF scalar new IntVar X Y new int 3 4 OBJ solver findOptimalSolution ResolutionPolicy MAXIMIZE OBJ 36 Chapter 6 Finding solutions Choco3 Documentation Release 3 3 1 6 2 1 Finding one optimal solution Finding one optimal solution is made through a call to the solver findOptimalSolution ResolutionPolicy IntVar method The first argument defines the kind of optimization required minimization ResolutionPolicy MINIMIZE or maximization ResolutionPolicy MAXIMIZE The second argument indicates the variable to optimize For instance solver findOptimalSolution ResolutionPolicy MAXIMIZE OBJ states that the variable OBJ must be maximized The method does not return any value However the best solution found so far is restored Important Because the best solution is restored all variables are instantiated after a call to solver findOptimalSolution The best solution found is the optimal one if the
19. NS 4 4 ST 3 e NS O 3 NS 1 1 NS 2 2 NS 3 4 NS 4 0 ST 3 18 43 subpath The subpath constraint involves e an array of integer variables VARS e an integer variable START e an integer variable END e an integer OFFSET and e an integer variable SIZE It ensures that the elements of VARS define a path of SIZE vertices leading from START to END where e VARS i OF FSET j means that j is the successor of i e VARS i OF FSET i means that vertex i is excluded from the path 108 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 Moreover VARS END OFFSET VARS OFESET See also subpath in the Global Constraint Catalog Implementation based on path circuit API Constraint subpath IntVar VARS IntVar START IntVar END int OFFSET IntVar SIZE Example Solver solver new Solver IntVar VS VF enumeratedArray VS 4 0 4 solver IntVar S VF enumerated S 0 3 solver IntVar E VF enumerated E 0 3 solver IntVar SI VF enumerated SI 2 3 solver solver post ICF subpath VS S E 0 SI solver findAllSolutions YA WR 4 KY Ye Some solutions of the problem are e VS O 1 VS 1 4 VS 2 2 VS 3 3 S 0 E 1 ST 2 e VS O 4 VS 1 1 VS 2 2 VS 3 0 S 3 E 0 SI 2 e VS O 3 VS 1 1 VS 2 4 VS 3 2 S 0 E 2 SI 3 e VS O 0
20. Some solutions of the problem are e VS 0 0 VS 1 0 VS 2 0 VS 3 0 VA 1 CO 0 e VS 0 0 VS 1 1 VS 2 1 VS 3 0 VA 1 CO 2 VS 0 0 VS 1 2 VS 2 2 VS 3 1 VA 3 CO 0 e VS 0 3 VS 1 3 VS 2 3 VS 3 3 VA 3 CO 4 18 16 cumulative The cumulative constraints involves e an array of task object TASKS e an array of integer variable HEIGHTS e an integer variable CAPACITY and e a boolean INCREMENTAL graph based self decomposition of FLP14 It ensures that at each point of the time the cumulative height of the set of tasks that overlap that point does not exceed the given capacity See also cumulative in the Global Constraint Catalog Implementation based on FLP14 API Constraint cumulative Task TASKS IntVar HEIGHTS IntVar CAPACITY Constraint cumulative Task TASKS IntVar HEIGHTS IntVar CAPACITY boolean INCRE ENTAL The first API relies on the second and set INCREMENTAL to TASKS length gt 500 Example 1 1 Solver solver new Solver 2 Task TS new Task 5 3 IntVar HE new IntVar 5 4 for int i 0 i lt TS length i 90 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 5 IntVar S VF bounded S_ i 0 4 solver 6 TS i VF task 7 S 8 VF fixed D_ i i 1 solver 9 VF offset S i 1 10 u
21. available in the library The exercise consists in choosing carefully what constraints combine to properly express the problem while taking advantage of the benefits they offer in terms of efficiency wikipedia 1 2 What is Choco Choco is a Free and Open Source Software dedicated to Constraint Programming It is written in Java under BSD license It aims at describing real combinatorial problems in the form of Constraint Satisfaction Problems and solving them with Constraint Programming techniques Choco is used for e teaching easy to use e research easy to extend e real life applications easy to integrate Choco is among the fastest CP solvers on the market In 2013 and 2014 Choco has been awarded two silver medals and three bronze medals at the MiniZinc challenge that is the world wide competition of constraint programming solvers In addition to these performance results Choco benefits from academic contributors who provide support and long term improvements and the consulting company COSLING which provides services ranging from training to the development and the integration of CP models into larger applications Choco official website is http www choco solver org Choco3 Documentation Release 3 3 1 1 3 Technical overview Choco 3 includes e various type of variables integer boolean set and real e various state of the art constraints alldifferent count nvalues etc e various search strategies
22. for instance x 5 Decisions are computed and applied until all the variables are instantiated that is a solution is found or a failure has been detected Choco 3 3 1 build a binary search tree each decision can be refuted When a decision has to be computed the search strategy is called to provide one for instance x 5 The decision is then applied the variable the domain of x is reduced to 5 and the decision is validated thanks to the propagation If the application of the decision leads to a failure the search backtracks and the decision is refuted 2 4 5 and validated through propagation Otherwise if there is no more free variables then a solution has been found else a new decision is computed Note There are many ways to explore the search space and this steps should not be overlooked Search strategies or heuristics have a strong impact on resolution performances Thus it is strongly recommended to adapt the search space exploration to the problem treated 8 2 Zoom on IntStrategy A search strategy Int Strategy is dedicated to Int Var only It is based on a list of variables scope a selector of variable varSelector a value selector valSelector and an optional decOperator 1 scope array of variables to branch on 2 varSelector a variable selector defines how to select the next variable to branch on 3 valSelector a value selector defines how to select a value in the domain of the selected variable
23. from basic ones to most complex impact based and activity based search e explanation based engine that enables conflict based back jumping dynamic backtracking and path repair But also facilities to interact with the search loop factories to help modeling many samples an interface to Ibex etc The source code of choco solver 3 is hosted on GitHub Choco also has many extensions including a FlatZinc parser to solve minizinc instances and a graph variable module to better solve graph problems such as the TSP An overview of the features of Choco 3 may also be found in the presentation made in the CP Solvers Modeling Applications Integration and Standardization workshop of CP2013 1 4 History The first version of Choco dates from the early 2000s A few years later Choco 2 has encountered a great success in both the academic and the industrial world For maintenance issue Choco has been completely rewritten in 2011 leading to Choco 3 The first beta version of Choco 3 has been released in 2012 The latest version is Choco 3 3 1 1 5 How to get support A forum is available on the website of Choco It is dedicated to technical questions about the Choco solver and basic modeling helps If you encounter any bug or would like some features to be added please feel free to open a discussion on the forum You can also use the following support mailing list choco3 support mines nantes fr As can be seen on the Choco website mos
24. solver solver post ICF absolute X Y solver findAllSolutions The solutions of the problem are X 0 Y 0 X 1 Y 1 X 1 Y 1 X 2 Y 2 18 2 alldifferent The alldifferent constraints involves two or more integer variables VARS and holds that all variables from VARS take a different value A signature offers the possibility to specify the filtering algorithm to use e BC filters on bounds only based on LopezOrtizQTvB03 e AC filters on the entire domain of the variables based on Regin94 It runs in O m n worst case time for the initial propagation The average runtime of further propagations is O n m DEFAULT uses BC plus a probabilistic AC propagator to get a compromise between BC and AC See also alldifferent in the Global Constraint Catalog 79 Choco3 Documentation Release 3 3 1 Implementation based on Regin94 LopezOrtizQTVB03 API Constraint alldifferent IntVar VARS Constraint alldifferent IntVar VARS String CONSISTENCY Example Solver solver new Solver IntVar W VF enumerated W 0 1 solver IntVar X VF enumerated X 1 2 solver IntVar Y VF enumerated Y 2 4 solver IntVar Z VF enumerated Z 5 7 solver solver post ICF alldifferent new IntVar W X Y 2 solver findAllSolutions Some solutions of the problem are e X 1 Y 2 Z 5 W 1 e X 1 Y 2 Z 7 W 0 e X
25. true 1 solver findAllSolutions Some solutions of the problem are 18 17 diffn 91 Choco3 Documentation Release 3 3 1 e X 0 0 X 1 1 X 2 0 X 3 1 Y 0 0 Y 1 0 Y 2 1 Y 3 e X 0 1 X 1 0 X 2 1 X 3 0 Y 0 0 Y 1 0 Y 2 2 Y 3 e X 0 0 X 1 1 X 2 0 X 3 1 Y 0 1 Y 1 0 Y 2 2 Y 3 18 18 distance The distance constraint involves either e two variables VAR and VAR2 an operator OP and a constant CSTE It ensures that VAR VAR2 OP CSTE where OP must be chosen in gt lt e or three variables VARI VAR2 and VAR3 and an operator OP It ensures that VARI VAR2 OP VAR3 where OP must be chosen in gt lt See also distance in the Global Constraint Catalog API Constraint distance IntVar VAR1 IntVar VAR2 String OP int CSTE Constraint distance IntVar VAR1 IntVar VAR2 String OP IntVar VAR3 Example 1 Solver solver new Solver IntVar X VF enumerated X 0 2 solver IntVar Y VF enumerated X 3 1 solver solver post ICF distance X Y 1 solver findAllSolutions u ae Y Ny n The solutions of the problem are e X 0 Y e X 0 Y 1 e X 1 Y 0 e X 2 Y l Example 2 Solver solver new Solver IntVar X VF enumerated X 1 3 solver IntVar Y VF enumerated Y 1 1 solver IntVar Z VF enumera
26. 1 P2 1 P3 1 N 1 e Pl 1 P2 1 P3 1 N 0 e Pl 1 P2 0 P3 1 N 0 e P1 0 P2 0 P3 1 N 1 22 19 addFalse Add a unit clause to the SAT constraint which states that the boolean variable BOOLVAR must be false equal to 0 API 136 Chapter 22 Sat solver e u N u e u N Choco3 Documentation Release 3 3 1 boolean addFalse BoolVar BOOLVAR Example Solver solver new Solver BoolVar B VF bool B solver SatFactory addFalse B solver findAllSolutions The solution of the problem is e B 0 22 20 addMaxBoolArrayLessEqVar Add a clause to the SAT constraint which states that maximum BOOLVARS lt TARGET API boolean addMaxBoolArrayLessEqVar BoolVar BOOLVARS BoolVar TARGET Example Solver solver new Solver BoolVar BVARS VF boolArray BS 3 BoolVar T VF bool T solver SatFactory addMaxBoolArrayLessEqVar BVARS solver findAllSolutions solver T Some solutions of the problem are BS O 1 BS 1 1 BS 2 1 T 1 e BS O 1 BS 1 0 BS 2 1 T 1 BS O 0 BS 1 1 BS 2 1 T 1 e BS O 0 BS 1 0 BS 2 0 T 0 22 21 addSumBoolArrayGreaterEqVar Add a clause to the SAT constraint which states that sum BOOLVARS gt TARGET API boolean addSumBoolArrayGreaterEqVar BoolVar BOOLVARS BoolVar TARGET Example 22 20
27. 3 1 Constraint path IntVar VARS IntVar START IntVar END int OFFSET Example Solver solver new Solver IntVar VS VF enumeratedArray VS 4 0 4 solver IntVar S VF enumerated S 0 3 solver IntVar E VF enumerated E 0 3 solver solver post ICF path VS S E 0 solver findAllSolutions P Some solutions of the problem are e VS 0 1 VS 1 2 VS 2 3 VS 3 4 S 0 E 3 e VS 0 1 VS 1 3 VS 2 0 VS 3 45 2 E 3 e VS 0 3 VS 1 4 VS 2 0 VS 3 1 5 2 E 1 e VS O 4 VS 1 3 VS 2 1 VS 3 0 S 2 E 0 18 38 regular The regular constraint involves e an array of integer variables VARS and e a deterministic finite automaton AUTOMATON It enforces the sequences of VARS to be a word recognized by AUTOMATON There are various ways to declare the automaton e create a FiniteAutomaton and add states initial and final ones and transitions see FiniteAutomaton API for more details e create a FiniteAutomaton with a regexp as argument Beware FiniteAutomaton only handles values between 0 and 65535 because it relies on java Character Implementation based on Pes04 API Constraint regular IntVar VARS IAutomaton AUTOMATON Example Solver solver new Solver IntVar CS VF enumeratedArray CS 4 1 5 solver solver post ICF regular CS new FiniteAutomaton 1 2 3x 415
28. API Constraint element IntVar INDEX SetVar SETS int OFFSET SetVar SET 116 Chapter 19 Constraints over set variables Choco3 Documentation Release 3 3 1 19 8 int_channel The int_channel constraint involves e an array of set variables SETS e an array of integer variables INTEGERS e two integers OFFSET_1 and OFFSET 2 It ensures that x SETS y OFFSET_1 gt INTEGERS x OFFSET_2 y The API is Constraint int_channel SetVar SETS IntVar INTEGERS int OFFSET_1 int OFFSET_2 19 9 int_values_union The int_values_union constraint involves e an array of integer variables VARS and e a set variable VALUES It ensures that VALUES VARS U VARS U U VARS The API is Constraint int_values_union IntVar VARS SetVar VALUES 19 10 intersection The intersection constraint involves e an array of set variables SETS and e a set variable INTERSECTION It ensures that INTERSECTION is the intersection of the sets SETS The API is Constraint intersection SetVar SETS SetVar INTERSECTION 19 11 inverse_set The inverse_set constraint involves e an array of set variables SETS e an array of set variable INVERSE_SETS and e two integers OFFSET_1 and OFFSET 2 19 8 int_channel 117 Choco3 Documentation Release 3 3 1 It ensures that x math in SETS y OFFSET_1 lt y INVERSE
29. HE i VF bounded HE_ i i 1 i 1 solver 12 13 IntVar CA VF enumerated CA 1 3 solver 14 solver post ICF cumulative TS HE CA true 15 solver findAllSolutions Some solutions of the problem are e S 0 0 HE_0 0 S_1 0 HE_1 0 S_2 0 HE_2 1 S_3 0 HE_3 2S 4 4 HE 4 3 CA 3 e S 0 4 HE 0 0 S_1 4 HE_1 0 8S_2 1 HE_2 1 S_3 0 HE_3 2S 4 4 HE 4 3 CA 3 e S 0 0 HE_O 1 S_1 0 HE_1 0 S_2 1 HE_2 1 S_3 0 HE_3 2S 4 4 HE 4 3 CA 3 18 17 diffn The diffn constraint involves e four arrays of integer variables X Y WIDTH and HEIGHT and a boolean USE_CUMUL It ensures that each rectangle i defined by its coordinates X i Y i and its dimensions WIDTH i HEIGHTT i does not overlap each other The option USE_CUMUL recommended indicates whether or not redundant cumulative constraints should be added on each dimension See also diffn in the Global Constraint Catalog Implementation based on FLP14 API Constraint diffn IntVar X IntVar Y IntVar WIDTH IntVar HEIGHT boolean USE_CUMUL Example 1 1 Solver solver new Solver 2 IntVar X VF boundedArray X 4 0 1 solver IntVar Y VF boundedArray Y 4 0 2 solver 4 IntVar D new IntVar 4 5 IntVar W new IntVar 4 6 for int i 0 i lt 4 i 7 D i VF fixed D_ i 1 solver 8 W i VF fixed W_ i i 1 solver 9 10 solver post ICF diffn X Y D W
30. Id Ee A ee A Ee ee ee Ae 19 23 WHOM A ee eek Gs A BRR Be EAS BARS aa ee Se HSE oe wa eS S Constraints over real variables Logical constraints Ale NOt 4 4 Say NN 202 MEM as ame Bow be ma bo ED as oe e oe Bee PS 21 3 atVhenBlse s ve 4 ee bee PE A Ee dd A 214 TOMICAIO 25 5005 oe RA Oe eR A ee eS YR ORS ESR Re eA eX Sat solver 22 1 addAtMostNMinusOne miis 2445 Ox b e PRADO Ewa eee oe a ae N 22 2 addAtMostOne lt n nH hh Rw ee ee eA A RS ew amp Gee Se Ow By Bow amp 22 3 addBoolAndArrayEqualFalSe ocs 2 404405 48 44484 e Se wee eee ee be Ee 224 addBoolAndArtaylg Var 0 edie e a eed be Bap ee oe e bo bw E ape A 22 3 AGUBOOIANGEGNAL 6 2 seh Se ed ge Sh ee Roe Ea ES ee pa ee eS 2210 addBO0lEd 4 2 236 2SG BH Reha beh te ease eee be bah bh es 22 1 aAgdBoollsEqVat see 4h 8 eRe 6 HER SL oe WER eRe WES She Ee eS 2258 Add BOOS MeVar 29 21 e Hue Goo tee Sed POG EE Be Na BG wise ate wo Beane g 22 9 AUUBOOMSIV al ooo seo 4 ghee a Ok he ee a gg Bae le Bees 22 10 addBoollsNeqVat errar PASO eda ee bade we ea eed ee A 22 11 addBoolkLe eo tale Ge ri eee Rs A Bow e amp Bek Se Sew Bay Bow amp 22 12 addBoollt 23 4459 N 4a Rowe ee ee be ea eee ee bee eee ee be ee aS 22 13 AddBOOINOt ga 5 505 o a a Be GRE a Be A ae ha EES BAG EE RES a 22 4 addBoolOrArayEquallme 04 54 28 25 bee ee o bed eb eG oe eG 22 13 Add BOolOrAgayEg Vals judo es Sebi a eee OREN e EA eRe Ee A ASS 22 16 addBoolOrB Var sh bos See A Blk oe eG a ES
31. SatFactory addClauses LogOp nor LogOp or LogOp nand a b c d SatFactory addClauses LogOp and LogOp nand LogOp nor a b LogOp or c d e 32 Chapter 5 Constraints and propagators Part II Solving problems 33 CHAPTER 6 Finding solutions Choco 3 provides different API offered by Solver to launch the problem resolution Before everything there are two methods which help interpreting the results Feasibility Once the resolution ends a call to the solver isFeasible method will return a boolean which indicates whether or not the problem is feasible e true at least one solution has been found the problem is proven to be feasible e false in principle the problem has no solution More precisely if the search space is guaranteed to be explored entirely it is proven that the problem has no solution Limitation When the resolution is limited See Limiting the resolution for details and examples one may guess if a limit has been reached The solver hasReachedLimit method returns t rue if a limit has bypassed the search process false if it has ended naturally Warning In some cases the search may not be complete For instance if one enables restart on each failure with a static search strategy there is a possibility that the same sub tree is explored permanently In those cases the search may never stop or the two above methods may not be sufficient to confirm th
32. SatFactory addTrue B solver findAllSolutions The solution of the problem is B 1 22 23 addTrue 139 Choco3 Documentation Release 3 3 1 140 Chapter 22 Sat solver CHAPTER 23 Variable selectors Important By default in case of equalities the variable with the smallest index in the input array is returned Otherwise consider using a VariableSelectorWithTies See Zoom on IntStrategy 23 1 lexico var selector A built in variable selector which chooses the first non instantiated integer variable to branch on regarding the lexi cographic order Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API VariableSelector lt IntVar gt lexico_var_selector 23 2 random_var_selector A built in variable selector which randomly chooses an integer variable among non instantiated ones to branch on Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API VariableSelector lt IntVar gt random_var_selector long SEED 23 3 minDomainSize_var_ selector A built in variable selector which chooses the non instantiated integer variable with the smallest domain to branch on Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory 141 Choco3 Documentation Release 3 3 1 API VariableSelector lt IntVar gt minDomainSize _var_selector
33. Se Ee 22 17 2dd Bool XoOrhqval 4 24 dod ieee de oe GEE AX eed BS BAS a Bhs a wie s 22 18 addClAUses cio se ea a e OS POE BOR RR e OR E a 115 115 115 115 115 116 116 116 117 117 117 117 118 118 119 119 120 120 120 120 121 121 121 121 123 125 125 125 125 125 23 24 25 26 27 22 19 AddFalSe conta aaa ara e ld A REA A hes Bs Base 22 20 addMaxBoolArrayLessEqVat 2 6 05 66645 Bea Ba we e E a E 22 21 addSumBoolArrayGreaterEqVar ooo cs eA RRR EER eo 22 22 addSumBoolArraylLessEq Var ice a BA A SNS OO Re a eS DALIA EA Bae is Aes Aes es tose E Eos be BMD aoe 4 toe eo Rie Sadr se AS Variable selectors 23M l xico Var seleciona id fe ee eae Oe a Bee oa be be ek he hee 23 2 Tandom Var selector vta ee ee ae Ba A OE Re ee ee A BE OS 23 3 minDomainSize_var_selector ee 23 4 maxDomain iz var selector se se be ek a Ae A ee a Re ER SS 23 3 aMaxRepret varselector secar eh A A ee ERE Re ES a oe Value selectors 241 min vale Selecion e cues cig GS ee ROS om ES ee OE we em ee a ee ta a ee SS 24 2 mid value_selector 2i4 e2 44 420058 4 2S RRA SESE AEE a R R 24 3 max value selector s s bs ehh a Bee A A a By Hees Soe a we a a we aa 24 4 tandomBoundvalue selector ce s r a ed eo ee a ee Oe Ee we es we ad ee Y 245 random Value selector 3 lt a se joe ee hk Be pe a le Se HR ee Decision operators DSM GASSVOM ad GB dL AN Te nd A ee ete te Ap na Bee Be en 23 2 TEMOVE x 0 4 a RS GOR Eee
34. The available extensions are choco parsers choco gui choco cpviz choco graph choco geost choco exppar 61_ext_eps Note Each of those extensions include all dependencies but choco solver classes which ease their usage Choco3 Documentation Release 3 3 1 To start using Choco 3 you need to be make sure that the right version of java is installed Then you can simply add the choco solver jar file and extension libraries to your classpath or declare them as dependency of a Maven based project 2 1 2 Update the classpath Simply add the jar file to the classpath of your project in a terminal or in your favorite IDE 2 1 3 As a Maven Dependency Choco is build and managed using Maven3 Choco is available on Maven Central Repository to declare Choco as a dependency of your project simply update the pom xm1 of your project by adding the following instruction lt dependency gt lt groupId gt org choco solver lt groupId gt lt artifactId gt choco solver lt artifactId gt lt version gt X Y Z lt version gt lt dependency gt where X Y Z is replaced by 3 3 1 Note that the artifact does not include any dependencies or logback xml Please refer to README md for the list of required dependencies 2 1 4 Compiling sources As a Maven based project Choco can be installed in a few instructions Once you have downloaded the source from the zip file or GitHub simply run the following command mvn
35. VARSI is lexicographically strictly less or equal than VARS2 See also lex_less_eq in the Global Constraint Catalog Implementation based on FHK 02 API Constraint lex_less_eq IntVar VARS1 IntVar VARS2 Example 1 Solver solver new Solver 2 IntVar X VF enumeratedArray X 3 1 1 solver 3 IntVar Y VF enumeratedArray Y 3 1 2 solver 4 solver post ICF lex_less_eq X Y 5 solver findAllSolutions Some solutions of the problems are e X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 e X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 e X 0 0 X 1 0 X 2 0 Y 0 2 Y 1 1 Y 2 2 e X 0 1 X 1 1 X 2 1 Y 0 2 Y 1 2 Y 2 2 98 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 18 29 maximum The maximum constraints involves a set of integer variables and a third party integer variable either e two integer variables VARZ and VAR2 and an integer variable MAX it ensures that MAX maximum VARI VAR2 e or an array of integer variables VARS and an integer variable MAX it ensures that MAX is the maximum value of the collection of domain variables VARS e or an array of boolean variables BVARS and a booean variable MAX it ensures that MAX is the maximum value of the collection of boolean variables BVARS See also maximum in the Global Constraint Catalog API
36. addMaxBoolArrayLessEqVar 137 u e Bw N u e uv N Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar BVARS VF boolArray BS 3 solver BoolVar T VF bool T solver SatFactory addSumBoolArrayGreaterEqVar BVARS T solver findAllSolutions Some solutions of the problem are BS O 1 BS 1 1 BS 2 1 T 1 e BS O 1 BS 1 0 BS 2 1 T 1 BS O 0 BS 1 1 BS 2 1 T 1 e BS O 0 BS 1 0 BS 2 0 T 0 22 22 addSumBoolArrayLessEqVar Add a clause to the SAT constraint which states that sum BOOLVARS lt TARGET API boolean addSumBoolArrayLessEqVar BoolVar BOOLVARS BoolVar TARGET Example Solver solver new Solver BoolVar BVARS VF boolArray BS 3 solver BoolVar T VF bool T solver SatFactory addSumBoolArrayLessEqVar BVARS T solver findAllSolutions Some solutions of the problem are e BS O 1 BS 1 1 BS 2 1T 1 e BS O 1 BS 1 0 BS 2 1T 1 e BS 0 0 BS 1 1 BS 2 1T 1 e BS 0 0 BS 1 0 BS 2 OT 1 22 23 addTrue Add a unit clause to the SAT constraint which states that the boolean variable BOOLVAR must be true equal to 1 API boolean addTrue BoolVar BOOLVAR Example 138 Chapter 22 Sat solver N Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar B VF bool B solver
37. clean install DskipTests This instruction downloads the dependencies required for Choco3 such as the trove4j and logback then compiles the sources The instruction DskipTests avoids running the tests after compilation and saves you a couple of hours Regression tests are run on a private continuous integration server Maven provides commands to generate files needed for an IDE project setup For example to create the project files for your favorite IDE IntelliJ Idea mvn idea idea Eclipse mvn eclipse eclipse 2 1 5 Note about logging In Choco we distinguish user trace and developer trace User trace is mainly dedicated to printing resolution statistics and solutions and other useful services The Chatterbox class is devoted to such aim it centralises almost all 10 Chapter 2 Getting started Choco3 Documentation Release 3 3 1 messaging services Developer trace is for debugging purpose In order to avoid imposing a logging framework on end user Choco 3 relies on SLF4J for the logging system SLF4J is a simple facade for logging systems allowing the end user to plug in the desired logging system at deployment time http www slf4j org faq html SLF4J is only a facade meaning that it does not provide a complete logging solution and a logging framework must be bound Otherwise you ll get the following error n LF4J Failed to load class org slf4j impl Sta
38. defined configurations Here is the way to declare LNS to solve a problem LNSFactory rlns solver ivars 30 20140909L new FailCounter 100 solver findOptimalSolution ResolutionPolicy MINIMIZE objective It declares a random LNS which on a solution computes a partial solution based on ivars If no solution are found within 100 fails FailCounter 100 a restart is forced Then every 30 calls to this neighborhood the number of fixed is randomly picked 20140909L is the seed for the java util Random The instruction LNSFactory rlns solver vars level seed frcounter runs LargeNeighborhoodSearch lns return lns new LargeNeighborhoodSearch solver solver getSearchlLoop plugSearchMonitor lns neighbor true The factory provides other LNS configurations together with built in neighbors 1 Paul Shaw Using constraint programming and local search methods to solve vehicle routing problems In Michael Maher and Jean Francois Puget editors Principles and Practice of Constraint Programming CP98 volume 1520 of Lecture Notes in Computer Science pages 417 431 Springer Berlin Heidelberg 1998 55 Choco3 Documentation Release 3 3 1 11 2 Neighbors While the implementation of LNS is straightforward the main difficulty lies in the design of neighborhoods able to move the search further Indeed the balance between diversification i e evaluating unexplored sub tr
39. envelope s cardinality minus kernel s cardinality and forces its smallest first unfixed value to be part of the kernel Scope Set Var Factory org chocosolver solver search strategy SetStrategyFactory API SetStrategy force_minDelta_first SetVar sets 26 5 lexico_LB A built in strategy which chooses the first non instantiated variable regarding the lexicographic order and assigns it to 1ts lower bound Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy lexico_LB IntVar VARS 26 6 lexico Neq LB A built in strategy which chooses the first non instantiated variable regarding the lexicographic order and removes its lower bound from its domain Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy lexico_Neq_LB IntVar VARS 148 Chapter 26 Built in strategies Choco3 Documentation Release 3 3 1 26 7 lexico_Split A built in strategy which chooses the first non instantiated variable regarding the lexicographic order and removes the second half of its domain Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy lexico_Split IntVar VARS 26 8 lexico UB A built in strategy which chooses the first non instantiated variable regarding the lexicographic order and assigns it to its upper bound Scop
40. even more of the given solver The method is called from the search loop after the initial propagation if no search strategy is de fined Otherwise it should be called before running the resolution The search binder to use must be declared in the Setting attached to a Solver see Settings 8 4 Composition of strategies Most of the time it is necessary to combine various strategies A StrategiesSequencer enables to compose various AbstractStrategy It is created on the basis of a list of AbstractStrategy The current active strategy is called to compute a decision through its getDecision method When no more decision can be computed for the current strategy the following one becomes active The intersection of variables from each strategy does not have to be empty When a variable appears in various strategy it is ignored as soon as it is instantiated When no environment is given in parameter the last active strategy is not stored and strategies are evaluated in lexicographical order to find the first active one based on its capacity to return a decision When an environment is given in parameter the last active strategy is stored API IntStrategyFactory sequencer AbstractStrategy strategies Note that a strategy sequencer is automatically generated when setting multiple strategies at the same time solver set strategyl strategy2 is equivalent to solver set ISF sequencer strategyl strategy2 Finally one c
41. https github com chocoteam choco parsers 28 2 choco gui choco gui is an extension of Choco 3 It provides a Graphical User Interface with various views which can be simply plugged on any Choco Solver object You will find it at https github com chocoteam choco gui 28 3 choco cpviz choco cpviz is an extension of Choco 3 to deal with cpviz library You will find it at https github com chocoteam choco cpviz 161 Choco3 Documentation Release 3 3 1 162 Chapter 28 IO extensions CHAPTER 29 Modeling extensions 29 1 choco graph choco graph is a Choco 3 module which allows to search for a graph which may be subject to graph constraints The domain of a graph variable G is a graph interval in the form G_lb G_ub G_lb is the graph representing vertices and edges which must belong to any single solution whereas G_ub is the graph representing vertices and edges which may belong to one solution Therefore any value G_v must satisfy the graph inclusion G_lb subgraph of G_v subgraph of G_ub One may see a strong connection with set variables A graph variable can be subject to graph constraints to ensure global graph properties e g connectedness acyclicity and channeling constraints to link the graph variable with some other binary integer or set variables The solving process consists of removing nodes and edges from G_ub and adding some others to G_lb until having G_lb G_ub i e until G gets instantiated T
42. i lt TOTAL_WEIGHT and y OCCURRENCES i x ENERGYTi TOTAL_ENERGY API Constraint knapsack IntVar OCCURRENCES IntVar TOTAL_WEIGHT IntVar TOTAL ENERGY int WEIGHT int ENERGY Example 1 Solver solver new Solver 2 IntVar IT new IntVar 3 3 items 3 IT O VF bounded IT_0 0 3 solver 4 IT 1 VF bounded IT_1 0 2 solver 5 IT 2 VF bounded IT_2 0 1 solver 6 IntVar WE VF bounded WE 0 8 solver 7 IntVar EN VF bounded EN 0 6 solver 8 int weights new int 1 3 4 9 int energies new int 1 4 6 10 solver post ICF knapsack IT WE EN weights energies 11 solver findAllSolutions Some solutions of the problems are e IT 0 0 IT_ 0 IT_2 0 WE 0 EN 0 e IT 0 3 IT_ 1 0 IT_2 0 WE 3 EN 3 e IT 0 1 IT_1 1 IT_2 0 WE 4 EN 5 e IT 0 2 1T 1 1 1IT 2 0 WE 5 EN 6 18 25 lex_chain_less The lex_chain_less constraint involves a matrix of integer variables VARS It ensures that for each pair of consecutive arrays VARS i and VARS i 1 VARS i is lexicographically strictly less than VARS i 1 See also lex_chain_less in the Global Constraint Catalog Implementation based on CB02 API Constraint lex_chain_less IntVar VARS Example 96 Chapter 18 Constraints over integer variables Choco3 Documentation R
43. in the Global Constraint Catalog Implementation based on Regin94 CL97 CB04 FL12 FL11 Fag14 API Constraint circuit IntVar VARS int OFFSET CircuitConf CONF Constraint circuit IntVar VARS int OFFSET with CircuitConf RD Example Solver solver new Solver IntVar NODES VF enumeratedArray NODES 5 0 4 solver solver post ICF circuit NODES 0 CircuitConf LIGHT solver findAllSolutions e uvu N Some solutions of the problem are e NODES 0 1 NODES 1 2 NODES 2 3 NODES 3 4 NODES 4 0 e NODES O 3 NODES 1 4 NODES 2 0 NODES 3 1 NODES 4 2 e NODES 0 4 NODES 1 2 NODES 2 3 NODES 3 0 NODES 4 1 e NODES 0 4 NODES 1 3 NODES 2 1 NODES 3 0 NODES 4 2 18 14 cost_regular The cost_regular constraint involves e an array of integer variables VARS e an integer variable COST and e a cost automaton CAUTOMATON It ensures that the assignment of a sequence of variables VARS is recognized by CAUTOMATON a deterministic finite automaton and that the sum of the costs associated to each assignment is bounded by the cost variable This version allows to specify different costs according to the automaton state at which the assignment occurs i e the transition starts The CAUOTMATON can be defined using the org chocosolver solver constraints nary automata FA CostAutomaton either e by creati
44. integer variables VARS e an integer variable NVALUES and e a boolean STRONG Let N be the number of distinct values assigned to the variables of the VARS collection The constraint enforces the condition N lt NVALUES to hold If the boolean STRONG is set to true then the filtering algorithm of FLapegue14 is added It automatically detects disequalities and alldifferent constraints This propagator is more powerful but more time consuming as well this is presumably worthwhile when NVALUES must be minimized See also atmost_nvalues in the Global Constraint Catalog Implementation based on FLapegue 14 API Constraint atmost_nvalues IntVar VARS IntVar NVALUES boolean GREEDY Example 1 Solver solver new Solver 2 IntVar XS VF enumeratedArray XS 4 0 2 solver 3 IntVar N VF enumerated N 1 3 solver 4 solver post ICF atmost_nvalues XS N false 5 solver findAllSolutions Some solutions of the problem are e XS O 0 XS 1 0 XS 2 0 XS 3 0 N 1 e XS 0 0 XS 1 0 XS 2 0 XS 3 0 N 2 e XS 0 0 XS 1 0 XS 2 0 XS 3 0 N 3 e XS 0 0 XS 1 0 XS 2 0 XS 3 1 N 2 e XS 0 0 XS 1 1 XS 2 1 XS 3 0 N 2 e XS 0 2 XS 1 2 XS 2 1 XS 3 0 N 3 18 9 bin_packing The bin_packing constraint involves an array of integer variables JTEM_BIN an array of integers ITEM_SIZE an array of i
45. just like BoolVar and provides the following API LogOp and ILogical operands create a conjunction results in true if all of its operands are true ogOp ifOnlyIf ILogical a ILogical b create a biconditional results in true if and only if both operands are false or both operands are true 5 4 SAT constraints 31 Choco3 Documentation Release 3 3 1 OgOp ifThenElse ILogical a ILogical b ILogical c create an implication re sults in true if a is true and b is true ora is false and cis true ogOp implies ILogical a ILogical b create an implication results in true if a is false or b is true LogOp reified BoolVar b ILogical tree create a logical connection between b and tree Log0p or ILogical operands create a disjunction results in true whenever one or more of its operands are true Log0p nand ILogical operands create an alternative denial results in if at least one of its operands is false LogOp nor ILogical operands create a joint denial results in true if all of its operands are false LogOp xor ILogical a ILogical b create an exclusive disjunction results in true when ever both operands differ ILogical negate ILogical 1 return the logical complement of l The resulting logical operation can be very verbose but certainly more easy to declare SatFactory addClauses LogOp and LogOp nand LogOp nor a b LogOp or c d e
46. remove Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API DecisionOperator lt IntVar gt assign 25 2 remove A built in decision operator which removes the selected value from the selected variable domain Its negation is assign Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API DecisionOperator lt IntVar gt remove 25 3 split A built in decision operator which splits the selected variable domain at the selected value that is it updates the upper bound of the variable to the selected value Its negation is reverse_split on value 1 Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API DecisionOperator lt IntVar gt split 145 Choco3 Documentation Release 3 3 1 25 4 reverse split A built in decision operator which splits the selected variable domain at the selected value that is it updates the lower bound of the variable to the selected value Its negation is split on value 1 Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API DecisionOperator lt IntVar gt reverse_split 146 Chapter 25 Decision operators CHAPTER 26 Built in strategies 26 1 custom To build a specific strategy based on IntVar or SetVar A strategy is based on a variable selector a value selector and an optional decisi
47. solver 4 3 Constants Fixed value integer variables should be created with a call to the following functions VariableFactory fixed seven 7 solver Or VariableFactory fixed 8 Solver where 7 and 8 are the constant values Not specifying a name to a constant enables the solver to use cache and avoid multiple occurrence of the same object in memory 4 4 Variable views Views are particular integer variables they can be used inside constraints Their domains are implicitly defined by a function and implied variables x is a constant IntVar x VariableFactory fixed 1 solver IntVar x VariableFactory offset y 2 x y IntVar x VariableFactory minus y x 3xy 4 3 Constants 25 Choco3 Documentation Release 3 3 1 IntVar x VariableFactory scale y 3 Views can be combined together IntVar x VariableFactory offset VariableFactory scale y 2 5 4 5 Set variable A set variable SV represents a set of integers Its domain is defined by a set interval S_E S_K e the envelope S_E is an ISet object which contains integers that potentially figure in at least one solution e the kernel S_K is an ISet object which contains integers that figure in every solutions Initial values for both S_K and S_E can be specified If no initial value is given for S_K it is empty by default Th
48. strategy by forcing some decisions to branch on variables involved in recent conflicts After each conflict the last assigned variable is selected in priority so long as a failure occurs Implementation based on LSTV09 Scope Variable 152 Chapter 26 Built in strategies Choco3 Documentation Release 3 3 1 Factory org chocosolver solver search strategy IntStrategyFactory API AbstractStrategy lastConflict Solver SOLVER AbstractStrategy lastConflict Solver SOLVER AbstractStrategy STRAT AbstractStrategy lastKConflicts Solver SOLVER int K AbstractStrategy STRAT 26 22 generateAndTest A strategy that simulate a Generate and Test behavior through a specific internal decision The main idea is from all the variables of a problem to generate and test the satisfiability of a complete instantiation The process does not rely on propagation anymore but on satisfaction only Such strategy can be triggered when the search space reached a given limit Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API AbstractStrategy lt IntVar gt generateAndTest Solver SOLVER AbstractStrategy lt IntVar gt generateAndTest Solver SOLVER AbstractStrategy lt IntVar gt mainStrategy int searchSpaceLimit 26 22 generateAndTest 153 Choco3 Documentation Release 3 3 1 154 Chapter 26 Built in strategies CHAPTER 27 Search Monitor
49. such as statistics execution time nodes etc or solutions Resolution data are available thanks to the Chatterbox class which outputs to System out It centralises widely used methods to have comprehensive feedbacks about the resolution process There two main types of methods those who need to be called before the resolution with a prefix show and those who need to called after the resolution with a prefix print For instance one can indicate to print the solutions all resolution long Chatterbox showSolutions solver solver findAllSolutions Or to print the search statistics once the search ends solver findSolution Chatterbox printStatistics solver On a call to Chatterbox printVersion the following message will be printed xx Choco 3 3 1 2015 05 Constraint Programming Solver Copyleft c 2010 2015 On a call to Chatterbox printVersion the following message will be printed Search complete No solution 0 solution s found Incomplete search Limit reached Unexpected interruption Solutions 0 Maximize 1 Minimize 2 Building time 3 s Initialisation 4 s Initial propagation 5 s Resolution 6 s Nodes 7 Backtracks 8 Fails 9 Restarts 10 Max depth 11 Memory 12 mb 47 Choco3 Documentation Release 3 3 1 Variables 13 Constraints 14 Curly brackets finstru
50. the solver might exceed the time limit e limitSolution stops the search when the given solution limit has been reached e limitNode stops the search when the given search node limit has been reached e limitFail stops the search when the given fail limit has been reached e limitBacktrack stops the search when the given backtrack limit has been reached 8 6 2 Custom search limits You can decide to interrupt the search process whenever you want with one of the following instructions 1 Resolution events are backtracks fails nodes solutions time or user defined ones 8 6 Limiting the resolution 45 Choco3 Documentation Release 3 3 1 solver getSearchLoop reachLimit solver getSearchLoop interrupt String message Both options will interrupt the search process but only the first one will inform the solver that the search stops because of a limit In other words calling solver hasReachedLimit will return false if the second option is used Going further Large Neighborhood Search Explanations 46 Chapier 8 Search Strategies CHAPTER 9 Resolution statistics Choco 3 distinguishes developer trace and user trace Developer trace is only dedicated to developers for debugging purpose Choco depends on SLF4J as described in Note about logging User trace is dedicated to users and devel opers to print information related to the resolution of a problem
51. 0 1007 978 3 540 30201 8_36 Ref04 Philippe Refalo Impact based search strategies for constraint programming In Principles and Practice of Constraint Programming CP 2004 10th International Conference CP 2004 Toronto Canada Septem ber 27 October 1 2004 Proceedings 357 571 2004 URL http dx doi org 10 1007 978 3 540 30201 8_41 doi 10 1007 978 3 540 30201 8_41 Regin94 Jean Charles R gin A filtering algorithm for constraints of difference in csps In Proceedings of the 12th National Conference on Artificial Intelligence Seattle WA USA July 31 August 4 1994 Volume 1 362 367 1994 URL http www aaai org Library AAAI 1994 aaai94 055 php Regin95 Jean Charles R gin D veloppement d outils algorithmiques pour l intelligence artificielle In Ph D The sis 1995 168 Bibliography
52. 2 Y 3 Z 5 W 0 e X 2 Y 4 Z2 7 W 1 18 3 alldifferent_conditionnal The alldifferent_conditionnal constraint is a variation of the alldifferent constraint It holds the alldifferent constraint on the subset of variables VARS which satisfies the given condition CONDITION A simple example is the alldifferent_except_0 variation of the alldifferent constraint API Constraint alldifferent_conditionnal IntVar VARS Condition CONDITION Constraint alldifferent_conditionnal IntVar VARS Condition CONDITION boolean AC One can force the AC algorithm to be used by calling the second signature Example Solver solver new Solver IntVar XS VF enumeratedArray XS 5 0 3 solver solver post ICF alldifferent_conditionnal XS x gt lx contains 1 amp amp x contains 3 Chatterbox showSolutions solver solver findAllSolutions solver findAllSolutions The condition in the example states that the values 7 and 3 can appear more than once unlike other values Some solutions of the problem are e XS 0 0 XS 1 1 XS 2 1 XS 3 1 XS 4 1 80 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 e XS 0 0 XS 1 1 XS 2 2 XS 3 1 XS 4 1 e XS 0 1 XS 1 2 XS 2 1 XS 3 1 XS 4 1 e XS O 0 XS 1 1 XS 2 2 XS 3 3 XS 4 3 18 4 alldifferent_except_0 The alldifferent_except_0 inv
53. 22 Sat solver DOGO aL N u e u N Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver BoolVar T VF bool T solver SatFactory addBoolIsLeVar L R T solver findAllSolutions The solutions of the problem are e L 1 R 1 T 1 e L 1 R 0 T 0 e L 0 R 1 T 1 e L 0 R 0 T 1 22 9 addBoollsLtVar Add a clause to the SAT constraint which states that LEFT lt RIGTH lt gt TARGET API boolean addBoolIsLtVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver BoolVar T VF bool T solver SatFactory addBoolIsLtVar L R T solver findAllSolutions The solutions of the problem are L 1 R 1 T 0 L 1 R 0 T 0 e L 0 R 1 T 1 e L 0 R 0 T 0 22 10 addBoollsNeqVar Add a clause to the SAT constraint which states that LEFT 4 RIGTH lt gt TARGET API boolean addBoolIsNeqVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET 22 9 addBoollsLtVar 131 DA u e Bw N u e uv N Choco3 Documentation Release 3 3 1 Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver BoolVar T VF bool T solver SatFactory addBoolIsNeqVar L R T solver findAllSolutions
54. 4 decOperator a decision operator defines how to modify the domain of the selected variable with the selected value On a call to IntStrategy getDecision varSelector try to find among scope a variable not yet instantiated If such a variable does not exist the method returns null saying that it can not compute decision anymore Otherwise valSelector selects a value within the domain of the selected variable A decision can then be computed with the selected variable and the selected value and is returned to the caller 41 Choco3 Documentation Release 3 3 1 By default the decision built is an assignment its application leads to an instantiation its refutation to a value removal It is possible create other types of decision by defining a decision operator DecisionOperator API IntStrategyFactory custom VariableSelector lt IntVar gt VAR_SELECTOR IntValueSelector VAL_SELECTOR DecisionOperator lt IntVar gt DEC_OPERATOR IntVar VARS IntStrategyFactory custom VariableSelector lt IntVar gt VAR_SELECTOR IntValueSelector VAL_SELECTOR IntVar VARS new IntStrategy IntVar scope VariableSelector lt IntVar gt varSelector IntValueSelector valSelector new IntStrategy IntVar scope VariableSelector lt IntVar gt varSelector IntValueSelector valSelector DecisionOperator lt IntVar gt decOperator Sometimes on a call to the variable selector several variables could be selected In that case the order in d
55. 5 2 8 solver IntVar vs VariableFactory enumeratedArray vs 5 new int 10 0 10 solver To create a matrix of 5x6 enumerated variables with same domains IntVar vs VariableFactory enumeratedMatrix vs 5 6 0 5 solver IntVar vs VariableFactory enumeratedMatrix vs 5 6 new int 1 2 3 5 6 99 solver Modelling Bounded or Enumerated The choice of representation of the domain variables should not be done lightly Not only the memory consumption should be considered but also the used constraints Indeed some constraints only update bounds of integer variables using them with bounded variables is enough Others make holes in variables domain using them with enumerated variables takes advantage of the power of the filtering algorithm Most of the time variables are associated with propagators of various power The choice of domain representation must then be done on a case by case basis 24 Chapter 4 Declaring variables Choco3 Documentation Release 3 3 1 4 2 3 Boolean variable Boolean variables Bool Var are specific Int Var which take their value in 0 1 To create a new boolean variable BoolVar b VariableFactory bool b solver To create an array of 5 boolean variables BoolVar bs VariableFactory boolArray bs 5 solver To create a matrix of 5x6 boolean variables BoolVar bs VariableFactory boolMatrix bs 5 6
56. AC if the domains are enumerated Otherwise BC is not guaranteed It also automatically imposes one alldifferent constraints on each array of variables API Constraint inverse_channeling IntVar VARS1 IntVar VARS2 int OFFSET1 int OFFSET2 Example 1 Solver solver new Solver 2 IntVar X VF enumeratedArray X 3 0 3 solver IntVar Y VF enumeratedArray Y 3 1 4 solver 4 solver post ICF inverse_channeling X Y 0 1 5 solver findAllSolutions The solutions of the problems are e X 0 0 X 1 1 X 2 2 Y 0 1 Y 1 2 Y 2 3 X 0 0 X 1 2 X 2 1 Y 0 1 Y 1 3 Y 2 2 e X 0 1 X 1 0 X 2 2 Y 0 2 Y 1 1 Y 2 3 e X 0 1 X 1 2 X 2 0 Y 0 3 Y 1 1 Y 2 2 e X 0 2 X 1 0 X 2 1 Y 0 2 Y 1 3 Y 2 1 e X 0 2 X 1 1 X 2 0 Y 0 3 Y 1 2 Y 2 1 18 23 inverse_channeling 95 Choco3 Documentation Release 3 3 1 18 24 knapsack The knapsack constraint involves an array of integer variables OCCURRENCES an integer variable TO TAL_ WEIGHT an integer variable TOTAL_ENERGY an array of integers WEIGHT and an an array of integers ENERGY It formulates the Knapsack Problem to determine the count of each item to include in a collection so that the total weight is less than or equal to a given limit and the total value is as large as possible e X OCCURRENCES i x WEIGHT
57. BVARS IntVar VAR int OFFSET Example u ae vnn Solver solver new Solver BoolVar BVARS VF boolArray BVARS 5 solver IntVar VAR VF enumerated VAR 1 5 solver solver post ICF boolean_channeling BVARS VAR 1 solver findAllSolutions The solutions of the problem are e VAR 1 BVARS O 1 BVARS 1 0 BVARS 2 0 BVARS 3 0 BVARS 4 0 VAR 2 BVARS O 0 BVARS 1 1 BVARS 2 0 BVARS 3 0 BVARS 4 0 VAR 3 BVARS 0 0 BVARS 1 0 BVARS 2 1 BVARS 3 0 BVARS 4 0 VAR 4 BVARS 0 0 BVARS 1 0 BVARS 2 0 BVARS 3 1 BVARS 4 0 VAR 5 BVARS O 0 BVARS 1 0 BVARS 2 0 BVARS 3 0 BVARS 4 1 86 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 18 12 clause_channeling The clause_channeling constraint involves e an integer variable VAR and e two arrays of boolean variables EVARS and LVARS It ensures that VAR i EVARS i OFFSET 7 and VAR lt i gt LVARS i OFFSET 7 where OFFSET is the initial lower bound of VAR API Constraint clause_channeling IntVar VAR BoolVar EVARS BoolVar LVARS Example 1 Solver solver new Solver 2 IntVar iv VF enumerated iv 1 3 solver 3 BoolVar eqs VF boolArray eq 3 solver 4 BoolVar lgqs VF boolArray lq 3 solver 5 solver post ICF clause_channeling iv eqs lqs
58. E a a BA Ee eis ie ws 19 27 a dIS OM ae 2 5 a ado Fe le eR a ee a bee A Pe a i 19 37 al egual oe is eh bee BHR Oe OHSS a Ae SADR ai Bees 19 bool Channel bs ois he tee Gece ceo By de gt eee aie te et nos Ae Ts fae sire lira Te eee a ea et eee da 19 5 CAIDA ci 34 ead wae ee he Bee RARER AR EEE AR ee ee eR EE a Ee N 19 6 GISJOMME 20 e ak o ir Boe A GSS RS ah SEES Bee de SS 1957 element s a cse es oe ome wh SE EE ee EGA a teh bee bee 8 ROS amntuchannel Leioa le cee sep var ert fords Gis an lo eso Et A os ces Ge rv ho dos Gx te Ge Go Gs se aa 19 9 mt Vald s UNION 00 dae e ae Hae oe eee 29 Be ae Bee Be ed 19 10 intersection s s eare a Sd as BAe ee AG Be Se he ee Ace Ge aed Be ae S HOST averse set lt 5 e Fete ee eae es Gre ba a goth bee be bee te Pete Pa 19 12 Max 2 48g Pete eae ea eee Se SS e ew eta Peed ee ete eee s TIAS MEME ora Yo A Boe es oe Re ee we Ae ee Re eS ee a Y Be ex 19 14 ot member lt reg e 2444 ta eaey eX PRES A SERA EPH ES OER EE OOH SG HAAS A A he ech shaw Be avin De te Ss ep Agee el dex Rea ee Ga ES es cae es Baht ee eS 19 16 nbEmply 18524466483 RR de Eee bea ee Bi bebe beeen bea es EN tea gosie es ley Be er He E TOTS OMS ra a Ge al A ee Md Se ee a a a a wl o r E E s ane go doe RA Ra pod hae eA E oO hs a A GS BSL Ba Sea a eS eo BG A PI 2O SUBSEA 6 key oo atom Se ty Sle oe BER hay Ge ae os he hy dew Oe Pe tee ae a 19 2 SUM 2024 5 4 oe the eA we ba Se RS SESE Sede RAS a eA eS es 1922 Syme ME oras MA Re a
59. IS 2 25 4244 8 o SESS REE Sees w A DDD NAA 17 19 A e Bice docs 20 a Aa bt 22 RR AAA a A 22 23 spas a e eon te te penis Be Biles 23 ity bw a Bye ko ESR E 23 Sava ada o GM fee aes BES 25 Ae Re A ee A ee 25 aia a ey Gh Be Yh eS 26 a ea Gee Aa teed eg 26 IHI Solving problems 6 Finding solutions 6 1 Satisfaction problems 6 2 Optimization problems 6 3 Multi objective optimization problems 64 Propagation oo 2 5404 448 24 4 Recording solutions 7 1 Solution storage 7 2 Solution recording 7 3 Solution restoration Search Strategies S A Brmciples osease ad 8 2 ZoomonIntStrategy 8 3 Default search strategies 8 4 Composition of strategies 85 Restarts cuido aca ita 8 6 Limiting the resolution Resolution statistics IV Advanced usage 10 11 12 13 14 15 16 Settings Large Neighborhood Search LNS ILI Principle a seg aa 11 2 Neighbors ss es e eee we ae Ss JLS Restarts o sia a al 114 Walking s i cecs eco be eae ees Multi thread resolution Explanations 13 1 Primciple 0 22568 gates 13 2 IMpractice esposos da Sk a 13 3 Explanations for the system 13 4 Explanations for the end user Search monitor 14 1 Principle siege oo A Re ape ee Defining its own search strategy 15 1 Selecting the variable 15 2 Selecting the value 15 3 Makingade
60. LOADS 1 2 BLOADS 2 5 18 10 bit_channeling The bit_channeling constraint involves e an array of boolean variables BVARS and e an integer variable VAR It ensures that VAR 2 x BITS 0 2 x BITS 1 math 2 n times BITS n BIT O is related to the first bit of VAR 2 BIT 1 is related to the second bit of VAR 2 etc The upper bound of VAR is given by 218 1 1 1 API Constraint bit_channeling BoolVar BITS IntVar VAR Example 18 10 bit_channeling 85 Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar BVARS VF boolArray BVARS 4 solver IntVar VAR VF enumerated VAR 0 15 solver solver post ICF bit_channeling BVARS VAR solver findAllSolutions The solutions of the problem are e VAR 0 BVARS O 0 BVARS 1 0 BVARS 2 0 BVARS 3 0 VAR 1 BVARS 0 1 BVARS 1 0 BVARS 2 0 BVARS 3 0 VAR 2 BVARS O 0 BVARS 1 1 BVARS 2 0 BVARS 3 0 VAR 11 BVARS 0 1 BVARS 1 1 BVARS 2 0 BVARS 3 1 VAR 15 BVARS 0 1 BVARS 1 1 BVARS 2 1 BVARS 3 1 18 11 boolean_channeling The boolean_channeling constraint involves e an array of boolean variables BVARS e an integer variable VAR and e an integer OF FSET It ensures that VAR i 4 gt BVARS i OF FSET 1 The OFFSET is typically set to 0 API Constraint boolean_channeling BoolVar
61. SU 3 18 45 table The table constraint involves either e two variables VAR and VAR2 a list of pair of values named TUPLES and an algorithm ALGORITHM e or an array of variables VARS a list of tuples of values named TUPLES and an algorithm ALGORITHM It is an extensional constraint enforcing most of the time arc consistency When only two variables are involved the available algorithms are e AC2001 applies the AC2001 algorithm e AC3 applies the AC3 algorithm e AC3rm applies the AC3rm algorithm e AC3bit rm default applies the AC3bit rm algorithm e FC applies the forward checking algorithm When more than two variables are involved the available algorithms are e GAC2001 applies the GAC2001 algorithm e GAC2001 applies the GAC2001 algorithm for allowed tuples only e GAC3rm applies the GAC3 algorithm e GAC3rm default applies the GAC3rm algorithm for allowed tuples only e GACSTR applies the GAC version STR for allowed tuples only e STR2 applies the GAC STR2 algorithm for allowed tuples only e FC applies the forward checking algorithm Implementation based on tbd API Constraint table IntVar VAR1 IntVar VAR2 Tuples TUPLES String ALGORITHM Constraint table IntVar VARS Tuples TUPLES String ALGORITHM Example 110 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 1 Solver solver new Solver
62. SolutionRecorder object or by simply using an ISolutionMonitor as follows 39 Choco3 Documentation Release 3 3 1 7 3 Solution restoration A Solution object can be restored 1 e variables are fixed back to their values in that solution For this purpose we recommend to restore initial domains and then restore the solution with the following code try solver getSearchLoop restoreRootNode solver getEnvironment worldPush solution restore eatch ContradictionException e throw new UnsupportedOperationException restoring the solution ended in a failure solver getEngine flush Note that if initial domains are not restored then the solution restoration may lead to a failure This would happen when trying to restore out of the current domain 40 Chapter 7 Recording solutions CHAPTER 8 Search Strategies 8 1 Principle The search space induces by variables domain is equal to S d x d2 x dn where d is the domain of the it variable Most of the time not to say always constraint propagation is not sufficient to build a solution that is to remove all values but one from integer variables domain Thus the search space needs to be explored using one or more search strategies A search strategy performs a performs a Depth First Search and reduces the search space by making decisions A decision involves a variables a value and an operator
63. VS 1 2 VS 2 4 VS 3 1 S 3 E 2 SI 3 18 44 sum The sum constraint involves e an array of integer or boolean variables VARS e an optional operator OPERATOR and e an integer variable SUM It ensures that sum VARS i OPERATOR SUM where operator must be chosen among gt lt gt lt 3 If no operator is defined is set by default Note that when the operator differs from an intermediate variable is declared and an arithm constraint is returned For performance reasons a specialization for boolean variables is provided See also scalar_product in the Global Constraint Catalog Implementation based on HS02 API Constraint sum IntVar VARS IntVar SUM Constraint sum IntVar VARS String OPERATOR IntVar SUM Constraint sum Constraint sum BoolVa BoolVar VARS IntVar SUM r VARS String OPERATOR IntVar SUM Example 18 44 sum 109 Choco3 Documentation Release 3 3 1 1 Solver solver new Solver 2 IntVar VS VF enumeratedArray VS 4 0 4 solver 3 IntVar SU VF enumerated SU 2 3 solver 4 solver post ICF sum VS lt SU 5 solver findAllSolutions Some solutions of the problem are VS 0 0 VS 1 0 VS 2 0 VS 3 0 SU 2 VS 0 0 VS 1 0 VS 2 0 VS 3 2 SU 2 VS 0 0 VS 1 0 VS 2 0 VS 3 3 SU 3 VS 0 1 VS 1 1 VS 2 0 VS 3 0
64. Var int 1 IntVar Extract from the solver variables those which are integer ie whose KIND is set to INT retrievelntVars that is including fixed integer variables ES trieveBoolVars Extract from the solver variables those which are boolean ie whose KIND is set to BOOL that is including Solver Z1 ERO and Solver ON E Se re tVar trieveSetVars Extract from the solver variables those which are set ie whose KIND is set to SET re RealVar trieveRealVars Extract from the solver variables those which are set ie whose KIND is set to REAL O 3 1 2 Constraints Method Definition Constraint getCstrs Return the array of constraints posted in the solver getNbCstrs Return the number of constraints posted in the solver 20 Chapter 3 The solver Choco3 Documentation Release 3 3 1 3 1 3 Other Method Definition String getName Return the name of the solver IMeasures getMeasures Return a reference to the measure recorder which stores resolution statistics AbstractStrategy getStrategy Return a reference to the declared search strategy Settings getSettings Return the current Sett ings used in the solver TSolutionRecorder getSolutionRecorder Return the solution recorder E TEnvironment getEnvironment
65. _SETS x OFFSET_2 API Constraint inverse_set SetVar SETS SetVar INVERSE_SETS int OFFSET_1 int OFFSET_ ty 19 12 max The max constraint involves e either a set variable SET an integer variable MAX_ELEMENT_VALUE and a boolean NOT_EMPTY It ensures that MIN_ELEMENT_VALUE is equal to the maximum element of SET a set variable SET an array of integer WEIGHTS an integer OF FSET an integer variable MAX_ELEMENT_VALUE and a boolean NOT_EMPTY It ensures that max WEIGHTS i OF FSET i in INDEXES MAX_ELEMENT_VALUE The boolean NOT_EMPTY set to true states that INDEXES cannot be empty API Constraint max SetVar SET IntVar MAX_ELEMENT_VALUE boolean NOT_EMPTY Constraint max SetVar INDEXES int WEIGHTS int OFFSET IntVar MAX_ELEMENT_VALUE boplean NOT_ 19 13 member The member constraint involves e either an array of set variables SETS and a set variable SET It ensures that SET belongs to SETS an integer variable INTEGER and a set variable SET It ensures that INTEGER is included in SET 118 Chapter 19 Constraints over set variables EMP T Choco3 Documentation Release 3 3 1 API Constraint member SetVar SETS SetVar SET Constraint member IntVar INTEGER SetVar SET 19 14 not_member The not_member constraint in
66. an create its own strategy see Defining its own search for more details 8 5 Restarts Restart means stopping the current tree search then starting a new tree search from the root node Restarting makes sense only when coupled with randomized dynamic branching strategies ensuring that the same enumeration tree is not constructed twice The branching strategies based on the past experience of the search such as adaptive search strategies are more accurate in combination with a restart approach Unless the number of allowed restarts is limited a tree search with restarts is not complete anymore It is a good strategy though when optimizing an NP hard problem in a limited time 44 Chapier 8 Search Strategies Choco3 Documentation Release 3 3 1 Some adaptive search strategies resolutions are improved by sometimes restarting the search exploration from the root node Thus the statistics computed on the bottom of the tree search can be applied on the top of it There a two restart strategies available in SearchMonitorFactory geometrical Solver solver int base double grow ICounter counter int limit It performs a search with restarts controlled by the resolution event counter which counts events occurring during the search Parameter base indicates the maximal number of events allowed in the first search tree Once this limit is reached a restart occurs and the search continues until base grow events are
67. andomly picked 1L is the seed Then the weight of each neighbor is subtracted from W as soon as W lt 0 the corresponding neighbor is selected For instance let s consider three neighbors n1 n2 and n3 their respective weights w1 2 w2 4 w3 1 W 3 is randomly picked between 1 and 7 Then the weight of nl is subtracted W 2 1 the weight of n2 is subtracted w 4 3 W is less than O and n2 is selected 11 2 3 Defining its own neighborhoods One can define its own neighbor by extending the abstract class ANeighbor It forces to implements the following methods 56 Chapter 11 Large Neighborhood Search LNS Choco3 Documentation Release 3 3 1 Method Definition void recordSolution Action to perform on a solution typicallu storing the current variables value void fixSomeVariables ICause Fix some variables to their value in the last solution cause throws computing a partial solution ContradictionException void restrictLess Relax the number of variables fixed Called when no solution was found during a LNS run trapped into a local optimum boolean isSearchComplete Indicates whether the neighbor is complete that is can end 11 3 Restarts A generic and common way to reinforce diversification of LNS is to introduce restart during the search process This technique has proven to be very flexible and to be easily integrated within standard backtracking proc
68. ated in a solution however if WARN logging is enable a trace is shown to inform the user Choco 3 includes several ways to record solutions the recommended way is to plug a SolutionMonitor in See Search monitor for more details 7 1 Solution storage A solution is usually stored through a Solution object which maps every variable with its current value Such an object can be erased to store new solutions 7 2 Solution recording 7 2 1 Built in solution recorders A solution recorder ISolut ionRecorder is an object in charge of recording variable values in solutions There exists many built in solution recorders LastSolutionRecorder only keeps variable values of the last solution found It is the default solution recorder Furthermore it is possible to restore that solution after the search process ends This is used by default when seeking an optimal solution Al1SolutionsRecorder records all solutions that are found As this may result in a memory explosion it is not used by default BestSolutionsRecorder records all solutions but removes from the solution set each solution that is worse than the best solution value found so far This may be used to enumerate all optimal or at least best solutions of a problem ParetoSolutionsRecorder records all solutions of the pareto front of the multi objective problem 7 2 2 Custom recorder You can build you own way of manipulating and recording solutions by either implementing your own I
69. ble limits are SMF limitTime solver 5000 SMF limitFail solver 100 etc 2 3 10 Restarts Restart policies may also be applied SMF geometrical and SMF luby are available 2 3 11 Logging Logging the search is possible There are variants but the main way to do it is made through the Chatterbox printStatistics solver It prints the main statistics of the search time nodes fails etc 2 3 12 Solving Finding if a problem has a solution is made through a call to solver findSolution Looking for the next solution is made thanks to next Solution findAllSolutions enables to enumerate all solutions of a problem To optimize an objective function call findOptimalSolution Resolutions perform a Depth First Search 2 3 13 Solutions By default the last solution is restored at the end of the search Solutions can be accessed as they are discovered by using an IMonitorSolution 2 3 14 Explanations Choco natively supports explained constraints to reduce the search space and to give feedback to the user Explanations are disabled by default 2 4 Choco 3 changes 2 4 1 3 3 1 e Addition Search Monitors Defining its own constraint e Major modification 14 Chapter 2 Getting started Choco3 Documentation Release 3 3 1 Explanations Search monitor 2 4 2 3 3 0 Addition Things to know about constraints Automaton based Constraints Declaring comp
70. blem are e L 1 R 0 e L 0 R 1 22 14 addBoolOrArrayEqualTrue Add a clause to the SAT constraint which states that BOOLVARS V BOOLVARS 3 V V BOOLVARS API boolean addBoolOrArrayEqualTrue BoolVar BOOLVARS Example Solver solver new Solver SatFactory addBoolOrArrayEqualTrue BVARS solver findAllSolutions BoolVar BVARS VF boolArray BS 4 solver 22 13 addBoolNot 133 u e uv N e u N Choco3 Documentation Release 3 3 1 Some solutions of the problem are BS 0 1 BS 1 1 BS 2 1 BS 3 1 BS 0 1 BS 1 1 BS 2 0 BS 3 0 e BS O 1 BS 1 0 BS 2 0 BS 3 0 e BS O 0 BS 1 1 BS 2 0 BS 3 0 BS O 0 BS 1 0 BS 2 0 BS 3 1 22 15 addBoolOrArrayEqVar Add a clause to the SAT constraint which states that BOOLVARS V BOOLVARS V V BOOLVARS gt TARGET API boolean addBoolOrArrayEqVar BoolVar BOOLVARS BoolVar TARGET Example Solver solver new Solver BoolVar BVARS VF boolArray BS 4 solver BoolVar T VF bool T solver SatFactory addBoolOrArrayEqVar BVARS T solver findAllSolutions Some solutions of the problem are e BS O 1 BS 1 1 BS 2 1 BS 3 1 T 1 e BS O 1 BS 1 1 BS 2 0 BS 3 1 T 1 e BS O 0 BS 1 1 BS 2 0 BS 3 0 T 1 BS O 0 BS 1 0 BS 2 0 BS 3
71. cision Defining its own constraint 16 1 Structure of a Propagator 16 2 Properties cece aa a 16 3 How to make a propagator idempotent 33 35 35 36 37 38 39 39 40 41 41 41 43 44 44 45 47 59 61 61 61 63 64 65 65 67 67 68 68 17 Ibex 17 1 Installing Ibex V Elements of Choco 18 Constraints over integer variables TS absolute oca e e ee SE aae See ia a Se a 18 2 18 3 18 4 18 5 18 6 18 7 alldifferent_conditionnal alldifferent_except_0 atleast_nvalues 18 8 atmost_nvalues 18 9 bin_packing 18 10 bit_channeling 18 11 boolean_channeling 18 12 clause_channeling o A E 18 14 cost_regular 18 15 count 18 16 cumulative 18 17 diffn 18 18 distance 18 19 element 18 20 eucl_div 18 21 FALSE 18 22 global_cardinality 18 23 inverse_channeling 18 24 knapsack 18 25 lex_chain_less 18 26 lex_chain_less_eq 18 27 lex_less 18 28 lex_less_eq 18 29 MAXIMUM e o a a a a a A 18 30 mddc 18 34 multicost_tegular osa be ia A ee ee A 18 35 not_member 18 36 nvalues 18 37 path 18 38 regular 18 39 scalar 18 40 sort VSAM squares 40466 eb ke ts A dd wo we We Bee id 18 42 subcircuit 18 43 subpath 18 44 sum 18 45 table 18 46 times 18 47 tree 75 75 19 20 21 22 ISAS TRUE aii e ao e a ca hy al WOR aye hee Be Re ai a IS ASMP is a A ta nd ehh he e a RA ta ENa Constraints over set variables 19 11 alldifferent i eiae as ete ee BG HH Ae Se he BS A
72. ction indicate alternative instructions Brackets instruction indicate an optional instruction If the search terminates the message Search complete appears on the first line followed with either the the number of solutions found or the message No solution Maximize resp Minimize indicates the best known value before exiting of the objective value using a ResolutionPolicy MAXIMIZE resp ResolutionPolicy MINIMIZE policy Curly braces value indicate search statistics 0 number of solutions found p objective value in maximization objective value in minimization building time in second from new Solver to findSolution or equivalent initialisation time in second before initial propagation initial propagation time in second resolution time in second from new Solver till now number of decision created that is nodes in the binary tree search number of backtracks achieved SO eA ON ee es number of failures that occurred number of restarts operated n n maximum depth reached in the binary tree search hn N estimation of the memory used ne 1s number of variables in the model 14 number of constraints in the model If the resolution process reached a limit before ending naturally the title of the message is set to Incomplete search Limit reached The body of the message remains the same The message is formatted thanks to the IMeasur
73. d instead 5 4 SAT constraints A SAT solver is embedded in Choco It is not designed to be accessed directly The SAT solver is internally managed as a constraint and a propagator that s why it is referred as SAT constraint in the following Important The SAT solver is directly inspired by MiniSat EenSorensson03 However it only propagates clauses no learning or search is implemented On a call to any methods of solver constraints SatFactory the SAT constraint and propagator is created and automatically posted to the solver 5 4 1 How to add clauses Clauses can be added with calls to the solver constraints SatFactory On one boolean variable addTrue addFalse On two boolean variables addBoolEq addBoolLe addBoolLt addBoolINot Reification on two boolean variables addBoollsEqVar addBoollsLeVar addBoollsLtVar addBoolIsNeqVar addBoolOrEqVar addBoolXorEqVar ad dBoolAndEqVar On undefined number of boolean variables addBoolOrArrayEqualTrue addAtMostNMinusOne addAtMostOne addBoolAndArrayEqualFalse addBoolAn dArrayEqVar addBoolOrArrayEqVar addClauses addMaxBoolArrayLessEqVar addSumBoolArrayGreaterEgqVar addSumBoolArrayLessEqVar 5 4 2 Declaring complex clauses There is a convenient way to declare complex clauses by calling addClauses The method takes a LogOp and an instance of Solver as input extracts the underlying clauses and add them to the SatFactory A LogOp is an implementation of ILogical
74. done and so on After each restart the limit number of events is increased by the geometric factor grow limit states the maximum number of restarts and luby Solver solver int base int grow ICounter counter int limit The Luby s restart policy is an alternative to the geometric restart policy It performs a search with restarts controlled by the number of resolution events counted by counter The maximum number of events allowed at a given restart iteration is given by base multiplied by the Las Vegas coefficient at this iteration The sequence of these coefficients is defined recursively on its prefix subsequences starting from the first prefix 1 the k 1 h prefix is the kth prefix repeated grow times and immediately followed by coefficient grow e the first coefficients for grow 2 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 1 e the first coefficients for grow 3 1 1 1 3 1 1 1 3 1 1 1 3 9 8 6 Limiting the resolution 8 6 1 Built in search limits The exploration of the search tree can be limited in various ways Some usual limits are provided in SearchMonitorFactory or SMF for short e limitTime stops the search when the given time limit has been reached This is the most common limit as many applications have a limited available runtime Note The potential search interruption occurs at the end of a propagation i e it will not interrupt a propagation algorithm so the overall runtime of
75. e Defines a limit over the run time defined in a separated thread When the limit is reached the resolution is stopped The limit can be either defined in millisecond or using a String which states the duration like WWd XXh YYm ZZs for example 1d2h3m4 5s one day two hours three minutes four seconds and 500 milliseconds lt p gt 2h30m two hours and 30 minutes lt p gt 30 5s 30 seconds and 500 ms lt p gt 180s three minutes Factory org chocosolver solver search loop monitors SearchMonitorFactory API void limitThreadTime Solver solver long limit void limitThreadTime Solver solver String duration convertInMilliseconds 156 Chapter 27 Search Monitors Choco3 Documentation Release 3 3 1 27 7 limitFail Defines a limit over the number of fails allowed during the resolution When the limit is reached the resolution is stopped Factory org chocosolver solver search loop monitors SearchMonitorFactory API void limitFail Solver solver long limit 27 8 limitBacktrack Defines a limit over the number of backtracks allowed during the resolution When the limit is reached the resolution is stopped Factory org chocosolver solver search loop monitors SearchMonitorFactory API void limitBacktrack Solver solver long limit 27 9 restartAfterEachSolution Force the resolution to restart at root node after each solution
76. e IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy lexico_UB IntVar VARS 26 9 minDom_LB A built in strategy which chooses the first non instantiated variable with the smallest domain size and assigns it to its lower bound Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy minDom_LB IntVar VARS 26 10 minDom_MidValue A built in strategy which chooses the first non instantiated variable with the smallest domain size and assigns it to the value closest to its middle of its domain Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy minDom_MidValue IntVar VARS 26 7 lexico_Split 149 Choco3 Documentation Release 3 3 1 26 11 maxDom_Split A built in strategy which chooses the first non instantiated variable with largest domain size and removes the second half of its domain Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy maxDom_Split IntVar VARS 26 12 minDom_UB A built in strategy which chooses the first non instantiated variable with the smallest domain size and assigns it to its upper bound Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy minDom_UB IntVar VARS 26 13 maxReg_LB
77. e 16th Eureopean Conference on Artificial Intelligence ECAI 2004 including Prestigious Applicants of Intelligent Systems PAIS 2004 Valencia Spain August 22 27 2004 146 150 2004 CB04 Hadrien Cambazard and Eric Bourreau Conception d une contrainte globale de chemin In Actes des 10e Journ es nationales sur la r solution pratique de problemes NP complets JNPC 04 107 121 Angers France France 2004 URL http hal archives ouvertes fr hal 00448531 CB02 Mats Carlsson and Nicolas Beldiceanu Arc consistency for a chain of lexicographic ordering constraints Technical Report 2002 CL97 Yves Caseau and Francois Laburthe Solving Small TSPs with Constraints In Lee Naish editor Proceedings of the 14th International Conference on Logic Programming ICLP 1997 316 330 MIT Press 1997 CY08 Kenil C K Cheng and Roland H C Yap Maintaining generalized arc consistency on ad hoc r ary constraints In Principles and Practice of Constraint Programming 14th International Conference CP 2008 Sydney Aus tralia September 14 18 2008 Proceedings 509 523 2008 URL http dx doi org 10 1007 978 3 540 85958 1_34 doi 10 1007 978 3 540 85958 1_34 DPR06 Sophie Demassey Gilles Pesant and Louis Martin Rousseau A cost regular based hybrid column generation approach Constraints 11 4 315 333 2006 URL http dx doi org 10 1007 s10601 006 9003 7 doi 10 1007 s 1060 1 006 9003 7 EenSorensson03 Niklas E n and N
78. e lack of solution 6 1 Satisfaction problems 6 1 1 Finding a solution A call to solver findSolution launches a resolution which stops on the first solution found if any 1 Create a Solver Solver solver new Solver my first problem 2 Create variables through the variable factory IntVar x VariableFactory bounded X 0 5 solver IntVar y VariableFactory bounded Y 0 5 solver 3 Create and post constraints by using constraint factories solver post IntConstraintFactory arithm x y lt 5 4 Define the search strategy solver set IntStrategyFactory lexico_LB x y 5 Launch the resolution process solver findSolution 6 Print search statistics Chatterbox printStatistics solver 35 Choco3 Documentation Release 3 3 1 If a solution has been found the resolution process stops on that solution thus each variable is instantiated to a value and the method returns t rue If the method returns false two cases must be considered e A limit has been reached There may be a solution but the solver has not been able to find it in the given limit or there is no solution but the solver has not been able to prove it i e to close to search tree in the given limit The resolution process stops in no particular place in the search tree and the resolution can be run again e No limit has been declared The problem has no solution the complete explorat
79. eRecorder which is a search monitor On a call to Chatterbox showSolutions solver on each solution the following message will be printed 0 Solutions Maximize 1 Minimize 2 Resolution 6 s 7 Nodes 8 Backtracks 9 Fails 10 Restarts followed by one line exposing the value of each decision variables those involved in the search strategy On acall to Chatterbox showDecisions solver on each node of the search tree a message will be printed indicating which decision is applied The message is prefixed by as many as nodes in the current branch of the search tree A decision is prefixed with R and a refutation is prefixed by L 48 Chapter 9 Resolution statistics Choco3 Documentation Release 3 3 1 Warning Chatterbox printDecisions Solver solver prints the tree search during the resolu tion Printing the decisions slows down the search process 49 Choco3 Documentation Release 3 3 1 50 Chapter 9 Resolution statistics Part IV Advanced usage 51 CHAPTER 10 Settings A Settings object is attached to each Solver It declares default behavior for various purposes from general purpose such as the welcome message modelling purpose such as enabling views or solving purpose such as the search binder The API is public String getWelcomeMessage Return the welcome message public Idem getIdempotencyStrategy Define
80. edures 11 4 Walking A complementary technique that appear to be efficient in practice is named Walking and consists in accepting equiv alent intermediate solutions in a search iteration instead of requiring a strictly better one This can be achieved by defining an Object iveManager like this solver set new ObjectiveManager objective ResolutionPolicy MAXIMIZE false Where the last parameter named strict must be set to false to accept equivalent intermediate solutions Other optimization policies may be encoded by using either search monitors or a custom Object iveManager 2 Laurent Perron Fast restart policies and large neighborhood search In Francesca Rossi editor Principles and Practice of Constraint Programming at CP 2003 volume 2833 of Lecture Notes in Computer Science Springer Berlin Heidelberg 2003 11 3 Restarts 57 Choco3 Documentation Release 3 3 1 58 Chapter 11 Large Neighborhood Search LNS CHAPTER 12 Multi thread resolution Choco 3 provides a simple way to use several thread to treat a problem This is achieved by declaring a MasterSolver to drive the search The main idea of that driver is to solve the same problem with various search strategies and to share few possible information The first step is to declare a model as usual by creating a solver adding variables and constraints One can declare a naive search strategy to point out the decision variables It
81. ee and intensification i e exploring them exhaustively should be well distributed 11 2 1 Generic neighbors One drawback of LNS is that the relaxation process is quite often problem dependent Some works have been dedicated to the selection of variables to relax through general concept not related to the class of the problem treated 5 24 However in conjunction with CP only one generic approach namely Propagation Guided LNS 24 has been shown to be very competitive with dedicated ones on a variation of the Car Sequencing Problem Nevertheless such generic approaches have been evaluated on a single class of problem and need to be thoroughly parametrized at the instance level which may be a tedious task to do It must in a way automatically detect the problem structure in order to be efficient 11 2 2 Combining neighborhoods There are two ways to combine neighbors Sequential Declare an instance of SequenceNeighborhood nl n2 nm Each neighbor ni is applied in a se quence until one of them leads to a solution At step k the k mod m neighbor is selected The sequence stops if at least one of the neighbor is complete Adaptive Declare an instance of AdaptiveNeighborhood 1L nl n2 nm At the beginning a weight of 1 at assigned to each neighbor ni Then if a neighbor leads to solution its weight w is increased by 1 Any time a partial solution has to be computed a value W between 1 and w1 w2 Wn is r
82. ee O we ee Be te ae See a 26 20 1Mpact 3 Kae bbe Gwe Ree EO eda ee bade ewe ea eed ead A 20 21 WastCommiety a i 2k ws bine al Bae bee Se ok i Seth ah debs ls Reggae kod lada oda 20 22 senerateAn Test ewe be eee EER Ce a READ ee ee A Search Monitors 2d SCOMEMICAN 2 44 ZR E eee eae See eee Bhi eee ee ES eR e Ei G 272 MODY so eo ees YR RR ES EE E OE Ae SOS A ae ee ee a ee 21 3 MMmiNode i704 6 2 eed EGE E RMSE REESE OH BS PARDEE SS Se HSS 274 MimMMitSOMMOM e a Bow a add AEA E is Ae ek Gow ee ee 141 141 141 141 142 142 143 143 143 143 144 144 145 145 145 145 146 147 147 147 148 148 148 148 149 149 149 149 150 150 150 150 151 151 151 151 152 152 152 153 155 155 155 155 156 21a A EIA 156 2756 Im TbreadlMe oir a we Bh eed e di 156 A A a a aai ae ae aa a aa ai i ae a a e ei te es a a ete dol ts leper cde 157 2728 MMIUBACkTACK mags sageu see eR la a a a ee 157 27 9 restartAtterEachSOlUMIO 46 2 e A e A RD Oe ia da S 157 21 10 nogeodRecordingOnSolition eel ed Ree ESR ad SE eee eG 157 21 11 nogoodRecordineFromRestants 24 4286 i42 0 4840 e604 Fe bee baw Be bbb aa Ss 157 VI Extensions of Choco 159 28 IO extensions 161 ZBI SCMOCO PALSerS fas Sx A gine Se BRE Ghote S BAe She ae be A te be aie S 161 2 2 COCO BUE tios Ge espa Bea ee a ee Boe Gaeta doe ee Ee aoe amp 4 161 20 5 CHOCO CPVIZ lt 42d bh dba e oe RRA De ee he EAS Be 161 29 Modeling extensions 163 e
83. effs R solver findAllSolutions Some solutions of the problem are e CS 0 1 CS 1 1 CS 2 1 CS 3 1 R 10 e CS 0 1 CS 1 2 CS 2 3 CS 3 1 R 18 e CS 0 1 CS 1 4 CS 2 2 CS 3 1 R 19 e CS 0 1 CS 1 2 CS 2 1 CS 3 3 R 20 18 40 sort The sort constraint involves two arrays of integer variables VARS and SORTEDVARS It ensures that the variables of SORTEDVARS correspond to the variables of VARS according to a permutation Moreover the variable of SORTED VARS are sorted in increasing order 106 Chapter 18 Constraints over integer variables u e u N Choco3 Documentation Release 3 3 1 See also sort in the Global Constraint Catalog Implementation based on MT00 API Constraint sort IntVar VARS IntVar SORTEDVARS Example Solver solver new Solver IntVar X VF enumeratedArray X 3 0 2 solver IntVar Y VF enumeratedArray Y 3 0 2 solver solver post ICF sort X Y solver findAllSolutions Some solutions of the problem are e X 0 0 X 1 0 X 2 0 Y 0 0 Y 1 0 Y 2 0 e X 0 1 X 1 0 X 2 2 Y 0 0 Y 1 1 Y 2 2 e X 0 2 X 1 1 X 2 0 Y 0 0 Y 1 1 Y 2 2 X 0 2 X 1 1 X 2 2 Y 0 1 Y 1 2 Y 2 2 18 41 square The square constraint involves two variables VAR and VAR2 It ensures that VAR VAR2
84. eger OFFSET It ensures that x SETS y OFFSET y SETS x OFFSET API Constraint symmetric SetVar S ETS int OFFSET 19 23 union The union constraint involves e an array of set variables SETS and e a set variable UNION It ensures that SET_UNION is equal to the union if the sets in SET_VARS The API is 19 20 subsetEq 121 Choco3 Documentation Release 3 3 1 Constraint union SetVar S ETS SetVar UNION 122 Chapter 19 Constraints over set variables CHAPTER 20 Constraints over real variables Real constraints are managed externally with bex Due to the limited number of declaration possibilities there is no factory for real constraints Indeed posting a RealConst raint is enough The available constructors are RealConstraint String name String functions int option RealVar rvars RealConstraint String name String functions RealVar rvars RealConstraint String functions RealVar rvars e name enables to set a name to the constraint e functions is a String which defines the list of functions to hold separated with semi colon A function is a declared using the following format e the i tag defines a variable where i is an explicit index the array of variables rvars e one or more operators lt gt lt gt exp In max min abs cos sin
85. elease 3 3 1 1 Solver solver new Solver 2 IntVar X VF enumeratedArray X 3 1 1 solver 3 IntVar Y VF enumeratedArray Y 3 1 2 solver 4 IntVar Z VF enumeratedArray Z 3 0 2 solver 5 solver post ICF lex_chain_less X Y 2 6 solver findAllSolutions Some solutions of the problems are X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 1 Z 1 1 Z 2 2 e X 0 0 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 1 Z 1 2 Z 2 0 e X 0 1 X 1 0 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 1 Z 1 2 Z 2 0 X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 2 Z 1 2 Z 2 1 18 26 lex_chain_less_eq The lex_chain_less_eq constraint involves a matrix of integer variables VARS It ensures that for each pair of consec utive arrays VARS i and VARS i 1 VARS i is lexicographically strictly less or equal than VARS i 1 See also lex_chain_less_eq in the Global Constraint Catalog Implementation based on CB021 API Constraint lex_chain_less_eq IntVar VARS Example 1 Solver solver new Solver 2 IntVar X VF enumeratedArray X 3 1 1 solver 3 IntVar Y VF enumeratedArray Y 3 1 2 solver 4 IntVar Z VF enumeratedArray Z 3 0 2 solver 5 solver post ICF lex_chain_less_eq X Y Z 6 solver findAllSolutions Some solut
86. em is proven to have no solution and search stops Factory solver explanations ExplanationFactory API CBJ plugin Solver solver boolean nogoodsOn boolean userFeedbackOn e solver the solver to explain e nogoodsOn set to true to extract nogood from each conflict Extracting nogoods slows down the overall resolution but can reduce the search space 13 3 Explanations for the system 63 Choco3 Documentation Release 3 3 1 e userFeedbackOn set to true to store the very last explanation of the search recommended value false 13 3 2 Dynamic backtracking This strategy Dynamic backtracking DBT corrects a lack of deduction of Conflict based backjumping On a failure explanations are retrieved From all left branch decisions explaining the failure the last taken return decision is stored to jump back to it Decisions from the current one to the return decision excluded are maintained only the return decision is refuted and the search goes on If the explanation is made of no left branch decision the problem is proven to have no solution and search stops Factory solver explanations ExplanationFactory API DBT plugin Solver solver boolean nogoodsOn boolean userFeedbackOn e solver the solver to explain e nogoodsOn set to true to extract nogood from each conflict Extracting nogoods slows down the overall resolution but can reduce the search space e userFeedbackOn
87. en decisions and filtering algorithms will remove integers from S_E and add some others to S_K A set variable is instantiated if and only if S_E S_K A set variable can be created as follows z initial domain int z_envelope new int 2 1 3 5 7 12 int z_kernel new int 2 z VariableFactory set z z_envelope z_kernel solver 4 6 Real variable Real variables have a specific status in Choco 3 Indeed continuous variables and constraints are managed with Ibex solver A real variable is declared with two doubles which defined its bound RealVar x VariableFactory real y 0 2d 1 0e8d 0 001d solver Or a real variable can be declared on the basis of on integer variable IntVar ivar VariableFactory bounded i 0 4 solver RealVar x VariableFactory real ivar 0 01d 26 Chapter 4 Declaring variables CHAPTER 5 Constraints and propagators 5 1 Principle A constraint is a logic formula that defines allowed combinations of values for its variables that is restrictions over variables that must be respected in order to get a feasible solution A constraint is equipped with a set of filtering algorithm s named propagator s A propagator removes from the domains of the targeted variables values that cannot correspond to a valid combination of values A solution of a problem is an assignment of all its variables simultaneously verifying al
88. entire search space has been explored The process is the following anytime a solution is found the value of the objective variable is stored and a cut is posted The cut is an additional constraint which states that the next solution must be strictly better than the current one ie in minimization strictly smaller 6 2 2 Finding all optimal solutions There could be more than one optimal solutions To find them all one can call findAllOptimalSolutions ResolutionPolicy IntVar boolean The two first arguments defines the optimisation policy and the variable to optimize The last argument states the way the solutions are computed Set to t rue the resolution will be achieved in two steps first finding and proving an optimal solution then enumerating all solutions of optimal cost Set to false the posted cuts are soft When an equivalent solution is found it is stored and the resolution goes on When a strictly better solution is found previous solutions are removed Setting the boolean to false allow finding non optimal intermediary solutions which may be time consuming 6 3 Multi objective optimization problems 6 3 1 Finding the pareto front It is possible to solve a multi objective optimization problems with Choco 3 using solver findParetoFront ResolutionPolicy policy IntVar objectives The first argument define the resolution policy which can be Resolution MINIMIZ ResolutionPolicy MAXIMIZE Then the second argument define
89. er new Solver BoolVar BVARS VF boolArray BS 4 SatFactory addAtMostNMinusOne BVARS solver findAllSolutions Some solutions of the problem are e BS O 1 BS 1 1 BS 2 1 BS 3 0 e BS O 1 BS 1 0 BS 2 1 BS 3 0 e BS O 0 BS 1 1 BS 2 1 BS 3 1 BS O 0 BS 1 0 BS 2 0 BS 3 1 BS O 0 BS 1 0 BS 2 0 BS 3 0 22 2 addAtMostOne Add a clause to the SAT constraint whic states that BOOLVARS BOOLVARS BOOLVARS lt 1 API boolean addAtMostOne BoolVar BOOLVARS Example 127 Ro ou N e u N Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar BVARS VF boolArray BS 4 solver SatFactory addAtMostOne BVARS solver findAllSolutions The solutions of the problem are e BS O 1 BS 1 0 BS 2 0 BS 3 0 e BS O 0 BS 1 1 BS 2 0 BS 3 0 BS O 0 BS 1 0 BS 2 1 BS 3 0 e BS O 0 BS 1 0 BS 2 0 BS 3 1 BS O 0 BS 1 0 BS 2 0 BS 3 0 22 3 addBoolAndArrayEqualFalse Add a clause to the SAT constraint whic states that not BOOLV ARS A BOOLVARS BOOLVARS API boolean addBoolAndArrayEqualFalse Bool Var BOOLVARS Example Solver solver new Solver BoolVar BVARS VF boolArray BS 4 solver SatFactory addBoolAndArrayEqualFalse BVARS solver findAllSol
90. est new IntDomainMin DecisionOperator int_eq Let s consider the following array of variables as input X Y Z where X 0 3 Y 0 4 and Z 1 4 Applying the first strategy declared will return X Applying the second one will return Z X and Z are batter than Y but equivalent compared to FirstFail but Z is better than X compared to Largest 15 2 Selecting the value The value to be selected must belong to the variable domain For Int Var the interface Int ValueSelector is required It imposes one method int selectValue IntVar var Return the value to constrain var with Important A value selector must consider the type of domain of the selected variable Indeed a value selector does not store the previous tries unkike an iterator and it may happen that for bounded variable the refutation of a decision has no effect and a value is selected twice or more For example consider IntDomainMiddle and a bounded variable 15 3 Making a decision A decision is made of a variable an decision operator and a value The decision operator should be selected in DecisionOperator among int_eg For IntVar represents an instantiation X 3 The refutation of the decision will be a value removal 68 Chapter 15 Defining its own search strategy Choco3 Documentation Release 3 3 1 int_neq For IntVar represents a value removal X 4 3 The refutation of the decision will be an instantiation int_split
91. et variables SETS It ensures that all sets from SETS are disjoint Note that there can be multiple empty sets API Constraint all_disjoint SetVar SETS 19 3 all_equal The all_equal constraint involves an array of set variables SETS It ensures that sets in SETS are all equal API Constraint all_equal SetVar SETS 19 4 bool_channel The bool_channel constraint involves e an array of boolean variables BOOLEANS e a set variable SET and 115 Choco3 Documentation Release 3 3 1 e an integer OFFSET It channels BOOLEANS and SET such that i SET BOOLEANS i OFFSET 1 API Constraint bool_channel BoolVar BOOLEANS SetVar SET int OFFSET 19 5 cardinality The cardinality constraint involves e a set variable SET and e an integer variable CARD It ensures that SET_VAR CARD The API is Constraint cardinality SetVar SET IntVar CARD 19 6 disjoint The disjoint constraint involves two set variables SET_I and SET_2 It ensures that SET_ and SET_2 are disjoint that is they cannot contain the same element Note that they can be both empty API Constraint disjoint SetVar SET_1 SetVar SET_2 19 7 element The element constraint involves e an integer variable INDEX e and array of set variables SETS e an integer OFFSET and e a set variable SET It ensures that SETS INDEX OFFSET SET
92. f a modi fication of at least one of its variables without knowing specifically which one s and what modifications occurred Important The array of variables given in parameter of a Propagator constructor is not cloned but referenced That is if a permutation occurs in the array of variables all propagators referencing the array will be incorrect ESat isEntailed This method is mandatory for reification It checks whether the propagator will be always satisfied ESat TRUE never satisfied ESat FALSE or undefined ESat UNDEFINED according to the cur rent state of its domain variables and or its internal structure By default it should consider the case where all variables are instantiated For instance A 4 B will always be satisfied when A 0 1 2 and B 4 5 For instance A B will never be satisfied when A 0 1 2 and B 4 5 For instance entailment of A 4 B cannot be defined when A 0 1 2 and B 1 2 3 This method is also called to check solutions when assertions are enabled i e when the ea JVM option is used void propagate int evtmask This method applies the global filtering algorithm of the propagator that is from scratch It is called once during initial propagation and then on a call to forcePropagate EventType There are two available types of event this method can receive Event Type FULL _PROPAGATION and Event Type CUSTOM _PROPAGATION The
93. gt 5 ges Sook he Pace he ee Ba BH Rake pp ae el he Gee AS S 163 29 2 ACOOCOSBEOS E io he ee AE ee ee ee EGA Woe eee Eee ee hee es 163 29 3 CMOCO ERP PAT ie fe hee de 8s bp ae Be Revd BGs a yk gOS A we se See Bob Ge Eden he He ee Swe 163 VII References 165 Bibliography 167 vi Choco3 Documentation Release 3 3 1 Warning This is a work in progress documentation If you have any questions suggestions or requests please send an email to choco Omines nantes fr Contents 1 Choco3 Documentation Release 3 3 1 2 Contents Part I Preliminaries CHAPTER 1 Main concepts 1 1 What is Constraint Programming Such a paradigm takes its features from various domains Operational Research Artificial Intelligence etc Constraint programming is now part of the portfolio of global solutions for processing real combinatorial problems Actually this technique provides tools to deal with a wide range of combinatorial problems These tools are designed to allow non specialists to address strategic as well as operational problems which include problems in planning scheduling logistics financial analysis or bio informatics Constraint programming differs from other methods of Operational Research by how it is implemented Usually the algorithms must be adapted to the specifications of the problem addressed This is not the case in Constraint Programming where the problem addressed is described using the tools
94. h its output domains returns its output domains In that case it has reached a fix point 2 monotonic calling a propagator with two input domains A and B for which A C B returns two output domains A and B for which A CB 72 Chapter 16 Defining its own constraint Choco3 Documentation Release 3 3 1 long size do size 0 for IntVar v vars sizet v getDomSize really update domain variables here for IntVar v vars size v getDomSize while size gt 0 Important Domain variable modifier returns a boolean valued to t rue if the domain variable has been modified Important In the case of SetVar or GraphVar replace getDomSize by getEnvSize getKerSize The decomposed option Split the original propagator into many propagators so that the fix point is performed through the propa gation engine For instance a channeling propagator A B can be decomposed into two propagators A Band B A The propagators can but does not have to react on fine events The azy option To be avoided has much as possible simply post the propagator twice Thus the fix point is performed through the propagation engine 16 3 How to make a propagator idempotent 73 Choco3 Documentation Release 3 3 1 74 Chapter 16 Defining its own constraint CHAPTER 17 Ibex IBEX is a C library for constraint processing over real numbers It provides
95. hese operations stem from both constraint propagation and search The benefits of graph variables stem from modeling convenience and performance This extension has documentation You will find it at https github com chocoteam choco graph 29 2 choco geost choco geost is a Choco 3 module which provides the GEOST global constraint This constraint is designed for ge ometrical and packing applications see http www emn fr z info sdemasse gccat Cgeost html You will find it at https github com chocoteam choco geost 29 3 choco exppar choco exppar is a Choco 3 module which provides an expression parser This enables to simplify the modeling step You will find it at https github com chocoteam choco exppar 163 Choco3 Documentation Release 3 3 1 164 Chapter 29 Modeling extensions Part VII References 165 Bibliography BessiereHH 05 Christian Bessi re Emmanuel Hebrard Brahim Hnich Zeynep Kiziltan and Toby Walsh Among common and disjoint constraints In Recent Advances in Constraints Joint ERCIM CoLogNET International Workshop on Constraint Solving and Constraint Logic Programming CSCLP 2005 Uppsala Sweden June 20 22 2005 Revised Selected and Invited Papers 29 43 2005 URL http dx doi org 10 1007 11754602_3 doi 10 1007 11754602_3 BHLS04 Fr d ric Boussemart Fred Hemery Christophe Lecoutre and Lakhdar Sais Boosting systematic search by weighting constraints In Proceedings of th
96. how to react when a propagator is not ensured to be idempotent public boolean enableViews Set to true to allow the creation of views in the VariableFactory Creates new variables with channeling constraints otherwise public int getMaxDomSizeForEnumerated Define the maximum domain size threshold to force inte ger variable to be enumerated instead of bounded while calling VariableFactory integer String int int Solver public boolean enableTableSubstitution Set to true to replace intension constraints by extension constraints public int getMaxTupleSizeForSubstitution Define the maximum domain size threshold to re place intension constraints by extension constraints Only checked when enableTableSubstitution is set to true public boolean plugExplanationIn Set to true to plug explanation engine in public boolean enablePropagatorInExplanation Set to true to add propagators in explanations public double getMCRPrecision Define the rounding precision for multicost_regular MUST BE lt 13 as java messes up the precisions starting from 10E 12 34 0 0 05 1 70000000000005 public double getMCRDecimalPrecision Defines the smallest used double for multicost_regular public short getFineEventPriority Defines for fine events for each priority the queue in which a propagator of such a priority should be scheduled in public short getCoarseEventPriority Defines for coarse events for each priority the q
97. ie aw PEG a See Adee a da a DIO ASPENS ce aere A eh bw we E PR ROR a ey be we ee e a a as 23 4 reverse Split ve Ge hehe Seles a E eb baie Se dei s bees Se eRe baa Built in strategies E ae hed ao ee es ee We pth day gs Be WO BO es eke Bo eee aay Mo ae R 26 2 TOME MrS e dba eee eh ee Bek ed eee Boe we eee eee BEE EEE AAS 26 3 force maxDelta first 2 siy aoa 6024 0 oY bbe D ESAS ER hE RS 26 4 force minDelta TSE zorras A Re He Re SOR ee OR eee de Ae eX 26 5 l xico LB i 2024 46 244A EHD ee BA Re PEAS EHR EYE a EER Ee Soke we aS 20 01 lexico Negd LB bd baie ed ak dom e ee Boe ia a tdo nee ed 26 7 lexico Splite s 2444 2442000028 abe ee 2h ee EG Ba Eee be kee 20 9 Mexico UB ea Be end oh di dm Je Sees toe do dl ds oe Bethy eer Hobe HD Je lee ey te de Ak a ay So 20 9 minDom LB 0 aia a ae Ee ee ee ee OR eR ee a eR Y 26 10 minDom_MidValue ee 26 11 maxDOMS Pl o io oe eb wa Re PAS eae Rae wa a sb A 26 12 MINDOM UB sado he ance eve St see Rs hp eee ak A ee Seah ch ace ie Be apc ae od lada Rote h 26 13 maxR e LB sos ewe e eA ER BAER a E 26 14 random bound z 2 s saci a Bede POA we ee eRe ee ee A Be ea be Rae eS 26 1 gt fandomnvale sos pi gaye dr ed ack a dom amp Bb Boe Sag te ag id add bE Sree ed 26 16 remove _fifst 224 54 4 4h See RS Be LR EAL DE a LEGA A RAS DOA SCQUCMICER 2 5 03 45 ea HRN eee toe a A GOR eee eS Se ere a ee Be Hh ee Re es 26 18 domOVEerW DES reip e A Ae EG BR a SG BAUS Ge ewe Bae A QO VO VACUVALY asn a ese ese B
98. iklas S rensson An extensible sat solver In Theory and Applications of Satisfi ability Testing 6th International Conference SAT 2003 Santa Margherita Ligure Italy May 5 8 2003 Selected Revised Papers 502 518 2003 URL http dx doi org 10 1007 978 3 540 24605 3_37 doi 10 1007 978 3 540 24605 3_37 Fag14 Jean Guillaume Fages On the use of graphs within constraint programming PhD thesis Ecole des Mines de Nantes 2014 URL http www a4cp org sites default files jean guillaume_fages_ on_the_use_of_graphs_within_constraint programming pdf FLapegue14 Jean Guillaume Fages and Tanguy Lap gue Filtering atmostnvalue with difference con straints application to the shift minimisation personnel task scheduling problem Artificial Intelli 167 Choco3 Documentation Release 3 3 1 gence 212 0 116 133 2014 URL http www sciencedirect com science article pii S00043702 14000423 doi http dx doi org 10 1016 j artint 2014 04 001 FL12 Jean Guillaume Fages and Xavier Lorca Improving the asymmetric tsp by considering graph structure CoRR 2012 URL http arxiv org abs 1206 3437 FLP14 Jean Guillaume Fages Xavier Lorca and Thierry Petit Self decomposable global constraints In Proceed ings of the 2014 Conference on ECAI 2014 21st European Conference on Artificial Intelligence IOS Press 2014 FL11 Jean Guillaume Fages and Xavier Lorca Revisiting the tree constraint In Principles and Practice of Co
99. ion algorithm which relies on the relation it defines over variables Warning Even if a naive and weak explanation algorithm could be provided by all constraints we made the choice to throw an SolverException whenever a propagator does not defined its own explanation algorithm This is restrictive but almost all non global constraints support explanation which enables reformulation The missing explanation schemas will be integrated all needs long 62 Chapter 13 Explanations Choco3 Documentation Release 3 3 1 For instance here is the algorithm of PropGreaterOrEqualX_YC x gt y c x and y are integer variables c is a constant public boolean why RuleStore ruleStore IntVar var IEventType evt int value boolean newrules ruleStore addPropagatorActivationRule this if var equals x newrules ruleStore addLowerBoundRule y else if var equals y newrules ruleStore addUpperBoundRule x else newrules super why ruleStore var evt value return newrules The first lines indicates that the deduction is due to the application of the propagator 1 2 maybe through reification Then depending on the variable touched by the deduction either the lower bound of y 1 4 or the upper bound of x 1 6 explains the deduction Indeed such a propagator only updates lower bound of y based on the upper bound of x and vice versa Let consider that the deduction in
100. ion of the search tree proved it To ensure the problem has no solution one may call solver hasReachedLimit It returns true if a limit has been reached false otherwise 6 1 2 Enumerating solutions Once the resolution has been started by a call to solver findSolution and if the problem is feasible the resolution can be resumed using solver nextSolution from the last solution found The method returns true if a new solution is found false otherwise a call to solver hasReachedLimit must confirm the lack of new solution If a solution has been found alike solver findSolution the resolution stops on this solution each variable is instantiated and the resolution can be resumed again until there is no more new solution One may enumerate all solution like this if solver findSolution do do something e g print out variables value while solver nextSolution solver findSolution and solver nextSolution are the only ways to resume a resolution process which has already began Tip On a solution one can get the value assigned to each variable by calling ivar getValue instantiation value of an IntVar return a int svar getValues instantiation values of a SerVar return a int rvar getLB lower bound of a RealVar return a double rvar getUB upper bound of a RealVar return a double An alternative is to call solver findAllSolutions
101. ions of the problems are X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 1 Z 1 1 Z 2 1 X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 1 Z 1 1 Z 2 1 X 0 0 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 Z 0 2 Z 1 1 Z 2 2 e X 0 1 X 1 1 X 2 0 Y 0 1 Y 1 1 Y 2 2 Z 0 2 Z 1 2 Z 2 2 18 27 lex_less The lex_less constraint involves two arrays of integer variables VARS and VARS2 It ensures that VARS is lexico graphically strictly less than VARS2 18 26 lex_chain_less eq 97 Choco3 Documentation Release 3 3 1 See also lex_less in the Global Constraint Catalog Implementation based on FHK 02 API Constraint lex_less IntVar VARS1 IntVar VARS2 Example Solver solver new Solver IntVar X VF enumeratedArray X 3 1 1 solver IntVar Y VF enumeratedArray Y 3 1 2 solver solver post ICF lex_less X Y solver findAllSolutions u e Ww No Some solutions of the problems are X 0 1 X 1 1 X 2 1 Y 0 1 Y 1 1 Y 2 1 e X 0 1 X 1 0 X 2 0 Y 0 1 Y 1 2 Y 2 1 e X 0 1 X 1 0 X 2 1 Y 0 2 Y 1 1 Y 2 1 X 0 1 X 1 1 X 2 0 Y 0 2 Y 1 2 Y 2 2 18 28 lex_less eq The Jex_less_eq constraint involves two arrays of integer variables VARSI and VARS2 It ensures that
102. is optional but highly recommended Then the problem declared in the solver is duplicated into n additional solvers The search strategies are then configured and each solver 1s run into a single thread On satisfaction problem the first solver who finds a solution advises the others On optimisation problem the best value found so far is shared among all the solvers The expected ways to solve a problem using MasterSolver is Solver solver new Solver declare the variables and constraints and an optional search strategy Ul aera Then create the master solver MasterSolver ms new MasterSolver duplicate the solver into 4 solvers 1 3 ms populate solver 3 configure the search strategies optional but recommended ms declareSettings settingsl settings2 settings3 Finally solve the problem ms findSolution The API of MasterSolver is deliberately kept reduced If a specific configuration of a solver needs to be done one has to do it by himself void populate Solver model int n Duplicate a given solver into n copies It populates the internal array Solver with n 1 solvers void declare Solver solvers An alternative to populate Solver model int n where the array of solvers is given The first solver in the array needs to be the original one required for optimization problem Solver getSolvers Return the array of solvers to drive 59 Choco3 Docume
103. l not be taken into account during the resolution process it may not be satisfied in all solutions 5 2 Posting constraints 29 Choco3 Documentation Release 3 3 1 Method Definition void Post permanently a constraint in the constraint network defined by the solver The post Constraint constraint is not propagated on posting but is added to the propagation engine Cc void Post permanently the constraints in the constraint network defined by the solver post Constraint cs void Post a constraint temporary in the constraint network The constraint will active on the postTemp Const rat wtrrent sub tree and be removed upon backtrack c void Remove permanently the constraint from the constraint network unpost Constraint c 5 3 Reifying constraints In Choco 3 it is possible to reify any constraint Reifying a constraint means associating it with a BoolVar to represent whether the constraint holds or not BoolVar b constraint reify Or BoolVar b VF bool b solver constraint reifyWith b The first API constraint reify creates the variable if it does not already exists and reify the constraint The second API constraint reifyWith b reify the constraint with the given variable Note A constraint is reified with only one boolean variable If multiple reification are required equality constraints will be created The Logica
104. l the constraints Constraint can be declared in extension by defining the valid invalid tuples or in intension by defining a relation between the variables Choco 3 provides various factories to declare constraints see Overview to have a list of available factories A list of constraints available through factories is given in List of available constraints Modelling Selecting the right constraints Constraints through propagators suppress forbidden values of the domain of the variables For a given paradigm there can be several propagators available A widely used example is the AllDifferent constraints which holds that all its variables should take a distinct value in a solution Such a rule can be formulated e using a clique of inequality constraints e using a global constraint either analysing bounds of variable Bound consistency or analysing all values of the variables Arc consistency e or using a table constraint an extension constraint which list the valid tuples The choice must be made by not only considering the gain in expressiveness of stress compared to others Indeed the effective yield of each option can be radically different as the efficiency in terms of computation time Many global constraints are used to model problems that are inherently NP complete And only a partial domain filtering variables can be done through a polynomial algorithm This is for example the case of NValue constraint that one as
105. lConstraintFactory enables to manipulate constraints through their reification Reifying a constraint means that we allow the constraint not to be satisfied Therefore the reified constraint should not be posted Only the reifying constraint should be posted Note also that for performance reasons some reifying constraints available in the LogicalConstraintFactory are automatically posted the factory method returns void For instance we can represent the constraint either x lt 0 or y gt 42 as the following Constraint a IntConstraintFactory arithm x lt 0 Constraint b IntConstraintFactory arithm y gt 42 Constraint c LogicalConstraintFactory or a b solver post c This will actually reify both constraints a and b and say that at least one of the corresponding boolean variables must be true Note that only the constraint c is posted As a second reification example let us consider if x lt 0 then y gt 42 30 Chapter 5 Constraints and propagators Choco3 Documentation Release 3 3 1 Constraint a IntConstraintFactory arithm x lt 0 Constraint b IntConstraintFactory arithm y gt 42 LogicalConstraintFactory ifThen a b This time the LogicalConstraintFactory ifThen returns void meaning that the constraint is automatically posted If one really needs to access an ifThen Constraint object then the LogicalConstraintFactory ifThen_reifiable method should be use
106. latter is propagator dependent and should be managed by the developer when incrementality is enabled Note that the forcePropagate method will call propagate int when the propagator does not have any pending events In other words it is called once and for all after many domain modifications 71 Choco3 Documentation Release 3 3 1 void propagate int vldx int mask This method is the main entry point to the propagator during propagation When the vI dx vari able of the propagator is modified data relative to the modification is stored for a future execu tion of the propagator Then when the propagation engine has to execute the propagator a call to this method is done with the data relative to the variable and its modifications One can dele gate filtering algorithm to propagate int with a call to forcePropagate see item void propagate int evtmask However developers have to be aware that a propagator will not be informed of a modification it has generated itself That s why a propagator has to be idempotent see Section nameref properties or being aware not to be Note that when conditions enable it a call to setPassive will deactivate the propagator temporary during the exploration of the sub search space When the conditions are not met anymore the propagator is activated again i e on backtrack int getPropagationConditions int vIdx This method returns the specific mask indicating the
107. lex clauses Settings Search binder Resolution statistics e New constraints mddc not_member e Major modification Multi thread resolution Defining its own search strategy 2 4 Choco 3 changes 15 Choco3 Documentation Release 3 3 1 16 Chapter 2 Getting started Part II Modelling problems CHAPTER 3 The solver The object Solver is the key component It is built as following Solver solver new Solver or Solver solver new Solver my problem This should be the first instruction prior to any other modelling instructions Indeed a solver is needed to declare variables and thus constraints Here is a list of the commonly used Solver API Note The API related to resolution are not described here but detailed in Solving Similarly API provided to add a constraint to the solver are detailed in Constraints The other missing methods are only useful for internal behavior 19 Choco3 Documentation Release 3 3 1 3 1 3 1 Getters 1 Variables Method Definition Variable Return the array of variables declared in the solver It includes all type of variables getVars declared integer boolean etc but also fixed variables such as Solver ONE int getNbVars Return the number of variables involved in the solver Variable Return the ith variable declared in the solver get
108. ls can be found on http www slf4j org manual html 2 2 Overview of Choco 3 The following steps should be enough to start using Choco 3 The minimal problem should at least contains a solver some variables and constraints to linked them together To facilitate the modeling Choco 3 provides factories for almost every required component of CSP and its resolution Factory Shortcut Enables to create VariableFactory VF Variables and views integer boolean set and real IntConstraintFactory ICF Constraints over integer variables SetConstraintFactory SCF Constraints over set variables LogicalConstraintFactory LCF Manages constraint reification IntStrategyFactory ISF Custom or black box search strategies SetStrategyFactory SSF Chatterbox Output messages and statistics SearchMonitorFactory SMF resolution limits restarts etc Note that in order to have a concise and readable model factories have shortcut names Furthermore they can be imported in a static way import static org chocosolver solver search strategy ISF x Let say we want to model and solve the following equation x y lt 5 where the x 0 5 and y 0 5 Here is a short example which illustrates the main steps of a CSP modeling and resolution with Choco 3 to treat this equation 1 Create a Solver Solver solver new Solver my first problem 2 Create variables through the va
109. lver To create a matrix of 5x6 bounded variables of initial domain 0 5 IntVar vs VariableFactory boundedMatrix vs 5 6 0 5 solver Note When using bounded variables branching decisions must either be domain splits or bound assign ments removals Indeed assigning a bounded variable to a value strictly comprised between its bounds may results in disastrous performances because such branching decisions will not be refutable 4 2 2 Enumerated variable Integer variables with enumerated domains or shortly enumerated variables take their value in a b where a and b are integers such that a lt b the case where a b is handled through views or in an array of ordered values a b c z where a lt b lt c lt z Enumerated variables provide more information than bounded variables but are heavier in memory usually the domain requires a bitset To create an enumerated variable the VariableFactory should be used IntVar v VariableFactory enumerated v 1 12 solver which is equivalent to IntVar v VariableFactory enumerated v new int 1 2 3 4 5 6 7 8 9 10 11 12 solv r To create a variable with holes in its initial domain IntVar v VariableFactory enumerated v new int 1 7 8 solver To create an array of 5 enumerated variables with same domains IntVar vs VariableFactory enumeratedArray vs
110. lver BoolVar T VF bool T solver R T The solutions of the problem are L R 1 T 1 L R 0 T 0 e L 0R 1 T 0 e L 0R 0 T 0 22 6 addBoolEq Add a clause to the SAT constraint which states that the two boolean variables LEFT and RIGHT are equal API boolean addBoolEq BoolVar LEFT BoolVar RIGHT Example 22 5 addBoolAndEqVar 129 u e Bw N o u e uv N Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver SatFactory addBoolEq L R solver findAllSolutions The solutions of the problem are e L 1 R 1 e L 0 R 0 22 7 addBoollsEqVar Add a clause to the SAT constraint which states that LEFT RIGTH lt gt TARGET API boolean addBoolIsEqVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET Example Solver solver new Solver BoolVar L VF bool L solver BoolVar R VF bool R solver BoolVar T VF bool T solver SatFactory addBoolIsEqVar L R T solver findAllSolutions The solutions of the problem are e L 1R 1T 1 e L 1 1 R 0 T 0 e L 0 R 1 T 0 e L 0 R 0 T 1 22 8 addBoollsLeVar Add a clause to the SAT constraint which states that LEFT lt RIGTH lt gt TARGET APT boolean addBoolIsLeVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET Example 130 Chapter
111. lves e an array of integer variables VARS e an array of integer variables CVARS and acost automaton CAUTOMATON It ensures that the assignment of a sequence of variables VARS is recognized by CAUTOMATON a deterministic finite automaton and that the sum of the cost array associated to each assignment is bounded by the CVARS This version allows to specify different costs according to the automaton state at which the assignment occurs i e the transition starts The CAUOTMATON can be defined using the org chocosolver solver constraints nary automata FA CostAutomaton either e by creating a CostAutomaton once created states should be added then initial and final states are defined and finally transitions are declared e or by first creating a FiniteAutomaton and then creating a matrix of costs and finally calling one of the following API from CostAutomaton ICostAutomaton makeMultiResources IAutomaton pi int layer_value_resource int infs int sups E ICostAutomaton makeMultiResources IAutomaton pi int layer_value_resource_state int infs int sups ICostAutomaton makeMultiResources IAutomaton auto int LIE IntVar z ICostAutomaton makeMultiResources IAutomaton auto int Y c IntVar z The other API of CostAutomaton makeSingleResource are dedicated to the cost_regular constraint 102 Chapter 18 Constraint
112. m choco graph releases tag choco graph 3 2 1 which includes powerful cost based fil tering 112 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 API Constraint tsp IntVar SUCCS IntVar COST int COST_MATRIX Example 1 Solver solver new Solver 2 IntVar VS VF enumeratedArray VS 4 0 4 solver 3 IntVar CO VF enumerated CO 0 15 solver 4 int costs new int 0 1 3 7 1 0 1 3 3 1 0 1 7 5 solver post ICF tsp VS CO costs 6 solver findAllSolutions The solutions of the problem are e VS O 2 VS 1 0 VS 2 3 VS 3 1 CO 8 e VS O 3 VS 1 0 VS 2 1 VS 3 2 CO 10 e VS O 1 VS 1 2 VS 2 3 VS 3 0 CO 10 e VS O 3 VS 1 2 VS 2 0 VS 3 1 CO 14 e VS 0 1 VS 1 3 VS 2 0 VS 3 2 CO 8 e VS O 2 VS 1 3 VS 2 1 VS 3 0 CO 14 18 49 tsp 113 Choco3 Documentation Release 3 3 1 114 Chapter 18 Constraints over integer variables CHAPTER 19 Constraints over set variables 19 1 all_different The all_different constraint involves an array of set variables SETS It ensures that sets in SETS are all different not necessarily disjoint Note that there cannot be more than two empty sets API Constraint all different SetVar SETS 19 2 all_disjoint The all_disjoint constraint involves an array of s
113. n straint Programming CP 2011 17th International Conference CP 2011 Perugia Italy September 12 16 2011 Proceedings 271 285 2011 URL http dx doi org 10 1007 978 3 642 23786 7_22 doi 10 1007 978 3 642 23786 7_22 FHK 02 Alan M Frisch Brahim Hnich Zeynep Kiziltan Ian Miguel and Toby Walsh Global constraints for lexicographic orderings In Principles and Practice of Constraint Programming CP 2002 8th Inter national Conference CP 2002 Ithaca NY USA September 9 13 2002 Proceedings 93 108 2002 URL http link springer de link service series 0558 bibs 2470 24700093 htm HS02 Warwick Harvey and Joachim Schimpf Bounds consistency techniques for long linear constraints In In Proceedings of TRICS Techniques foR Implementing Constraint programming Systems 39 46 2002 LSTV09 Christophe Lecoutre Lakhdar Sais S bastien Tabary and Vincent Vidal Reasoning from last conflict s in constraint programming Artif Intell 173 18 1592 1614 2009 URL http dx doi org 10 1016 j artint 2009 09 002 doi 10 1016 j artint 2009 09 002 LopezOrtizQTvB03 Alejandro L pez Ortiz Claude Guy Quimper John Tromp and Peter van Beek A fast and simple algorithm for bounds consistency of the alldifferent constraint In JCAI 03 Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence Acapulco Mexico August 9 15 2003 245 250 2003 MTO00 Kurt Mehlhorn and Sven Thiel Faster algorithms f
114. ne explainer Set the explanation engine to use during resolution The default one is ExplanationEngine which does nothing set ObjectiveManager om Set the objective manager to use during the resolution For advanced usage only 3 3 Others Method Definition Solver duplicateModel Duplicate the model associates with a solver ie only variables and constraints and return a new solver sm void Add a strategy to the declared one in order to ensure that all variables makeCompleteSearch boolean are covered by at least one strategy isComplete void Put a search monitor to react on search events solutions decisions plugMonitor ISearchMonitor fails void Add an filtering monitor that is an object that is kept informed of all plugMonitor FilteringMonitdxpropagation events generated during the resolution fm 22 Chapter 3 The solver CHAPTER 4 Declaring variables 4 1 Principle A variable is an unknown mathematically speaking The goal of a resolution is to assign a value to each declared variable In Constraint Programming the domain set of values that a variable can initially take must be defined Choco 3 includes five types of variables IntVar BoolVar SetVar and RealVar A factory is available to ease the declaration of variables VariableFactory or VE for short At least a variable requi
115. new int 3 1 2 20 costs 3 new int 3 2 1 21 costs 4 new int 2 1 3 22 23 solver post ICF cost_regular VARS COST CostAutomaton makeSingleResource 24 solver findAllSolutions Some solutions of the problem are e VARS O 0 VARS 1 0 VARS 2 0 VARS 3 0 VARS 4 1 COST 10 e VARS O 0 VARS 1 0 VARS 2 0 VARS 3 1 VARS 4 1 COST 9 e VARS O 0 VARS 1 0 VARS 2 1 VARS 3 2 VARS 4 1 COST 6 e VARS O 1 VARS 1 2 VARS 2 1 VARS 3 0 VARS 4 1 COST 8 18 15 count The count constraint involves e an integer VALUE e an array of integer variables VARS and e an integer variable LIMIT The constraint holds that LIMIT is equal to the number of variables from VARS assigned to the value VALUE An alternate signature enables VALUE to be an integer variable 18 15 count fauto costs Choco3 Documentation Release 3 3 1 See also count in the Global Constraint Catalog API Constraint count int VALUE IntVar VARS IntVar LIMIT Constraint count IntVar VALUE IntVar VARS IntVar LIMIT Example Solver solver new Solver IntVar VS VF enumeratedArray VS 4 0 3 solver IntVar VA VF enumerated VA new int 1 3 solver IntVar CO VF enumerated CO new int 0 2 4 solver solver post ICF count VA VS CO solver findAllSolutions Dn nF uv N oo
116. ng a CostAutomaton once created states should be added then initial and final states are defined and finally transitions are declared e or by first creating a FiniteAutomaton and then creating a matrix of costs and finally calling one of the following API from CostAutomaton ICostAutomaton makeSingleResource IAutomaton pi int costs int inf int sup ICostAutomaton makeSingleResource IAutomaton pi int costs int inf int sup 88 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 The other API of CostAutomaton makeMultiResources are dedicated to the multi cost_regular constraint Implementation based on DPRO6 API Constraint cost_regular IntVar VARS IntVar COST ICostAutomaton CAUTOMATON Example 1 Solver solver new Solver 2 IntVar VARS VF enumeratedArray VARS 5 0 2 solver 3 IntVar COST VF enumerated COST 0 10 solver 4 FiniteAutomaton fauto new FiniteAutomaton 5 int start fauto addState 6 int end fauto addState T 8 9 F fauto setInitialState start fauto setFinal start end 10 fauto addTransition start start 0 1 fauto addTransition start end 2 13 fauto addTransition end end 1 14 fauto addTransition end start 0 2 15 16 int costs new int 5 3 17 costs 0 new int l 2 3 18 costs 1 new int 2 3 1 19 costs 2
117. ntation Release 3 3 1 void declareSettings Settings settings Declare a specific Settings to each solver Set tings Calling this method is highly recommended to at least configure the search strategies for each solver ESat isFeasible Indicate if one solver at least has found a solution for the given problem boolean hasReachedLimit Indicate if all solvers have reached a limit boolean findSolution Deal with satisfaction problem the solvers are distributed the first one which finds a solution stops the process It returns t rue if one solver has found a solution false otherwise void findOptimalSolution ResolutionPolicy policy IntVar objective Deal with opti misation problem the solvers are distributed and anytime a solver found a solution it shares the value with the others It one proofs the optimality it stops the process void wishGranted For internal uses only 60 Chapter 12 Multi thread resolution CHAPTER 13 Explanations Choco 3 natively support explanations However no explanation engine is plugged in by default 13 1 Principle Nogoods and explanations have long been used in various paradigms for improving search An explanation records some sufficient information to justify an inference made by the solver domain reduction contradiction etc It is made of a subset of the original propagators of the problem and a subset of decisions applied during search Explana tions represent
118. nteger variables Choco3 Documentation Release 3 3 1 4 solver post ICF arithm X 5 solver findAllSolutions tesi Y t 100 The solutions of the problem are X 0 Y 1 X 0 Y 0 X 0 Y 1 X 1 Y 0 X 1 Y 1 X 2Y 1 18 7 atleast_nvalues The atleast_nvalues constraint involves e an array of integer variables VARS e an integer variable NVALUES and e a boolean AC Let N be the number of distinct values assigned to the variables of the VARS collection The constraint enforces the condition N gt NVALUES to hold The boolean AC set to true enforces arc consistency See also atleast_nvalues in the Global Constraint Catalog Implementation based on Regin95 API Constraint atleast_nvalues IntVar VARS IntVar NVALUES boolean AC Example 1 Solver solver new Solver 2 IntVar XS VF enumeratedArray XS 4 0 2 solver 3 IntVar N VF enumerated N 2 3 solver 4 solver post ICF atleast_nvalues XS N true 5 solver findAllSolutions Some solutions of the problem are e XS 0 0 XS 1 0 XS 2 0 XS 3 1N 2 e XS 0 0 XS 1 1 XS 2 0 XS 3 1N 2 e XS 0 0 XS 1 1 XS 2 2 XS 3 1N 2 e XS 0 2 XS 1 0 XS 2 2 XS 3 1 N 3 e XS 0 2 XS 1 2 XS 2 1 XS 3 O N 3 18 7 atleast_nvalues 83 Choco3 Documentation Release 3 3 1 18 8 atmost_nvalues The atmost_nvalues constraint involves e an array of
119. nteger variables BIN_LOAD and an integer OF FSET 84 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 It holds the Bin Packing Problem rules a set of items with various SIZES to pack into bins with respect to the capacity of each bin e ITEM_BIN represents the bin of each item that is ITEM_BIN i j states that the i ITEM is put in the bin e ITEM_SIZE represents the size of each item e BIN_LOAD represents the load of each bin that is the sum of size of the items in it This constraint is not a built in constraint and is based on various propagators See also bin_packing in the Global Constraint Catalog API Constraint bin_packing IntVar ITEM_BIN int ITEM_SIZE IntVar BIN_LOAD int OFFSET Example 1 Solver solver new Solver 2 IntVar IBIN VF enumeratedArray IBIN 5 1 3 solver 3 int sizes new int 2 3 1 4 2 4 IntVar BLOADS VF enumeratedArray BLOADS 3 0 5 solver 5 solver post ICF bin_packing IBIN sizes BLOADS 1 6 solver findAllSolutions Some solutions of the problem are e IBIN O 1 IBIN 1 1 IBIN 2 2 IBIN 3 2 IBIN 4 3 BLOADS 0 5 BLOADS 1 5 BLOADS 2 2 e IBIN O 1 IBIN 1 3 IBIN 2 1 IBIN 3 2 IBIN 4 1 BLOADS 0 5 BLOADS 1 4 BLOADS 2 3 e IBIN O 2 IBIN 1 3 IBIN 2 1 IBIN 3 1 IBIN 4 3 BLOADS 0 5 B
120. o NBTREES anti arborescences e SUCCS i OF FSET j means that j is the successor of i e SUCCS i OFFSET i means that i is a root See also tree in the Global Constraint Catalog Implementation based on FL11 API Constraint tree IntVar SUCCS IntVar NBTREES int OFFSET Example 1 Solver solver new Solver 2 IntVar VS VF enumeratedArray VS 4 0 4 solver 3 IntVar NT VF enumerated NT 2 3 solver 4 solver post ICF tree VS NT 0 Some solutions of the problem are e VS O 0 VS 1 1 VS 2 1 VS 3 1 NT 2 e VS O 1 VS 1 1 VS 2 2 VS 3 1 NT 2 e VS O 2 VS 1 0 VS 2 2 VS 3 3 NT 2 e VS O 0 VS 1 3 VS 2 2 VS 3 3 NT 3 e VS O 3 VS 1 1 VS 2 2 VS 3 3 NT 3 18 48 TRUE The TRUE constraint is always satisfied It should only be used with LogicalFactory 18 49 tsp The tsp constraint involves e an array of integer variables SUCCS e an integer variable COST and e a matrix of integers COST_MATRIX It formulates the Travelling Salesman Problem the variables SUCCS form a hamiltonian circuit of value COST Going from i to j SUCCS i j costs COST_MATRIX i 5 This constraint is not a built in constraint and is based on various propagators The filtering power of this constraint remains limited For stronger filtering use the choco graph extension https github com chocotea
121. olves an array of variables VARS It ensures that all variables from VAR take a distinct value or 0 that is all values but 0 can t appear more than once See also alldifferent_except_0 in the Global Constraint Catalog API Constraint alldifferent_except_0 IntVar VARS Example Solver solver new Solver IntVar XS VF enumeratedArray XS 4 0 2 solver solver post ICF alldifferent_except_0 XS solver findAllSolutions Some solutions of the problem are e XS O 0 XS 1 0 XS 2 0 XS 3 0 e XS O 0 XS 1 1 XS 2 2 XS 3 0 e XS O 0 XS 1 2 XS 2 0 XS 3 0 e XS 0 2 XS 1 1 XS 2 0 XS 3 0 18 5 among The among constraint involves e an integer variable NVAR e an array of integer variables VARIABLES and an array of integers It holds that NVAR is the number of variables of the collection VARIABLES that take their value in VALUES See also among in the Global Constraint Catalog Implementation based on BessiereHH 05 API Constraint among IntVar NVAR IntVar VARS int VALUES Example 18 4 alldifferent_except_0 81 u e Bw N Rob N Choco3 Documentation Release 3 3 1 Solver solver new Solver IntVar N VF enumerated N 2 3 solver IntVar XS VF enumeratedArray XS 4 0 6 solver solver post ICF among N XS new int 1 2 3 solver findAllSolutions
122. on operator Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntStrategy custom Variableselector lt IntVar gt VAR_SELECTOR IntValueSelector VAL SELECTOR DecisionOperator lt IntVar gt DEC_OPERATOR IntVar VARS IntStrategy custom Variableselector lt IntVar gt VAR_SELECTOR IntValueSelector VAL SELECTOR IntVar VARS SetStrategy custom VariableSelector lt SetVar gt varS SetValueSelector valS boolean enforteFirst SetVar sets 26 2 force first A built in strategy which chooses the first non instantiated variable regarding the lexicographic order and forces its first smallest unfixed value to be part of the kernel Scope SetVar Factory org chocosolver solver search strategy SetStrategyFactory API SetStrategy force_first SetVar sets 147 Choco3 Documentation Release 3 3 1 26 3 force _maxDelta_first A built in strategy which chooses the first non instantiated variable of maximum delta envelope s cardinality minus kernel s cardinality and forces its smallest unfixed value to be part of the kernel Scope SetVar Factory org chocosolver solver search strategy SetStrategyFactory API SetStrategy force_maxDelta_first SetVar sets 26 4 force _minDelta_ first A built in strategy which chooses the first non instantiated variable of minimum delta
123. onflict solution and are then evaluated and kept if relevant to get the explanation 13 2 In practice Consider the following example 1 Narendra Jussien The versatility of using explanations within constraint programming Technical Report 03 04 INFO 2003 61 Choco3 Documentation Release 3 3 1 Solver solver new Solver BoolVar bvars VF boolArray B 4 solver solver post ICF arithm bvars 2 bvars 3 solver post ICF arithm bvars 2 bvars 3 solver set ISF lexico_LB bvars solver findAllSolutions The problem has no solution since the two constraints cannot be satisfied together A naive strategy such as ISF lexico_LB bvars which selects the variables in lexicographical order will detect lately and many times the failure By plugging in an explanation engine on each failure the reasons of the conflict will be explained ExplanationFactory CBJ plugin solver false false The explanation engine records deductions and causes in order to compute explanations In that small example when an explanation engine is plugged in the two first failures will enable to conclude that the problem has no solution Only three nodes are created to close the search seven are required without explanations Note Only unary binary ternary and sum propagators over integer variables have a dedicated explanation algorithm Although global constraints over integer va
124. or bound consistency of the sortedness and the alldifferent constraint In Principles and Practice of Constraint Programming CP 2000 6th International Conference Sin gapore September 18 21 2000 Proceedings 306 319 2000 URL http dx doi org 10 1007 3 540 45349 0_23 doi 10 1007 3 540 45349 0_23 MD09 Julien Menana and Sophie Demassey Sequencing and counting with the multicost regular constraint In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems 6th International Conference CPAIOR 2009 Pittsburgh PA USA May 27 31 2009 Proceedings 178 192 2009 URL http dx doi org 10 1007 978 3 642 01929 6_14 doi 10 1007 978 3 642 01929 6_14 MH12 Laurent Michel and Pascal Van Hentenryck Activity based search for black box constraint programming solvers In Integration of AI and OR Techniques in Contraint Programming for Combinatorial Optimzation Prob lems 9th International Conference CPAIOR 2012 Nantes France May 28 Junel 2012 Proceedings 228 243 2012 URL http dx doi org 10 1007 978 3 642 29828 8_15 do1 10 1007 978 3 642 29828 8_15 Pes04 Gilles Pesant A regular language membership constraint for finite sequences of variables In Principles and Practice of Constraint Programming CP 2004 10th International Conference CP 2004 Toronto Canada September 27 October 1 2004 Proceedings 482 495 2004 URL http dx doi org 10 1007 978 3 540 30201 8_36 doi 1
125. ore detailed are given in Defining its own constraint Choco 3 provides various types of constraints 5 1 1 Available constraints FALSE TRUE On one integer variable arithm member not_member On two integer variables absolute arithm distance square table times On three integer variables arithm distance eucl_div maximum minimum mod times On an undefined number of integer variables element sort table mddc alldifferent alldifferent_conditionnal alldifferent_except_0 global_cardinality among atleast_nvalues atmost_nvalues count nvalues boolean_channeling clause_channeling inverse_channeling cumulative diffn lex_chain_less lex_chain_less_eq lex_less lex_less_eq maximum minimum scalar sum cost_regular multicost_regular regular circuit path subcircuit subpath tree bin_packing knapsack tsp On one set variable notEmpty On two set variables disjoint offSet On an undefined number of set variables 28 Chapter 5 Consiraints and propagators Choco3 Documentation Release 3 3 1 all_different all_disjoint all_equal bool_channel intersection inverse_set member nbEmpty partition subsetEq symmetric union On integer and set variables cardinality element int_channel max member not_member min sum On real variables Constraints over real variables 5 1 2 Things to know about constraints Automaton based Constraints cost_regular multicost_regula
126. other variable domain Available views are not offset eq minus scale and real Views 2 3 4 Constants Fixed value integer variables should be created with the specific VF fixed int Solver function Constants 2 3 5 Constraints Several constraint factories ease the creation of constraints LogicalConstraintFactory LCF IntConstraintFactory ICF and SetConstraintsFactory SCF RealConstraint is created with a call to new and to addFunction method It requires the Ibex solver Constraints hold once posted solver post c Reified constraints should not be posted Constraints 2 3 6 Search Defining a specific way to traverse the search space is made thanks to solver set AbstractStrategy Predefined strategies are available in IntStrategyFactory ISF SetStrategyFactory and RealStrategyFactory 2 3 7 Large Neighborhood Search LNS Various LNS random propagation guided etc can be created from the LNSFactory to improve performance on optimization problems 2 3 Choco 3 quick documentation 13 Choco3 Documentation Release 3 3 1 2 3 8 Monitors An ISearchMonitor is a callback which enables to react on some resolution events failure branching restarts solutions etc SearchMonitorFactory SMF lists most useful monitors User defined monitors can be added with solver plugMonitor 2 3 9 Limits A limit may be imposed on the search The search stops once a limit is reached Availa
127. pect relates to the problem of minimum hitting set Finally the global nature of this type of constraint also simplifies the work of the solver in that it provides all or part of the structure of the problem If we want an integer variable sum to be equal to the sum of values of variables in the set at Least we can use the IntConstraintFactory sum constraint all others configurations may be chosen A constraint may define its specific checker through the method isSat isfied but most of the time the checker is given by checking the entailment of each of its propagators The satisfaction of the constraints solver is done on each solution if assertions are enabled 27 Choco3 Documentation Release 3 3 1 Note One can enable assertions by adding the ea instruction in the JVM arguments It can thus be slower if the checker is often called which is not the case in general The advantage of this framework is the economy of code less constraints need to be implemented the avoidance of useless redundancy when several constraints use the same propagators for instance IntegerChanneling constraint involves A11Different constraint which leads to better performances and an easier maintenance Note To ease modelling it is not required to manipulate propagators but only constraints However one can define specific constraints by defining combinations of propagators and or its own propagators M
128. r and regular rely on an automaton declared implicitly or explicitly There are two kinds of TAutomaton FiniteAutomaton needed for cost_regular and CostAutomaton required for multi cost_regular and regular A CostAutomaton is an extension of FiniteAutomaton where costs can be declared per transition FiniteAutomaton embeds an Automaton object provided by the dk brics automaton library Such an automaton accepts fixed size words made of multiple char s but the regular constraints rely on IntVar s So mapping between char needed by the underlying library and int declared in IntVar is made The mapping enables declaring regular expressions where a symbol is not only a digit between 0 and 9 but any positive number Then to distinct in the word 701 the symbols 0 1 10 and 101 two additional char are allowed in a regexp lt and gt which delimits numbers In summary a valid regexp for the cost_regular multicost_regular and regular constraints is a combination of digits and Java Regexp special characters Examples of allowed RegExp 0x11111110 10 10 11111110x 11 0 1 2 x00 0 lt 10 gt lt 20 gt x 0 lt 10 gt Example of forbidden RegExp abcl alb c 5 2 Posting constraints To be effective a constraint must be posted to the solver This is achieved using the method solver post Constraint cstr Otherwise if the solver post Constraint cstr method is not called the constraint wil
129. reliable algorithms for handling non linear constraints In particular round off errors are also taken into account It is based on interval arithmetic and affine arithmetic http www ibex lib org To manage continuous constraints with Choco an interface with Ibex has been done It needs Ibex to be installed on your system Then simply declare the following VM options Djava library path path to Ibex lib The path path to Ibex lib points to the lib directory of the Ibex installation directory 17 1 Installing Ibex See the installation instructions of Ibex to complied Ibex on your system More spe cially take a look at Installation as a dynamic library and do not forget to add the with java package org chocosolver solver constraints real configuration option Once the installation is completed the JVM needs to know where Ibex is installed to fully benefit from the Choco Ibex bridge and declare real variables and constraints 75 Choco3 Documentation Release 3 3 1 76 Chapter 17 Ibex Part V Elements of Choco 77 u OR Bw N CHAPTER 18 Constraints over integer variables 18 1 absolute The absolute constraint involves two variables VAR and VAR2 It ensures that VARI VAR2 API Constraint absolute IntVar VAR1 IntVar VAR2 Example Solver solver new Solver IntVar X VF enumerated X 0 2 solver IntVar Y VF enumerated X 6 1
130. res a name and a solver to be declared in The name is only helpful for the user to read the results computed 4 2 Integer variable An integer variable is based on domain made with integer values There exists under three different forms bounded enumerated or boolean An alternative is to declare variable based views Important It is highly advisable not to define domain like Integer MIN_VALUE Integer MAX_VALUE Indeed such domain definition may lead to e incorrect domain size Integer MAX_VALUE Integer MIN_VALUE 1 0 e and to numeric overflow underflow operations during propagation If undefined domain is really required the following range should be considered VariableFactory MIN_INT_BOUND VariableFactory MAX_INT_BOUND Such an interval defines 42949673 values from 21474836 to 21474836 4 2 1 Bounded variable Bounded integer variables take their value in a b where a and b are integers such that a lt b the case where a b is handled through views Those variables are pretty light in memory the domain requires two integers but cannot represent holes in the domain To create a bounded variable the VariableFactory should be used IntVar v VariableFactory bounded v 1 12 solver To create an array of 5 bounded variables of initial domain 2 8 23 Choco3 Documentation Release 3 3 1 IntVar vs VariableFactory boundedArray vs 5 2 8 so
131. riable factory IntVar x VariableFactory bounded X 0 5 solver IntVar y VariableFactory bounded Y 0 5 solver 3 Create and post constraints by using constraint factories solver post IntConstraintFactory arithm x y lt 5 5 4 Define the search strategy solver set IntStrategyFactory lexico_LB x y 5 Launch the resolution process solver findSolution 6 Print search statistics Chatterbox printStatistics solver One may notice that there is no distinction between model objects and solver objects This makes easier for beginners to model and solve problems reduction of concepts and terms to know and for developers to implement their own constraints and strategies short cutting process Don t be afraid to take a look at the sources we think it is a good start point 12 Chapter 2 Getting started Choco3 Documentation Release 3 3 1 2 3 Choco 3 quick documentation 2 3 1 Solver The Solver is a central object and must be created first Solver solver new Solver Solver 2 3 2 Variables The VariableFactory VF for short eases the creation of variables Available variables are BoolVar IntVar SetVar GraphVar and RealVar Note that an IntVar domain can be bounded only bounds are stored or enumerated all values are stored a boolean variable is a 0 1 IntVar Variables 2 3 3 Views A view is a variable whose domain is defined by a function over an
132. riables are compatible with explanations they should be either accurately explained or reformulated to fully benefit from explanations 13 2 1 Cause A cause implements ICause and must defined the boolean why RuleStore ruleStore IntVar var IEventType evt int value method Such a method add new event filtering rules to the ruleStore in pa rameter in order to filter relevant events among all generated during the search Every time a variable is modified the cause is specified in order to compute explanations afterwards For instance when a propagator updates the bound of an integer variable the cause is the propagator itself So do decisions objective manager etc 13 2 2 Computing explanations When a contradiction occurs during propagation it can only be thrown by e a propagator which detects unsatisfiability based on the current domain of its variables e ora variable whom domain became empty Consequently in addition to causes variables can also explain the current state of their domain Computing the explanation of a failure consists in going up in the stack of all events generated in the current branch of the search tree and filtering the one relative to the conflict The entry point is either a the unsatisfiabable propagator or the empty variable Note Explanations can be computed without failure The entry point is a variable and only removed values can be explained Each propagator embeds its own explanat
133. s 27 1 geometrical Plug a geometrical restart strategy to the solver It performs a search with restarts controlled by the resolution event counter which counts events occurring during the search Parameter base indicates the maximal number of events allowed in the first search tree Once this limit is reached a restart occurs and the search continues until base x grow events are done and so on After each restart the limit number of events is increased by the geometric factor grow 1imit states the maximum number of restarts Factory org chocosolver solver search loop monitors SearchMonitorFactory API void geometrical Solver solver int base double grow ICounter counter int limit 27 2 luby Branch a luby restart strategy to the solver It is an alternative to the geometric restart policy It performs a search with restarts controlled by the number of resolution events counted by counter The maximum number of events allowed at a given restart iteration is given by base multiplied by the Las Vegas coefficient at this iteration The sequence of these coefficients is defined recursively on its prefix subsequences starting from the first prefix 1 the k 1 h prefix is the kth prefix repeated grow times and immediately followed by coefficient grow e the first coefficients for grow 2 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 1 e the first coefficients for grow 3 1 1 1 3 1 1 1 3 1 1 1 3 9 Factor
134. s it involves a integer variable VAR and an array of distinct values TABLE It ensures that VAR takes its values in TABLE e or two bounds included it involves a integer variable VAR and two integer LB and UB It ensures that VAR takes its values in LB UB API Constraint member IntVar VAR int TABLE Constraint member IntVar VAR int LB int UB Example 1 Solver solver new Solver IntVar X VF enumerated X 1 4 solver solver post ICF member X new int 2 1 0 1 2 solver findAllSolutions The solutions of the problem are X e X 2 Example 2 1 Solver solver new Solver 2 IntVar X VF enumerated X 1 4 solver solver post ICF member X 2 5 4 solver findAllSolutions The solutions of the problem are 100 Chapter 18 Constraints over integer variables N o u e v Choco3 Documentation Release 3 3 1 e X 2 e X 3 e X 4 18 32 minimum The minimum constraints involves a set of integer variables and a third party integer variable either e two integer variables VARI and VAR2 and an integer variable MIN it ensures that MIN minimum VARI VAR2 e or an array of integer variables VARS and an integer variable MIN it ensures that MIN is the minimum value of the collection of domain variables VARS e or an array of boolean variables BVARS and a booean variable MIN it ensures that MIN is the minimum
135. s over integer variables N Choco3 Documentation Release 3 3 1 Implementation based on MD09 API Constraint multicost_regular IntVar VARS IntVar CVARS ICostAutomaton CAUTOMATON Example TBD 18 35 not_member A constraint which prevents a variable to be assigned to some values defined by either e a list of values it involves a integer variable VAR and an array of distinct values TABLE It ensures that VAR does not take its values in TABLE e two bounds included it involves a integer variable VAR and two integer LB and UB It ensures that VAR does not take its values in LB UB The constraint API Constraint not_member IntVar VAR int TABLE Constraint not_member IntVar VAR int LB int UB Example 1 Solver solver new Solver IntVar X VF enumerated X 1 4 solver solver post ICF not_member X new int 2 1 0 1 2 solver findAllSolutions The solutions of the problem are eX 3 e X 4 Example Solver solver new Solver IntVar X VF enumerated X 1 4 solver solver post ICF not_member X 2 5 solver findAllSolutions The solution of the problem is e X 18 35 not_member 103 u e u N Choco3 Documentation Release 3 3 1 18 36 nvalues The nvalues constraint involves e an array of integer variables VARS and e an integer variable NVALUES The constraint ensures tha
136. s the list of variables to optimize Gl or Note All variables should respect the same resolution policy The underlying approach is naive but it simplifies the process Anytime a solution is found a cut is posted which states that at least one of the objective variables must be better Such as Xo lt bo V X1 lt b V V Xn lt bn where X is the ith objective variable and b its best known value The method ends by restoring the last solution found so far if any 6 3 Multi objective optimization problems 37 Choco3 Documentation Release 3 3 1 Here is a simple illustration 6 4 Propagation One may want to propagate each constraint manually This can be achieved by calling solver propagate This method runs in turn the domain reduction algorithms of the constraints until it reaches a fix point It may throw a ContradictionException if a contradiction occurs In that case the propagation engine must be flushed calling solver getEngine flush to ensure there is no pending events Warning If there are still pending events in the propagation engine the propagation may results in unexpected results 38 Chapier 6 Finding solutions CHAPTER 7 Recording solutions Choco 3 requires that each decision variable that is which is declared in the search strategy is instantiated in a solution Otherwise an exception will be thrown Non decision variables can be uninstanti
137. set to true to store the very last explanation of the search recommended value false 13 4 Explanations for the end user Explaining the last failure of a complete search without solution provides information about the reasons why a problem has no solution For the moment there is no simplified way to get such explanations CBJ and DBT enable retrieving an explanation of the last conflict problem definition First manually plug CBJ or DBT ExplanationEngine ee new ExplanationEngine solver userFeedbackOn ConflictBackJumping cbj new ConflictBackJumping ee solver nogoodsOn solver plugMonitor cbj if solver findSolution If the problem has no solution the end user explanation can be retrieved System out println cbj getLastExplanation Incomplete search leads to incomplete explanations as far as at least one decision is part of the explanation there is no guarantee the failure does not come from that decision On the other hand when there is no decision the explanation is complete 64 Chapter 13 Explanations CHAPTER 14 Search monitor 14 1 Principle A search monitor is an observer of the search loop It gives user access before and after executing each main step of the search loop initialize when the search loop starts initial propagator when the initial propagation is run open node when a decision is computed down left branch on going down in
138. ssary Using specific strategy dedicated to a type of variable such as Int St rat egy is enough The one above has an alternate constructor public IntStrategy IntVar scope VariableSelector lt IntVar gt varSelector IntValueSelector valSelector DecisionOperator lt IntVar gt decOperator And defining your own strategy is really crucial start by copying pasting an existing one Indeed decisions are stored in pool managers to avoid creating too many decision objects and thus garbage collecting too often 15 3 Making a decision 69 Choco3 Documentation Release 3 3 1 70 Chapter 15 Defining its own search strategy CHAPTER 16 Defining its own constraint In Choco 3 constraints is basically a list of filtering algorithms called propagators A propagator is a function from domains to domains which removes impossible values from variable domains 16 1 Structure of a Propagator A propagator needs to extends the Propagator abstract class Then a constructor and some methods have to be implemented super a call to super is mandatory The list of variables which determines the index of the variable in the propagator and the priority for the propagation engine are required An optional boolean t rue is the default value can be set to false to avoid reacting on fine events see item void propagate int vidx int mask More precisely if set to false the propagator will only be informed o
139. ssignment decisions over bounded variables because the decision negation would result in no inference Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntValueSelector mid_value_ selector 24 3 max_value_ selector A built in value selector which selects the variable upper bound Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory 143 Choco3 Documentation Release 3 3 1 API IntValueSelector max_value_selector 24 4 randomBound_value selector A built in value selector which randomly selects either the lower bound or the upper bound of the variable Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntValueSelector randomBound_value_selector long SEED 24 5 random_value selector Selects randomly a value in the variable domain Important random_value_selector should not be used with assignment decisions over bounded variables because the decision negation could result in no inference Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API IntValueSelector random_value_selector long SEED 144 Chapter 24 Value selectors CHAPTER 25 Decision operators 25 1 assign A built in decision operator which assigns the selected variable to the selected value Its negation is
140. st activity is selected from the domain of the variable Implementation based on MH 12 Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API AbstractStrategy lt IntVar gt activity IntVar VARS double GAMMA double DELTA int ALPHA int FORCE_SAMPLING long SEED AbstractStrategy lt IntVar gt activity IntVar VARS long SEED default 0 999d 0 2d 1 26 20 impact A black box strategy for IntVar which selects the non instantiated variable with the largest impact Vaina x Hu a I x a denotes the impact of assigning the variable x to a value a from its domain d x The impact of an assignment measures the search space reduction induced by a decision by evaluating the size of the search before and after the application of a decision The higher the impact the greater the search space reduction Then the value with the least impact is selected from the domain of the variable An approximation of the impacts is preprocessed Implementation based on Ref04 Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API AbstractStrategy lt IntVar gt impact IntVar VARS int ALPHA int SPLIT int NODEIMPACT long SEED boolean INITONLY AbstractStrategy lt IntVar gt impact IntVar VARS long SEED default 2 3 10 true 26 21 lastConflict A composite heuristic which override the defined
141. t NVALUES is the number of distinct values assigned to the variables of the VARS array This constraint is a combination of the atleast_nvalues and atmost_nvalues constraints This constraint is not a built in constraint and is based on various propagators See also nvalues in the Global Constraint Catalog Implementation based on atleast_nvalues and atmost_nvalues API Constraint nvalues IntVar VARS IntVar NVALUES Example Solver solver new Solver IntVar VS VF enumeratedArray VS 4 0 2 solver IntVar N VF enumerated N 0 3 solver solver post ICF nvalues VS N solver findAllSolutions Some solutions of the problem are e VS 0 0 VS 1 0 VS 2 0 VS 3 ON 1 e VS 0 0 VS 1 0 VS 2 0 VS 3 1N 2 e VS O 0 VS 1 1 VS 2 2 VS 3 2 N 3 18 37 path The path constraint involves e an array of integer variables VARS e an integer variable START e an integer variable END and e an integer OF FSET It ensures that the elements of VARS define a covering path from START to END where VARS i OF FSET means that j is the successor of i Moreover VARS END OFFSET VARS OFFSET The constraint relies on the circuit propagators See also path in the Global Constraint Catalog Implementation based on circuit API 104 Chapter 18 Constraints over integer variables Dun e Bw N u ae v N Choco3 Documentation Release 3
142. t support requests are answered very fast However this free service is provided with no guarantee If you want an expert to build a CP model for your application or if you need professional support please contact COSLING 1 6 How to cite Choco A reference to this manual or more generally to Choco 3 is made like this manual choco3 author Charles Prud homme and Jean Guillaume Fages and Xavier Lorca title Choco3 Documentation year 2014 organization TASC INRIA Rennes LINA CNRS UMR 6241 COSLING S A S timestamp Thu 11 May 2015 url http www choco solver org 6 Chapter 1 Main concepts Choco3 Documentation Release 3 3 1 1 7 Who contributes to Choco Core developers Charles Prud homme TASC INRIA Rennes LINA CNRS UMR 6241 and Jean Guillaume Fages COSLING S A S Main Xavier Lorca Narendra Jussien Fabien Hermenier Jimmy Liang contributors Previous Francois Laburthe Hadrien Cambazard Guillaume Rochart Arnaud Malapert Sophie versions Demassey Nicolas Beldiceanu Julien Menana Guillaume Richaud Thierry Petit Julien contributors Vion St phane Zampelli If you want to contribute let us know Choco is developed with Intellij IDEA and JProfiler that are kindly provided for free 1 7 Who contributes to Choco 7 Choco3 Documentation Release 3 3 1 8 Chapter 1 Main concepts CHAPTER 2 Getting s
143. t value will then be selected Here is the code of the FirstFail variable selector which selects first the variable with the smallest domain 1 public class FirstFail implements VariableSelector lt IntVar gt VariableEvaluator lt IntVar gt 2 4 Override 5 public IntVar getVariable IntVar variables 6 int small_idx 1 7 int small_dsize Integer MAX_VALUE 8 for int idx 0 idx lt variables length idx 9 int dsize variables idx getDomainSize 10 if dsize gt 1 amp amp dsize lt small_dsize 1 small_dsize dsize 12 small_idx idx 13 14 67 Choco3 Documentation Release 3 3 1 15 return small_idx gt 1 variables small_idx null 16 17 18 Override 19 public double evaluate IntVar variable 20 return variable getDomainSize 21 22 There is a distinction between VariableSelector and VariableEvaluator On the one hand a VariableSelector breaks ties lexicographically that is the first variable in the input array which respects the specification is returned new IntStrategy variables new FirstFail new IntDomainMin DecisionOperator int_eq On the other hand a VariableEvaluator selects all variables which respect the specifications and let another VariableE valuator breaks ties if any or acts like a VariableSelector new IntStrategy variables new VariableSelectorWithTies new FirstFail new Larg
144. tEmpty SetVar SET 19 18 offSet The offset constraint involves e two set variables SET_ and SET_2 and e an integer OFFSET It ensures that to any value x in SET_1 the value x OF FSET is in SET_2 and reciprocally API Constraint offSet SetVar SET_1 SetVar SET_2 int OFFSET 19 19 partition The partition constraint involves e an array of set variables SETS and e a set variable UNIVERSE It ensures that UNVIVERSE is partitioned in disjoint sets SETS API Constraint partition SetVar SETS SetVar UNIVERSE 120 Chapter 19 Constraints over set variables Choco3 Documentation Release 3 3 1 19 20 subsetEq The subsetEg constraint involves an array of set variables SETS It ensures that i lt j SET_VARS i C SET_VARS j The API is Constraint subsetEq SetVar S ETS 19 21 sum The sum constraint involves e a set variables INDEXES e an array of integer WEIGHTS e an integer OFFSET e an integer variable SUM and a boolean NOT_EMPTY The constraint ensures that sum WEIGHTS i OFFSET i in INDEXES true states that INDEXES cannot be empty API SUM The boolean NOT_EMPTY set to Constraint sum SetVar INDEXES int WEIGHTS int OFFSET IntVar SUM boolean NOT_ EMPTY 19 22 symmetric The symmetric constraint involves e an array of set variables SETS and e an int
145. tarted 2 1 Installing Choco 3 Choco 3 is a java library based on Java 8 The main library is named choco solver and can be seen as the core library Some extensions are also provided such as choco parsers or choco cpviz and rely on but do not include choco solver 2 1 1 Which jar to select We provide a zip file which contains the following files choco solver 3 3 1 with dependencies jar An ready to use jar file including dependencies it provides tools to de clare a Solver the variables the constraints the search strategies etc In a few words it enables modeling and solving CP problems choco solver 3 3 1 jar A jar file excluding all dependencies and configuration file Enable using choco solver as a dependency of an application Otherwise it provides the same code as the jar with dependencies choco solver 3 3 1 sources jar The source of the core library choco samples 3 3 1 sources jar The source of the artifact choco samples made of problems modeled with Choco It is a good start point to see what it is possible to do with Choco apidocs 3 3 1 zip Javadoc of Choco 3 3 1 logback xml The logback configuration file may be needed when choco solver is used as a library Please refer to README md for more details Note Java 7 compliant jars are also available post fixed with jk7 Extensions There are also official extensions thus maintained by the Choco team They are provided apart from the zip file
146. tatement is either a binary variable 0 1 or a reified constraint satisfied violated Note that the method returns void you cannot reify that constraint which is automatically posted If you wish to reify it use ifThen_reifiable whose implementation differ 21 3 iffhenElse Creates and automatically post a constraint ensuring that if the IF statement is true then the THEN statement must be true as well Otherwise the ELSE statement must be true A statement is either a binary variable 0 1 or a reified constraint satisfied violated Note that the method returns void you cannot reify that constraint which is automatically posted If you wish to reify it use i fThenElse_reifiable whose implementation differ 21 4 reification Creates and automatically post a constraint maintaining the equivalent between a binary variable being equal to 1 and a constraint being satisfied 125 Choco3 Documentation Release 3 3 1 Note that the method returns void you cannot reify that constraint which is automatically posted If you wish to reify 1t use reification_reifiable whose implementation differ 126 Chapter 21 Logical constraints Ro u N CHAPTER 22 Sat solver 22 1 addAtMostNMinusOne Add a clause to the SAT constraint whic states that BOOLVARS BOOLVARS3 IBOOLVARSI API BOOLVARS lt boolean addAtMostNMinusOne BoolVar BOOLVARS Example Solver solv
147. ted Z 2 3 solver solver post ICF distance X Y lt Z solver findAllSolutions DA we Bw N YE The solutions of the problem are e X 1 Y 0 Z 2 X 1 Y 1 Z 2 e X 2Y 1Z 2 92 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 eX 1Y 1Z 3 e X 1 Y 0 Z 3 X 1 Y 1 Z 3 X 2 Y 0 Z 3 X 2Y 1Z 3 X 3Y 1Z 3 18 19 element The element constraint involves either e two variables VALUE and INDEX an array of values TABLE an offset OFFSET and an ordering property SORT SORT must be chosen among none if values in TABLE are not sorted asc if values in TABLE are sorted in increasing order desc if values in TABLE are sorted in decreasing order detect let the constraint detects the ordering of values in TABLE if any default value e or an integer variable VALUE an array of integer variables TABLE an integer variable INDEX and an integer OFFSET The element constraint ensures that VALUE TABLE INDEX OFFSET OFFSET matches INDEX LB and TA BLE 0 0 by default See also element in the Global Constraint Catalog API Constraint element IntVar VALUE int TABLE IntVar INDEX Constraint element IntVar VALUE int TABLE IntVar INDEX int OFFSET String SORT Constraint element IntVar VALUE IntVar TABLE IntVar INDEX int OFFSET Example Solver solver ne
148. tegies If no search strategy is specified in the model Choco 3 will rely on the default one defined by a DefaultSearchBinder in Settings In many cases this strategy will not be sufficient to produce satisfy ing performances and it will be necessary to specify a dedicated strategy using solver set The default search strategy distinguishes variables per types and defines a specific search strategy per each type sequentially applied 1 integer variables and boolean variables IntStrategyFactory domOverWDeg ivars 0 2 set variables SetStrategyFactory force_minDelta_first svars 3 real variables RealStrategyFactory cyclic_middle rvars 8 3 Default search strategies 43 Choco3 Documentation Release 3 3 1 4 objective variable 1f any lower bound or upper bound depending on the ResolutionPolicy Note that ISF lastConflict solver is also plugged in Constants are excluded from search strategies variable scope and the creation order is maintained per types IntStrategyFactory SetStrategyFactory and RealStrategyFactory offer several built in search strategies and a simple framework to build custom searches 8 3 1 Search binder It is possible to override the default search strategy by implementing an ISearchBinder By default a Solver is created with a DefaultSearchBinder declared in its settings An ISearchBinder has the following API void configureSearch Solver solver Configure the search strategy and
149. the logical chain of inferences made by the solver during propagation in an efficient and usable manner In a way they provide some kind of a trace of the behavior of the solver as any operation needs to be explained Explanations have been successfully used for improving constraint programming search process Both complete as the mac dbt algorithm and incomplete as the decision repair algorithm techniques have been proposed Those techniques follow a similar pattern learning from failures by recording each domain modification with its associated explanation provided by the solver and taking advantage of the information gathered to be able to react upon failure by directly pointing to relevant decisions to be undone Complete techniques follow a most recent based pattern while incomplete technique design heuristics to be used to focus on decisions more prone to allow a fast recovery upon failure The current explanation engine is coded to be Asynchronous Reverse Low intrusive and Lazy Asynchronous Explanations are not computed during the propagation Reverse Explanations are computed in a bottom up way from the conflict to the first event generated keeping only relevant events to compute the explanation of the conflict Low intrusive Basically propagators need to implement only one method to furnish a convenient explanation schema Lazy Explanations are computed on request To do so all events are stored during the descent to a c
150. the tree search applying a decision down right branch on going down in the tree search refuting a decision up branch on going up in the tree search to reconsider a decision solution when a solution is got restart search when the search is restarted to a previous node commonly the root node close when the search loop ends contradiction on a failure interruption on the interruption of the search loop With the accurate search monitor one can easily interact with the search loop from pretty printing of a solution to forcing a restart or many other actions The interfaces to implement are IMonitorInitialize IMonitorInitPropagation TMonitorOpenNode IMonitorDownBranch IMonitorUpBranch IMonitorSolution IMonitorRestart IMonitorContradiction IMonitorInterruption 65 Choco3 Documentation Release 3 3 1 e IMonitorClose Most of them gives the opportunity to do something before and after a step The other ones are called after a step For instance NogoodStoreFromRestarts monitors restarts Before a restart is done the nogoods are extracted from the current decision path after the restart has been done the newly created nogoods are added and the nogoods are propagated Thus the framework is almost not intrusive 1 public class NogoodFromRestarts implements IMonitorRestart 2 public void beforeRestart 3 extractNogoodFromPath 4 5 public void afterRestart 6
151. ticLoggerBinder LF4J Defaulting to no operation NOP logger implementation LF4J See http www slf4j org codes html StaticLoggerBinder for further details n n Choco is developed using Logback but other framework are available such as log4j a exhaustive list is given on SL4J Declaring a logging framework is as simple as adding jar files to the classpath of your application Command line For logback java cp choco solver 3 3 1 jar logback core 1 0 13 jar logback classic 1 0 13 jar my project Main Note Logback relies on property file namely logback xml provided in the zip file Where should the configuration files such as logback groovy logback test xml or logback xml be located on the classpath For log4j java cp choco solver 3 3 1 jar sl 4j log4j12 1 7 7 jar my project Main Maven For logback lt dependency gt lt groupId gt ch qos logback lt groupId gt lt artifactId gt logback classic lt artifactId gt lt version gt 1 0 13 lt version gt lt dependency gt For log4j lt dependency gt lt groupId gt org slf4j lt groupId gt lt artifactId gt s1f4j 10g4412 lt artifactId gt lt version gt 1 7 7 lt version gt lt dependency gt 1 Indeed Choco 3 is not a stand alone application but a library likely to be embedded in an application 2 1 Installing Choco 3 11 Choco3 Documentation Release 3 3 1 More detai
152. uced by VARS is used to break tie the variable with the smallest index is selected However it is pos sible to break tie with other VAR_SELECTOR s They should be declared as parameters of WVariablesSelectorWithTies solver set ISF custom new VariableSelectorWithTies new FirstFail new Random 123L new IntDomainMin vars The variable with the smallest domain is selected first If there are more than one variable whose domain size is the smallest ties are randomly broken Note Only variable selectors which implement VariableEvaluator can be used to break ties Very similar operations are achieved in Set Strategy and RealStrategy See solver search strategy IntStrategyFactoryand solver search strategy SetStrategyFactory for built in strategies and selectors 8 2 1 Available variable selectors For integer variables lexico_var_selector random_var_selector minDomainSize_var_selector maxDomainSize_var_selector maxRe gret_var_selector For set variables See solver search strategy selectors variables MaxDelta solver search strategy selectors va For real variables See solver search strategy selectors variables Cyclic 8 2 2 Available value selectors For integer variables min_value_selector mid_value_selector max_value_selector randomBound_value_selector ran dom_value_selector For set variables 42 Chapter 8 Search Strategies Choco3 Documentation Release 3 3 1
153. uentially the strategies in its scope Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API AbstractStrategy sequencer AbstractStrategy strategies 26 18 domOverWDeg d x w x d x denotes the domain size of a variable x and w x its weighted degree The weighted degree of a variable sums the weight of each of the constraint it is involved in where at least 2 variables remains uninstantiated The weight of a constraint is initialized to 7 and increased by one each time a constraint propagation fails during the search where A black box strategy for Int Var which selects the non instantiated variable with the smallest ratio Implementation based on BHLS04 Scope IntVar Factory org chocosolver solver search strategy IntStrategyFactory API 26 15 random_value 151 Choco3 Documentation Release 3 3 1 AbstractStrategy lt IntVar gt domOverWDeg IntVar VARS long SEED IntValueSelector VAL SELECTOR AbstractStrategy lt IntVar gt domOverWDeg IntVar VARS long SEED default min value s lector 26 19 activity A black box strategy for IntVar which selects the non instantiated variable with the largest ratio ao where d x denotes the domain size of a variable x and a x its activity The activity of a variable measures how often the domain of the variable is reducing during the search Then the value with the lea
154. ues defined in VALUES The underlying propagator does not ensure any well defined level of consistency See also global_cardinality in the Global Constraint Catalog API Constraint global_cardinality IntVar VARS int VALUES IntVar OCCURRENCES boolean CLOSED Example 94 Chapter 18 Constraints over integer variables Choco3 Documentation Release 3 3 1 1 Solver solver new Solver 2 IntVar VS VF boundedArray VS 4 0 4 solver 3 int values new int 1 1 2 4 IntVar OCC VF boundedArray OCC 3 0 2 solver 5 solver post ICF global_cardinality VS values OCC true 6 solver findAllSolutions The solutions of the problem are e VS 0 1 VS 1 1 VS 2 2 VS 3 2 OCC O 0 OCC 1 2 OCC 2 2 e VS 0 1 VS 1 2 VS 2 1 VS 3 2 OCC O 0 OCC 1 2 OCC 2 2 e VS 0 1 VS 1 2 VS 2 2 VS 3 1 OCC O 0 OCC 1 2 OCC 2 2 e VS 0 2 VS 1 1 VS 2 1 VS 3 2 OCC O 0 OCC 1 2 OCC 2 2 e VS 0 2 VS 1 1 VS 2 2 VS 3 1 OCC O 0 OCC 1 2 OCC 2 2 e VS 0 2 VS 1 2 VS 2 1 VS 3 1 OCC O 0 OCC 1 2 OCC 2 2 18 23 inverse_channeling The inverse_channeling constraint involves e two arrays of integer variables VARSI and VARS2 and e two integers OFFSETI and OFFSET2 It ensures that VARS1 i OFFSET2 gt VARS2 j OFFSET i It performs
155. ueue in which a propagator of such a priority should be scheduled in public ISearchBinder getSearchBinder Return the default Search binder 53 Choco3 Documentation Release 3 3 1 54 Chapter 10 Settings N CHAPTER 11 Large Neighborhood Search LNS Local search techniques are very effective to solve hard optimization problems Most of them are by nature in complete In the context of constraint programming CP for optimization problems one of the most well known and widely used local search techniques is the Large Neighborhood Search LNS algorithm The basic idea is to iteratively relax a part of the problem then to use constraint programming to evaluate and bound the new solution 11 1 Principle LNS is a two phase algorithm which partially relaxes a given solution and repairs it Given a solution as input the relaxation phase builds a partial solution or neighborhood by choosing a set of variables to reset to their initial domain The remaining ones are assigned to their value in the solution This phase is directly inspired from the classical Local Search techniques Even though there are various ways to repair the partial solution we focus on the technique in which Constraint Programming is used to bound the objective variable and to assign a value to variables not yet instantiated These two phases are repeated until the search stops optimality proven or limit reached The LNSFactory provides pre
156. utions Some solutions of the problem are e BS O 1 BS 1 1 BS 2 1 BS 3 0 e BS O 1 BS 1 0 BS 2 1 BS 3 1 e BS O 1 BS 1 0 BS 2 0 BS 3 0 e BS O 0 BS 1 1 BS 2 0 BS 3 1 BS O 0 BS 1 0 BS 2 0 BS 3 0 22 4 addBoolAndArrayEqVar Add a clause to the SAT constraint which states that BOOLVARS A BOOLVARS 3 A BOOLVARS gt TARGET API boolean addBoolAndArrayEqVar BoolVar BOOLVARS BoolVar TARGET Example 128 Chapter 22 Sat solver Dun e u N Choco3 Documentation Release 3 3 1 Solver solver BoolVar BVARS BoolVar T VF bool T solver findAllSolutions new Solver VF boolArray BS 4 solver SatFactory addBoolAndArrayEqVar BVARS T solver Some solutions of the problem are e BS O 1 BS 1 1 BS 2 1 BS 3 1T 1 e BS O 1 BS 1 1 BS 2 0 BS 3 1 T 0 e BS O 0 BS 1 1 BS 2 0 BS 3 0 T 0 e BS O 0 BS 1 0 BS 2 0 BS 3 0 T 0 22 5 addBoolAndEqVar Add a clause to the SAT constraint which states that LEFT A RIGTH lt gt TARGET API boolean addBoolAndEqVar BoolVar LEFT BoolVar RIGHT BoolVar TARGET Example Solver solver new Solver SatFactory addBoolAndEqvVar L solver findAllSolutions BoolVar L VF bool L solver BoolVar R VF bool R so
157. value of the collection of boolean variables BVARS See also minimum in the Global Constraint Catalog API Constraint minimum IntVar MIN IntVar VARI IntVar VAR2 Constraint minimum IntVar MIN IntVar VARS Constraint minimum BoolVar MIN BoolVar VARS Example Solver solver new Solver IntVar MIN VF enumerated MIN IntVar Y VF enumerated Y 1 IntVar Z VF enumerated Z 2 3 solver post ICF minimum MIN Y Z solver findAllSolutions 3 solver solver solver T 1 y The solutions of the problem are e MIN 2 Y 1 Z 2 e MIN 2 Y 0 Z 2 e MIN 2 Y 1 Z 2 e MIN 3 Y 1 Z 3 MIN 3 Y 0 Z 3 MIN 3 Y 1 Z 3 18 33 mod The mod constraints involves three variables X Y and Z It ensures that X mod Y Z There is no native constraint for mod so this is reformulated with the help of additional variables The API is Constraint mod IntVar X IntVar Y IntVar Z 18 32 minimum 101 Choco3 Documentation Release 3 3 1 Example 1 Solver solver new Solver 2 IntVar X VF enumerated X 2 4 solver IntVar Y VF enumerated Y 1 4 solver 4 IntVar Z VF enumerated Z 1 3 solver 5 solver post ICF mod X Y Z 6 solver findAllSolutions The solutions of the problem are e X 2Y 3Z 2 e X 2 Y 4 Z 2 X 3 Y 2 Z 1 X 3Y 4Z 3 X 4 Y 3 Z 1 18 34 multicost_regular The multicost_regular constraint invo
158. variable events on which the propagator reacts for the vidx variable This method is related to propagate int int a wrong mask prevents the propagator from being informed of an event occurring on a variable Event masks are not nested and all event masks have to be defined 16 2 Properties We distinguish two kinds of propagators Basis propagators that ensure constraints to be satisfied Redundant or Implied propagators that come in addition to some basis propagators in order to get a stronger filtering A basis propagator should be idempotent A redundant propagator does not have to be idempotent Some propagators cannot be idempotent because they are not even monotonic Lagrangian relaxation use of randomness etc Forcing to reach the fix point may decrease performances Important A redundant propagator can directly return ESat TRUE in the body of the isEntailed method Indeed it comes in addition to basis propagators that will already ensure constraint satisfaction 16 3 How to make a propagator idempotent Trying to make a propagator idempotent directly may not be straightforward We provide three implementation possi bilities The coarse option the propagator will perform its fix point by itself The propagator does not react to fine events The coarse filtering algorithm should be surrounded like this 1 idempotent calling a propagator twice has no effect i e calling it wit
159. volves e an integer variable INTEGER and e aset variable SET It ensures that INTEGER is not included in SET API Constraint not_member IntVar INTEGER SetVar SET 19 15 min The min constraint involves e either a set variable SET an integer variable MIN_ELEMENT_VALUE and a boolean NOT_EMPTY It ensures that MIN_ELEMENT_VALUE is equal to the minimum element of SET a set variable SET an array of integer WEIGHTS an integer OFFSET an integer variable MAX_ELEMENT_VALUE and a boolean NOT_EMPTY It ensures that min WEIGHTS i OFFSET i in INDEXES MIN_ELEMENT_VALUE The boolean NOT_EMPTY set to true states that INDEXES cannot be empty API Constraint min SetVar SET IntVar MIN_ELEMENT_VALUE boolean NOT_EMPTY Constraint min SetVar INDEXES int WEIGHTS int OFFSET IntVar MIN_ELEMENT_VALUE boplean NOT_EMPT 19 14 not_member 119 Choco3 Documentation Release 3 3 1 19 16 nbEmpty The nbEmpty constraint involves e an array of set variables SETS and e an integer variable NB_EMPTY_SETS It restricts the number of empty sets in SETS to be equal NB_EMPTY_SET API Constraint nbEmpty SetVar SETS IntVar NB_EMPTY_SETS 19 17 notEmpty The notEmpty constraint involves a set variable SET It prevents SET to be empty API Constraint no
160. volves x and is explained by the lower bound of y The lower bound y needs to be explained A new rule is added to the ruleStore to specify that events on the lower bound of y needs to be kept during the event stack analyse only events generated before the current are relevant When such events are found the ruleStore can be updated until the first event is analyzed The results is a set of branching decisions and a set a propagators which applied altogether leads the conflict and thus explained it 13 3 Explanations for the system Explanations for the system which try to reduce the search space differ from the ones giving feedback to a user about the unsatisfiability of its model Both rely on the capacity of the explanation engine to motivate a failure during the search form system explanations and once the search is complete for user ones Important Most of the time explanations are raw and need to be processed to be easily interpreted by users 13 3 1 Conflict based backjumping When Conflict based Backjumping CBJ is plugged in the search is hacked in the following way On a failure explanations are retrieved From all left branch decisions explaining the failure the last taken return decision is stored to jump back to it Decisions from the current one to the return decision excluded are erased Then the return decision is refuted and the search goes on If the explanation is made of no left branch decision the probl
161. w Solver solver post ICF element V new int 2 solver findAllSolutions Wk Ww N IntVar V VF enumerated V 2 2 solver IntVar I VF enumerated I 0 5 solver 2 5 1 a The solutions of the problem are V 2 1 1 e V 1 1 3 e V 0 1 4 V 1 1 2 e V 2 1 0 18 19 element 93 Choco3 Documentation Release 3 3 1 18 20 eucl_div The eucl_div constraints involves three variables DIVIDEND DIVISOR and RESULT It ensures that DIVIDEND DIVISOR RESULT rounding towards 0 The API is Constraint eucl_div IntVar DIVIDEND IntVar DIVISOR IntVar RESULT Example 1 Solver solver new Solver 2 IntVar X VF enumerated X 1 3 solver 3 IntVar Y VF enumerated Y 1 1 solver 4 IntVar Z VF enumerated Z 2 3 solver 5 solver post ICF eucl_div X Y Z 6 solver findAllSolutions The solutions of the problem are e X 2 Y Z 2 e X 3 Y Z 3 18 21 FALSE The FALSE constraint is always unsatisfied It should only be used with LogicalFactory 18 22 global_cardinality The global_cardinality constraint involves e an array of integer variables VARS e an array of integer VALUES e an array of integer variables OCCURRENCES and e a boolean CLOSED It ensures that each value VALUES i is taken by exactly OCCURRENCES i variables in VARS The boolean CLOSED set to true restricts the domain of VARS to the val
162. y org chocosolver solver search loop monitors SearchMonitorFactory API luby Solver solver int base int grow ICounter counter int limit 27 3 limitNode Defines a limit over the number of nodes allowed during the resolution When the limit is reached the resolution is stopped 155 Choco3 Documentation Release 3 3 1 Factory org chocosolver solver search loop monitors SearchMonitorFactory API void limitNode Solver solver long limit 27 4 limitSolution Defines a limit over the number of solutions allowed during the resolution When the limit is reached the resolution 1s stopped Factory org chocosolver solver search loop monitors SearchMonitorFactory API void limitSolution Solver solver long limit 27 5 limitTime Defines a limit over the run time When the limit is reached the resolution is stopped The limit can be either defined in millisecond or using a String which states the duration like WWd XXh Y Ym ZZs for example 1d2h3m4 5s one day two hours three minutes four seconds and 500 milliseconds lt p gt 2h30m two hours and 30 minutes lt p gt 30 55 30 seconds and 500 ms lt p gt 180s three minutes Factory org chocosolver solver search loop monitors SearchMonitorFactory API void limitTime Solver solver long limit void limitTime Solver solver String duration 27 6 limitThreadTim
163. ying the declaration of clauses by providing some static methods However it should be considered as a last resort due to the verbosity it comes with 22 17 addBoolXorEqVar 135 o o xnu oau e Vv N u a Bw nN a Choco3 Documentation Release 3 3 1 e The second API add one or more clauses defined by two arrays POSLITS and NEGLITS The first array declares positive boolean variables those who should be satisfied the second array declares negative boolean variables those who should not be satisfied API boolean addClauses LogOp TREE boolean addClauses BoolVar Solver SOLVER POSLITS BoolVar NEGLITS Example 1 Solver solver new Solver BoolVar Cl VF bool C1 solver BoolVar C2 VF bool C2 solver BoolVar R VF bool R solver BoolVar AR VF bool AR solver SatFactory addClauses LogOp ifThenElse LogOp nand Cl solver solver findAllSolutions C2 R AR Some solutions of the problem are e Cl 1 C2 0 R 1 AR 1 e Cl 1 C2 0 R 0 AR 1 e C1 0 C2 1 R 1 AR 0 e C1 0 C2 0 R 0 AR 1 Example 2 Solver solver new Solver BoolVar Pl VF bool P1 solver BoolVar P2 VF bool P2 solver BoolVar P3 VF bool P3 solver BoolVar N VF bool N solver SatFactory addClauses new BoolVar P1 solver findAllSolutions P2 P3 new BoolVar N Some solutions of the problem are e Pl
Download Pdf Manuals
Related Search
Related Contents
2ème partie de la circulaire - format : PDF Instruction manual XDVD1262 - Dual Electronics Kramer Electronics FC-5000 User's Manual HP 4600 Digital Flatbed Scanners User`s Manual Philips AVENT DECT baby monitor SCD520 USER MANUAL L`assolement dans le Gard - Réseau Semences Paysannes Copyright © All rights reserved.
Failed to retrieve file