ubc.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: 2008-02-27 11:24:12 +0100 (Wed, 27 Feb 2008) $ by $Author: tack $ 00011 * $Revision: 6323 $ 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 namespace Gecode { namespace Int { namespace GCC { 00038 00060 template <class View, class Card, bool shared> 00061 inline ExecStatus 00062 ubc(Space* home, ViewArray<View>& x, int& nb, 00063 HallInfo hall[], Rank rank[], 00064 PartialSum<Card>* ups, 00065 int mu[], int nu[]){ 00066 ExecStatus es = ES_FIX; 00067 00068 int rightmost = nb + 1; // rightmost accesible value in bounds 00069 int bsize = nb + 2; // number of unique bounds including sentinels 00070 00071 //Narrow lower bounds (UBC) 00072 00073 /* 00074 * Initializing tree structure with the values from bounds 00075 * and the interval capacities of neighboured values 00076 * from left to right 00077 */ 00078 00079 00080 hall[0].h = 0; 00081 hall[0].t = 0; 00082 hall[0].d = 0; 00083 00084 for (int i = 1; i < bsize; i++) { 00085 int pred = i - 1; 00086 hall[i].h = pred; 00087 hall[i].t = pred; 00088 hall[i].d = ups->sumup(hall[pred].bounds, hall[i].bounds - 1); 00089 } 00090 hall[bsize].h = bsize-1; 00091 hall[bsize].t = bsize-1; 00092 00093 int n = x.size(); 00094 00095 for (int i = 0; i < n; i++) { 00096 00097 // visit intervals in increasing max order 00098 int x0 = rank[mu[i]].min; 00099 int succ = x0 + 1; 00100 int y = rank[mu[i]].max; 00101 int z = pathmax_t(hall, succ); 00102 int j = hall[z].t; 00103 00104 /* DOMINATION: 00105 * v^i_j denotes 00106 * unused values in the current interval. If the difference d 00107 * between to critical capacities v^i_j and v^i_z 00108 * is equal to zero, j dominates z 00109 * 00110 * i.e. [hall[l].bounds, hall[nb+1].bounds] is not left-maximal and 00111 * [hall[j].bounds, hall[l].bounds] is a Hall set iff 00112 * [hall[j].bounds, hall[l].bounds] processing a variable x_i uses up a value in the interval 00113 * [hall[z].bounds,hall[z+1].bounds] according to the intervals 00114 * capacity. Therefore, if d = 0 00115 * the considered value has already been used by processed variables 00116 * m-times, where m = u[i] for value v_i. Since this value must not 00117 * be reconsidered the path can be compressed 00118 */ 00119 if (--hall[z].d == 0){ 00120 hall[z].t = z + 1; 00121 z = pathmax_t(hall, hall[z].t); 00122 if (z >= bsize) { 00123 z--; 00124 } 00125 assert(z < bsize); 00126 hall[z].t = j; 00127 } 00128 pathset_t(hall, succ, z, z); // path compression 00129 /* NEGATIVE CAPACITY: 00130 * A negative capacity results in a failure.Since a 00131 * negative capacity signals that the number of variables 00132 * whose domain is contained in the set S is larger than 00133 * the maximum capacity of S => UBC is not satisfiable, 00134 * i.e. there are more variables than values to instantiate them 00135 */ 00136 00137 if (hall[z].d < ups->sumup(hall[y].bounds, hall[z].bounds - 1)){ 00138 return ES_FAILED; 00139 } 00140 00141 /* UPDATING LOWER BOUND: 00142 * If the lower bound min_i lies inside a Hall interval [a,b] 00143 * i.e. a <= min_i <=b <= max_i 00144 * min_i is set to min_i := b+1 00145 */ 00146 if (hall[x0].h > x0) { 00147 int w = pathmax_h(hall, hall[x0].h); 00148 int m = hall[w].bounds; 00149 00150 ModEvent me = x[mu[i]].gq(home, m); 00151 if (me_failed(me)) { 00152 return ES_FAILED; 00153 } 00154 if (me_modified(me) && (m != x[mu[i]].min())) { 00155 es = ES_NOFIX; 00156 } 00157 if (shared && me_modified(me)) { 00158 es = ES_NOFIX; 00159 } 00160 pathset_h(hall, x0, w, w); // path compression 00161 } 00162 00163 /* ZEROTEST: 00164 * (using the difference between capacity pointers) 00165 * zero capacity => the difference between critical capacity 00166 * pointers is equal to the maximum capacity of the interval,i.e. 00167 * the number of variables whose domain is contained in the 00168 * interval is equal to the sum over all u[i] for a value v_i that 00169 * lies in the Hall-Intervall which can also be thought of as a 00170 * Hall-Set 00171 * 00172 * ZeroTestLemma: Let k and l be succesive critical indices. 00173 * v^i_k=0 => v^i_k = max_i+1-l+d 00174 * <=> v^i_k = y + 1 - z + d 00175 * <=> d = z-1-y 00176 * if this equation holds the interval [j,z-1] is a hall intervall 00177 */ 00178 00179 if (hall[z].d == ups->sumup(hall[y].bounds, hall[z].bounds - 1)) { 00180 /* 00181 *mark hall interval [j,z-1] 00182 * hall pointers form a path to the upper bound of the interval 00183 */ 00184 int predj = j - 1; 00185 pathset_h(hall, hall[y].h, predj, y); 00186 hall[y].h = predj; 00187 } 00188 } 00189 00190 /* Narrow upper bounds (UBC) 00191 * symmetric to the narrowing of the lower bounds 00192 */ 00193 for (int i = 0; i < rightmost; i++) { 00194 int succ = i + 1; 00195 hall[i].h = succ; 00196 hall[i].t = succ; 00197 hall[i].d = ups->sumup(hall[i].bounds, hall[succ].bounds - 1); 00198 } 00199 00200 for (int i = n; i--; ) { 00201 // visit intervals in decreasing min order 00202 int x0 = rank[nu[i]].max; 00203 int pred = x0 - 1; 00204 int y = rank[nu[i]].min; 00205 int z = pathmin_t(hall, pred); 00206 int j = hall[z].t; 00207 00208 // DOMINATION: 00209 if (--hall[z].d == 0){ 00210 hall[z].t = z - 1; 00211 z = pathmin_t(hall, hall[z].t); 00212 hall[z].t = j; 00213 } 00214 pathset_t(hall, pred, z, z); 00215 00216 // NEGATIVE CAPACITY: 00217 if (hall[z].d < ups->sumup(hall[z].bounds,hall[y].bounds-1)){ 00218 return ES_FAILED; 00219 } 00220 00221 /* UPDATING UPPER BOUND: 00222 * If the upper bound max_i lies inside a Hall interval [a,b] 00223 * i.e. min_i <= a <= max_i < b 00224 * max_i is set to max_i := a-1 00225 */ 00226 if (hall[x0].h < x0) { 00227 int w = pathmin_h(hall, hall[x0].h); 00228 int m = hall[w].bounds - 1; 00229 ModEvent me = x[nu[i]].lq(home, m); 00230 if (me_failed(me)) { 00231 return ES_FAILED; 00232 } 00233 if (me_modified(me) && (m != x[nu[i]].max())) { 00234 es = ES_NOFIX; 00235 } 00236 if (me_modified(me) && shared) { 00237 es = ES_NOFIX; 00238 } 00239 pathset_h(hall, x0, w, w); 00240 } 00241 // ZEROTEST 00242 if (hall[z].d == ups->sumup(hall[z].bounds, hall[y].bounds - 1)) { 00243 //mark hall interval [y,j] 00244 int succj = j + 1; 00245 pathset_h(hall, hall[y].h, succj, y); 00246 hall[y].h = succj; 00247 } 00248 } 00249 return es; 00250 } 00251 00252 }}} 00253 00254 // STATISTICS: int-prop 00255