bnd.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 * Contributing authors: 00007 * Christian Schulte <schulte@gecode.org> 00008 * Guido Tack <tack@gecode.org> 00009 * 00010 * Copyright: 00011 * Patrick Pekczynski, 2004/2005 00012 * Christian Schulte, 2009 00013 * Guido Tack, 2009 00014 * 00015 * Last modified: 00016 * $Date: 2010-03-03 17:32:21 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $ 00017 * $Revision: 10364 $ 00018 * 00019 * This file is part of Gecode, the generic constraint 00020 * development environment: 00021 * http://www.gecode.org 00022 * 00023 * Permission is hereby granted, free of charge, to any person obtaining 00024 * a copy of this software and associated documentation files (the 00025 * "Software"), to deal in the Software without restriction, including 00026 * without limitation the rights to use, copy, modify, merge, publish, 00027 * distribute, sublicense, and/or sell copies of the Software, and to 00028 * permit persons to whom the Software is furnished to do so, subject to 00029 * the following conditions: 00030 * 00031 * The above copyright notice and this permission notice shall be 00032 * included in all copies or substantial portions of the Software. 00033 * 00034 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00035 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00036 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00037 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00038 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00039 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00040 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00041 * 00042 */ 00043 00044 namespace Gecode { namespace Int { namespace GCC { 00045 00046 template<class Card> 00047 forceinline 00048 Bnd<Card>:: 00049 Bnd(Home home, ViewArray<IntView>& x0, ViewArray<Card>& k0, 00050 bool cf, bool nolbc) : 00051 Propagator(home), x(x0), y(home, x0), k(k0), 00052 card_fixed(cf), skip_lbc(nolbc) { 00053 y.subscribe(home, *this, PC_INT_BND); 00054 k.subscribe(home, *this, PC_INT_BND); 00055 } 00056 00057 template<class Card> 00058 forceinline 00059 Bnd<Card>:: 00060 Bnd(Space& home, bool share, Bnd<Card>& p) 00061 : Propagator(home, share, p), 00062 card_fixed(p.card_fixed), skip_lbc(p.skip_lbc) { 00063 x.update(home, share, p.x); 00064 y.update(home, share, p.y); 00065 k.update(home, share, p.k); 00066 } 00067 00068 template<class Card> 00069 forceinline size_t 00070 Bnd<Card>::dispose(Space& home) { 00071 y.cancel(home,*this, PC_INT_BND); 00072 k.cancel(home,*this, PC_INT_BND); 00073 (void) Propagator::dispose(home); 00074 return sizeof(*this); 00075 } 00076 00077 template<class Card> 00078 Actor* 00079 Bnd<Card>::copy(Space& home, bool share) { 00080 return new (home) Bnd<Card>(home,share,*this); 00081 } 00082 00083 template<class Card> 00084 PropCost 00085 Bnd<Card>::cost(const Space&, 00086 const ModEventDelta& med) const { 00087 int n_k = Card::propagate ? k.size() : 0; 00088 if (IntView::me(med) == ME_INT_VAL) 00089 return PropCost::linear(PropCost::LO, y.size() + n_k); 00090 else 00091 return PropCost::quadratic(PropCost::LO, x.size() + n_k); 00092 } 00093 00094 00095 template<class Card> 00096 forceinline ExecStatus 00097 Bnd<Card>::lbc(Space& home, int& nb, 00098 HallInfo hall[], Rank rank[], int mu[], int nu[]) { 00099 int n = x.size(); 00100 00101 /* 00102 * Let I(S) denote the number of variables whose domain intersects 00103 * the set S and C(S) the number of variables whose domain is containded 00104 * in S. Let further min_cap(S) be the minimal number of variables 00105 * that must be assigned to values, that is 00106 * min_cap(S) is the sum over all l[i] for a value v_i that is an 00107 * element of S. 00108 * 00109 * A failure set is a set F if 00110 * I(F) < min_cap(F) 00111 * An unstable set is a set U if 00112 * I(U) = min_cap(U) 00113 * A stable set is a set S if 00114 * C(S) > min_cap(S) and S intersetcs nor 00115 * any failure set nor any unstable set 00116 * forall unstable and failure sets 00117 * 00118 * failure sets determine the satisfiability of the LBC 00119 * unstable sets have to be pruned 00120 * stable set do not have to be pruned 00121 * 00122 * hall[].ps ~ stores the unstable 00123 * sets that have to be pruned 00124 * hall[].s ~ stores sets that must not be pruned 00125 * hall[].h ~ contains stable and unstable sets 00126 * hall[].d ~ contains the difference between interval bounds, i.e. 00127 * the minimal capacity of the interval 00128 * hall[].t ~ contains the critical capacity pointer, pointing to the 00129 * values 00130 */ 00131 00132 // LBC lower bounds 00133 00134 int i = 0; 00135 int j = 0; 00136 int w = 0; 00137 int z = 0; 00138 int v = 0; 00139 00140 //initialization of the tree structure 00141 int rightmost = nb + 1; // rightmost accesible value in bounds 00142 int bsize = nb + 2; 00143 w = rightmost; 00144 00145 // test 00146 // unused but uninitialized 00147 hall[0].d = 0; 00148 hall[0].s = 0; 00149 hall[0].ps = 0; 00150 00151 for (i = bsize; --i; ) { // i must not be zero 00152 int pred = i - 1; 00153 hall[i].s = pred; 00154 hall[i].ps = pred; 00155 hall[i].d = lps.sumup(hall[pred].bounds, hall[i].bounds - 1); 00156 00157 /* Let [hall[i].bounds,hall[i-1].bounds]=:I 00158 * If the capacity is zero => min_cap(I) = 0 00159 * => I cannot be a failure set 00160 * => I is an unstable set 00161 */ 00162 if (hall[i].d == 0) { 00163 hall[pred].h = w; 00164 } else { 00165 hall[w].h = pred; 00166 w = pred; 00167 } 00168 } 00169 00170 w = rightmost; 00171 for (i = bsize; i--; ) { // i can be zero 00172 hall[i].t = i - 1; 00173 if (hall[i].d == 0) { 00174 hall[i].t = w; 00175 } else { 00176 hall[w].t = i; 00177 w = i; 00178 } 00179 } 00180 00181 /* 00182 * The algorithm assigns to each value v in bounds 00183 * empty buckets corresponding to the minimal capacity l[i] to be 00184 * filled for v. (the buckets correspond to hall[].d containing the 00185 * difference between the interval bounds) Processing it 00186 * searches for the smallest value v in dom(x_i) that has an 00187 * empty bucket, i.e. if all buckets are filled it is guaranteed 00188 * that there are at least l[i] variables that will be 00189 * instantiated to v. Since the buckets are initially empty, 00190 * they are considered as FAILURE SETS 00191 */ 00192 00193 for (i = 0; i < n; i++) { 00194 // visit intervals in increasing max order 00195 int x0 = rank[mu[i]].min; 00196 int y = rank[mu[i]].max; 00197 int succ = x0 + 1; 00198 z = pathmax_t(hall, succ); 00199 j = hall[z].t; 00200 00201 /* 00202 * POTENTIALLY STABLE SET: 00203 * z \neq succ \Leftrigharrow z>succ, i.e. 00204 * min(D_{\mu(i)}) is guaranteed to occur min(K_i) times 00205 * \Rightarrow [x0, min(y,z)] is potentially stable 00206 */ 00207 00208 if (z != succ) { 00209 w = pathmax_ps(hall, succ); 00210 v = hall[w].ps; 00211 pathset_ps(hall, succ, w, w); 00212 w = std::min(y, z); 00213 pathset_ps(hall, hall[w].ps, v, w); 00214 hall[w].ps = v; 00215 } 00216 00217 /* 00218 * STABLE SET: 00219 * being stable implies being potentially stable, i.e. 00220 * [hall[y].ps, hall[y].bounds-1] is the largest stable subset of 00221 * [hall[j].bounds, hall[y].bounds-1]. 00222 */ 00223 00224 if (hall[z].d <= lps.sumup(hall[y].bounds, hall[z].bounds - 1)) { 00225 w = pathmax_s(hall, hall[y].ps); 00226 pathset_s(hall, hall[y].ps, w, w); 00227 // Path compression 00228 v = hall[w].s; 00229 pathset_s(hall, hall[y].s, v, y); 00230 hall[y].s = v; 00231 } else { 00232 /* 00233 * FAILURE SET: 00234 * If the considered interval [x0,y] is neither POTENTIALLY STABLE 00235 * nor STABLE there are still buckets that can be filled, 00236 * therefore d can be decreased. If d equals zero the intervals 00237 * minimum capacity is met and thepath can be compressed to the 00238 * next value having an empty bucket. 00239 * see DOMINATION in "ubc" 00240 */ 00241 if (--hall[z].d == 0) { 00242 hall[z].t = z + 1; 00243 z = pathmax_t(hall, hall[z].t); 00244 hall[z].t = j; 00245 } 00246 00247 /* 00248 * FINDING NEW LOWER BOUND: 00249 * If the lower bound belongs to an unstable or a stable set, 00250 * remind the new value we might assigned to the lower bound 00251 * in case the variable doesn't belong to a stable set. 00252 */ 00253 if (hall[x0].h > x0) { 00254 hall[i].newBound = pathmax_h(hall, x0); 00255 w = hall[i].newBound; 00256 pathset_h(hall, x0, w, w); // path compression 00257 } else { 00258 // Do not shrink the variable: take old min as new min 00259 hall[i].newBound = x0; 00260 } 00261 00262 /* UNSTABLE SET 00263 * If an unstable set is discovered 00264 * the difference between the interval bounds is equal to the 00265 * number of variables whose domain intersect the interval 00266 * (see ZEROTEST in "gcc") 00267 */ 00268 // CLEARLY THIS WAS NOT STABLE == UNSTABLE 00269 if (hall[z].d == lps.sumup(hall[y].bounds, hall[z].bounds - 1)) { 00270 if (hall[y].h > y) 00271 /* 00272 * y is not the end of the potentially stable set 00273 * thus ensure that the potentially stable superset is marked 00274 */ 00275 y = hall[y].h; 00276 // Equivalent to pathmax since the path is fully compressed 00277 pathset_h(hall, hall[y].h, j-1, y); 00278 // mark the new unstable set [j,y] 00279 hall[y].h = j-1; 00280 } 00281 } 00282 pathset_t(hall, succ, z, z); // path compression 00283 } 00284 00285 /* If there is a FAILURE SET left the minimum occurences of the values 00286 * are not guaranteed. In order to satisfy the LBC the last value 00287 * in the stable and unstable datastructure hall[].h must point to 00288 * the sentinel at the beginning of bounds. 00289 */ 00290 if (hall[nb].h != 0) 00291 return ES_FAILED; 00292 00293 // Perform path compression over all elements in 00294 // the stable interval data structure. This data 00295 // structure will no longer be modified and will be 00296 // accessed n or 2n times. Therefore, we can afford 00297 // a linear time compression. 00298 for (i = bsize; --i;) 00299 if (hall[i].s > i) 00300 hall[i].s = w; 00301 else 00302 w = i; 00303 00304 /* 00305 * UPDATING LOWER BOUND: 00306 * For all variables that are not a subset of a stable set, 00307 * shrink the lower bound, i.e. forall stable sets S we have: 00308 * x0 < S_min <= y <=S_max or S_min <= x0 <= S_max < y 00309 * that is [x0,y] is NOT a proper subset of any stable set S 00310 */ 00311 for (i = n; i--; ) { 00312 int x0 = rank[mu[i]].min; 00313 int y = rank[mu[i]].max; 00314 // update only those variables that are not contained in a stable set 00315 if ((hall[x0].s <= x0) || (y > hall[x0].s)) { 00316 // still have to check this out, how skipping works (consider dominated indices) 00317 int m = lps.skipNonNullElementsRight(hall[hall[i].newBound].bounds); 00318 GECODE_ME_CHECK(x[mu[i]].gq(home, m)); 00319 } 00320 } 00321 00322 // LBC narrow upper bounds 00323 w = 0; 00324 for (i = 0; i <= nb; i++) { 00325 hall[i].d = lps.sumup(hall[i].bounds, hall[i + 1].bounds - 1); 00326 if (hall[i].d == 0) { 00327 hall[i].t = w; 00328 } else { 00329 hall[w].t = i; 00330 w = i; 00331 } 00332 } 00333 hall[w].t = i; 00334 00335 w = 0; 00336 for (i = 1; i <= nb; i++) 00337 if (hall[i - 1].d == 0) { 00338 hall[i].h = w; 00339 } else { 00340 hall[w].h = i; 00341 w = i; 00342 } 00343 hall[w].h = i; 00344 00345 for (i = n; i--; ) { 00346 // visit intervals in decreasing min order 00347 // i.e. minsorted from right to left 00348 int x0 = rank[nu[i]].max; 00349 int y = rank[nu[i]].min; 00350 int pred = x0 - 1; // predecessor of x0 in the indices 00351 z = pathmin_t(hall, pred); 00352 j = hall[z].t; 00353 00354 /* If the variable is not in a discovered stable set 00355 * (see above condition for STABLE SET) 00356 */ 00357 if (hall[z].d > lps.sumup(hall[z].bounds, hall[y].bounds - 1)) { 00358 // FAILURE SET 00359 if (--hall[z].d == 0) { 00360 hall[z].t = z - 1; 00361 z = pathmin_t(hall, hall[z].t); 00362 hall[z].t = j; 00363 } 00364 // FINDING NEW UPPER BOUND 00365 if (hall[x0].h < x0) { 00366 w = pathmin_h(hall, hall[x0].h); 00367 hall[i].newBound = w; 00368 pathset_h(hall, x0, w, w); // path compression 00369 } else { 00370 hall[i].newBound = x0; 00371 } 00372 // UNSTABLE SET 00373 if (hall[z].d == lps.sumup(hall[z].bounds, hall[y].bounds - 1)) { 00374 if (hall[y].h < y) { 00375 y = hall[y].h; 00376 } 00377 int succj = j + 1; 00378 // mark new unstable set [y,j] 00379 pathset_h(hall, hall[y].h, succj, y); 00380 hall[y].h = succj; 00381 } 00382 } 00383 pathset_t(hall, pred, z, z); 00384 } 00385 00386 // UPDATING UPPER BOUND 00387 for (i = n; i--; ) { 00388 int x0 = rank[nu[i]].min; 00389 int y = rank[nu[i]].max; 00390 if ((hall[x0].s <= x0) || (y > hall[x0].s)) { 00391 int m = lps.skipNonNullElementsLeft(hall[hall[i].newBound].bounds - 1); 00392 GECODE_ME_CHECK(x[nu[i]].lq(home, m)); 00393 } 00394 } 00395 return ES_OK; 00396 } 00397 00398 00399 template<class Card> 00400 forceinline ExecStatus 00401 Bnd<Card>::ubc(Space& home, int& nb, 00402 HallInfo hall[], Rank rank[], int mu[], int nu[]) { 00403 int rightmost = nb + 1; // rightmost accesible value in bounds 00404 int bsize = nb + 2; // number of unique bounds including sentinels 00405 00406 //Narrow lower bounds (UBC) 00407 00408 /* 00409 * Initializing tree structure with the values from bounds 00410 * and the interval capacities of neighboured values 00411 * from left to right 00412 */ 00413 00414 00415 hall[0].h = 0; 00416 hall[0].t = 0; 00417 hall[0].d = 0; 00418 00419 for (int i = bsize; --i; ) { 00420 hall[i].h = hall[i].t = i-1; 00421 hall[i].d = ups.sumup(hall[i-1].bounds, hall[i].bounds - 1); 00422 } 00423 00424 int n = x.size(); 00425 00426 for (int i = 0; i < n; i++) { 00427 // visit intervals in increasing max order 00428 int x0 = rank[mu[i]].min; 00429 int succ = x0 + 1; 00430 int y = rank[mu[i]].max; 00431 int z = pathmax_t(hall, succ); 00432 int j = hall[z].t; 00433 00434 /* DOMINATION: 00435 * v^i_j denotes 00436 * unused values in the current interval. If the difference d 00437 * between to critical capacities v^i_j and v^i_z 00438 * is equal to zero, j dominates z 00439 * 00440 * i.e. [hall[l].bounds, hall[nb+1].bounds] is not left-maximal and 00441 * [hall[j].bounds, hall[l].bounds] is a Hall set iff 00442 * [hall[j].bounds, hall[l].bounds] processing a variable x_i uses up a value in the interval 00443 * [hall[z].bounds,hall[z+1].bounds] according to the intervals 00444 * capacity. Therefore, if d = 0 00445 * the considered value has already been used by processed variables 00446 * m-times, where m = u[i] for value v_i. Since this value must not 00447 * be reconsidered the path can be compressed 00448 */ 00449 if (--hall[z].d == 0) { 00450 hall[z].t = z + 1; 00451 z = pathmax_t(hall, hall[z].t); 00452 if (z >= bsize) 00453 z--; 00454 hall[z].t = j; 00455 } 00456 pathset_t(hall, succ, z, z); // path compression 00457 00458 /* NEGATIVE CAPACITY: 00459 * A negative capacity results in a failure.Since a 00460 * negative capacity signals that the number of variables 00461 * whose domain is contained in the set S is larger than 00462 * the maximum capacity of S => UBC is not satisfiable, 00463 * i.e. there are more variables than values to instantiate them 00464 */ 00465 if (hall[z].d < ups.sumup(hall[y].bounds, hall[z].bounds - 1)) 00466 return ES_FAILED; 00467 00468 /* UPDATING LOWER BOUND: 00469 * If the lower bound min_i lies inside a Hall interval [a,b] 00470 * i.e. a <= min_i <=b <= max_i 00471 * min_i is set to min_i := b+1 00472 */ 00473 if (hall[x0].h > x0) { 00474 int w = pathmax_h(hall, hall[x0].h); 00475 int m = hall[w].bounds; 00476 GECODE_ME_CHECK(x[mu[i]].gq(home, m)); 00477 pathset_h(hall, x0, w, w); // path compression 00478 } 00479 00480 /* ZEROTEST: 00481 * (using the difference between capacity pointers) 00482 * zero capacity => the difference between critical capacity 00483 * pointers is equal to the maximum capacity of the interval,i.e. 00484 * the number of variables whose domain is contained in the 00485 * interval is equal to the sum over all u[i] for a value v_i that 00486 * lies in the Hall-Intervall which can also be thought of as a 00487 * Hall-Set 00488 * 00489 * ZeroTestLemma: Let k and l be succesive critical indices. 00490 * v^i_k=0 => v^i_k = max_i+1-l+d 00491 * <=> v^i_k = y + 1 - z + d 00492 * <=> d = z-1-y 00493 * if this equation holds the interval [j,z-1] is a hall intervall 00494 */ 00495 00496 if (hall[z].d == ups.sumup(hall[y].bounds, hall[z].bounds - 1)) { 00497 /* 00498 *mark hall interval [j,z-1] 00499 * hall pointers form a path to the upper bound of the interval 00500 */ 00501 int predj = j - 1; 00502 pathset_h(hall, hall[y].h, predj, y); 00503 hall[y].h = predj; 00504 } 00505 } 00506 00507 /* Narrow upper bounds (UBC) 00508 * symmetric to the narrowing of the lower bounds 00509 */ 00510 for (int i = 0; i < rightmost; i++) { 00511 hall[i].h = hall[i].t = i+1; 00512 hall[i].d = ups.sumup(hall[i].bounds, hall[i+1].bounds - 1); 00513 } 00514 00515 for (int i = n; i--; ) { 00516 // visit intervals in decreasing min order 00517 int x0 = rank[nu[i]].max; 00518 int pred = x0 - 1; 00519 int y = rank[nu[i]].min; 00520 int z = pathmin_t(hall, pred); 00521 int j = hall[z].t; 00522 00523 // DOMINATION: 00524 if (--hall[z].d == 0) { 00525 hall[z].t = z - 1; 00526 z = pathmin_t(hall, hall[z].t); 00527 hall[z].t = j; 00528 } 00529 pathset_t(hall, pred, z, z); 00530 00531 // NEGATIVE CAPACITY: 00532 if (hall[z].d < ups.sumup(hall[z].bounds,hall[y].bounds-1)) 00533 return ES_FAILED; 00534 00535 /* UPDATING UPPER BOUND: 00536 * If the upper bound max_i lies inside a Hall interval [a,b] 00537 * i.e. min_i <= a <= max_i < b 00538 * max_i is set to max_i := a-1 00539 */ 00540 if (hall[x0].h < x0) { 00541 int w = pathmin_h(hall, hall[x0].h); 00542 int m = hall[w].bounds - 1; 00543 GECODE_ME_CHECK(x[nu[i]].lq(home, m)); 00544 pathset_h(hall, x0, w, w); 00545 } 00546 00547 // ZEROTEST 00548 if (hall[z].d == ups.sumup(hall[z].bounds, hall[y].bounds - 1)) { 00549 //mark hall interval [y,j] 00550 pathset_h(hall, hall[y].h, j+1, y); 00551 hall[y].h = j+1; 00552 } 00553 } 00554 return ES_OK; 00555 } 00556 00557 template<class Card> 00558 ExecStatus 00559 Bnd<Card>::pruneCards(Space& home) { 00560 // Remove all values with 0 max occurrence 00561 // and remove corresponding occurrence variables from k 00562 00563 // The number of zeroes 00564 int n_z = 0; 00565 for (int i=k.size(); i--;) 00566 if (k[i].max() == 0) 00567 n_z++; 00568 00569 if (n_z > 0) { 00570 Region r(home); 00571 int* z = r.alloc<int>(n_z); 00572 n_z = 0; 00573 int n_k = 0; 00574 for (int i=0; i<k.size(); i++) 00575 if (k[i].max() == 0) { 00576 z[n_z++] = k[i].card(); 00577 } else { 00578 k[n_k++] = k[i]; 00579 } 00580 k.size(n_k); 00581 Support::quicksort(z,n_z); 00582 for (int i=x.size(); i--;) { 00583 Iter::Values::Array zi(z,n_z); 00584 GECODE_ME_CHECK(x[i].minus_v(home,zi,false)); 00585 } 00586 lps.reinit(); ups.reinit(); 00587 } 00588 return ES_OK; 00589 } 00590 00591 template<class Card> 00592 ExecStatus 00593 Bnd<Card>::propagate(Space& home, const ModEventDelta& med) { 00594 if (IntView::me(med) == ME_INT_VAL) { 00595 GECODE_ES_CHECK(prop_val<Card>(home,*this,y,k)); 00596 return home.ES_NOFIX_PARTIAL(*this,IntView::med(ME_INT_BND)); 00597 } 00598 00599 if (Card::propagate) 00600 GECODE_ES_CHECK(pruneCards(home)); 00601 00602 Region r(home); 00603 int* count = r.alloc<int>(k.size()); 00604 00605 for (int i = k.size(); i--; ) 00606 count[i] = 0; 00607 bool all_assigned = true; 00608 int noa = 0; 00609 for (int i = x.size(); i--; ) { 00610 if (x[i].assigned()) { 00611 noa++; 00612 int idx; 00613 // reduction is essential for order on value nodes in dom 00614 // hence introduce test for failed lookup 00615 if (!lookupValue(k,x[i].val(),idx)) 00616 return ES_FAILED; 00617 count[idx]++; 00618 } else { 00619 all_assigned = false; 00620 // We only need the counts in the view case or when all 00621 // x are assigned 00622 if (!Card::propagate) 00623 break; 00624 } 00625 } 00626 00627 if (Card::propagate) { 00628 // before propagation performs inferences on cardinality variables: 00629 if (noa > 0) 00630 for (int i = k.size(); i--; ) 00631 if (!k[i].assigned()) { 00632 GECODE_ME_CHECK(k[i].lq(home, x.size() - (noa - count[i]))); 00633 GECODE_ME_CHECK(k[i].gq(home, count[i])); 00634 } 00635 00636 if (!card_consistent<Card>(x, k)) 00637 return ES_FAILED; 00638 00639 GECODE_ES_CHECK(prop_card<Card>(home, x, k)); 00640 00641 // Cardinalities may have been modified, so recompute 00642 // count and all_assigned 00643 for (int i = k.size(); i--; ) 00644 count[i] = 0; 00645 all_assigned = true; 00646 for (int i = x.size(); i--; ) { 00647 if (x[i].assigned()) { 00648 int idx; 00649 // reduction is essential for order on value nodes in dom 00650 // hence introduce test for failed lookup 00651 if (!lookupValue(k,x[i].val(),idx)) 00652 return ES_FAILED; 00653 count[idx]++; 00654 } else { 00655 // We won't need the remaining counts, they're only used when 00656 // all x are assigned 00657 all_assigned = false; 00658 break; 00659 } 00660 } 00661 } 00662 00663 if (all_assigned) { 00664 for (int i = k.size(); i--; ) 00665 GECODE_ME_CHECK(k[i].eq(home, count[i])); 00666 return home.ES_SUBSUMED(*this); 00667 } 00668 00669 if (Card::propagate) 00670 GECODE_ES_CHECK(pruneCards(home)); 00671 00672 int n = x.size(); 00673 00674 int* mu = r.alloc<int>(n); 00675 int* nu = r.alloc<int>(n); 00676 00677 for (int i = n; i--; ) 00678 nu[i] = mu[i] = i; 00679 00680 // Create sorting permutation mu according to the variables upper bounds 00681 MaxInc<IntView> max_inc(x); 00682 Support::quicksort<int, MaxInc<IntView> >(mu, n, max_inc); 00683 00684 // Create sorting permutation nu according to the variables lower bounds 00685 MinInc<IntView> min_inc(x); 00686 Support::quicksort<int, MinInc<IntView> >(nu, n, min_inc); 00687 00688 // Sort the cardinality bounds by index 00689 MinIdx<Card> min_idx; 00690 Support::quicksort<Card, MinIdx<Card> >(&k[0], k.size(), min_idx); 00691 00692 if (!lps.initialized()) { 00693 assert (!ups.initialized()); 00694 lps.init(home, k, false); 00695 ups.init(home, k, true); 00696 } else if (Card::propagate) { 00697 // if there has been a change to the cardinality variables 00698 // reconstruction of the partial sum structure is necessary 00699 if (lps.check_update_min(k)) 00700 lps.init(home, k, false); 00701 if (ups.check_update_max(k)) 00702 ups.init(home, k, true); 00703 } 00704 00705 // assert that the minimal value of the partial sum structure for 00706 // LBC is consistent with the smallest value a variable can take 00707 assert(lps.minValue() <= x[nu[0]].min()); 00708 // assert that the maximal value of the partial sum structure for 00709 // UBC is consistent with the largest value a variable can take 00710 00711 /* 00712 * Setup rank and bounds info 00713 * Since this implementation is based on the theory of Hall Intervals 00714 * additional datastructures are needed in order to represent these 00715 * intervals and the "partial-sum" data structure (cf."gcc/bnd-sup.hpp") 00716 * 00717 */ 00718 00719 HallInfo* hall = r.alloc<HallInfo>(2 * n + 2); 00720 Rank* rank = r.alloc<Rank>(n); 00721 00722 int nb = 0; 00723 // setup bounds and rank 00724 int min = x[nu[0]].min(); 00725 int max = x[mu[0]].max() + 1; 00726 int last = lps.firstValue + 1; //equivalent to last = min -2 00727 hall[0].bounds = last; 00728 00729 /* 00730 * First the algorithm merges the arrays minsorted and maxsorted 00731 * into bounds i.e. hall[].bounds contains the ordered union 00732 * of the lower and upper domain bounds including two sentinels 00733 * at the beginning and at the end of the set 00734 * ( the upper variable bounds in this union are increased by 1 ) 00735 */ 00736 00737 { 00738 int i = 0; 00739 int j = 0; 00740 while (true) { 00741 if (i < n && min < max) { 00742 if (min != last) { 00743 last = min; 00744 hall[++nb].bounds = last; 00745 } 00746 rank[nu[i]].min = nb; 00747 if (++i < n) 00748 min = x[nu[i]].min(); 00749 } else { 00750 if (max != last) { 00751 last = max; 00752 hall[++nb].bounds = last; 00753 } 00754 rank[mu[j]].max = nb; 00755 if (++j == n) 00756 break; 00757 max = x[mu[j]].max() + 1; 00758 } 00759 } 00760 } 00761 00762 int rightmost = nb + 1; // rightmost accesible value in bounds 00763 hall[rightmost].bounds = ups.lastValue + 1 ; 00764 00765 if (Card::propagate) { 00766 skip_lbc = true; 00767 for (int i = k.size(); i--; ) 00768 if (k[i].min() != 0) { 00769 skip_lbc = false; 00770 break; 00771 } 00772 } 00773 00774 if (!card_fixed && !skip_lbc) 00775 GECODE_ES_CHECK((lbc(home, nb, hall, rank, mu, nu))); 00776 00777 GECODE_ES_CHECK((ubc(home, nb, hall, rank, mu, nu))); 00778 00779 if (Card::propagate) 00780 GECODE_ES_CHECK(prop_card<Card>(home, x, k)); 00781 00782 for (int i = k.size(); i--; ) 00783 count[i] = 0; 00784 for (int i = x.size(); i--; ) 00785 if (x[i].assigned()) { 00786 int idx; 00787 if (!lookupValue(k,x[i].val(),idx)) 00788 return ES_FAILED; 00789 count[idx]++; 00790 } else { 00791 // We won't need the remaining counts, they're only used when 00792 // all x are assigned 00793 return ES_NOFIX; 00794 } 00795 00796 for (int i = k.size(); i--; ) 00797 GECODE_ME_CHECK(k[i].eq(home, count[i])); 00798 00799 return home.ES_SUBSUMED(*this); 00800 } 00801 00802 00803 template<class Card> 00804 ExecStatus 00805 Bnd<Card>::post(Home home, 00806 ViewArray<IntView>& x, ViewArray<Card>& k) { 00807 bool cardfix = true; 00808 for (int i=k.size(); i--; ) 00809 if (!k[i].assigned()) { 00810 cardfix = false; break; 00811 } 00812 bool nolbc = true; 00813 for (int i=k.size(); i--; ) 00814 if (k[i].min() != 0) { 00815 nolbc = false; break; 00816 } 00817 00818 GECODE_ES_CHECK(postSideConstraints<Card>(home, x, k)); 00819 00820 if (isDistinct<Card>(home,x,k)) 00821 return Distinct::Bnd<IntView>::post(home,x); 00822 00823 (void) new (home) Bnd<Card>(home,x,k,cardfix,nolbc); 00824 return ES_OK; 00825 } 00826 00827 }}} 00828 00829 // STATISTICS: int-prop