Generated on Mon Nov 30 23:53:29 2009 for Gecode by doxygen 1.6.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: 2009-10-14 12:19:49 +0200 (Wed, 14 Oct 2009) $ by $Author: schulte $
00011  *     $Revision: 9909 $
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 ES_SUBSUMED(p,home);
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   size_t
00374   Sorted<View,Perm>::dispose(Space& home) {
00375     assert(!home.failed());
00376     x.cancel(home,*this, PC_INT_BND);
00377     y.cancel(home,*this, PC_INT_BND);
00378     if (Perm)
00379       z.cancel(home,*this, PC_INT_BND);
00380     (void) Propagator::dispose(home);
00381     return sizeof(*this);
00382   }
00383 
00384   template<class View, bool Perm>
00385   Actor* Sorted<View,Perm>::copy(Space& home, bool share) {
00386     return new (home) Sorted<View,Perm>(home, share, *this);
00387   }
00388 
00389   template<class View, bool Perm>
00390   PropCost Sorted<View,Perm>::cost(const Space&, const ModEventDelta&) const {
00391     return PropCost::linear(PropCost::LO, x.size());
00392   }
00393 
00394   template<class View, bool Perm>
00395   ExecStatus
00396   Sorted<View,Perm>::propagate(Space& home, const ModEventDelta&) {
00397     int  n           = x.size();
00398     bool secondpass  = false;
00399     bool nofix       = false;
00400     int  dropfst     = 0;
00401 
00402     bool subsumed    = false;
00403     bool array_subs  = false;
00404     bool match_fixed = false;
00405 
00406     // normalization of x and y
00407     if (!normalize(home, y, x, nofix))
00408       return ES_FAILED;
00409 
00410     // create sigma sorting
00411     sort_sigma<View,Perm>(home,x,z);
00412 
00413     bool noperm_bc = false;
00414     if (!array_assigned<View,Perm>
00415         (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc))
00416       return ES_FAILED;
00417 
00418     if (array_subs)
00419       return ES_SUBSUMED(*this,home);
00420 
00421     sort_sigma<View,Perm>(home,x,z);
00422 
00423     // in this case check_subsumptions is guaranteed to find
00424     // the xs ordered by sigma
00425 
00426     if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst))
00427       return ES_FAILED;
00428 
00429     if (subsumed)
00430       return ES_SUBSUMED(*this,home);
00431 
00432     if (Perm) {
00433       // dropping possibly yields inconsistent indices on permutation variables
00434       if (dropfst) {
00435         reachable = w[dropfst - 1].max();
00436         bool unreachable = true;
00437         for (int i = x.size(); unreachable && i-- ; ) {
00438           unreachable &= (reachable < x[i].min());
00439         }
00440 
00441         if (unreachable) {
00442           x.drop_fst(dropfst, home, *this, PC_INT_BND);
00443           y.drop_fst(dropfst, home, *this, PC_INT_BND);
00444           z.drop_fst(dropfst, home, *this, PC_INT_BND);
00445         } else {
00446           dropfst = 0;
00447         }
00448       }
00449 
00450       n = x.size();
00451 
00452       if (n < 2) {
00453         if (x[0].max() < y[0].min() || y[0].max() < x[0].min())
00454           return ES_FAILED;
00455         if (Perm) {
00456           GECODE_ME_CHECK(z[0].eq(home, w.size() - 1));
00457         }
00458         GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0])));
00459       }
00460 
00461       // check whether shifting the permutation variables
00462       // is necessary after dropping x and y vars
00463       // highest reachable index
00464       int  valid = n - 1;
00465       int  index = 0;
00466       int  shift = 0;
00467 
00468       for (int i = n; i--; ){
00469         if (z[i].max() > index)
00470           index = z[i].max();
00471         if (index > valid)
00472           shift = index - valid;
00473       }
00474 
00475       if (shift) {
00476         ViewArray<OffsetView> ox(home,n), oy(home,n), oz(home,n);
00477 
00478         for (int i = n; i--; ) {
00479           GECODE_ME_CHECK(z[i].gq(home, shift));
00480 
00481           oz[i] = OffsetView(z[i], -shift);
00482           ox[i] = OffsetView(x[i], 0);
00483           oy[i] = OffsetView(y[i], 0);
00484         }
00485 
00486         GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm>
00487                          (home,*this,ox,oy,oz,secondpass,nofix,match_fixed)));
00488 
00489         if (secondpass) {
00490           GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm>
00491                            (home,*this,ox,oy,oz,secondpass,nofix,match_fixed)));
00492         }
00493       } else {
00494         GECODE_ES_CHECK((bounds_propagation<View,Perm>
00495                          (home,*this,x,y,z,secondpass,nofix,match_fixed)));
00496 
00497         if (secondpass) {
00498           GECODE_ES_CHECK((bounds_propagation<View,Perm>
00499                            (home,*this,x,y,z,secondpass,nofix,match_fixed)));
00500         }
00501       }
00502     } else {
00503       // dropping has no consequences
00504       if (dropfst) {
00505         x.drop_fst(dropfst, home, *this, PC_INT_BND);
00506         y.drop_fst(dropfst, home, *this, PC_INT_BND);
00507       }
00508 
00509       n = x.size();
00510 
00511       if (n < 2) {
00512         if (x[0].max() < y[0].min() || y[0].max() < x[0].min())
00513           return ES_FAILED;
00514         GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0])));
00515       }
00516 
00517       GECODE_ES_CHECK((bounds_propagation<View,Perm>
00518                        (home, *this, x, y, z,secondpass, nofix, match_fixed)));
00519       // no second pass possible if there are no permvars
00520     }
00521 
00522     if (!normalize(home, y, x, nofix))
00523       return ES_FAILED;
00524 
00525     Region r(home);
00526     int* tau = r.alloc<int>(n);
00527     if (match_fixed) {
00528       // sorting is determined
00529       // sigma and tau coincide
00530       for (int i = x.size(); i--; ) {
00531         int pi = z[i].val();
00532         tau[pi] = i;
00533       }
00534     } else {
00535       for (int i = n; i--; ) {
00536         tau[i] = i;
00537       }
00538     }
00539 
00540     sort_tau<View,Perm>(x,z,tau);
00541     // recreate consistency for already assigned subparts
00542     // in order of the upper bounds starting at the end of the array
00543     bool xbassigned = true;
00544     for (int i = x.size(); i--; ) {
00545       if (x[tau[i]].assigned() && xbassigned) {
00546         GECODE_ME_CHECK(y[i].eq(home, x[tau[i]].val()));
00547       } else {
00548         xbassigned = false;
00549       }
00550     }
00551 
00552     subsumed   = true;
00553     array_subs = false;
00554     noperm_bc  = false;
00555 
00556     // creating sorting anew
00557     sort_sigma<View,Perm>(home,x,z);
00558 
00559     if (Perm) {
00560       for (int i = 0; i < x.size() - 1; i++) {
00561         // special case of subsccs of size2 for the lower bounds
00562         // two x variables are in the same scc of size 2
00563         if (z[i].min() == z[i+1].min() &&
00564             z[i].max() == z[i+1].max() &&
00565             z[i].size() == 2 && z[i].range()) {
00566           if (x[i].min() < x[i+1].min()) {
00567             ModEvent me = y[z[i].min()].gq(home, x[i].min());
00568             GECODE_ME_CHECK(me);
00569             nofix |= (me_modified(me) &&
00570                       y[z[i].min()].min() != x[i].min());
00571 
00572             me = y[z[i+1].max()].gq(home, x[i+1].min());
00573             GECODE_ME_CHECK(me);
00574             nofix |= (me_modified(me) &&
00575                       y[z[i+1].max()].min() != x[i+1].min());
00576           }
00577         }
00578       }
00579     }
00580 
00581     // check assigned
00582     // should be sorted
00583     bool xassigned = true;
00584     for (int i = 0; i < x.size(); i++) {
00585       if (x[i].assigned() && xassigned) {
00586         GECODE_ME_CHECK(y[i].eq(home,x[i].val()));
00587       } else {
00588         xassigned = false;
00589       }
00590     }
00591 
00592     // sorted check bounds
00593     // final check that variables are consitent with least and greatest possible
00594     // values
00595     int tlb = std::min(x[0].min(), y[0].min());
00596     int tub = std::max(x[x.size() - 1].max(), y[y.size() - 1].max());
00597     for (int i = x.size(); i--; ) {
00598       ModEvent me = y[i].lq(home, tub);
00599       GECODE_ME_CHECK(me);
00600       nofix |= me_modified(me) && (y[i].max() != tub);
00601 
00602       me = y[i].gq(home, tlb);
00603       GECODE_ME_CHECK(me);
00604       nofix |= me_modified(me) && (y[i].min() != tlb);
00605 
00606       me = x[i].lq(home, tub);
00607       GECODE_ME_CHECK(me);
00608       nofix |= me_modified(me) && (x[i].max() != tub);
00609 
00610       me = x[i].gq(home, tlb);
00611       GECODE_ME_CHECK(me);
00612       nofix |= me_modified(me) && (x[i].min() != tlb);
00613     }
00614 
00615     if (!array_assigned<View,Perm>
00616         (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc))
00617       return ES_FAILED;
00618 
00619     if (array_subs)
00620       return ES_SUBSUMED(*this,home);
00621 
00622     if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst))
00623       return ES_FAILED;
00624 
00625     if (subsumed)
00626       return ES_SUBSUMED(*this,home);
00627 
00628     return nofix ? ES_NOFIX : ES_FIX;
00629   }
00630 
00631   template<class View, bool Perm>
00632   ExecStatus
00633   Sorted<View,Perm>::
00634   post(Home home,
00635        ViewArray<View>& x0, ViewArray<View>& y0, ViewArray<View>& z0) {
00636     int n = x0.size();
00637     if (n < 2) {
00638       if ((x0[0].max() < y0[0].min()) || (y0[0].max() < x0[0].min()))
00639         return ES_FAILED;
00640       GECODE_ES_CHECK((Rel::EqBnd<View,View>::post(home,x0[0],y0[0])));
00641       if (Perm) {
00642         GECODE_ME_CHECK(z0[0].eq(home,0));
00643       }
00644     } else {
00645       if (Perm) {
00646         ViewArray<View> z(home,n);
00647         for (int i=n; i--; ) {
00648           z[i]=z0[i];
00649           GECODE_ME_CHECK(z[i].gq(home,0));
00650           GECODE_ME_CHECK(z[i].lq(home,n-1));
00651         }
00652         GECODE_ES_CHECK(Distinct::Bnd<View>::post(home,z));
00653       }
00654       new (home) Sorted<View,Perm>(home,x0,y0,z0);
00655     }
00656     return ES_OK;
00657   }
00658 
00659 }}}
00660 
00661 // STATISTICS: int-prop
00662 
00663 
00664