lbc.icc
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: 2007-08-09 15:30:21 +0200 (Thu, 09 Aug 2007) $ by $Author: tack $ 00011 * $Revision: 4790 $ 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 namespace Gecode { namespace Int { namespace GCC { 00039 00061 template <class View, class Card, bool shared> 00062 inline ExecStatus 00063 lbc(Space* home, ViewArray<View>& x, int& nb, 00064 HallInfo hall[], Rank rank[], 00065 PartialSum<Card>* lps, 00066 int mu[], int nu[]){ 00067 00068 ExecStatus es = ES_FIX; 00069 int n = x.size(); 00070 00071 /* 00072 * Let I(S) denote the number of variables whose domain intersects 00073 * the set S and C(S) the number of variables whose domain is containded 00074 * in S. Let further min_cap(S) be the minimal number of variables 00075 * that must be assigned to values, that is 00076 * min_cap(S) is the sum over all l[i] for a value v_i that is an 00077 * element of S. 00078 * 00079 * A failure set is a set F if 00080 * I(F) < min_cap(F) 00081 * An unstable set is a set U if 00082 * I(U) = min_cap(U) 00083 * A stable set is a set S if 00084 * C(S) > min_cap(S) and S intersetcs nor 00085 * any failure set nor any unstable set 00086 * forall unstable and failure sets 00087 * 00088 * failure sets determine the satisfiability of the LBC 00089 * unstable sets have to be pruned 00090 * stable set do not have to be pruned 00091 * 00092 * hall[].ps ~ stores the unstable 00093 * sets that have to be pruned 00094 * hall[].s ~ stores sets that must not be pruned 00095 * hall[].h ~ contains stable and unstable sets 00096 * hall[].d ~ contains the difference between interval bounds, i.e. 00097 * the minimal capacity of the interval 00098 * hall[].t ~ contains the critical capacity pointer, pointing to the 00099 * values 00100 */ 00101 00102 // LBC lower bounds 00103 00104 int i = 0; 00105 int j = 0; 00106 int w = 0; 00107 int z = 0; 00108 int v = 0; 00109 00110 //initialization of the tree structure 00111 int rightmost = nb + 1; // rightmost accesible value in bounds 00112 int bsize = nb + 2; 00113 w = rightmost; 00114 00115 // test 00116 // unused but uninitialized 00117 hall[0].d = 0; 00118 hall[0].s = 0; 00119 hall[0].ps = 0; 00120 00121 for (i = bsize; --i; ) { // i must not be zero 00122 int pred = i - 1; 00123 hall[i].s = pred; 00124 hall[i].ps = pred; 00125 hall[i].d = lps->sumup(hall[pred].bounds, hall[i].bounds - 1); 00126 00127 /* Let [hall[i].bounds,hall[i-1].bounds]=:I 00128 * If the capacity is zero => min_cap(I) = 0 00129 * => I cannot be a failure set 00130 * => I is an unstable set 00131 */ 00132 if (hall[i].d == 0) { 00133 hall[pred].h = w; 00134 } else { 00135 hall[w].h = pred; 00136 w = pred; 00137 } 00138 } 00139 00140 w = rightmost; 00141 for (i = bsize; i--; ) { // i can be zero 00142 hall[i].t = i - 1; 00143 if (hall[i].d == 0) { 00144 hall[i].t = w; 00145 } else { 00146 hall[w].t = i; 00147 w = i; 00148 } 00149 } 00150 00151 /* 00152 * The algorithm assigns to each value v in bounds 00153 * empty buckets corresponding to the minimal capacity l[i] to be 00154 * filled for v. (the buckets correspond to hall[].d containing the 00155 * difference between the interval bounds) Processing it 00156 * searches for the smallest value v in dom(x_i) that has an 00157 * empty bucket, i.e. if all buckets are filled it is guaranteed 00158 * that there are at least l[i] variables that will be 00159 * instantiated to v. Since the buckets are initially empty, 00160 * they are considered as FAILURE SETS 00161 */ 00162 00163 for (i = 0; i < n; i++) { 00164 // visit intervals in increasing max order 00165 int x0 = rank[mu[i]].min; 00166 int y = rank[mu[i]].max; 00167 int succ = x0 + 1; 00168 z = pathmax_t(hall, succ); 00169 j = hall[z].t; 00170 00171 /* 00172 * POTENTIALLY STABLE SET: 00173 * z \neq succ \Leftrigharrow z>succ, i.e. 00174 * min(D_{\mu(i)}) is guaranteed to occur min(K_i) times 00175 * \Rightarrow [x0, min(y,z)] is potentially stable 00176 */ 00177 00178 if (z != succ) { 00179 w = pathmax_ps(hall, succ); 00180 v = hall[w].ps; 00181 pathset_ps(hall, succ, w, w); 00182 w = std::min(y, z); 00183 pathset_ps(hall, hall[w].ps, v, w); 00184 hall[w].ps = v; 00185 } 00186 00187 /* 00188 * STABLE SET: 00189 * being stable implies being potentially stable, i.e. 00190 * [hall[y].ps, hall[y].bounds-1] is the largest stable subset of 00191 * [hall[j].bounds, hall[y].bounds-1]. 00192 */ 00193 00194 if (hall[z].d <= lps->sumup(hall[y].bounds, hall[z].bounds - 1)) { 00195 w = pathmax_s(hall, hall[y].ps); 00196 pathset_s(hall, hall[y].ps, w, w); 00197 // Path compression 00198 v = hall[w].s; 00199 pathset_s(hall, hall[y].s, v, y); 00200 hall[y].s = v; 00201 } else { 00202 /* 00203 * FAILURE SET: 00204 * If the considered interval [x0,y] is neither POTENTIALLY STABLE 00205 * nor STABLE there are still buckets that can be filled, 00206 * therefore d can be decreased. If d equals zero the intervals 00207 * minimum capacity is met and thepath can be compressed to the 00208 * next value having an empty bucket. 00209 * see DOMINATION in "gcc/ubc.icc" 00210 */ 00211 if (--hall[z].d == 0) { 00212 hall[z].t = z + 1; 00213 z = pathmax_t(hall, hall[z].t); 00214 hall[z].t = j; 00215 } 00216 00217 /* 00218 * FINDING NEW LOWER BOUND: 00219 * If the lower bound belongs to an unstable or a stable set, 00220 * remind the new value we might assigned to the lower bound 00221 * in case the variable doesn't belong to a stable set. 00222 */ 00223 if (hall[x0].h > x0) { 00224 hall[i].newBound = pathmax_h(hall, x0); 00225 w = hall[i].newBound; 00226 pathset_h(hall, x0, w, w); // path compression 00227 } else { 00228 // Do not shrink the variable: take old min as new min 00229 hall[i].newBound = x0; 00230 } 00231 00232 /* UNSTABLE SET 00233 * If an unstable set is discovered 00234 * the difference between the interval bounds is equal to the 00235 * number of variables whose domain intersect the interval 00236 * (see ZEROTEST in "gcc/ubc.icc") 00237 */ 00238 // CLEARLY THIS WAS NOT STABLE == UNSTABLE 00239 if (hall[z].d == lps->sumup(hall[y].bounds, hall[z].bounds - 1)) { 00240 if (hall[y].h > y) 00241 /* 00242 * y is not the end of the potentially stable set 00243 * thus ensure that the potentially stable superset is marked 00244 */ 00245 y = hall[y].h; 00246 // Equivalent to pathmax since the path is fully compressed 00247 int predj = j - 1; 00248 pathset_h(hall, hall[y].h, predj, y); 00249 // mark the new unstable set [j,y] 00250 hall[y].h = predj; 00251 } 00252 } 00253 pathset_t(hall, succ, z, z); // path compression 00254 } 00255 00256 /* If there is a FAILURE SET left the minimum occurences of the values 00257 * are not guaranteed. In order to satisfy the LBC the last value 00258 * in the stable and unstable datastructure hall[].h must point to 00259 * the sentinel at the beginning of bounds. 00260 */ 00261 if (hall[nb].h != 0) { 00262 return ES_FAILED; // no solution 00263 } 00264 00265 // Perform path compression over all elements in 00266 // the stable interval data structure. This data 00267 // structure will no longer be modified and will be 00268 // accessed n or 2n times. Therefore, we can afford 00269 // a linear time compression. 00270 for (i = bsize; --i;) { 00271 if (hall[i].s > i) { 00272 hall[i].s = w; 00273 } else { 00274 w = i; 00275 } 00276 } 00277 00278 /* 00279 * UPDATING LOWER BOUND: 00280 * For all variables that are not a subset of a stable set, 00281 * shrink the lower bound, i.e. forall stable sets S we have: 00282 * x0 < S_min <= y <=S_max or S_min <= x0 <= S_max < y 00283 * that is [x0,y] is NOT a proper subset of any stable set S 00284 */ 00285 for (i = n; i--; ) { 00286 int x0 = rank[mu[i]].min; 00287 int y = rank[mu[i]].max; 00288 // update only those variables that are not contained in a stable set 00289 if ((hall[x0].s <= x0) || (y > hall[x0].s)) { 00290 //still have to check this out, how skipping works (consider dominated indices) 00291 int m = lps->skipNonNullElementsRight(hall[hall[i].newBound].bounds); 00292 ModEvent me = x[mu[i]].gq(home, m); 00293 GECODE_ME_CHECK(me); 00294 if (me_modified(me) && m != x[mu[i]].min()) { 00295 es = ES_NOFIX; 00296 } 00297 if (shared && me_modified(me)) { 00298 es = ES_NOFIX; 00299 } 00300 } 00301 } 00302 00303 //LBC narrow upper bounds 00304 00305 w = 0; 00306 for (i = 0; i <= nb; i++) { 00307 hall[i].d = lps->sumup(hall[i].bounds, hall[i + 1].bounds - 1); 00308 if (hall[i].d == 0) { 00309 hall[i].t = w; 00310 } else { 00311 hall[w].t = i; 00312 w = i; 00313 } 00314 } 00315 hall[w].t = i; 00316 00317 w = 0; 00318 for (i = 1; i <= nb; i++) { 00319 if (hall[i - 1].d == 0) { 00320 hall[i].h = w; 00321 } else { 00322 hall[w].h = i; 00323 w = i; 00324 } 00325 } 00326 hall[w].h = i; 00327 00328 for (i = n; i--; ) { 00329 // visit intervals in decreasing min order 00330 // i.e. minsorted from right to left 00331 int x0 = rank[nu[i]].max; 00332 int y = rank[nu[i]].min; 00333 int pred = x0 - 1; // predecessor of x0 in the indices 00334 z = pathmin_t(hall, pred); 00335 j = hall[z].t; 00336 00337 /* If the variable is not in a discovered stable set 00338 * (see above condition for STABLE SET) 00339 */ 00340 if (hall[z].d > lps->sumup(hall[z].bounds, hall[y].bounds - 1)) { 00341 //FAILURE SET 00342 if (--hall[z].d == 0) { 00343 hall[z].t = z - 1; 00344 z = pathmin_t(hall, hall[z].t); 00345 hall[z].t = j; 00346 } 00347 //FINDING NEW UPPER BOUND 00348 if (hall[x0].h < x0) { 00349 w = pathmin_h(hall, hall[x0].h); 00350 hall[i].newBound = w; 00351 pathset_h(hall, x0, w, w); // path compression 00352 } else { 00353 hall[i].newBound = x0; 00354 } 00355 //UNSTABLE SET 00356 if (hall[z].d == lps->sumup(hall[z].bounds, hall[y].bounds - 1)) { 00357 if (hall[y].h < y) { 00358 y = hall[y].h; 00359 } 00360 int succj = j + 1; 00361 //mark new unstable set [y,j] 00362 pathset_h(hall, hall[y].h, succj, y); 00363 hall[y].h = succj; 00364 } 00365 } 00366 pathset_t(hall, pred, z, z); 00367 } 00368 00369 // UPDATING UPPER BOUND 00370 for (i = n; i--; ) { 00371 int x0 = rank[nu[i]].min; 00372 int y = rank[nu[i]].max; 00373 if ((hall[x0].s <= x0) || (y > hall[x0].s)){ 00374 int m = lps->skipNonNullElementsLeft(hall[hall[i].newBound].bounds - 1); 00375 ModEvent me = x[nu[i]].lq(home, m); 00376 GECODE_ME_CHECK(me); 00377 if (me_modified(me) && m != x[nu[i]].max()) { 00378 es = ES_NOFIX; 00379 } 00380 if (shared && me_modified(me)) { 00381 es = ES_NOFIX; 00382 } 00383 } 00384 } 00385 return es; 00386 } 00387 00388 }}} 00389 00390 // STATISTICS: int-prop 00391