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-03-03 17:32:21 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $ 00011 * $Revision: 10364 $ 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 // minimum bound 00108 int mib = y[0].min(); 00109 // maximum bound 00110 int mab = y[n - 1].max(); 00111 // interval size 00112 int ivs = (mab - mib + 1); 00113 Rank* allbnd = r.alloc<Rank>(ivs); 00114 int iter = mib; 00115 int idx = 0; 00116 while(iter <= mab && idx < n) { 00117 if (y[idx].min() > iter) { 00118 // idx cannot be zero because consisteny in posting 00119 assert(idx > 0); 00120 allbnd[iter - mib].min = idx; 00121 allbnd[iter - mib].max = idx - 1; 00122 iter++; 00123 } else { 00124 if (y[idx].min() <= iter && iter <= y[idx].max() ) { 00125 allbnd[iter - mib].min = idx; 00126 allbnd[iter - mib].max = idx; 00127 iter++; 00128 } else { 00129 idx++; 00130 } 00131 } 00132 } 00133 00134 iter = mab; 00135 idx = n -1; 00136 while(iter >= mib && idx >= 0) { 00137 if (y[idx].min() > iter) { 00138 // idx cannot be zero because consisteny in posting 00139 assert(idx > 0); 00140 allbnd[iter - mib].max = idx - 1; 00141 iter--; 00142 } else { 00143 if (y[idx].min() <= iter && iter <= y[idx].max() ) { 00144 allbnd[iter - mib].max = idx; 00145 iter--; 00146 } else { 00147 idx--; 00148 } 00149 } 00150 } 00151 00152 for (int i = n; i--; ) { 00153 // minimum reachable y-variable 00154 int minr = allbnd[x[i].min() - mib].min; 00155 int maxr = allbnd[x[i].max() - mib].max; 00156 00157 ModEvent me = x[i].gq(home, y[minr].min()); 00158 if (me_failed(me)) 00159 return ES_FAILED; 00160 nofix |= (me_modified(me) && (x[i].min() != y[minr].min())); 00161 00162 me = x[i].lq(home, y[maxr].max()); 00163 if (me_failed(me)) 00164 return ES_FAILED; 00165 nofix |= (me_modified(me) && (x[i].min() != y[maxr].max())); 00166 00167 me = z[i].gq(home, minr); 00168 if (me_failed(me)) 00169 return ES_FAILED; 00170 nofix |= (me_modified(me) && (z[i].min() != minr)); 00171 00172 me = z[i].lq(home, maxr); 00173 if (me_failed(me)) 00174 return ES_FAILED; 00175 nofix |= (me_modified(me) && (z[i].max() != maxr)); 00176 } 00177 00178 // channel information from x to y through permutation variables in z 00179 if (!channel(home,x,y,z,nofix)) 00180 return ES_FAILED; 00181 if (nofix) 00182 return ES_NOFIX; 00183 } 00184 00185 /* 00186 * STEP 1: 00187 * normalization is implemented in "order.hpp" 00188 * o setting the lower bounds of the y_i domains (\lb E_i) 00189 * to max(\lb E_{i-1},\lb E_i) 00190 * o setting the upper bounds of the y_i domains (\ub E_i) 00191 * to min(\ub E_i,\ub E_{i+1}) 00192 */ 00193 00194 if (!normalize(home, y, x, nofix)) 00195 return ES_FAILED; 00196 00197 if (Perm) { 00198 // check consistency of channeling after normalization 00199 if (!channel(home,x,y,z,nofix)) 00200 return ES_FAILED; 00201 if (nofix) 00202 return ES_NOFIX; 00203 } 00204 00205 00206 // if bounds have changed we have to recreate sigma to restore 00207 // optimized dropping of variables 00208 00209 sort_sigma<View,Perm>(home,x,z); 00210 00211 bool subsumed = true; 00212 bool array_subs = false; 00213 int dropfst = 0; 00214 bool noperm_bc = false; 00215 00216 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst) || 00217 !array_assigned<View,Perm>(home,x,y,z,array_subs,match_fixed,nofix,noperm_bc)) 00218 return ES_FAILED; 00219 00220 if (subsumed || array_subs) 00221 return home.ES_SUBSUMED(p); 00222 00223 /* 00224 * STEP 2: creating tau 00225 * Sort the domains of the x variables according 00226 * to their lower bounds, where we use an 00227 * intermediate array of integers for sorting 00228 */ 00229 sort_tau<View,Perm>(x,z,tau); 00230 00231 /* 00232 * STEP 3: 00233 * Compute the matchings \phi and \phi' between 00234 * the x and the y variables 00235 * with Glover's matching algorithm. 00236 * o phi is computed with the glover function 00237 * o phiprime is computed with the revglover function 00238 * glover and revglover are implemented in "matching.hpp" 00239 */ 00240 00241 if (!match_fixed) { 00242 if (!glover(x,y,tau,phi,sequence,vertices)) 00243 return ES_FAILED; 00244 } else { 00245 for (int i = x.size(); i--; ) { 00246 phi[i] = z[i].val(); 00247 phiprime[i] = phi[i]; 00248 } 00249 } 00250 00251 for (int i = n; i--; ) 00252 if (!y[i].assigned()) { 00253 // phiprime is not needed to narrow the domains of the x-variables 00254 if (!match_fixed && 00255 !revglover(x,y,tau,phiprime,sequence,vertices)) 00256 return ES_FAILED; 00257 00258 if (!narrow_domy(home,x,y,phi,phiprime,nofix)) 00259 return ES_FAILED; 00260 00261 if (nofix && !match_fixed) { 00262 // data structures (matching) destroyed by domains with holes 00263 00264 for (int j = y.size(); j--; ) 00265 phi[j]=phiprime[j]=0; 00266 00267 if (!glover(x,y,tau,phi,sequence,vertices)) 00268 return ES_FAILED; 00269 00270 if (!revglover(x,y,tau,phiprime,sequence,vertices)) 00271 return ES_FAILED; 00272 00273 if (!narrow_domy(home,x,y,phi,phiprime,nofix)) 00274 return ES_FAILED; 00275 } 00276 break; 00277 } 00278 00279 /* 00280 * STEP 4: 00281 * Compute the strongly connected components in 00282 * the oriented intersection graph 00283 * the computation of the sccs is implemented in 00284 * "narrowing.hpp" in the function narrow_domx 00285 */ 00286 00287 int* scclist = r.alloc<int>(n); 00288 SccComponent* sinfo = r.alloc<SccComponent>(n); 00289 00290 for(int i = n; i--; ) 00291 sinfo[i].left=sinfo[i].right=sinfo[i].rightmost=sinfo[i].leftmost= i; 00292 00293 computesccs(home,x,y,phi,sinfo,scclist); 00294 00295 /* 00296 * STEP 5: 00297 * Narrow the domains of the variables 00298 * Also implemented in "narrowing.hpp" 00299 * in the functions narrow_domx and narrow_domy 00300 */ 00301 00302 if (!narrow_domx<View,Perm>(home,x,y,z,tau,phi,scclist,sinfo,nofix)) 00303 return ES_FAILED; 00304 00305 if (Perm) { 00306 if (!noperm_bc && 00307 !perm_bc<View> 00308 (home, tau, sinfo, scclist, x,z, repairpass, nofix)) 00309 return ES_FAILED; 00310 00311 // channeling also needed after normal propagation steps 00312 // in order to ensure consistency after possible modification in perm_bc 00313 if (!channel(home,x,y,z,nofix)) 00314 return ES_FAILED; 00315 if (nofix) 00316 return ES_NOFIX; 00317 } 00318 00319 sort_tau<View,Perm>(x,z,tau); 00320 00321 if (Perm) { 00322 // special case of sccs of size 2 denoted by permutation variables 00323 // used to enforce consistency from x to y 00324 // case of the upper bound ordering tau 00325 for (int i = x.size() - 1; i--; ) { 00326 // two x variables are in the same scc of size 2 00327 if (z[tau[i]].min() == z[tau[i+1]].min() && 00328 z[tau[i]].max() == z[tau[i+1]].max() && 00329 z[tau[i]].size() == 2 && z[tau[i]].range()) { 00330 // if bounds are strictly smaller 00331 if (x[tau[i]].max() < x[tau[i+1]].max()) { 00332 ModEvent me = y[z[tau[i]].min()].lq(home, x[tau[i]].max()); 00333 if (me_failed(me)) 00334 return ES_FAILED; 00335 nofix |= (me_modified(me) && 00336 y[z[tau[i]].min()].max() != x[tau[i]].max()); 00337 00338 me = y[z[tau[i+1]].max()].lq(home, x[tau[i+1]].max()); 00339 if (me_failed(me)) 00340 return ES_FAILED; 00341 nofix |= (me_modified(me) && 00342 y[z[tau[i+1]].max()].max() != x[tau[i+1]].max()); 00343 } 00344 } 00345 } 00346 } 00347 return nofix ? ES_NOFIX : ES_FIX; 00348 } 00349 00350 template<class View, bool Perm> 00351 forceinline Sorted<View,Perm>:: 00352 Sorted(Space& home, bool share, Sorted<View,Perm>& p): 00353 Propagator(home, share, p), 00354 reachable(p.reachable) { 00355 x.update(home, share, p.x); 00356 y.update(home, share, p.y); 00357 z.update(home, share, p.z); 00358 w.update(home, share, p.w); 00359 } 00360 00361 template<class View, bool Perm> 00362 Sorted<View,Perm>:: 00363 Sorted(Home home, 00364 ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) : 00365 Propagator(home), x(x0), y(y0), z(z0), w(home,y0), reachable(-1) { 00366 x.subscribe(home, *this, PC_INT_BND); 00367 y.subscribe(home, *this, PC_INT_BND); 00368 if (Perm) 00369 z.subscribe(home, *this, PC_INT_BND); 00370 } 00371 00372 template<class View, bool Perm> 00373 forceinline size_t 00374 Sorted<View,Perm>::dispose(Space& home) { 00375 x.cancel(home,*this, PC_INT_BND); 00376 y.cancel(home,*this, PC_INT_BND); 00377 if (Perm) 00378 z.cancel(home,*this, PC_INT_BND); 00379 (void) Propagator::dispose(home); 00380 return sizeof(*this); 00381 } 00382 00383 template<class View, bool Perm> 00384 Actor* Sorted<View,Perm>::copy(Space& home, bool share) { 00385 return new (home) Sorted<View,Perm>(home, share, *this); 00386 } 00387 00388 template<class View, bool Perm> 00389 PropCost Sorted<View,Perm>::cost(const Space&, const ModEventDelta&) const { 00390 return PropCost::linear(PropCost::LO, x.size()); 00391 } 00392 00393 template<class View, bool Perm> 00394 ExecStatus 00395 Sorted<View,Perm>::propagate(Space& home, const ModEventDelta&) { 00396 int n = x.size(); 00397 bool secondpass = false; 00398 bool nofix = false; 00399 int dropfst = 0; 00400 00401 bool subsumed = false; 00402 bool array_subs = false; 00403 bool match_fixed = false; 00404 00405 // normalization of x and y 00406 if (!normalize(home, y, x, nofix)) 00407 return ES_FAILED; 00408 00409 // create sigma sorting 00410 sort_sigma<View,Perm>(home,x,z); 00411 00412 bool noperm_bc = false; 00413 if (!array_assigned<View,Perm> 00414 (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc)) 00415 return ES_FAILED; 00416 00417 if (array_subs) 00418 return home.ES_SUBSUMED(*this); 00419 00420 sort_sigma<View,Perm>(home,x,z); 00421 00422 // in this case check_subsumptions is guaranteed to find 00423 // the xs ordered by sigma 00424 00425 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst)) 00426 return ES_FAILED; 00427 00428 if (subsumed) 00429 return home.ES_SUBSUMED(*this); 00430 00431 if (Perm) { 00432 // dropping possibly yields inconsistent indices on permutation variables 00433 if (dropfst) { 00434 reachable = w[dropfst - 1].max(); 00435 bool unreachable = true; 00436 for (int i = x.size(); unreachable && i-- ; ) { 00437 unreachable &= (reachable < x[i].min()); 00438 } 00439 00440 if (unreachable) { 00441 x.drop_fst(dropfst, home, *this, PC_INT_BND); 00442 y.drop_fst(dropfst, home, *this, PC_INT_BND); 00443 z.drop_fst(dropfst, home, *this, PC_INT_BND); 00444 } else { 00445 dropfst = 0; 00446 } 00447 } 00448 00449 n = x.size(); 00450 00451 if (n < 2) { 00452 if (x[0].max() < y[0].min() || y[0].max() < x[0].min()) 00453 return ES_FAILED; 00454 if (Perm) { 00455 GECODE_ME_CHECK(z[0].eq(home, w.size() - 1)); 00456 } 00457 GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0]))); 00458 } 00459 00460 // check whether shifting the permutation variables 00461 // is necessary after dropping x and y vars 00462 // highest reachable index 00463 int valid = n - 1; 00464 int index = 0; 00465 int shift = 0; 00466 00467 for (int i = n; i--; ){ 00468 if (z[i].max() > index) 00469 index = z[i].max(); 00470 if (index > valid) 00471 shift = index - valid; 00472 } 00473 00474 if (shift) { 00475 ViewArray<OffsetView> ox(home,n), oy(home,n), oz(home,n); 00476 00477 for (int i = n; i--; ) { 00478 GECODE_ME_CHECK(z[i].gq(home, shift)); 00479 00480 oz[i] = OffsetView(z[i], -shift); 00481 ox[i] = OffsetView(x[i], 0); 00482 oy[i] = OffsetView(y[i], 0); 00483 } 00484 00485 GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm> 00486 (home,*this,ox,oy,oz,secondpass,nofix,match_fixed))); 00487 00488 if (secondpass) { 00489 GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm> 00490 (home,*this,ox,oy,oz,secondpass,nofix,match_fixed))); 00491 } 00492 } else { 00493 GECODE_ES_CHECK((bounds_propagation<View,Perm> 00494 (home,*this,x,y,z,secondpass,nofix,match_fixed))); 00495 00496 if (secondpass) { 00497 GECODE_ES_CHECK((bounds_propagation<View,Perm> 00498 (home,*this,x,y,z,secondpass,nofix,match_fixed))); 00499 } 00500 } 00501 } else { 00502 // dropping has no consequences 00503 if (dropfst) { 00504 x.drop_fst(dropfst, home, *this, PC_INT_BND); 00505 y.drop_fst(dropfst, home, *this, PC_INT_BND); 00506 } 00507 00508 n = x.size(); 00509 00510 if (n < 2) { 00511 if (x[0].max() < y[0].min() || y[0].max() < x[0].min()) 00512 return ES_FAILED; 00513 GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0]))); 00514 } 00515 00516 GECODE_ES_CHECK((bounds_propagation<View,Perm> 00517 (home, *this, x, y, z,secondpass, nofix, match_fixed))); 00518 // no second pass possible if there are no permvars 00519 } 00520 00521 if (!normalize(home, y, x, nofix)) 00522 return ES_FAILED; 00523 00524 Region r(home); 00525 int* tau = r.alloc<int>(n); 00526 if (match_fixed) { 00527 // sorting is determined 00528 // sigma and tau coincide 00529 for (int i = x.size(); i--; ) { 00530 int pi = z[i].val(); 00531 tau[pi] = i; 00532 } 00533 } else { 00534 for (int i = n; i--; ) { 00535 tau[i] = i; 00536 } 00537 } 00538 00539 sort_tau<View,Perm>(x,z,tau); 00540 // recreate consistency for already assigned subparts 00541 // in order of the upper bounds starting at the end of the array 00542 bool xbassigned = true; 00543 for (int i = x.size(); i--; ) { 00544 if (x[tau[i]].assigned() && xbassigned) { 00545 GECODE_ME_CHECK(y[i].eq(home, x[tau[i]].val())); 00546 } else { 00547 xbassigned = false; 00548 } 00549 } 00550 00551 subsumed = true; 00552 array_subs = false; 00553 noperm_bc = false; 00554 00555 // creating sorting anew 00556 sort_sigma<View,Perm>(home,x,z); 00557 00558 if (Perm) { 00559 for (int i = 0; i < x.size() - 1; i++) { 00560 // special case of subsccs of size2 for the lower bounds 00561 // two x variables are in the same scc of size 2 00562 if (z[i].min() == z[i+1].min() && 00563 z[i].max() == z[i+1].max() && 00564 z[i].size() == 2 && z[i].range()) { 00565 if (x[i].min() < x[i+1].min()) { 00566 ModEvent me = y[z[i].min()].gq(home, x[i].min()); 00567 GECODE_ME_CHECK(me); 00568 nofix |= (me_modified(me) && 00569 y[z[i].min()].min() != x[i].min()); 00570 00571 me = y[z[i+1].max()].gq(home, x[i+1].min()); 00572 GECODE_ME_CHECK(me); 00573 nofix |= (me_modified(me) && 00574 y[z[i+1].max()].min() != x[i+1].min()); 00575 } 00576 } 00577 } 00578 } 00579 00580 // check assigned 00581 // should be sorted 00582 bool xassigned = true; 00583 for (int i = 0; i < x.size(); i++) { 00584 if (x[i].assigned() && xassigned) { 00585 GECODE_ME_CHECK(y[i].eq(home,x[i].val())); 00586 } else { 00587 xassigned = false; 00588 } 00589 } 00590 00591 // sorted check bounds 00592 // final check that variables are consitent with least and greatest possible 00593 // values 00594 int tlb = std::min(x[0].min(), y[0].min()); 00595 int tub = std::max(x[x.size() - 1].max(), y[y.size() - 1].max()); 00596 for (int i = x.size(); i--; ) { 00597 ModEvent me = y[i].lq(home, tub); 00598 GECODE_ME_CHECK(me); 00599 nofix |= me_modified(me) && (y[i].max() != tub); 00600 00601 me = y[i].gq(home, tlb); 00602 GECODE_ME_CHECK(me); 00603 nofix |= me_modified(me) && (y[i].min() != tlb); 00604 00605 me = x[i].lq(home, tub); 00606 GECODE_ME_CHECK(me); 00607 nofix |= me_modified(me) && (x[i].max() != tub); 00608 00609 me = x[i].gq(home, tlb); 00610 GECODE_ME_CHECK(me); 00611 nofix |= me_modified(me) && (x[i].min() != tlb); 00612 } 00613 00614 if (!array_assigned<View,Perm> 00615 (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc)) 00616 return ES_FAILED; 00617 00618 if (array_subs) 00619 return home.ES_SUBSUMED(*this); 00620 00621 if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst)) 00622 return ES_FAILED; 00623 00624 if (subsumed) 00625 return home.ES_SUBSUMED(*this); 00626 00627 return nofix ? ES_NOFIX : ES_FIX; 00628 } 00629 00630 template<class View, bool Perm> 00631 ExecStatus 00632 Sorted<View,Perm>:: 00633 post(Home home, 00634 ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) { 00635 int n = x0.size(); 00636 if (n < 2) { 00637 if ((x0[0].max() < y0[0].min()) || (y0[0].max() < x0[0].min())) 00638 return ES_FAILED; 00639 GECODE_ES_CHECK((Rel::EqBnd<View,View>::post(home,x0[0],y0[0]))); 00640 if (Perm) { 00641 GECODE_ME_CHECK(z0[0].eq(home,0)); 00642 } 00643 } else { 00644 if (Perm) { 00645 ViewArray<View> z(home,n); 00646 for (int i=n; i--; ) { 00647 z[i]=z0[i]; 00648 GECODE_ME_CHECK(z[i].gq(home,0)); 00649 GECODE_ME_CHECK(z[i].lq(home,n-1)); 00650 } 00651 GECODE_ES_CHECK(Distinct::Bnd<View>::post(home,z)); 00652 } 00653 new (home) Sorted<View,Perm>(home,x0,y0,z0); 00654 } 00655 return ES_OK; 00656 } 00657 00658 }}} 00659 00660 // STATISTICS: int-prop 00661 00662 00663