this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Patrick Pekczynski <pekczynski@ps.uni-sb.de>
5 *
6 * Copyright:
7 * Patrick Pekczynski, 2004
8 *
9 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34#include <gecode/int/rel.hh>
35#include <gecode/int/distinct.hh>
36
37namespace Gecode { namespace Int { namespace Sorted {
38
39
40 /*
41 * Summary of the propagation algorithm as implemented in the
42 * propagate method below:
43 *
44 * STEP 1: Normalize the domains of the y variables
45 * STEP 2: Sort the domains of the x variables according to their lower
46 * and upper endpoints
47 * STEP 3: Compute the matchings phi and phiprime with
48 * Glover's matching algorithm
49 * STEP 4: Compute the strongly connected components in
50 * the oriented intersection graph
51 * STEP 5: Narrow the domains of the variables
52 *
53 */
54
55 /**
56 * \brief Perform bounds consistent sortedness propagation
57 *
58 * Implements the propagation algorithm for Sorted::Sorted
59 * and is provided as seperate function, because a second pass of
60 * the propagation algorithm is needed in order to achieve idempotency
61 * in case explicit permutation variables are provided.
62 *
63 * If \a Perm is true, permutation variables form the
64 * third argument which implies additional inferences,
65 * consistency check on the permutation variables and eventually a
66 * second pass of the propagation algorithm.
67 * Otherwise, the algorithm does not take care of the permutation
68 * variables resulting in a better performance.
69 */
70
71 template<class View, bool Perm>
72 ExecStatus
73 bounds_propagation(Space& home, Propagator& p,
74 ViewArray<View>& x,
75 ViewArray<View>& y,
76 ViewArray<View>& z,
77 bool& repairpass,
78 bool& nofix,
79 bool& match_fixed){
80
81 int n = x.size();
82
83 Region r;
84 int* tau = r.alloc<int>(n);
85 int* phi = r.alloc<int>(n);
86 int* phiprime = r.alloc<int>(n);
87 OfflineMinItem* sequence = r.alloc<OfflineMinItem>(n);
88 int* vertices = r.alloc<int>(n);
89
90 if (match_fixed) {
91 // sorting is determined, sigma and tau coincide
92 for (int i=0; i<n; i++)
93 tau[z[i].val()] = i;
94 } else {
95 for (int i=0; i<n; i++)
96 tau[i] = i;
97 }
98
99 if (Perm) {
100 // normalized and sorted
101 // collect all bounds
102
103 Rank* allbnd = r.alloc<Rank>(x.size());
104#ifndef NDEBUG
105 for (int i=n; i--;)
106 allbnd[i].min = allbnd[i].max = -1;
107#endif
108 for (int i=n; i--;) {
109 int min = x[i].min();
110 int max = x[i].max();
111 for (int j=0; j<n; j++) {
112 if ( (y[j].min() > min) ||
113 (y[j].min() <= min && min <= y[j].max()) ) {
114 allbnd[i].min = j;
115 break;
116 }
117 }
118 for (int j=n; j--;) {
119 if (y[j].min() > max) {
120 allbnd[i].max = j-1;
121 break;
122 } else if (y[j].min() <= max && min <= y[j].max()) {
123 allbnd[i].max = j;
124 break;
125 }
126 }
127 }
128
129 for (int i=0; i<n; i++) {
130 // minimum reachable y-variable
131 int minr = allbnd[i].min;
132 assert(minr != -1);
133 int maxr = allbnd[i].max;
134 assert(maxr != -1);
135
136 ModEvent me = x[i].gq(home, y[minr].min());
137 if (me_failed(me))
138 return ES_FAILED;
139 nofix |= (me_modified(me) && (x[i].min() != y[minr].min()));
140
141 me = x[i].lq(home, y[maxr].max());
142 if (me_failed(me))
143 return ES_FAILED;
144 nofix |= (me_modified(me) && (x[i].min() != y[maxr].max()));
145
146 me = z[i].gq(home, minr);
147 if (me_failed(me))
148 return ES_FAILED;
149 nofix |= (me_modified(me) && (z[i].min() != minr));
150
151 me = z[i].lq(home, maxr);
152 if (me_failed(me))
153 return ES_FAILED;
154 nofix |= (me_modified(me) && (z[i].max() != maxr));
155 }
156
157 // channel information from x to y through permutation variables in z
158 if (!channel(home,x,y,z,nofix))
159 return ES_FAILED;
160 if (nofix)
161 return ES_NOFIX;
162 }
163
164 /*
165 * STEP 1:
166 * normalization is implemented in "order.hpp"
167 * o setting the lower bounds of the y_i domains (\lb E_i)
168 * to max(\lb E_{i-1},\lb E_i)
169 * o setting the upper bounds of the y_i domains (\ub E_i)
170 * to min(\ub E_i,\ub E_{i+1})
171 */
172
173 if (!normalize(home, y, x, nofix))
174 return ES_FAILED;
175
176 if (Perm) {
177 // check consistency of channeling after normalization
178 if (!channel(home,x,y,z,nofix))
179 return ES_FAILED;
180 if (nofix)
181 return ES_NOFIX;
182 }
183
184
185 // if bounds have changed we have to recreate sigma to restore
186 // optimized dropping of variables
187
188 sort_sigma<View,Perm>(x,z);
189
190 bool subsumed = true;
191 bool array_subs = false;
192 int dropfst = 0;
193 bool noperm_bc = false;
194
195 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst) ||
196 !array_assigned<View,Perm>(home,x,y,z,array_subs,match_fixed,nofix,noperm_bc))
197 return ES_FAILED;
198
199 if (subsumed || array_subs)
200 return home.ES_SUBSUMED(p);
201
202 /*
203 * STEP 2: creating tau
204 * Sort the domains of the x variables according
205 * to their lower bounds, where we use an
206 * intermediate array of integers for sorting
207 */
208 sort_tau<View,Perm>(x,z,tau);
209
210 /*
211 * STEP 3:
212 * Compute the matchings \phi and \phi' between
213 * the x and the y variables
214 * with Glover's matching algorithm.
215 * o phi is computed with the glover function
216 * o phiprime is computed with the revglover function
217 * glover and revglover are implemented in "matching.hpp"
218 */
219
220 if (!match_fixed) {
221 if (!glover(x,y,tau,phi,sequence,vertices))
222 return ES_FAILED;
223 } else {
224 for (int i=0; i<x.size(); i++) {
225 phi[i] = z[i].val();
226 phiprime[i] = phi[i];
227 }
228 }
229
230 for (int i = n; i--; )
231 if (!y[i].assigned()) {
232 // phiprime is not needed to narrow the domains of the x-variables
233 if (!match_fixed &&
234 !revglover(x,y,tau,phiprime,sequence,vertices))
235 return ES_FAILED;
236
237 if (!narrow_domy(home,x,y,phi,phiprime,nofix))
238 return ES_FAILED;
239
240 if (nofix && !match_fixed) {
241 // data structures (matching) destroyed by domains with holes
242
243 for (int j = y.size(); j--; )
244 phi[j]=phiprime[j]=0;
245
246 if (!glover(x,y,tau,phi,sequence,vertices))
247 return ES_FAILED;
248
249 if (!revglover(x,y,tau,phiprime,sequence,vertices))
250 return ES_FAILED;
251
252 if (!narrow_domy(home,x,y,phi,phiprime,nofix))
253 return ES_FAILED;
254 }
255 break;
256 }
257
258 if (Perm) {
259 // check consistency of channeling after normalization
260 if (!channel(home,x,y,z,nofix))
261 return ES_FAILED;
262 if (nofix)
263 return ES_NOFIX;
264 }
265
266 /*
267 * STEP 4:
268 * Compute the strongly connected components in
269 * the oriented intersection graph
270 * the computation of the sccs is implemented in
271 * "narrowing.hpp" in the function narrow_domx
272 */
273
274 int* scclist = r.alloc<int>(n);
275 SccComponent* sinfo = r.alloc<SccComponent>(n);
276
277 for(int i = n; i--; )
278 sinfo[i].left=sinfo[i].right=sinfo[i].rightmost=sinfo[i].leftmost= i;
279
280 computesccs(x,y,phi,sinfo,scclist);
281
282 /*
283 * STEP 5:
284 * Narrow the domains of the variables
285 * Also implemented in "narrowing.hpp"
286 * in the functions narrow_domx and narrow_domy
287 */
288
289 if (!narrow_domx<View,Perm>(home,x,y,z,tau,phi,scclist,sinfo,nofix))
290 return ES_FAILED;
291
292 if (Perm) {
293 if (!noperm_bc &&
294 !perm_bc<View>
295 (home, tau, sinfo, scclist, x,z, repairpass, nofix))
296 return ES_FAILED;
297
298 // channeling also needed after normal propagation steps
299 // in order to ensure consistency after possible modification in perm_bc
300 if (!channel(home,x,y,z,nofix))
301 return ES_FAILED;
302 if (nofix)
303 return ES_NOFIX;
304 }
305
306 sort_tau<View,Perm>(x,z,tau);
307
308 if (Perm) {
309 // special case of sccs of size 2 denoted by permutation variables
310 // used to enforce consistency from x to y
311 // case of the upper bound ordering tau
312 for (int i = x.size() - 1; i--; ) {
313 // two x variables are in the same scc of size 2
314 if (z[tau[i]].min() == z[tau[i+1]].min() &&
315 z[tau[i]].max() == z[tau[i+1]].max() &&
316 z[tau[i]].size() == 2 && z[tau[i]].range()) {
317 // if bounds are strictly smaller
318 if (x[tau[i]].max() < x[tau[i+1]].max()) {
319 ModEvent me = y[z[tau[i]].min()].lq(home, x[tau[i]].max());
320 if (me_failed(me))
321 return ES_FAILED;
322 nofix |= (me_modified(me) &&
323 y[z[tau[i]].min()].max() != x[tau[i]].max());
324
325 me = y[z[tau[i+1]].max()].lq(home, x[tau[i+1]].max());
326 if (me_failed(me))
327 return ES_FAILED;
328 nofix |= (me_modified(me) &&
329 y[z[tau[i+1]].max()].max() != x[tau[i+1]].max());
330 }
331 }
332 }
333 }
334 return nofix ? ES_NOFIX : ES_FIX;
335 }
336
337 template<class View, bool Perm>
338 forceinline Sorted<View,Perm>::
339 Sorted(Space& home, Sorted<View,Perm>& p):
340 Propagator(home, p),
341 reachable(p.reachable) {
342 x.update(home, p.x);
343 y.update(home, p.y);
344 z.update(home, p.z);
345 w.update(home, p.w);
346 }
347
348 template<class View, bool Perm>
349 Sorted<View,Perm>::
350 Sorted(Home home,
351 ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) :
352 Propagator(home), x(x0), y(y0), z(z0), w(home,y0), reachable(-1) {
353 x.subscribe(home, *this, PC_INT_BND);
354 y.subscribe(home, *this, PC_INT_BND);
355 if (Perm)
356 z.subscribe(home, *this, PC_INT_BND);
357 }
358
359 template<class View, bool Perm>
360 forceinline size_t
361 Sorted<View,Perm>::dispose(Space& home) {
362 x.cancel(home,*this, PC_INT_BND);
363 y.cancel(home,*this, PC_INT_BND);
364 if (Perm)
365 z.cancel(home,*this, PC_INT_BND);
366 (void) Propagator::dispose(home);
367 return sizeof(*this);
368 }
369
370 template<class View, bool Perm>
371 Actor* Sorted<View,Perm>::copy(Space& home) {
372 return new (home) Sorted<View,Perm>(home, *this);
373 }
374
375 template<class View, bool Perm>
376 PropCost Sorted<View,Perm>::cost(const Space&, const ModEventDelta&) const {
377 return PropCost::linear(PropCost::LO, x.size());
378 }
379
380 template<class View, bool Perm>
381 void
382 Sorted<View,Perm>::reschedule(Space& home) {
383 x.reschedule(home, *this, PC_INT_BND);
384 y.reschedule(home, *this, PC_INT_BND);
385 if (Perm)
386 z.reschedule(home, *this, PC_INT_BND);
387 }
388
389 template<class View, bool Perm>
390 ExecStatus
391 Sorted<View,Perm>::propagate(Space& home, const ModEventDelta&) {
392 int n = x.size();
393 bool secondpass = false;
394 bool nofix = false;
395 int dropfst = 0;
396
397 bool subsumed = false;
398 bool array_subs = false;
399 bool match_fixed = false;
400
401 // normalization of x and y
402 if (!normalize(home, y, x, nofix))
403 return ES_FAILED;
404
405 // create sigma sorting
406 sort_sigma<View,Perm>(x,z);
407
408 bool noperm_bc = false;
409 if (!array_assigned<View,Perm>
410 (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc))
411 return ES_FAILED;
412
413 if (array_subs)
414 return home.ES_SUBSUMED(*this);
415
416 sort_sigma<View,Perm>(x,z);
417
418 // in this case check_subsumptions is guaranteed to find
419 // the xs ordered by sigma
420
421 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst))
422 return ES_FAILED;
423
424 if (subsumed)
425 return home.ES_SUBSUMED(*this);
426
427 if (Perm) {
428 // dropping possibly yields inconsistent indices on permutation variables
429 if (dropfst) {
430 reachable = w[dropfst - 1].max();
431 bool unreachable = true;
432 for (int i = x.size(); unreachable && i-- ; ) {
433 unreachable &= (reachable < x[i].min());
434 }
435
436 if (unreachable) {
437 x.drop_fst(dropfst, home, *this, PC_INT_BND);
438 y.drop_fst(dropfst, home, *this, PC_INT_BND);
439 z.drop_fst(dropfst, home, *this, PC_INT_BND);
440 } else {
441 dropfst = 0;
442 }
443 }
444
445 n = x.size();
446
447 if (n < 2) {
448 if (x[0].max() < y[0].min() || y[0].max() < x[0].min())
449 return ES_FAILED;
450 if (Perm) {
451 GECODE_ME_CHECK(z[0].eq(home, w.size() - 1));
452 }
453 GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0])));
454 }
455
456 // check whether shifting the permutation variables
457 // is necessary after dropping x and y vars
458 // highest reachable index
459 int valid = n - 1;
460 int index = 0;
461 int shift = 0;
462
463 for (int i = n; i--; ){
464 if (z[i].max() > index)
465 index = z[i].max();
466 if (index > valid)
467 shift = index - valid;
468 }
469
470 if (shift) {
471 ViewArray<OffsetView> ox(home,n), oy(home,n), oz(home,n);
472
473 for (int i = n; i--; ) {
474 GECODE_ME_CHECK(z[i].gq(home, shift));
475
476 oz[i] = OffsetView(z[i], -shift);
477 ox[i] = OffsetView(x[i], 0);
478 oy[i] = OffsetView(y[i], 0);
479 }
480
481 GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm>
482 (home,*this,ox,oy,oz,secondpass,nofix,match_fixed)));
483
484 if (secondpass) {
485 GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm>
486 (home,*this,ox,oy,oz,secondpass,nofix,match_fixed)));
487 }
488 } else {
489 GECODE_ES_CHECK((bounds_propagation<View,Perm>
490 (home,*this,x,y,z,secondpass,nofix,match_fixed)));
491
492 if (secondpass) {
493 GECODE_ES_CHECK((bounds_propagation<View,Perm>
494 (home,*this,x,y,z,secondpass,nofix,match_fixed)));
495 }
496 }
497 } else {
498 // dropping has no consequences
499 if (dropfst) {
500 x.drop_fst(dropfst, home, *this, PC_INT_BND);
501 y.drop_fst(dropfst, home, *this, PC_INT_BND);
502 }
503
504 n = x.size();
505
506 if (n < 2) {
507 if (x[0].max() < y[0].min() || y[0].max() < x[0].min())
508 return ES_FAILED;
509 GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0])));
510 }
511
512 GECODE_ES_CHECK((bounds_propagation<View,Perm>
513 (home, *this, x, y, z,secondpass, nofix, match_fixed)));
514 // no second pass possible if there are no permvars
515 }
516
517 if (!normalize(home, y, x, nofix))
518 return ES_FAILED;
519
520 Region r;
521 int* tau = r.alloc<int>(n);
522 if (match_fixed) {
523 // sorting is determined
524 // sigma and tau coincide
525 for (int i = x.size(); i--; ) {
526 int pi = z[i].val();
527 tau[pi] = i;
528 }
529 } else {
530 for (int i = n; i--; ) {
531 tau[i] = i;
532 }
533 }
534
535 sort_tau<View,Perm>(x,z,tau);
536 // recreate consistency for already assigned subparts
537 // in order of the upper bounds starting at the end of the array
538 bool xbassigned = true;
539 for (int i = x.size(); i--; ) {
540 if (x[tau[i]].assigned() && xbassigned) {
541 GECODE_ME_CHECK(y[i].eq(home, x[tau[i]].val()));
542 } else {
543 xbassigned = false;
544 }
545 }
546
547 subsumed = true;
548 array_subs = false;
549 noperm_bc = false;
550
551 // creating sorting anew
552 sort_sigma<View,Perm>(x,z);
553
554 if (Perm) {
555 for (int i = 0; i < x.size() - 1; i++) {
556 // special case of subsccs of size2 for the lower bounds
557 // two x variables are in the same scc of size 2
558 if (z[i].min() == z[i+1].min() &&
559 z[i].max() == z[i+1].max() &&
560 z[i].size() == 2 && z[i].range()) {
561 if (x[i].min() < x[i+1].min()) {
562 ModEvent me = y[z[i].min()].gq(home, x[i].min());
563 GECODE_ME_CHECK(me);
564 nofix |= (me_modified(me) &&
565 y[z[i].min()].min() != x[i].min());
566
567 me = y[z[i+1].max()].gq(home, x[i+1].min());
568 GECODE_ME_CHECK(me);
569 nofix |= (me_modified(me) &&
570 y[z[i+1].max()].min() != x[i+1].min());
571 }
572 }
573 }
574 }
575
576 // check assigned
577 // should be sorted
578 bool xassigned = true;
579 for (int i = 0; i < x.size(); i++) {
580 if (x[i].assigned() && xassigned) {
581 GECODE_ME_CHECK(y[i].eq(home,x[i].val()));
582 } else {
583 xassigned = false;
584 }
585 }
586
587 // sorted check bounds
588 // final check that variables are consitent with least and greatest possible
589 // values
590 int tlb = std::min(x[0].min(), y[0].min());
591 int tub = std::max(x[x.size() - 1].max(), y[y.size() - 1].max());
592 for (int i = x.size(); i--; ) {
593 ModEvent me = y[i].lq(home, tub);
594 GECODE_ME_CHECK(me);
595 nofix |= me_modified(me) && (y[i].max() != tub);
596
597 me = y[i].gq(home, tlb);
598 GECODE_ME_CHECK(me);
599 nofix |= me_modified(me) && (y[i].min() != tlb);
600
601 me = x[i].lq(home, tub);
602 GECODE_ME_CHECK(me);
603 nofix |= me_modified(me) && (x[i].max() != tub);
604
605 me = x[i].gq(home, tlb);
606 GECODE_ME_CHECK(me);
607 nofix |= me_modified(me) && (x[i].min() != tlb);
608 }
609
610 if (!array_assigned<View,Perm>
611 (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc))
612 return ES_FAILED;
613
614 if (array_subs)
615 return home.ES_SUBSUMED(*this);
616
617 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst))
618 return ES_FAILED;
619
620 if (subsumed)
621 return home.ES_SUBSUMED(*this);
622
623 return nofix ? ES_NOFIX : ES_FIX;
624 }
625
626 template<class View, bool Perm>
627 ExecStatus
628 Sorted<View,Perm>::
629 post(Home home,
630 ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) {
631 int n = x0.size();
632 if (n < 2) {
633 if ((x0[0].max() < y0[0].min()) || (y0[0].max() < x0[0].min()))
634 return ES_FAILED;
635 GECODE_ES_CHECK((Rel::EqBnd<View,View>::post(home,x0[0],y0[0])));
636 if (Perm) {
637 GECODE_ME_CHECK(z0[0].eq(home,0));
638 }
639 } else {
640 if (Perm) {
641 ViewArray<View> z(home,n);
642 for (int i=n; i--; ) {
643 z[i]=z0[i];
644 GECODE_ME_CHECK(z[i].gq(home,0));
645 GECODE_ME_CHECK(z[i].lq(home,n-1));
646 }
647 GECODE_ES_CHECK(Distinct::Bnd<View>::post(home,z));
648 }
649 new (home) Sorted<View,Perm>(home,x0,y0,z0);
650 }
651 return ES_OK;
652 }
653
654}}}
655
656// STATISTICS: int-prop
657
658
659