Generated on Tue Jul 27 2010 21:59:15 for Gecode by doxygen 1.7.1

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