propagate.hpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Patrick Pekczynski <pekczynski@ps.uni-sb.de> 00005 * 00006 * Copyright: 00007 * Patrick Pekczynski, 2004 00008 * 00009 * Last modified: 00010 * $Date: 2010-08-24 15:54:10 +0200 (Tue, 24 Aug 2010) $ by $Author: tack $ 00011 * $Revision: 11359 $ 00012 * 00013 * This file is part of Gecode, the generic constraint 00014 * development environment: 00015 * http://www.gecode.org 00016 * 00017 * Permission is hereby granted, free of charge, to any person obtaining 00018 * a copy of this software and associated documentation files (the 00019 * "Software"), to deal in the Software without restriction, including 00020 * without limitation the rights to use, copy, modify, merge, publish, 00021 * distribute, sublicense, and/or sell copies of the Software, and to 00022 * permit persons to whom the Software is furnished to do so, subject to 00023 * the following conditions: 00024 * 00025 * The above copyright notice and this permission notice shall be 00026 * included in all copies or substantial portions of the Software. 00027 * 00028 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00029 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00030 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00031 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00032 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00033 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00034 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00035 * 00036 */ 00037 00038 #include <gecode/int/rel.hh> 00039 #include <gecode/int/distinct.hh> 00040 00041 namespace Gecode { namespace Int { namespace Sorted { 00042 00043 00044 /* 00045 * Summary of the propagation algorithm as implemented in the 00046 * propagate method below: 00047 * 00048 * STEP 1: Normalize the domains of the y variables 00049 * STEP 2: Sort the domains of the x variables according to their lower 00050 * and upper endpoints 00051 * STEP 3: Compute the matchings phi and phiprime with 00052 * Glover's matching algorithm 00053 * STEP 4: Compute the strongly connected components in 00054 * the oriented intersection graph 00055 * STEP 5: Narrow the domains of the variables 00056 * 00057 */ 00058 00075 template<class View, bool Perm> 00076 ExecStatus 00077 bounds_propagation(Space& home, Propagator& p, 00078 ViewArray<View>& x, 00079 ViewArray<View>& y, 00080 ViewArray<View>& z, 00081 bool& repairpass, 00082 bool& nofix, 00083 bool& match_fixed){ 00084 00085 int n = x.size(); 00086 00087 Region r(home); 00088 int* tau = r.alloc<int>(n); 00089 int* phi = r.alloc<int>(n); 00090 int* phiprime = r.alloc<int>(n); 00091 OfflineMinItem* sequence = r.alloc<OfflineMinItem>(n); 00092 int* vertices = r.alloc<int>(n); 00093 00094 if (match_fixed) { 00095 // sorting is determined, sigma and tau coincide 00096 for (int i=n; i--; ) 00097 tau[z[i].val()] = i; 00098 } else { 00099 for (int i = n; i--; ) 00100 tau[i] = i; 00101 } 00102 00103 if (Perm) { 00104 // normalized and sorted 00105 // collect all bounds 00106 00107 Rank* allbnd = r.alloc<Rank>(x.size()); 00108 #ifndef NDEBUG 00109 for (int i=n; i--;) 00110 allbnd[i].min = allbnd[i].max = -1; 00111 #endif 00112 for (int i=n; i--;) { 00113 int min = x[i].min(); 00114 int max = x[i].max(); 00115 for (int j=0; j<n; j++) { 00116 if ( (y[j].min() > min) || 00117 (y[j].min() <= min && min <= y[j].max()) ) { 00118 allbnd[i].min = j; 00119 break; 00120 } 00121 } 00122 for (int j=n; j--;) { 00123 if (y[j].min() > max) { 00124 allbnd[i].max = j-1; 00125 break; 00126 } else if (y[j].min() <= max && min <= y[j].max()) { 00127 allbnd[i].max = j; 00128 break; 00129 } 00130 } 00131 } 00132 00133 for (int i = n; i--; ) { 00134 // minimum reachable y-variable 00135 int minr = allbnd[i].min; 00136 assert(minr != -1); 00137 int maxr = allbnd[i].max; 00138 assert(maxr != -1); 00139 00140 ModEvent me = x[i].gq(home, y[minr].min()); 00141 if (me_failed(me)) 00142 return ES_FAILED; 00143 nofix |= (me_modified(me) && (x[i].min() != y[minr].min())); 00144 00145 me = x[i].lq(home, y[maxr].max()); 00146 if (me_failed(me)) 00147 return ES_FAILED; 00148 nofix |= (me_modified(me) && (x[i].min() != y[maxr].max())); 00149 00150 me = z[i].gq(home, minr); 00151 if (me_failed(me)) 00152 return ES_FAILED; 00153 nofix |= (me_modified(me) && (z[i].min() != minr)); 00154 00155 me = z[i].lq(home, maxr); 00156 if (me_failed(me)) 00157 return ES_FAILED; 00158 nofix |= (me_modified(me) && (z[i].max() != maxr)); 00159 } 00160 00161 // channel information from x to y through permutation variables in z 00162 if (!channel(home,x,y,z,nofix)) 00163 return ES_FAILED; 00164 if (nofix) 00165 return ES_NOFIX; 00166 } 00167 00168 /* 00169 * STEP 1: 00170 * normalization is implemented in "order.hpp" 00171 * o setting the lower bounds of the y_i domains (\lb E_i) 00172 * to max(\lb E_{i-1},\lb E_i) 00173 * o setting the upper bounds of the y_i domains (\ub E_i) 00174 * to min(\ub E_i,\ub E_{i+1}) 00175 */ 00176 00177 if (!normalize(home, y, x, nofix)) 00178 return ES_FAILED; 00179 00180 if (Perm) { 00181 // check consistency of channeling after normalization 00182 if (!channel(home,x,y,z,nofix)) 00183 return ES_FAILED; 00184 if (nofix) 00185 return ES_NOFIX; 00186 } 00187 00188 00189 // if bounds have changed we have to recreate sigma to restore 00190 // optimized dropping of variables 00191 00192 sort_sigma<View,Perm>(home,x,z); 00193 00194 bool subsumed = true; 00195 bool array_subs = false; 00196 int dropfst = 0; 00197 bool noperm_bc = false; 00198 00199 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst) || 00200 !array_assigned<View,Perm>(home,x,y,z,array_subs,match_fixed,nofix,noperm_bc)) 00201 return ES_FAILED; 00202 00203 if (subsumed || array_subs) 00204 return home.ES_SUBSUMED(p); 00205 00206 /* 00207 * STEP 2: creating tau 00208 * Sort the domains of the x variables according 00209 * to their lower bounds, where we use an 00210 * intermediate array of integers for sorting 00211 */ 00212 sort_tau<View,Perm>(x,z,tau); 00213 00214 /* 00215 * STEP 3: 00216 * Compute the matchings \phi and \phi' between 00217 * the x and the y variables 00218 * with Glover's matching algorithm. 00219 * o phi is computed with the glover function 00220 * o phiprime is computed with the revglover function 00221 * glover and revglover are implemented in "matching.hpp" 00222 */ 00223 00224 if (!match_fixed) { 00225 if (!glover(x,y,tau,phi,sequence,vertices)) 00226 return ES_FAILED; 00227 } else { 00228 for (int i = x.size(); i--; ) { 00229 phi[i] = z[i].val(); 00230 phiprime[i] = phi[i]; 00231 } 00232 } 00233 00234 for (int i = n; i--; ) 00235 if (!y[i].assigned()) { 00236 // phiprime is not needed to narrow the domains of the x-variables 00237 if (!match_fixed && 00238 !revglover(x,y,tau,phiprime,sequence,vertices)) 00239 return ES_FAILED; 00240 00241 if (!narrow_domy(home,x,y,phi,phiprime,nofix)) 00242 return ES_FAILED; 00243 00244 if (nofix && !match_fixed) { 00245 // data structures (matching) destroyed by domains with holes 00246 00247 for (int j = y.size(); j--; ) 00248 phi[j]=phiprime[j]=0; 00249 00250 if (!glover(x,y,tau,phi,sequence,vertices)) 00251 return ES_FAILED; 00252 00253 if (!revglover(x,y,tau,phiprime,sequence,vertices)) 00254 return ES_FAILED; 00255 00256 if (!narrow_domy(home,x,y,phi,phiprime,nofix)) 00257 return ES_FAILED; 00258 } 00259 break; 00260 } 00261 00262 /* 00263 * STEP 4: 00264 * Compute the strongly connected components in 00265 * the oriented intersection graph 00266 * the computation of the sccs is implemented in 00267 * "narrowing.hpp" in the function narrow_domx 00268 */ 00269 00270 int* scclist = r.alloc<int>(n); 00271 SccComponent* sinfo = r.alloc<SccComponent>(n); 00272 00273 for(int i = n; i--; ) 00274 sinfo[i].left=sinfo[i].right=sinfo[i].rightmost=sinfo[i].leftmost= i; 00275 00276 computesccs(home,x,y,phi,sinfo,scclist); 00277 00278 /* 00279 * STEP 5: 00280 * Narrow the domains of the variables 00281 * Also implemented in "narrowing.hpp" 00282 * in the functions narrow_domx and narrow_domy 00283 */ 00284 00285 if (!narrow_domx<View,Perm>(home,x,y,z,tau,phi,scclist,sinfo,nofix)) 00286 return ES_FAILED; 00287 00288 if (Perm) { 00289 if (!noperm_bc && 00290 !perm_bc<View> 00291 (home, tau, sinfo, scclist, x,z, repairpass, nofix)) 00292 return ES_FAILED; 00293 00294 // channeling also needed after normal propagation steps 00295 // in order to ensure consistency after possible modification in perm_bc 00296 if (!channel(home,x,y,z,nofix)) 00297 return ES_FAILED; 00298 if (nofix) 00299 return ES_NOFIX; 00300 } 00301 00302 sort_tau<View,Perm>(x,z,tau); 00303 00304 if (Perm) { 00305 // special case of sccs of size 2 denoted by permutation variables 00306 // used to enforce consistency from x to y 00307 // case of the upper bound ordering tau 00308 for (int i = x.size() - 1; i--; ) { 00309 // two x variables are in the same scc of size 2 00310 if (z[tau[i]].min() == z[tau[i+1]].min() && 00311 z[tau[i]].max() == z[tau[i+1]].max() && 00312 z[tau[i]].size() == 2 && z[tau[i]].range()) { 00313 // if bounds are strictly smaller 00314 if (x[tau[i]].max() < x[tau[i+1]].max()) { 00315 ModEvent me = y[z[tau[i]].min()].lq(home, x[tau[i]].max()); 00316 if (me_failed(me)) 00317 return ES_FAILED; 00318 nofix |= (me_modified(me) && 00319 y[z[tau[i]].min()].max() != x[tau[i]].max()); 00320 00321 me = y[z[tau[i+1]].max()].lq(home, x[tau[i+1]].max()); 00322 if (me_failed(me)) 00323 return ES_FAILED; 00324 nofix |= (me_modified(me) && 00325 y[z[tau[i+1]].max()].max() != x[tau[i+1]].max()); 00326 } 00327 } 00328 } 00329 } 00330 return nofix ? ES_NOFIX : ES_FIX; 00331 } 00332 00333 template<class View, bool Perm> 00334 forceinline Sorted<View,Perm>:: 00335 Sorted(Space& home, bool share, Sorted<View,Perm>& p): 00336 Propagator(home, share, p), 00337 reachable(p.reachable) { 00338 x.update(home, share, p.x); 00339 y.update(home, share, p.y); 00340 z.update(home, share, p.z); 00341 w.update(home, share, p.w); 00342 } 00343 00344 template<class View, bool Perm> 00345 Sorted<View,Perm>:: 00346 Sorted(Home home, 00347 ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) : 00348 Propagator(home), x(x0), y(y0), z(z0), w(home,y0), reachable(-1) { 00349 x.subscribe(home, *this, PC_INT_BND); 00350 y.subscribe(home, *this, PC_INT_BND); 00351 if (Perm) 00352 z.subscribe(home, *this, PC_INT_BND); 00353 } 00354 00355 template<class View, bool Perm> 00356 forceinline size_t 00357 Sorted<View,Perm>::dispose(Space& home) { 00358 x.cancel(home,*this, PC_INT_BND); 00359 y.cancel(home,*this, PC_INT_BND); 00360 if (Perm) 00361 z.cancel(home,*this, PC_INT_BND); 00362 (void) Propagator::dispose(home); 00363 return sizeof(*this); 00364 } 00365 00366 template<class View, bool Perm> 00367 Actor* Sorted<View,Perm>::copy(Space& home, bool share) { 00368 return new (home) Sorted<View,Perm>(home, share, *this); 00369 } 00370 00371 template<class View, bool Perm> 00372 PropCost Sorted<View,Perm>::cost(const Space&, const ModEventDelta&) const { 00373 return PropCost::linear(PropCost::LO, x.size()); 00374 } 00375 00376 template<class View, bool Perm> 00377 ExecStatus 00378 Sorted<View,Perm>::propagate(Space& home, const ModEventDelta&) { 00379 int n = x.size(); 00380 bool secondpass = false; 00381 bool nofix = false; 00382 int dropfst = 0; 00383 00384 bool subsumed = false; 00385 bool array_subs = false; 00386 bool match_fixed = false; 00387 00388 // normalization of x and y 00389 if (!normalize(home, y, x, nofix)) 00390 return ES_FAILED; 00391 00392 // create sigma sorting 00393 sort_sigma<View,Perm>(home,x,z); 00394 00395 bool noperm_bc = false; 00396 if (!array_assigned<View,Perm> 00397 (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc)) 00398 return ES_FAILED; 00399 00400 if (array_subs) 00401 return home.ES_SUBSUMED(*this); 00402 00403 sort_sigma<View,Perm>(home,x,z); 00404 00405 // in this case check_subsumptions is guaranteed to find 00406 // the xs ordered by sigma 00407 00408 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst)) 00409 return ES_FAILED; 00410 00411 if (subsumed) 00412 return home.ES_SUBSUMED(*this); 00413 00414 if (Perm) { 00415 // dropping possibly yields inconsistent indices on permutation variables 00416 if (dropfst) { 00417 reachable = w[dropfst - 1].max(); 00418 bool unreachable = true; 00419 for (int i = x.size(); unreachable && i-- ; ) { 00420 unreachable &= (reachable < x[i].min()); 00421 } 00422 00423 if (unreachable) { 00424 x.drop_fst(dropfst, home, *this, PC_INT_BND); 00425 y.drop_fst(dropfst, home, *this, PC_INT_BND); 00426 z.drop_fst(dropfst, home, *this, PC_INT_BND); 00427 } else { 00428 dropfst = 0; 00429 } 00430 } 00431 00432 n = x.size(); 00433 00434 if (n < 2) { 00435 if (x[0].max() < y[0].min() || y[0].max() < x[0].min()) 00436 return ES_FAILED; 00437 if (Perm) { 00438 GECODE_ME_CHECK(z[0].eq(home, w.size() - 1)); 00439 } 00440 GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0]))); 00441 } 00442 00443 // check whether shifting the permutation variables 00444 // is necessary after dropping x and y vars 00445 // highest reachable index 00446 int valid = n - 1; 00447 int index = 0; 00448 int shift = 0; 00449 00450 for (int i = n; i--; ){ 00451 if (z[i].max() > index) 00452 index = z[i].max(); 00453 if (index > valid) 00454 shift = index - valid; 00455 } 00456 00457 if (shift) { 00458 ViewArray<OffsetView> ox(home,n), oy(home,n), oz(home,n); 00459 00460 for (int i = n; i--; ) { 00461 GECODE_ME_CHECK(z[i].gq(home, shift)); 00462 00463 oz[i] = OffsetView(z[i], -shift); 00464 ox[i] = OffsetView(x[i], 0); 00465 oy[i] = OffsetView(y[i], 0); 00466 } 00467 00468 GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm> 00469 (home,*this,ox,oy,oz,secondpass,nofix,match_fixed))); 00470 00471 if (secondpass) { 00472 GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm> 00473 (home,*this,ox,oy,oz,secondpass,nofix,match_fixed))); 00474 } 00475 } else { 00476 GECODE_ES_CHECK((bounds_propagation<View,Perm> 00477 (home,*this,x,y,z,secondpass,nofix,match_fixed))); 00478 00479 if (secondpass) { 00480 GECODE_ES_CHECK((bounds_propagation<View,Perm> 00481 (home,*this,x,y,z,secondpass,nofix,match_fixed))); 00482 } 00483 } 00484 } else { 00485 // dropping has no consequences 00486 if (dropfst) { 00487 x.drop_fst(dropfst, home, *this, PC_INT_BND); 00488 y.drop_fst(dropfst, home, *this, PC_INT_BND); 00489 } 00490 00491 n = x.size(); 00492 00493 if (n < 2) { 00494 if (x[0].max() < y[0].min() || y[0].max() < x[0].min()) 00495 return ES_FAILED; 00496 GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0]))); 00497 } 00498 00499 GECODE_ES_CHECK((bounds_propagation<View,Perm> 00500 (home, *this, x, y, z,secondpass, nofix, match_fixed))); 00501 // no second pass possible if there are no permvars 00502 } 00503 00504 if (!normalize(home, y, x, nofix)) 00505 return ES_FAILED; 00506 00507 Region r(home); 00508 int* tau = r.alloc<int>(n); 00509 if (match_fixed) { 00510 // sorting is determined 00511 // sigma and tau coincide 00512 for (int i = x.size(); i--; ) { 00513 int pi = z[i].val(); 00514 tau[pi] = i; 00515 } 00516 } else { 00517 for (int i = n; i--; ) { 00518 tau[i] = i; 00519 } 00520 } 00521 00522 sort_tau<View,Perm>(x,z,tau); 00523 // recreate consistency for already assigned subparts 00524 // in order of the upper bounds starting at the end of the array 00525 bool xbassigned = true; 00526 for (int i = x.size(); i--; ) { 00527 if (x[tau[i]].assigned() && xbassigned) { 00528 GECODE_ME_CHECK(y[i].eq(home, x[tau[i]].val())); 00529 } else { 00530 xbassigned = false; 00531 } 00532 } 00533 00534 subsumed = true; 00535 array_subs = false; 00536 noperm_bc = false; 00537 00538 // creating sorting anew 00539 sort_sigma<View,Perm>(home,x,z); 00540 00541 if (Perm) { 00542 for (int i = 0; i < x.size() - 1; i++) { 00543 // special case of subsccs of size2 for the lower bounds 00544 // two x variables are in the same scc of size 2 00545 if (z[i].min() == z[i+1].min() && 00546 z[i].max() == z[i+1].max() && 00547 z[i].size() == 2 && z[i].range()) { 00548 if (x[i].min() < x[i+1].min()) { 00549 ModEvent me = y[z[i].min()].gq(home, x[i].min()); 00550 GECODE_ME_CHECK(me); 00551 nofix |= (me_modified(me) && 00552 y[z[i].min()].min() != x[i].min()); 00553 00554 me = y[z[i+1].max()].gq(home, x[i+1].min()); 00555 GECODE_ME_CHECK(me); 00556 nofix |= (me_modified(me) && 00557 y[z[i+1].max()].min() != x[i+1].min()); 00558 } 00559 } 00560 } 00561 } 00562 00563 // check assigned 00564 // should be sorted 00565 bool xassigned = true; 00566 for (int i = 0; i < x.size(); i++) { 00567 if (x[i].assigned() && xassigned) { 00568 GECODE_ME_CHECK(y[i].eq(home,x[i].val())); 00569 } else { 00570 xassigned = false; 00571 } 00572 } 00573 00574 // sorted check bounds 00575 // final check that variables are consitent with least and greatest possible 00576 // values 00577 int tlb = std::min(x[0].min(), y[0].min()); 00578 int tub = std::max(x[x.size() - 1].max(), y[y.size() - 1].max()); 00579 for (int i = x.size(); i--; ) { 00580 ModEvent me = y[i].lq(home, tub); 00581 GECODE_ME_CHECK(me); 00582 nofix |= me_modified(me) && (y[i].max() != tub); 00583 00584 me = y[i].gq(home, tlb); 00585 GECODE_ME_CHECK(me); 00586 nofix |= me_modified(me) && (y[i].min() != tlb); 00587 00588 me = x[i].lq(home, tub); 00589 GECODE_ME_CHECK(me); 00590 nofix |= me_modified(me) && (x[i].max() != tub); 00591 00592 me = x[i].gq(home, tlb); 00593 GECODE_ME_CHECK(me); 00594 nofix |= me_modified(me) && (x[i].min() != tlb); 00595 } 00596 00597 if (!array_assigned<View,Perm> 00598 (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc)) 00599 return ES_FAILED; 00600 00601 if (array_subs) 00602 return home.ES_SUBSUMED(*this); 00603 00604 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst)) 00605 return ES_FAILED; 00606 00607 if (subsumed) 00608 return home.ES_SUBSUMED(*this); 00609 00610 return nofix ? ES_NOFIX : ES_FIX; 00611 } 00612 00613 template<class View, bool Perm> 00614 ExecStatus 00615 Sorted<View,Perm>:: 00616 post(Home home, 00617 ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) { 00618 int n = x0.size(); 00619 if (n < 2) { 00620 if ((x0[0].max() < y0[0].min()) || (y0[0].max() < x0[0].min())) 00621 return ES_FAILED; 00622 GECODE_ES_CHECK((Rel::EqBnd<View,View>::post(home,x0[0],y0[0]))); 00623 if (Perm) { 00624 GECODE_ME_CHECK(z0[0].eq(home,0)); 00625 } 00626 } else { 00627 if (Perm) { 00628 ViewArray<View> z(home,n); 00629 for (int i=n; i--; ) { 00630 z[i]=z0[i]; 00631 GECODE_ME_CHECK(z[i].gq(home,0)); 00632 GECODE_ME_CHECK(z[i].lq(home,n-1)); 00633 } 00634 GECODE_ES_CHECK(Distinct::Bnd<View>::post(home,z)); 00635 } 00636 new (home) Sorted<View,Perm>(home,x0,y0,z0); 00637 } 00638 return ES_OK; 00639 } 00640 00641 }}} 00642 00643 // STATISTICS: int-prop 00644 00645 00646