root/trunk/modules/choco/source/search.cl @ 239

Revision 239, 55.4 KB (checked in by x.pechoultres, 7 years ago)

Import CHOCO
  • Property svn:eol-style set to native
  • Property svn:keywords set to Author Date Id Revision
Line 
1// ********************************************************************
2// * CHOCO, version 0.99 feb. 25th 2001                               *
3// * file: main.cl                                                    *
4// *    solving                                                       *
5// * Copyright (C) F. Laburthe, 1999-2000, see readme.txt             *
6// ********************************************************************
7
8// ------------------  File Overview  ---------------------------------
9// * A. Global search                                                 *
10// *   Part 0: object model                                           *
11// *   Part 1: utils and solution management                          *
12// *   Part 2: exploring  one level of branching                      *
13// *   Part 3: Feeding the engine with a library of branching objects *
14// *   Part 4: Using branching classes within globalSearchSolver's    *
15// * B. Local search (generating assignments, improving them by LO)   *
16// *   Part 5: utils and solution management                          *
17// *   Part 6: Feeding the engine with a library of neighborhoods     *
18// *   Part 7: Using neighborhood classes within LocalSearchSolver's  *
19// --------------------------------------------------------------------
20
21// ********************************************************************
22// *   Part 0: object model                                           *
23// ********************************************************************
24
25;choco/AbstractBranching <: Ephemeral(
26;        manager:GlobalSearchSolver,
27;        nextBranching:AbstractBranching)
28
29// v1.013 the range of the abstract interface properties needs be specified
30// v1.013 add a parameter to getNextBranch and finishedBranching (index of the previous branch),
31//        introduce getFirstBranch
32choco/selectBranchingObject :: property(range = any)
33choco/goDownBranch :: property(range = void)
34choco/traceDownBranch :: property(range = void)
35choco/getFirstBranch :: property(range = integer)  // v1.013
36choco/getNextBranch :: property(range = integer)
37choco/goUpBranch :: property(range = void)
38choco/traceUpBranch :: property(range = void)
39choco/finishedBranching :: property(range = boolean)
40choco/branchOn :: property(range = boolean)
41
42// v0.9906
43[selectBranchingObject(b:AbstractBranching) : any
44 -> error("selectBranchingObject not defined on the abstract class AbstractBranching"), unknown]
45[goDownBranch(b:AbstractBranching,x:any,i:integer) : void
46 -> error("goDownBranch not defined on the abstract class AbstractBranching (called with ~S,~S)",x,i)]
47[traceDownBranch(b:AbstractBranching,x:any,i:integer) : void
48 -> error("traceDownBranch not defined on the abstract class AbstractBranching (called with ~S,~S)",x,i)]
49// v0.9906: <thb> definitions required in order to have dynamic dispatch of the above interface methods
50[choco/getFirstBranch(b:AbstractBranching,x:any) : integer          // v1.013
51 -> error("getFirstBranch not defined on the abstract class AbstractBranching (called with ~S)",x), 0]
52[choco/getNextBranch(b:AbstractBranching,x:any,i:integer) : integer // v1.013
53 -> error("getNextBranch not defined on the abstract class AbstractBranching (called with ~S)",x), 0]
54[choco/goUpBranch(b:AbstractBranching,x:any,i:integer) : void
55 -> error("goUpBranch not defined on the abstract class AbstractBranching (called with ~S,~S)",x,i)]
56[choco/traceUpBranch(b:AbstractBranching,x:any,i:integer) : void
57 -> error("traceUpBranch not defined on the abstract class AbstractBranching (called with ~S,~S)",x,i)]
58[choco/finishedBranching(b:AbstractBranching,x:any,i:integer) : boolean
59 -> error("finishedBranching not defined on the abstract class AbstractBranching (called with ~S)",x), true]
60[choco/branchOn(b:AbstractBranching,v:any,n:integer) : boolean
61 -> error("branchOn not defined on the abstract class AbstractBranching (called with ~S,~S)",v,n), false]
62 
63// v0.9907 <thb> must be declared abstract
64(abstract(selectBranchingObject),
65 abstract(goDownBranch),
66 abstract(traceDownBranch),
67 abstract(getFirstBranch),
68 abstract(getNextBranch),
69 abstract(goUpBranch),
70 abstract(traceUpBranch),
71 abstract(finishedBranching))
72
73// v1.0
74(interface(AbstractBranching,
75    selectBranchingObject,
76    goDownBranch,traceDownBranch,goUpBranch,traceUpBranch,
77    getFirstBranch,getNextBranch,finishedBranching,branchOn))
78// v1.0
79(interface(selectBranchingObject),
80 interface(getFirstBranch),
81 interface(getNextBranch),
82 interface(goDownBranch),
83 interface(traceDownBranch),
84 interface(goUpBranch),
85 interface(traceUpBranch),
86 interface(finishedBranching),
87 interface(branchOn))
88 
89choco/LargeBranching <: AbstractBranching()
90choco/BinBranching <: AbstractBranching()
91
92// v1.013 using a binary branching object as a large branching one
93[choco/goUpBranch(b:LargeBranching,x:any,i:integer) : void -> nil]
94[choco/traceUpBranch(b:LargeBranching,x:any,i:integer) : void -> nil]
95[choco/getFirstBranch(b:LargeBranching,x:any) : integer -> 1]
96[choco/getNextBranch(b:LargeBranching,x:any,i:integer) : integer -> 2]
97[choco/finishedBranching(b:LargeBranching,x:any,i:integer) : boolean -> (i = 2)]
98
99// v1.013: a new class for branching objects
100// that may alternatively branch from several sub-branching objects
101choco/CompositeBranching <: LargeBranching(
102     alternatives:AbstractBranching)
103// the only method that should be defined
104[choco/selectBranching(b:CompositeBranching) : AbstractBranching
105 -> error("selectBranching not defined on the abstract class CompositeBranching"), b]
106[choco/selectBranchingObject(b:CompositeBranching) : any
107 -> let alt := selectBranching(b),
108        x   := selectBranchingObject(alt) in tuple(alt,x)]
109[choco/getFirstBranch(b:CompositeBranching,xpair:any) : integer
110  -> let xp := (xpair as tuple(AbstractBranching,any)),
111         alt := (xp[1] as AbstractBranching), x := xp[2] in
112      getFirstBranch(alt,x)]
113[choco/getNextBranch(b:CompositeBranching,xpair:any,i:integer) : integer
114  -> let xp := (xpair as tuple(AbstractBranching,any)),
115         alt := (xp[1] as AbstractBranching), x := xp[2] in
116      getNextBranch(alt,x,i)]
117[choco/goUpBranch(b:CompositeBranching,xpair:any,i:integer) : void
118  -> let xp := (xpair as tuple(AbstractBranching,any)),
119         alt := (xp[1] as AbstractBranching), x := xp[2] in
120      goUpBranch(alt,x,i)]
121[choco/traceUpBranch(b:CompositeBranching,xpair:any,i:integer) : void
122  -> let xp := (xpair as tuple(AbstractBranching,any)),
123         alt := (xp[1] as AbstractBranching), x := xp[2] in
124      traceUpBranch(alt,x,i)]
125[choco/goDownBranch(b:CompositeBranching,xpair:any,i:integer) : void
126  -> let xp := (xpair as tuple(AbstractBranching,any)),
127         alt := (xp[1] as AbstractBranching), x := xp[2] in
128      goDownBranch(alt,x,i)]
129[choco/traceDownBranch(b:CompositeBranching,xpair:any,i:integer) : void
130  -> let xp := (xpair as tuple(AbstractBranching,any)),
131         alt := (xp[1] as AbstractBranching), x := xp[2] in
132      traceDownBranch(alt,x,i)]
133[choco/finishedBranching(b:CompositeBranching,xpair:any,i:integer) : boolean
134  -> let xp := (xpair as tuple(AbstractBranching,any)),
135         alt := (xp[1] as AbstractBranching), x := xp[2] in
136      finishedBranching(alt,x,i)]
137
138// v1.318: introducing heuristics
139choco/VarSelector <: Ephemeral(
140      branching:AbstractBranching)
141[selectVar(vs:VarSelector) : (IntVar U {unknown}) -> error("selectVar is not defined on ~S",vs), unknown]
142(interface(selectVar), interface(VarSelector,selectVar))
143
144choco/MinDomain <: VarSelector(problem:Problem, vars:list<IntVar>)
145[selectVar(vs:MinDomain) : (IntVar U {unknown})
146 -> if (length(vs.vars) > 0) getSmallestDomainUnassignedVar(vs.vars)
147    else getSmallestDomainUnassignedVar(getProblem(getSearchManager(vs.branching)))]
148
149choco/MaxDeg <: VarSelector(problem:Problem, vars:list<IntVar>)
150[selectVar(vs:MaxDeg) : (IntVar U {unknown})
151 -> if (length(vs.vars) > 0) getMostConstrainedUnassignedVar(vs.vars)
152    else getMostConstrainedUnassignedVar(getProblem(getSearchManager(vs.branching)))]
153
154choco/DomDeg <: VarSelector(problem:Problem, vars:list<IntVar>)
155[selectVar(vs:DomDeg) : (IntVar U {unknown})
156 -> if (length(vs.vars) > 0) getDomOverDegBestUnassignedVar(vs.vars)
157    else getDomOverDegBestUnassignedVar(getProblem(getSearchManager(vs.branching)))]
158
159choco/StaticVarOrder <: VarSelector(vars:list[IntVar])
160[selectVar(vs:StaticVarOrder) : (IntVar U {unknown})
161 -> some(v in vs.vars | not(isInstantiated(v)))]
162
163choco/ValIterator <: Ephemeral(
164      branching:AbstractBranching)
165[isOver(vi:ValIterator, x:IntVar, i:integer) : boolean -> error("isOver is not defined on ~S",vi), true]
166[getFirstVal(vi:ValIterator, x:IntVar) : integer -> error("getFirstVal is not defined on ~S",vi), 0]
167[getNextVal(vi:ValIterator, x:IntVar, i:integer) : integer -> error("getNextVal is not defined on ~S",vi), 0]
168( interface(isOver),interface(getFirstVal),interface(getNextVal),
169  interface(ValIterator,isOver,getFirstVal,getNextVal) )
170
171choco/IncreasingDomain <: ValIterator()
172[isOver(vi:IncreasingDomain, x:IntVar, i:integer) : boolean
173 -> (i >= x.sup)]
174[getFirstVal(vi:IncreasingDomain, x:IntVar) : integer
175 -> x.inf]
176[getNextVal(vi:IncreasingDomain, x:IntVar, i:integer) : integer
177 -> getNextDomainValue(x,i)]
178
179choco/DecreasingDomain <: ValIterator()
180[isOver(vi:DecreasingDomain, x:IntVar, i:integer) : boolean
181 -> (i <= x.inf)]
182[getFirstVal(vi:DecreasingDomain, x:IntVar) : integer
183 -> x.sup]
184[getNextVal(vi:DecreasingDomain, x:IntVar, i:integer) : integer
185 -> getPrevDomainValue(x,i)]
186
187choco/ValSelector <: Ephemeral(
188      branching:AbstractBranching)
189[getBestVal(vh:ValSelector, x:IntVar) : integer -> error("getBestVal is not defined on ~S",vh), 0]
190( interface(getBestVal),
191  interface(ValSelector,getBestVal) )
192
193MidValHeuristic <: ValSelector()
194MinValHeuristic <: ValSelector()
195MaxValHeuristic <: ValSelector()
196[getBestVal(vh:MidValHeuristic, x:IntVar) : integer
197 -> x.inf + (x.sup - x.inf) / 2]
198[getBestVal(vh:MinValHeuristic, x:IntVar) : integer
199 -> x.inf]
200[getBestVal(vh:MaxValHeuristic, x:IntVar) : integer
201 -> x.sup]
202
203choco/AssignVar <: LargeBranching(
204     varHeuristic:VarSelector,
205     valHeuristic:ValIterator)
206choco/SplitDomain <: BinBranching(
207     varHeuristic:VarSelector,
208     valHeuristic:ValSelector,
209     dichotomyThreshold:integer = 5)
210choco/AssignOrForbid <: BinBranching(
211     varHeuristic:VarSelector,
212     valHeuristic:ValSelector)
213
214// note: this could be enriched into a LargeBranching, considering LargeDisjunctions
215// v1.010: the branching now explicitly stores the list of disjunctions
216choco/SettleBinDisjunction <: BinBranching(disjunctions:list<Disjunction>)
217
218;choco/GlobalSearchLimit <: Ephemeral()
219;
220;choco/GlobalSearchSolver <: Solver(
221;    // slots for global search
222;   private/stopAtFirstSol:boolean = true,
223;   choco/nbSol:integer = 0,        // nb of solutions found
224;   choco/nbBk:integer = 0,         // nb of backtracks in one tree
225;   choco/nbNd:integer = 0,         // nb of nodes (== nb calls to assign) expanded in one tree
226;   choco/maxNbBk:integer = 100000,   // limit on the total number of backtracks
227;   choco/maxPrintDepth:integer = 5,  // maximal depth of printing
228;    // slots for managing the solutions generated during the search
229;   private/storeBestSol:boolean = false, // do we store the best solution while optimizing
230;   private/branchingComponents:list[AbstractBranching],
231;   private/limits:list<GlobalSearchLimit>
232;   )
233
234choco/Solve <: GlobalSearchSolver()
235
236choco/AbstractOptimize <: GlobalSearchSolver(
237   choco/doMaximize:boolean,
238   choco/objective:IntVar,   // v1.0 moved from Problem to AbstractOptimize
239   choco/lowerBound:integer = MININT,  // the bounds of the objective value
240   choco/upperBound:integer = MAXINT,  // (problem definition + strengthened by the search history -solution found & nogoods-)
241   choco/targetLowerBound:integer = MININT, // v1.08: the bounds for the current tentative search
242   choco/targetUpperBound:integer = MAXINT  // v1.013: generalized this data structure, originally on OptimizeWithRestart
243   )
244
245// v1.0 accessing the objective value of an optimization problem
246// (note that the objective value may not be instantiated)
247choco/getObjectiveValue :: property(range = integer)
248[choco/getObjectiveValue(a:AbstractOptimize) : integer
249 -> (if a.doMaximize a.objective.sup else a.objective.inf)]
250// v1.0 for PaLM
251(abstract(getObjectiveValue))
252
253// v1.05 <thb> getBestObjectiveValue
254[choco/getBestObjectiveValue(a:AbstractOptimize) : integer
255 -> (if a.doMaximize a.lowerBound else a.upperBound)]
256
257// v1.08: the target for the objective function: we are searching for a solution
258// at least as good as this
259[choco/getObjectiveTarget(a:AbstractOptimize) : integer
260 -> (if a.doMaximize a.targetLowerBound
261     else a.targetUpperBound)]
262
263// v1.013 initialization of the optimization bound data structure
264[choco/initBounds(a:AbstractOptimize) : void
265 -> let obj := a.objective in
266     (a.lowerBound := getInf(obj), a.upperBound := getSup(obj),
267      a.targetLowerBound := getInf(obj), a.targetUpperBound := getSup(obj))]
268
269// v1.02: returns a boolean indicating whether the search found solutions or not
270[choco/getFeasibility(a:GlobalSearchSolver) : boolean
271 -> a.problem.feasible]
272
273// v1.325: change the interface of search limit objects
274choco/newNode :: property(range = boolean)
275choco/endNode :: property(range = void)
276choco/reset :: property(range = void)
277// Basic limits implementation:
278[newNode(lim:GlobalSearchLimit,a:GlobalSearchSolver) : boolean -> true]
279 // returns true if it allows to create the node  (side effect: increment an internal counter when returning true)
280 // newNode is called by GlobalSearchSolver before each pushWorld, returning false cause backtrack (default: returns true)
281[endNode(lim:GlobalSearchLimit,a:GlobalSearchSolver) : void -> nil]
282 // increment a local counter if needed (default: does nothing)
283 // endNode is called by  GlobalSearchSolver after each popWorld
284[reset(lim:GlobalSearchLimit, start:boolean) : void -> nil]
285 // reset the internal counter to its internal value and possibly accumulate its old value in another slot
286 //  with start=true: called at the end of the tree search
287(interface(newNode), interface(endNode), interface(reset))
288(interface(GlobalSearchLimit, newNode, endNode, reset))
289
290// special case: units that are measured by accumulating a quantity
291[reset(lim:CounterLimit, start:boolean) : void -> if start lim.nb := 0 else lim.totNb :+ lim.nb]
292[newNode(lim:CounterLimit,a:GlobalSearchSolver) : boolean -> (lim.nb <= lim.maxNb)]
293[self_print(lim:CounterLimit) : void
294-> if (lim.nb = 0) printf("tot=~S~A",lim.totNb,lim.unit) else printf("~S~A",lim.nb,lim.unit)]
295
296// checks whether the creation of a new node is allowed. If so, register it in its own counters
297[newNode(lim:NodeLimit,a:GlobalSearchSolver) : boolean
298-> lim.nb :+ 1, newNode@CounterLimit(lim,a)]
299; -> if (lim.nb < lim.maxNb) (lim.nb :+ 1, true)  else false]
300[endNode(lim:BacktrackLimit,a:GlobalSearchSolver) : void -> lim.nb :+ 1]
301
302[newNode(lim:TimeLimit, algo:GlobalSearchSolver) : boolean -> (time_read() <= lim.maxNb)]
303[reset(lim:TimeLimit, start:boolean) : void
304-> if start time_set() else lim.totNb :+ time_get()]
305[self_print(lim:TimeLimit) : void
306-> let t := time_read() in
307    (if (t = 0) printf("tot=~S~A",lim.totNb,lim.unit) else printf("~S~A",t,lim.unit))]
308
309// LDS limit
310// branchCounter accumulates accounts of 1 per left branch + 2 per second branch, ...
311;DiscLimit <: GlobalSearchLimit(branchCounter:integer = 0,
312;                               maxNbDisc:integer)
313;(store(branchCounter))
314[newNode(lim:DiscLimit, algo:GlobalSearchSolver) : boolean
315-> lim.branchCounter :+ 1,
316   (lim.branchCounter - (world?() - algo.baseWorld + 1) <= lim.maxNbDisc)]
317[reset(lim:DiscLimit, start:boolean) : void
318-> if start lim.branchCounter := 0]
319[self_print(lim:DiscLimit) : void -> printf("~S~A",lim.branchCounter - (world?() - lim.searchSolver.baseWorld + 1),lim.unit)]
320
321choco/BranchAndBound <: AbstractOptimize()
322
323// used for optimization by branch and bound
324choco/OptimizeWithRestarts <: AbstractOptimize(
325   choco/nbIter:integer = 0,
326   choco/baseNbSol:integer = 0,
327   choco/nbBkTot:integer = 0, // total nb of backtracks (all trees in the optimization process)
328   choco/nbNdTot:integer = 0  // total nb of nodes expanded in all trees
329   )
330
331[choco/copyParameters(oldSolver:GlobalSearchSolver, newSolver:GlobalSearchSolver) : void
332 -> when d := get(maxPrintDepth, oldSolver) in newSolver.maxPrintDepth := d,
333    when storeBest := get(maxSolutionStorage, oldSolver) in newSolver.maxSolutionStorage := storeBest, // v1.013
334    when varsShow := get(varsToShow, oldSolver) in newSolver.varsToShow := varsShow]
335
336// v1.08 new name attachGlobalSearchSolver -> attach
337[choco/attach(newSolver:GlobalSearchSolver, pb:Problem) : void
338 -> ;when oldSolver := get(globalSearchSolver,pb) in
339    ;     copyParameters(oldSolver, newSolver),
340    pb.globalSearchSolver := newSolver,
341    newSolver.problem := pb]
342
343// v1.0, v1.013: more precise return type
344[composeGlobalSearch(algo:GlobalSearchSolver, l:list[AbstractBranching]) : type[algo] // GlobalSearchSolver
345 -> let n := length(l), l2 := l in // v1.018: no longer a copy // list{copy(t) | t in l} in
346     (algo.branchingComponents := l2,
347      for i in (1 .. n - 1)
348         (l2[i] as AbstractBranching).nextBranching := (l2[i + 1] as AbstractBranching),
349      for comp in l2 comp.manager := algo,
350      algo)]
351
352// ********************************************************************
353// *   Part 1: utils and solution management                          *
354// ********************************************************************
355
356[choco/getSmallestDomainUnassignedVar(pb:Problem) : (IntVar U {unknown})
357 -> getSmallestDomainUnassignedVar(pb.vars)]
358
359// v1.02 inlined <thb>
360[choco/getSmallestDomainUnassignedVar(l:list[IntVar]) : (IntVar U {unknown})
361 => let minsize := MAXINT, v0:(IntVar U {unknown}) := unknown in
362        (for v in list{v in l | not(isInstantiated(v))}
363           let dsize := getDomainSize(v) in
364              (if (dsize < minsize)
365                  (minsize := dsize, v0 := v)),
366         v0)]
367
368// v1.010: a new variable selection heuristic
369[choco/getDomOverDegBestUnassignedVar(pb:Problem) : (IntVar U {unknown})
370 -> getDomOverDegBestUnassignedVar(pb.vars)]
371[choco/getDomOverDegBestUnassignedVar(l:list[IntVar]) : (IntVar U {unknown})
372 => let minsize := MAXINT, maxdeg := 0, v0:(IntVar U {unknown}) := unknown in
373        (for v in list{v in l | not(isInstantiated(v))}
374           let dsize := getDomainSize(v), deg := getDegree(v) in
375              (if (dsize * maxdeg < minsize * deg)
376                  (minsize := dsize, maxdeg := deg,v0 := v)),
377         v0)]
378
379// v1.010: a new variable selection heuristic
380[choco/getMostConstrainedUnassignedVar(pb:Problem) : (IntVar U {unknown})
381 -> getMostConstrainedUnassignedVar(pb.vars)]
382[choco/getMostConstrainedUnassignedVar(l:list[IntVar]) : (IntVar U {unknown})
383 => let maxdeg := 0, v0:(IntVar U {unknown}) := unknown in
384        (for v in list{v in l | not(isInstantiated(v))}
385           let deg := getDegree(v) in
386              (if (maxdeg < deg)
387                  (maxdeg := deg, v0 := v)),
388         v0)]
389
390// stores information from the current state in the next solution of the problem
391// note: only instantiated variables are recorded in the Solution object
392//       either all variables or a user-defined subset of them are recorded
393//       this may erase a soolution that was previously stored in the ith position
394//       this may also increase the size of the pb.solutions vector.
395// v1.013: code has been redesigned
396[choco/storeCurrentSolution(a:Solver) : void
397 -> let sol := makeSolutionFromCurrentState(a) in
398        storeSolution(a,sol)]
399[choco/makeSolutionFromCurrentState(a:Solver) : Solution
400 -> let lvar := (if a.varsToStore a.varsToStore else a.problem.vars),
401        // lvar is a reference list of variables of interest, which value is to be recorded in a solution
402        nbv := length(lvar),                // v0.28: size vs. length
403        sol := makeSolution(a,nbv) in
404     (;sol.time := time_read(), // v1.013
405      ;sol.nbBk := a.nbBk,
406      ;sol.nbNd := a.nbNd,
407      case a (AbstractOptimize
408                sol.objectiveValue := getObjectiveValue(a)),
409      for i in (1 .. nbv)
410        let v := lvar[i] in
411           (if isInstantiated(v)  // bug in v1.324 !!!!
412               sol.lval[i] := v.value),
413      sol)]
414[choco/storeSolution(a:Solver,sol:Solution) : void
415 -> //[SVIEW] store solution ~S // sol,
416    if (length(a.solutions) = a.maxSolutionStorage)
417       a.solutions := (a.solutions << 1),
418    a.solutions :add sol] // v1.014
419
420// v1.013 no longer an integer parameter
421[choco/existsSolution(a:Solver) : boolean
422 -> (length(a.solutions) > 0)]
423
424// v1.013 no longer an integer parameter
425[choco/restoreBestSolution(a:Solver) : void
426 -> restoreSolution(last(a.solutions))]
427
428[choco/restoreSolution(s:Solution) : void
429 -> let a := s.algo,
430        lvar := (if a.varsToStore a.varsToStore else a.problem.vars),
431        lval := s.lval,
432        nbv := length(lvar) in        // v0.28: size vs. length
433     (for i in (1 .. nbv)
434         (if (lval[i] != unknown)
435             setVal(lvar[i],lval[i])),
436      propagate(a.problem))]
437
438// printing the current state of domains when a solution has been reached
439[showSolution(a:Solver)
440 -> if (verbose() >= STALK)
441      let S := (if (a.varsToShow) a.varsToShow
442                else a.problem.vars) in
443        for x in S printf("~S\n",x)]
444;        for x in S printf("~I\n",self_print(x))]
445
446// ********************************************************************
447// *   Part 2: exploring  one level of branching                      *
448// ********************************************************************
449
450// explore is a general method that applies on any new descendent or AbtractBranching
451choco/explore :: property()
452;(interface(AbstractBranching, explore))
453
454// The heart of the search engine:
455// exploring the branches of one choice point
456[choco/explore(b:AbstractBranching,n:integer) : boolean
457 -> let algo := b.manager, pb := algo.problem in
458     (when v := selectBranchingObject(b) in branchOn(b,v,n)
459      else (when b2 := get(nextBranching,b) in
460                    explore(b2,n)
461            else (recordSolution(algo),
462                  showSolution(algo),
463                  algo.stopAtFirstSol)))]
464
465// v1.010: <thb> new method responsible for expanding a node of the search tree
466// once the branching object has been generated
467[choco/branchOn(b:LargeBranching,v:any,n:integer) : boolean
468 -> let algo := b.manager, pb := algo.problem,
469        nodeSuccess := false, nodeFinished := false, i := getFirstBranch(b,v) in
470      (newTreeNode(algo),
471       try
472          (until (nodeSuccess | nodeFinished)
473             let branchSuccess := false in
474               (try (checkCleanState(pb.propagationEngine),
475                     pushWorld(pb),
476                     if (n <= algo.maxPrintDepth)
477                        traceDownBranch(b,v,i),
478                     goDownBranch(b,v,i),
479                     if explore(b,n + 1) branchSuccess := true)
480                catch contradiction nil,
481                if not(branchSuccess)
482                  (popWorld(pb),
483                   endTreeNode(algo),
484                   postDynamicCut(algo),
485                   if (n <= algo.maxPrintDepth)
486                      traceUpBranch(b,v,i),
487                   goUpBranch(b,v,i)),
488                if branchSuccess nodeSuccess := true,
489                if not(finishedBranching(b,v,i)) i := getNextBranch(b,v,i)
490                else nodeFinished := true
491                ))
492       catch contradiction nodeSuccess := false,
493       nodeSuccess)]
494
495// v1.103: the branches of a BinBranching are no longer labelled with a boolean
496// but with an integer (1/2) like LargeBranching
497[choco/branchOn(b:BinBranching,v:any,n:integer) : boolean
498 -> let algo := b.manager, pb := algo.problem, success := false in
499      (newTreeNode(algo),
500       try (checkCleanState(pb.propagationEngine),
501            pushWorld(pb),
502            if (n <= algo.maxPrintDepth)
503               traceDownBranch(b,v,1),
504            goDownBranch(b,v,1),
505            if explore(b,n + 1) success := true)
506       catch contradiction nil,
507       if not(success)
508         (popWorld(pb),
509          endTreeNode(algo),
510          try (postDynamicCut(algo),
511               if (n <= algo.maxPrintDepth)
512                  traceDownBranch(b,v,2),
513               goDownBranch(b,v,2),
514               if explore(b,n + 1) success := true)
515          catch contradiction success := false),
516       success)]
517
518// ********************************************************************
519// *   Part 3: Feeding the engine with a library of branching objects *
520// ********************************************************************
521
522// library of choice points (Branching classes)
523// v1.010: now caching the middle of the domain (and not recomputing it)
524;choco/SplitDomain <: BinBranching(dichotomyThreshold:integer = 5)
525[selectBranchingObject(b:SplitDomain) : any
526 -> when x := selectVar(b.varHeuristic) in
527       (if (getDomainSize(x) >= b.dichotomyThreshold)  // <ega> v0.9906: typo
528           tuple(x, getBestVal(b.valHeuristic, x))
529        else unknown)
530    else unknown]
531
532[goDownBranch(b:SplitDomain,x:any,first:integer) : void
533 -> let xp := (x as tuple(IntVar, integer)),
534        v := (xp[1] as IntVar), mid := (xp[2] as integer) in
535     (if (first = 1) setMax(v,mid)
536      else setMin(v,mid + 1),
537      propagate(b.manager.problem) )]
538[traceDownBranch(b:SplitDomain,x:any,first:integer) : void
539 -> let xp := (x as tuple(IntVar, integer)),
540        v := (xp[1] as IntVar), mid := (xp[2] as integer) in
541     (if (first = 1) //[STALK] !!! branch ~S: ~S <= ~S // world?(),v,mid
542      else //[STALK] !!! branch ~S: ~S > ~S // world?(),v,mid
543     )]  // <ega> v0.9907 removed ugly call to propagate !!
544
545;choco/AssignOrForbid <: VarBinBranching()
546// v1.010: now caching the best value in the domain (and not recomputing it)
547[selectBranchingObject(b:AssignOrForbid) : any
548 -> when x := selectVar(b.varHeuristic) in
549         tuple(x, getBestVal(b.valHeuristic, x))
550    else unknown]
551
552[goDownBranch(b:AssignOrForbid,x:any,first:integer) : void
553 -> let xp := (x as tuple(IntVar, integer)),
554        v := (xp[1] as IntVar), best := (xp[2] as integer) in
555     (if (first = 1) setVal(v,best)
556      else remVal(v,best),
557      propagate(b.manager.problem)) ]
558[traceDownBranch(b:AssignOrForbid,x:any,first:integer) : void
559 -> let xp := (x as tuple(IntVar, integer)),
560        v := (xp[1] as IntVar), best := (xp[2] as integer) in
561     (if (first = 1) //[STALK]  !! branch ~S: ~S == ~S // world?(),v,best
562      else //[STALK]  !! branch ~S: ~S !== ~S // world?(),v,best
563     )]
564
565;choco/AssignVar <: LargeBranching()
566[selectBranchingObject(b:AssignVar) : any
567 -> selectVar(b.varHeuristic)]
568
569// v1.013
570[finishedBranching(b:AssignVar,x:any,i:integer) : boolean
571 -> let y := (x as IntVar) in
572      isOver(b.valHeuristic, y, i)]
573[getFirstBranch(b:AssignVar,x:any) : integer
574 -> let y := (x as IntVar) in
575      getFirstVal(b.valHeuristic, y)]
576[getNextBranch(b:AssignVar,x:any,i:integer) : integer
577 -> let y := (x as IntVar) in
578      getNextVal(b.valHeuristic, y, i)]
579[goDownBranch(b:AssignVar,x:any,i:integer) : void
580 -> let y := (x as IntVar) in
581      (setVal(y,i), propagate(b.manager.problem))]
582[goUpBranch(b:AssignVar,x:any,i:integer) : void
583 -> let y := (x as IntVar) in
584      (remVal(y,i), propagate(b.manager.problem))]
585[traceDownBranch(b:AssignVar,x:any,i:integer) : void
586 -> let y := (x as IntVar) in
587      //[STALK]  !! branch ~S: ~S == ~S // world?(),y,i
588]     
589[traceUpBranch(b:AssignVar,x:any,i:integer) : void
590 -> let y := (x as IntVar) in
591      //[STALK]  !! branch ~S: ~S !== ~S // world?(),y,i
592]     
593
594// note: this could be enriched into a LargeBranching, considering LargeDisjunctions
595// v1.010: store the disjunction list into the branching object
596[selectBranchingObject(b:SettleBinDisjunction) : any
597 -> some(c in b.disjunctions |
598           not(knownStatus(c,1)) & not(knownTargetStatus(c,1))     // v1.02 using the new status methods
599           & not(knownStatus(c,2)) & not(knownTargetStatus(c,2)) )]  // v1.05 typo <franck>
600[goDownBranch(b:SettleBinDisjunction,d:any,first:integer) : void
601 -> case d
602     (Disjunction (setBranch(d,first,true),
603                   propagate(b.manager.problem)),
604      any error("Typing error: should be a Disjunction"))]
605[traceDownBranch(b:SettleBinDisjunction,d:any,first:integer) : void
606 -> case d
607     (Disjunction
608        (if (first = 1) //[STALK] !! branch ~S[1]: try ~S // world?(),d.const1
609         else //[STALK] !! branch ~S[2]: try ~S // world?(),d.const2
610        ),
611      any error("Typing error: should be a Disjunction"))]
612
613// ********************************************************************
614// *   Part 4: Using branching classes within globalSearchSolver's    *
615// ********************************************************************
616
617// The main method is run
618//   it calls a few general submethods
619
620;(interface(GlobalSearchSolver, run,
621;                               newTreeSearch, endTreeSearch,
622;                               newNode,       endNode,
623;                               recordSolution,showSolution,
624;                               postDynamicCut))))
625
626// general definitions, v1.325: new use of limits
627[newTreeSearch(a:GlobalSearchSolver) : void
628 -> assert(a.problem.globalSearchSolver = a), // v1.011 <thb> consistency check
629    for lim in a.limits reset(lim,true),
630    a.nbSol := 0, a.baseWorld := world?()]   
631[endTreeSearch(algo:GlobalSearchSolver) : void
632 -> for lim in algo.limits reset(lim,false),
633    trace(SVIEW,"solve => ~A solution ~S\n",(if not(algo.problem.feasible) "no" else string!(algo.nbSol)),algo.limits)]
634                               
635[newTreeNode(a:GlobalSearchSolver) : void
636 -> for lim in a.limits
637       (if not(newNode(lim,a))
638           raiseContradiction(a.problem.propagationEngine,lim))]
639[endTreeNode(a:GlobalSearchSolver) : void
640-> for lim in a.limits endNode(lim,a)]
641
642[recordSolution(a:GlobalSearchSolver) : void
643 -> a.problem.feasible := true, a.nbSol :+ 1,
644    trace(SVIEW,"... solution [~S]\n",a.limits),  // v1.011 <thb>
645    if (a.maxSolutionStorage > 0) storeCurrentSolution(a)]  // v1.013
646[postDynamicCut(a:GlobalSearchSolver) : void                // v1.019
647 -> nil]
648[recordSolution(a:AbstractOptimize) : void
649 -> let obj := a.objective, objval := getObjectiveValue(a) in
650       (a.problem.feasible := true, a.nbSol :+ 1,
651        trace(SVIEW,"... solution with ~A:~S [~S]\n",obj.name,objval,a.limits),  // v1.011 <thb>
652        setBound(a),  // v1.013
653        setTargetBound(a),
654        if (a.maxSolutionStorage > 0) storeCurrentSolution(a))] // v1.013
655
656// v1.013 resetting the optimization bounds
657[setBound(a:AbstractOptimize) : void
658 -> let objval := getObjectiveValue(a) in
659       (if a.doMaximize a.lowerBound :max objval
660        else a.upperBound :min objval)]
661// v1.08: resetting the values of the target bounds (bounds for the remaining search)
662[setTargetBound(a:AbstractOptimize) : void
663 -> if a.doMaximize setTargetLowerBound(a)
664    else setTargetUpperBound(a)]
665[setTargetLowerBound(a:AbstractOptimize) : void
666 -> let newBound := a.lowerBound + 1 in
667     (if not(a.problem.feasible) trace(STALK,"search first sol ...")
668      else (a.targetLowerBound := newBound,
669            trace(STALK,"search target: ~A >= ~S ... ",a.objective.name,newBound)) )]
670[setTargetUpperBound(a:AbstractOptimize) : void
671 -> let newBound := a.upperBound - 1 in
672     (if not(a.problem.feasible) trace(STALK,"search first sol ...")
673      else (a.targetUpperBound := newBound,
674            trace(STALK,"search target: ~A <= ~S ... ",a.objective.name,newBound)) )]
675// v1.013: propagating the optimization cuts from the new target bounds
676[postTargetBound(a:AbstractOptimize) : void
677 -> if a.doMaximize postTargetLowerBound(a)
678    else postTargetUpperBound(a)]
679[postTargetLowerBound(a:AbstractOptimize) : void
680 -> setMin(a.objective, a.targetLowerBound)]
681[postTargetUpperBound(a:AbstractOptimize) : void
682 -> setMax(a.objective, a.targetUpperBound)]
683
684// v1.325: new use of limit objects
685[newTreeSearch(a:OptimizeWithRestarts) : void
686 -> newTreeSearch@GlobalSearchSolver(a),
687    a.nbIter :+ 1,
688    a.baseNbSol := a.nbSol,
689    postTargetBound(a),  // v1.013
690    propagate(a.problem)]
691[endTreeSearch(a:OptimizeWithRestarts) : void
692 -> for lim in a.limits reset(lim,false),
693    backtrack(a.baseWorld)]
694   
695[postDynamicCut(a:OptimizeWithRestarts) : void
696 -> nil]
697
698// generic method
699[choco/run(algo:GlobalSearchSolver) : void
700 -> error("run is not implemented on ~S",algo)]
701
702// searching for one solution
703// v1.02: note: the initial propagation must be done before pushing any world level. It is therefore kept before restoring a solution
704[choco/run(algo:Solve) : void
705 -> newTreeSearch(algo),
706    let pb := algo.problem, feasibleRootState := true in
707       (try propagate(pb)
708        catch contradiction feasibleRootState := false,
709        if feasibleRootState
710          (try (pushWorld(pb),
711                explore(algo.branchingComponents[1],1))
712           catch contradiction popWorld(pb)),
713           try (if (algo.maxSolutionStorage > 0 & // v1.011 <thb> restoring best solution
714                    not(algo.stopAtFirstSol) &
715                    existsSolution(algo))
716                  restoreBestSolution(algo) )
717           catch contradiction error("contradiction while restoring the best solution found: BUG !!")),
718    endTreeSearch(algo) ]  // v1.02: returns void
719
720// v0.25 adding a world level for avoiding conflicts between the proof of optimality
721// and the restoring of best sol
722// v1.02: note: the initial propagation must be done before pushing any world level. It is therefore kept before restoring a solution
723[choco/run(algo:BranchAndBound) : void
724 -> newTreeSearch(algo),
725    let pb := algo.problem, feasibleRootState := true in
726       (try propagate(pb)
727        catch contradiction feasibleRootState := false,
728        if feasibleRootState
729          (try (pushWorld(pb),
730                explore(algo.branchingComponents[1],1),
731                popWorld(pb))
732           catch contradiction popWorld(pb),  // v1.02 if there was a contradiction, it happened during explore
733           try (if (algo.maxSolutionStorage > 0 & existsSolution(algo)) // v0.9907 <thb> checking that one solution has indeed been found
734                   restoreBestSolution(algo) )  // 1.011: restore the best solution out of the above try...catch
735           catch contradiction error("contradiction while restoring the best solution found: BUG !!")),
736        endTreeSearch(algo) )] // v0.9907 <thb>  // v1.02 returns void
737
738// v1.013: we use  targetBound data structures for the optimization cuts
739[postDynamicCut(a:BranchAndBound) : void
740 -> postTargetBound(a),
741    propagate(a.problem)]
742[newTreeSearch(a:BranchAndBound) : void
743 -> initBounds(a),
744    for lim in a.limits reset(lim,true)]
745
746// v1.02: removed reference to baseWorld
747[endTreeSearch(a:BranchAndBound) : void
748 -> for lim in a.limits reset(lim,false),
749    if a.problem.feasible
750       //[SVIEW] solve => ~S sol, best:~S [~S]// a.nbSol,(if a.doMaximize a.lowerBound else a.upperBound),a.limits
751    else //[SVIEW] solve => no sol [~S]// a.limits
752]
753
754[newLoop(a:OptimizeWithRestarts) : void -> initBounds(a), time_set()] // should we call a fullReset on limits ? (to reset cumulated counter?)
755[endLoop(a:OptimizeWithRestarts) : void
756 -> let t := time_get() in
757    trace(SVIEW,"Optimisation over => ~A(~A) = ~S found in ~S iterations, [~S], ~S ms.\n",
758           (if a.doMaximize "max" else "min"),a.objective.name,
759           getBestObjectiveValue(a),  // v1.013 using the accessor
760           a.nbIter,a.limits,t)]
761// v1.08
762[recordNoSolution(a:OptimizeWithRestarts) : void
763  -> let obj := a.objective, objtgt := getObjectiveTarget(a) in
764       (trace(SVIEW,"... no solution with ~A:~S [~S]\n",obj.name,objtgt,a.limits),
765        if a.doMaximize  // v1.014
766           a.upperBound :min objtgt - 1
767        else a.lowerBound :max objtgt + 1)]
768
769// v1.08: loop until the lower bound equals the upper bound
770[oneMoreLoop(a:OptimizeWithRestarts) : boolean
771 -> (a.lowerBound < a.upperBound)]
772
773// v1.02: note: the initial propagation must be done before pushing any world level. It is therefore kept before restoring a solution
774// v1.08: <ega> requires a more careful management of lower/upperBounds
775[choco/run(algo:OptimizeWithRestarts) : void // v1.02 returns void
776 -> let w := world?() + 1, pb := algo.problem, finished := false in
777      (newLoop(algo),
778       try propagate(pb)
779       catch contradiction (finished := true, recordNoSolution(algo)),
780       if not(finished)   // v1.014
781         (pushWorld(pb),
782          while oneMoreLoop(algo)
783            let foundSolution := false in
784             (try (newTreeSearch(algo),
785                if explore(algo.branchingComponents[1],1)
786                   foundSolution := true)
787              catch contradiction nil,
788              endTreeSearch(algo),
789              if not(foundSolution) recordNoSolution(algo)
790             ),
791          assert(world?() = w),
792          popWorld(pb)),
793       endLoop(algo),
794       if (algo.maxSolutionStorage > 0 & existsSolution(algo)) // v0.9907 <thb> checking that one solution has indeed been found
795          restoreBestSolution(algo))]  // v1.02 returns void
796// ********************************************************************
797// *   Part 5: utils and solution management                          *
798// ********************************************************************
799
800// V0.9907
801[choco/makeConflictCount() : ConflictCount
802 -> ConflictCount(nbViolatedConstraints = 0,
803;                  conflictingVars = list<IntVar>(),
804;                  assignedThenUnassignedVars = list<IntVar>(),
805                  lastAssignedVar = 0) ]
806
807[choco/attachInvariantEngine(pb:Problem, ie:InvariantEngine) : void
808 -> pb.invariantEngine := ie,
809    ie.problem := pb]
810
811// returns +1 when the status of c changes from true to false when v goes from a to b
812//         -1                                   false to true
813//         0  when c does not change (remains satisfied or violated)
814[private/unitaryDeltaConflict(v:IntVar,a:integer,b:integer,c:AbstractConstraint) : integer
815 -> assert(v.value = a),
816    assert(testIfInstantiated(c)),
817    let OKbefore := not(c.violated),
818        OKafter := OKbefore in
819      (v.value := b, OKafter := testIfTrue(c), v.value := a,
820       //[LDEBUG]:  -- flipping ~S from ~S to ~S: ~S goes from ~S to ~S // v,a,b,c,OKbefore,OKafter,
821       if (OKafter = OKbefore) 0  // no change for the constraint
822       else if (OKbefore) 1       // the constraint became a conflict
823       else -1) ]                 // the conflicting constraint was repaired
824
825// computes the change in the number of conflicting constraints
826// when v is flipped from value a to b
827[choco/deltaNbConflicts(v:IntVar,a:integer,b:integer) : integer
828 -> let delta := 0 in
829      (for c in v.constraints
830          delta :+ unitaryDeltaConflict(v,a,b,c),
831       //[LDEBUG] flipping ~S from ~S to ~S yields delta = ~S // v,a,b,delta,
832       delta)]
833
834[choco/getMinConflictValue(v:IntVar) : integer
835 -> let a := v.value, minDelta := MAXINT, bestvalue := a in
836       (for b in (domain(v) but a)
837            let delta := deltaNbConflicts(v,a,b) in
838               (//[LDEBUG] for ~S(~S), value ~S adds ~S conflicts // v,a,b,delta,
839                if (delta < minDelta) (minDelta := delta, bestvalue := b)),
840        bestvalue)]
841
842// saving and retrieving assignments
843[choco/computeConflictAccount(ie:ConflictCount) : void
844 -> let p := ie.problem in
845       (for v in p.vars
846            v.nbViolatedConstraints := 0,
847        ie.nbViolatedConstraints := 0,
848        for c in {c2 in p.constraints | testIfInstantiated(c2)}  // should be extended for handling global constraints
849           (if testIfTrue(c)  // v0.26 wrong interface call: testIfTrue instead of testIfSatisfied
850               c.violated := false
851            else (c.violated := true,
852                  ie.nbViolatedConstraints :+ 1,
853                  case c (UnIntConstraint c.v1.nbViolatedConstraints :+ 1,
854                          BinIntConstraint (c.v1.nbViolatedConstraints :+ 1,
855                                            c.v2.nbViolatedConstraints :+ 1),
856                          LargeIntConstraint                // v0.15
857                            for v in c.vars
858                                v.nbViolatedConstraints :+ 1,
859                          any error("Cannot build assignment with such constraint ~S",c)))),
860        ie.conflictingVars := list<IntVar>{v in p.vars | v.inf < v.sup & v.nbViolatedConstraints > 0}) ]
861
862// this function is called when the local search mode is started after a global search
863// (feasible mode)
864[choco/resetInvariants(ie:InvariantEngine) : void -> error("resetInvariants should be defined for ~S",ie)]
865[choco/resetInvariants(ie:ConflictCount) : void
866 -> let p := ie.problem in
867       (// all constraints are either yet uninstantiated, or trivially satisfied
868        assert(forall(c in p.constraints |
869                        (not(testIfInstantiated(c)) | testIfTrue(c)))),
870        for c in p.constraints c.violated := false,
871        for v in p.vars v.nbViolatedConstraints := 0,
872        ie.nbViolatedConstraints := 0)]
873
874// interface
875[choco/getLocalSearchObjectiveValue(ie:InvariantEngine) : integer -> error("getObjective should be defined for ~S",ie), 0]
876[choco/getLocalSearchObjectiveValue(ie:ConflictCount) : integer -> ie.nbViolatedConstraints]
877
878[choco/restoreBestAssignment(algo:LocalSearchSolver) : void
879 -> //[LTALK] restoring the best assignment found so far //,
880    let p := algo.problem in
881       (for v in {v1 in p.vars | v1.inf < v1.sup}
882            v.value := v.savedAssignment,
883        computeConflictAccount(p.invariantEngine))]
884
885[choco/saveAssignment(algo:LocalSearchSolver) : void
886 -> for v in algo.problem.vars v.savedAssignment := v.value]
887
888// v0.9907
889;[choco/setFeasibleMode(pb:Problem, b:boolean) : void
890; -> if (b != pb.feasibleMode)
891;       (if (b = false)
892;           let ie := pb.invariantEngine,
893;               l1 := list<IntVar>{v in pb.vars | v.inf = v.sup},
894;               l2 := list<IntVar>{v in pb.vars | v.inf != v.sup} in
895;            (ie.assignedThenUnassignedVars := (l1 /+ l2),
896;             ie.lastAssignedVar := length(l1),
897;             resetInvariants(ie)),
898;         pb.feasibleMode := false)]
899[choco/setFeasibleMode(pb:Problem, b:boolean) : void
900 -> if (b != pb.feasibleMode)
901       (if (b = false)
902           let ie := (pb.invariantEngine as ConflictCount),
903               l := ie.assignedThenUnassignedVars in
904            (shrink(l, 0),
905             for v in pb.vars
906                (if (v.inf = v.sup) add(l,v)),
907             let n := length(l) in
908               ie.lastAssignedVar := n,
909             for v in pb.vars
910                (if (v.inf != v.sup) add(l,v)),
911             resetInvariants(ie)),
912         pb.feasibleMode := false)]
913
914; TODO: watchout: commenting out the 2 next lines may prevent from doing more than one move of local opt
915;    for v in a.problem.unassignedVars
916;       erase(value,v),
917
918;choco/ConstructiveHeuristic <: Ephemeral(
919;   private/manager:LocalSearchSolver)
920choco/AssignmentHeuristic <: ConstructiveHeuristic()
921
922;choco/MoveNeighborhood <: Ephemeral(
923;    private/manager:LocalSearchSolver)
924
925choco/FlipNeighborhood <: MoveNeighborhood()
926
927;choco/LocalSearchSolver <: Solver(
928;    // slots for generating an assignment
929;   choco/buildAssignment:ConstructiveHeuristic,
930;   choco/changeAssignment:MoveNeighborhood,
931;   choco/maxNbLocalSearch:integer = 20,
932;   choco/maxNbLocalMoves:integer = 5000)
933;(store(assignedThenUnassignedVars,lastAssignedVar)) // v0.37: haveAwakenConstraints need to be stored
934
935choco/MultipleDescent <: LocalSearchSolver(
936   choco/nbLocalSearch:integer = 0,
937   choco/nbLocalMoves:integer = 0)
938
939// ********************************************************************
940// *   Part 6: Feeding the engine with a library of neighborhoods     *
941// ********************************************************************
942
943[selectMoveVar(a:AssignmentHeuristic) : (IntVar U {unknown})
944 -> let ie := a.manager.problem.invariantEngine, l := ie.assignedThenUnassignedVars,
945        n := length(l), j := ie.lastAssignedVar in
946     (if (j = n) unknown
947      else l[j + 1 + random(n - j)])]
948[selectValue(a:AssignmentHeuristic, v:IntVar) : integer
949 -> if unknown?(bucket,v) random(v.inf,v.sup)
950    else random(v.bucket)]
951[assignOneVar(a:AssignmentHeuristic) : boolean
952 -> when v := selectMoveVar(a) in
953         let val := selectValue(a,v) in
954            (assignVal(v,val),
955             true)
956    else false]
957[build(a:AssignmentHeuristic) : void
958 -> eraseAssignment(a.manager.problem.invariantEngine),
959    while assignOneVar(a) nil,
960  ;  maintainConflictAccount(a),
961    //[LTALK]   ++ initial solution built with ~S violated const. // a.manager.problem.invariantEngine.nbViolatedConstraints,
962    checkCleanState(a.manager.problem.invariantEngine)]
963
964// v1.0 erasing the previous assignment before constructing a new one.
965[choco/eraseAssignment(ie:ConflictCount) : void // v1.02 return void
966 -> let pb := ie.problem in
967     (for v:IntVar in pb.vars // claire3 port: type annotation for v
968         (if (v.inf != v.sup)
969;             (erase(value,v as IntVar), // claire3 port: type annotation for v
970             (v.value := UNKNOWNINT,
971              v.nbViolatedConstraints := 0)),
972      ie.conflictingVars := list<IntVar>{v in pb.vars | v.nbViolatedConstraints > 0},
973      let nbconflicts := 0 in
974        (for c in pb.constraints
975           (if testIfInstantiated(c)
976              (if not(testIfTrue(c)) nbconflicts :+ 1)
977            else c.violated := false),
978         ie.nbViolatedConstraints := nbconflicts),
979;      let l1 := list{v in pb.vars | v.inf = v.sup},
980;          l2 := list{v in pb.vars | v.inf != v.sup} in
981;        (ie.assignedThenUnassignedVars := (l1 /+ l2),
982;         ie.lastAssignedVar := length(l1)) 
983      let l := ie.assignedThenUnassignedVars in
984        (shrink(l, 0),
985         for v in pb.vars
986            (if (v.inf = v.sup) add(l,v)),
987         let n := length(l) in
988             ie.lastAssignedVar := n,
989         for v in pb.vars
990            (if (v.inf != v.sup) add(l,v)) )
991      )]
992 
993// checks that the invariant engine is in a proper state
994[choco/checkCleanState(ie:ConflictCount)
995 => #if (compiler.active? & compiler.safety > 2) nil
996    else let pb := ie.problem, bizarre := false in
997      (for c in list{c in pb.constraints | testIfInstantiated(c)}
998          (if (c.violated = testIfTrue(c))
999              (printf("~S registered as violated:~S, while testIfTrue:~S\n",c,c.violated,testIfTrue(c)),
1000               bizarre := true)),     
1001       if (ie.nbViolatedConstraints != count(list{c in pb.constraints | c.violated = true}))
1002          (printf("wrong violated constraint count:~S instead of ~S",
1003                  ie.nbViolatedConstraints,count(list{c in pb.constraints | c.violated = true})),
1004           bizarre := true),
1005       for v in pb.vars
1006          (if (v % ie.conflictingVars)
1007              (if forall(c in v.constraints | c.violated = false)
1008                 (printf("~S registered as conflicting with all constraints OK\n",v),
1009                  bizarre := true))
1010           else (when c := some(c in v.constraints | c.violated = true) in
1011                    (printf("~S not registered as conflicting, while ~S is violated\n",v,c),
1012                     bizarre := true))),
1013      if bizarre error("corrupted state for ~S, stop and look why",ie) )]
1014
1015// TODO: there should be another move scheme than FlipNeighborhood
1016// select a constraint rather than a variable and repair it
1017//       incremental structure => keep the sublist of violated constraints
1018
1019[selectMoveVar(m:FlipNeighborhood) : (IntVar U {unknown})
1020 -> let l := m.manager.problem.invariantEngine.conflictingVars in
1021       (if l (random(l) as IntVar)
1022        else unknown)]
1023[newValue(m:FlipNeighborhood, v:IntVar) : integer
1024 -> getMinConflictValue(v)]
1025
1026[move(m:FlipNeighborhood) : boolean
1027 -> when v := selectMoveVar(m) in
1028      let b := newValue(m,v) in
1029         (changeVal(v,b), true)
1030    else (assert(length(m.manager.problem.invariantEngine.conflictingVars) = 0),
1031          false)]
1032[finishedLoop(algo:LocalSearchSolver) : boolean
1033 -> let ie := algo.problem.invariantEngine in
1034       (if (ie.nbViolatedConstraints = 0)
1035           (assert(length(ie.conflictingVars) = 0),
1036            true)
1037        else (assert(length(ie.conflictingVars) > 0),
1038              if (algo.nbLocalMoves >= algo.maxNbLocalMoves) true
1039              else false))]
1040[initLoop(algo:LocalSearchSolver) : void
1041 -> algo.nbLocalSearch :+ 1,
1042    algo.nbLocalMoves := 0]
1043[endLoop(algo:LocalSearchSolver) : void
1044 -> let ie := algo.problem.invariantEngine in
1045       (if (ie.nbViolatedConstraints < ie.minNbViolatedConstraints)
1046           (//[LVIEW] found a solution with ~S violated constraints // ie.nbViolatedConstraints,
1047            ie.minNbViolatedConstraints := ie.nbViolatedConstraints,
1048            saveAssignment(algo)))]
1049
1050[choco/copyParameters(oldSolver:LocalSearchSolver, newSolver:LocalSearchSolver) : void
1051 -> when nbs := get(maxNbLocalSearch, oldSolver) in newSolver.maxNbLocalSearch := nbs,
1052    when nbm := get(maxNbLocalMoves, oldSolver) in newSolver.maxNbLocalMoves := nbm]
1053
1054[choco/attachLocalSearchSolver(pb:Problem, newSolver:LocalSearchSolver) : void
1055 -> when oldSolver := get(localSearchSolver,pb) in
1056         copyParameters(oldSolver, newSolver),
1057    pb.localSearchSolver := newSolver,
1058    newSolver.problem := pb]
1059
1060// ********************************************************************
1061// *   Part 7: Using neighborhood classes within LocalSearchSolver's  *
1062// ********************************************************************
1063
1064[runLocalSearch(algo:LocalSearchSolver) : void
1065 -> setFeasibleMode(algo.problem,false),  // v0.9907
1066    initIterations(algo),
1067    while not(finishedIterations(algo))
1068       (build(algo.buildAssignment),
1069        initLoop(algo),
1070        while not(finishedLoop(algo))
1071             (move(algo.changeAssignment),
1072              oneMoreMove(algo)),
1073        endLoop(algo)),
1074    restoreBestAssignment(algo)]
1075
1076// v0.9906
1077[initIterations(algo:MultipleDescent) : void
1078 -> let pb := algo.problem, pe := pb.propagationEngine in
1079       (if (; getNbObjects(pe.delayedConst1.partition) > 0 |
1080            getNbObjects(pe.delayedConst2.partition) > 0 |
1081            getNbObjects(pe.delayedConst3.partition) > 0 |
1082            getNbObjects(pe.delayedConst4.partition) > 0)
1083          error("local moves not implemented on problems with global constraints"),
1084        if exists(c in pb.constraints | c % CompositeConstraint)  // v1.010
1085           error("local moves not implemented on problems with Boolean combinations of constraints"),
1086        algo.nbLocalSearch := 0)]
1087
1088// V0.9907
1089[choco/finishedIterations(algo:LocalSearchSolver) : boolean
1090 -> (algo.nbLocalSearch >= algo.maxNbLocalSearch |
1091     algo.problem.invariantEngine.minNbViolatedConstraints = 0)]
1092// V0.9907
1093[choco/oneMoreMove(algo:LocalSearchSolver) : void
1094 -> algo.nbLocalMoves :+ 1]
1095
1096// v1.0 generic event: a constraint becomes conflicting
1097[choco/becomesAConflict(c:AbstractConstraint,ie:ConflictCount) : void
1098 -> c.violated := true, ie.nbViolatedConstraints :+ 1,
1099    let n := getNbVars(c) in
1100     (for i in (1 .. n) addOneConflict(ie,getVar(c,i) as IntVar))]
1101[choco/becomesAConflict(c:UnIntConstraint,ie:ConflictCount) : void
1102 -> c.violated := true, ie.nbViolatedConstraints :+ 1,
1103    addOneConflict(ie,c.v1)]
1104[choco/becomesAConflict(c:BinIntConstraint,ie:ConflictCount) : void
1105 -> c.violated := true, ie.nbViolatedConstraints :+ 1,
1106    addOneConflict(ie,c.v1), addOneConflict(ie,c.v2)]
1107[choco/becomesAConflict(c:TernIntConstraint,ie:ConflictCount) : void
1108 -> c.violated := true, ie.nbViolatedConstraints :+ 1,
1109    addOneConflict(ie,c.v1), addOneConflict(ie,c.v2), addOneConflict(ie,c.v3)]
1110[choco/becomesAConflict(c:LargeIntConstraint,ie:ConflictCount) : void
1111 -> c.violated := true, ie.nbViolatedConstraints :+ 1,
1112    for v in c.vars addOneConflict(ie, v)]
1113
1114// v1.0 generic event: a constraint becomes un-conflicting
1115[choco/becomesSatisfied(c:AbstractConstraint,ie:ConflictCount) : void
1116 -> c.violated := false, ie.nbViolatedConstraints :- 1,
1117    let n := getNbVars(c) in
1118     (for i in (1 .. n) removeOneConflict(ie,getVar(c,i) as IntVar))]
1119[choco/becomesSatisfied(c:UnIntConstraint,ie:ConflictCount) : void
1120 -> c.violated := false, ie.nbViolatedConstraints :- 1,
1121    removeOneConflict(ie,c.v1)]
1122[choco/becomesSatisfied(c:BinIntConstraint,ie:ConflictCount) : void
1123 -> c.violated := false, ie.nbViolatedConstraints :- 1,
1124    removeOneConflict(ie,c.v1), removeOneConflict(ie,c.v2)]
1125[choco/becomesSatisfied(c:TernIntConstraint,ie:ConflictCount) : void
1126 -> c.violated := false, ie.nbViolatedConstraints :- 1,
1127    removeOneConflict(ie,c.v1), removeOneConflict(ie,c.v2), removeOneConflict(ie,c.v3)]
1128[choco/becomesSatisfied(c:LargeIntConstraint,ie:ConflictCount) : void
1129 -> c.violated := false, ie.nbViolatedConstraints :- 1,
1130    for v in c.vars removeOneConflict(ie, v)]
1131
1132// v1.0 two simple uitilities
1133// addOneConflict registers that variable v appears in one more conflicting constraints
1134[choco/addOneConflict(ie:ConflictCount,v:IntVar) : void
1135 -> v.nbViolatedConstraints :+ 1,
1136    if (v.nbViolatedConstraints = 1) ie.conflictingVars :add v
1137    else assert(v % ie.conflictingVars)]
1138
1139// register that variable v appears in one conflicting constraint less
1140[choco/removeOneConflict(ie:ConflictCount,v:IntVar) : void
1141 -> v.nbViolatedConstraints :- 1,
1142    if (v.nbViolatedConstraints = 0) ie.conflictingVars :delete v
1143    else assert(v % ie.conflictingVars)]
1144
1145// Note: the events are not stored: immediate reaction
1146// we maintain incrementally:
1147//   - the sub-list of instantiated variables
1148//   - for each constraint, its status (violated vs. satisfied)
1149//   - a count of all conflicts (total #of constraints, #of constraints per var)
1150//   - a sub-list of variables occurring in violated constraints
1151[choco/postAssignVal(ie:ConflictCount,v:IntVar,a:integer) : void
1152 -> let l := ie.assignedThenUnassignedVars, n := length(l),
1153        i := get(l,v), j := ie.lastAssignedVar in
1154   (if (i = 0) error("~S is not present in algo.unassignedVars",v)
1155    else (assert(i > j & i <= n),  // <fl> 0.36 i may point to the last variable from l
1156          //[IDEBUG] assign ~S to ~Sth unassigned var (~S), cursor:~S // a,i,v,j,
1157          store(l,i,l[j + 1],true),
1158          store(l,j + 1,v,true),
1159          ie.lastAssignedVar := j + 1,
1160          // <fx> 0.34 incremental conflict counts
1161          for c in v.constraints
1162             (if testIfInstantiated(c)
1163                (if testIfTrue(c) c.violated := false
1164                 else becomesAConflict(c,ie)))))]
1165
1166// The reaction to the unassignment is performed while the value is still in place
1167// the value is erased only after the reaction
1168[choco/postUnAssignVal(ie:ConflictCount,v:IntVar) : void
1169 -> let l := ie.assignedThenUnassignedVars, n := length(l),
1170        i := get(l,v), j := ie.lastAssignedVar in
1171     (if (i = 0) error("~S is not present in pb.unassignedVars",v),
1172      assert(i <= j & j <= n),
1173      assert(isInstantiated(v)),
1174      // <fx> 0.34 decremental conflict counts
1175      for c in v.constraints
1176         (if (testIfInstantiated(c) & not(testIfTrue(c)))
1177              becomesSatisfied(c,ie),
1178          store(l,i,l[j],true),
1179          store(l,j,v,true),
1180          ie.lastAssignedVar := j - 1))]
1181
1182[choco/postChangeVal(ie:ConflictCount,v:IntVar,a:integer,b:integer) : void
1183 -> assert(v.value = a),
1184    let nbConflictsBefore := v.nbViolatedConstraints in
1185      (//[LTALK] change val ~S [~S]:~S -> ~S // v,nbConflictsBefore,a,b,       
1186       if (nbConflictsBefore = 0 & get(ie.conflictingVars,v) != 0)
1187          error("~S with no conflicts and conflictingVars:~S",v,ie.conflictingVars),
1188       assert((if (nbConflictsBefore = 0) (get(ie.conflictingVars,v) = 0) else true)),
1189       for c in v.constraints // should be extended for handling global constraints
1190         let OKBefore := not(c.violated),
1191             OKNow := OKBefore in
1192          (v.value := b, OKNow := testIfTrue(c),
1193           //[LDEBUG] ---- ~S: ~S -> ~S // c,OKBefore, OKNow,
1194           if (OKNow != OKBefore)
1195              (if OKNow                            // TODO: shrink list of violated constraints
1196                 (if not(c.violated) error("~S should be violated and c.viol=~S",c,c.violated),
1197                  assert(c.violated = true),
1198                  becomesSatisfied(c,ie))
1199               else
1200                 (if c.violated error("~S should not be violated and c.viol=~S",c,c.violated),
1201                  assert(c.violated = false),
1202                  becomesAConflict(c,ie))),
1203           v.value := a) )]
Note: See TracBrowser for help on using the browser.