Generated on Tue Mar 5 2013 22:37:16 for Gecode by doxygen 1.8.3.1
propagate.hpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Patrick Pekczynski <pekczynski@ps.uni-sb.de>
5  *
6  * Copyright:
7  * Patrick Pekczynski, 2004
8  *
9  * Last modified:
10  * $Date: 2010-08-24 23:54:10 +1000 (Tue, 24 Aug 2010) $ by $Author: tack $
11  * $Revision: 11359 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 #include <gecode/int/rel.hh>
39 #include <gecode/int/distinct.hh>
40 
41 namespace Gecode { namespace Int { namespace Sorted {
42 
43 
44  /*
45  * Summary of the propagation algorithm as implemented in the
46  * propagate method below:
47  *
48  * STEP 1: Normalize the domains of the y variables
49  * STEP 2: Sort the domains of the x variables according to their lower
50  * and upper endpoints
51  * STEP 3: Compute the matchings phi and phiprime with
52  * Glover's matching algorithm
53  * STEP 4: Compute the strongly connected components in
54  * the oriented intersection graph
55  * STEP 5: Narrow the domains of the variables
56  *
57  */
58 
75  template<class View, bool Perm>
78  ViewArray<View>& x,
79  ViewArray<View>& y,
80  ViewArray<View>& z,
81  bool& repairpass,
82  bool& nofix,
83  bool& match_fixed){
84 
85  int n = x.size();
86 
87  Region r(home);
88  int* tau = r.alloc<int>(n);
89  int* phi = r.alloc<int>(n);
90  int* phiprime = r.alloc<int>(n);
92  int* vertices = r.alloc<int>(n);
93 
94  if (match_fixed) {
95  // sorting is determined, sigma and tau coincide
96  for (int i=n; i--; )
97  tau[z[i].val()] = i;
98  } else {
99  for (int i = n; i--; )
100  tau[i] = i;
101  }
102 
103  if (Perm) {
104  // normalized and sorted
105  // collect all bounds
106 
107  Rank* allbnd = r.alloc<Rank>(x.size());
108 #ifndef NDEBUG
109  for (int i=n; i--;)
110  allbnd[i].min = allbnd[i].max = -1;
111 #endif
112  for (int i=n; i--;) {
113  int min = x[i].min();
114  int max = x[i].max();
115  for (int j=0; j<n; j++) {
116  if ( (y[j].min() > min) ||
117  (y[j].min() <= min && min <= y[j].max()) ) {
118  allbnd[i].min = j;
119  break;
120  }
121  }
122  for (int j=n; j--;) {
123  if (y[j].min() > max) {
124  allbnd[i].max = j-1;
125  break;
126  } else if (y[j].min() <= max && min <= y[j].max()) {
127  allbnd[i].max = j;
128  break;
129  }
130  }
131  }
132 
133  for (int i = n; i--; ) {
134  // minimum reachable y-variable
135  int minr = allbnd[i].min;
136  assert(minr != -1);
137  int maxr = allbnd[i].max;
138  assert(maxr != -1);
139 
140  ModEvent me = x[i].gq(home, y[minr].min());
141  if (me_failed(me))
142  return ES_FAILED;
143  nofix |= (me_modified(me) && (x[i].min() != y[minr].min()));
144 
145  me = x[i].lq(home, y[maxr].max());
146  if (me_failed(me))
147  return ES_FAILED;
148  nofix |= (me_modified(me) && (x[i].min() != y[maxr].max()));
149 
150  me = z[i].gq(home, minr);
151  if (me_failed(me))
152  return ES_FAILED;
153  nofix |= (me_modified(me) && (z[i].min() != minr));
154 
155  me = z[i].lq(home, maxr);
156  if (me_failed(me))
157  return ES_FAILED;
158  nofix |= (me_modified(me) && (z[i].max() != maxr));
159  }
160 
161  // channel information from x to y through permutation variables in z
162  if (!channel(home,x,y,z,nofix))
163  return ES_FAILED;
164  if (nofix)
165  return ES_NOFIX;
166  }
167 
168  /*
169  * STEP 1:
170  * normalization is implemented in "order.hpp"
171  * o setting the lower bounds of the y_i domains (\lb E_i)
172  * to max(\lb E_{i-1},\lb E_i)
173  * o setting the upper bounds of the y_i domains (\ub E_i)
174  * to min(\ub E_i,\ub E_{i+1})
175  */
176 
177  if (!normalize(home, y, x, nofix))
178  return ES_FAILED;
179 
180  if (Perm) {
181  // check consistency of channeling after normalization
182  if (!channel(home,x,y,z,nofix))
183  return ES_FAILED;
184  if (nofix)
185  return ES_NOFIX;
186  }
187 
188 
189  // if bounds have changed we have to recreate sigma to restore
190  // optimized dropping of variables
191 
192  sort_sigma<View,Perm>(home,x,z);
193 
194  bool subsumed = true;
195  bool array_subs = false;
196  int dropfst = 0;
197  bool noperm_bc = false;
198 
199  if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst) ||
200  !array_assigned<View,Perm>(home,x,y,z,array_subs,match_fixed,nofix,noperm_bc))
201  return ES_FAILED;
202 
203  if (subsumed || array_subs)
204  return home.ES_SUBSUMED(p);
205 
206  /*
207  * STEP 2: creating tau
208  * Sort the domains of the x variables according
209  * to their lower bounds, where we use an
210  * intermediate array of integers for sorting
211  */
212  sort_tau<View,Perm>(x,z,tau);
213 
214  /*
215  * STEP 3:
216  * Compute the matchings \phi and \phi' between
217  * the x and the y variables
218  * with Glover's matching algorithm.
219  * o phi is computed with the glover function
220  * o phiprime is computed with the revglover function
221  * glover and revglover are implemented in "matching.hpp"
222  */
223 
224  if (!match_fixed) {
225  if (!glover(x,y,tau,phi,sequence,vertices))
226  return ES_FAILED;
227  } else {
228  for (int i = x.size(); i--; ) {
229  phi[i] = z[i].val();
230  phiprime[i] = phi[i];
231  }
232  }
233 
234  for (int i = n; i--; )
235  if (!y[i].assigned()) {
236  // phiprime is not needed to narrow the domains of the x-variables
237  if (!match_fixed &&
238  !revglover(x,y,tau,phiprime,sequence,vertices))
239  return ES_FAILED;
240 
241  if (!narrow_domy(home,x,y,phi,phiprime,nofix))
242  return ES_FAILED;
243 
244  if (nofix && !match_fixed) {
245  // data structures (matching) destroyed by domains with holes
246 
247  for (int j = y.size(); j--; )
248  phi[j]=phiprime[j]=0;
249 
250  if (!glover(x,y,tau,phi,sequence,vertices))
251  return ES_FAILED;
252 
253  if (!revglover(x,y,tau,phiprime,sequence,vertices))
254  return ES_FAILED;
255 
256  if (!narrow_domy(home,x,y,phi,phiprime,nofix))
257  return ES_FAILED;
258  }
259  break;
260  }
261 
262  /*
263  * STEP 4:
264  * Compute the strongly connected components in
265  * the oriented intersection graph
266  * the computation of the sccs is implemented in
267  * "narrowing.hpp" in the function narrow_domx
268  */
269 
270  int* scclist = r.alloc<int>(n);
271  SccComponent* sinfo = r.alloc<SccComponent>(n);
272 
273  for(int i = n; i--; )
274  sinfo[i].left=sinfo[i].right=sinfo[i].rightmost=sinfo[i].leftmost= i;
275 
276  computesccs(home,x,y,phi,sinfo,scclist);
277 
278  /*
279  * STEP 5:
280  * Narrow the domains of the variables
281  * Also implemented in "narrowing.hpp"
282  * in the functions narrow_domx and narrow_domy
283  */
284 
285  if (!narrow_domx<View,Perm>(home,x,y,z,tau,phi,scclist,sinfo,nofix))
286  return ES_FAILED;
287 
288  if (Perm) {
289  if (!noperm_bc &&
290  !perm_bc<View>
291  (home, tau, sinfo, scclist, x,z, repairpass, nofix))
292  return ES_FAILED;
293 
294  // channeling also needed after normal propagation steps
295  // in order to ensure consistency after possible modification in perm_bc
296  if (!channel(home,x,y,z,nofix))
297  return ES_FAILED;
298  if (nofix)
299  return ES_NOFIX;
300  }
301 
302  sort_tau<View,Perm>(x,z,tau);
303 
304  if (Perm) {
305  // special case of sccs of size 2 denoted by permutation variables
306  // used to enforce consistency from x to y
307  // case of the upper bound ordering tau
308  for (int i = x.size() - 1; i--; ) {
309  // two x variables are in the same scc of size 2
310  if (z[tau[i]].min() == z[tau[i+1]].min() &&
311  z[tau[i]].max() == z[tau[i+1]].max() &&
312  z[tau[i]].size() == 2 && z[tau[i]].range()) {
313  // if bounds are strictly smaller
314  if (x[tau[i]].max() < x[tau[i+1]].max()) {
315  ModEvent me = y[z[tau[i]].min()].lq(home, x[tau[i]].max());
316  if (me_failed(me))
317  return ES_FAILED;
318  nofix |= (me_modified(me) &&
319  y[z[tau[i]].min()].max() != x[tau[i]].max());
320 
321  me = y[z[tau[i+1]].max()].lq(home, x[tau[i+1]].max());
322  if (me_failed(me))
323  return ES_FAILED;
324  nofix |= (me_modified(me) &&
325  y[z[tau[i+1]].max()].max() != x[tau[i+1]].max());
326  }
327  }
328  }
329  }
330  return nofix ? ES_NOFIX : ES_FIX;
331  }
332 
333  template<class View, bool Perm>
335  Sorted(Space& home, bool share, Sorted<View,Perm>& p):
336  Propagator(home, share, p),
337  reachable(p.reachable) {
338  x.update(home, share, p.x);
339  y.update(home, share, p.y);
340  z.update(home, share, p.z);
341  w.update(home, share, p.w);
342  }
343 
344  template<class View, bool Perm>
348  Propagator(home), x(x0), y(y0), z(z0), w(home,y0), reachable(-1) {
349  x.subscribe(home, *this, PC_INT_BND);
350  y.subscribe(home, *this, PC_INT_BND);
351  if (Perm)
352  z.subscribe(home, *this, PC_INT_BND);
353  }
354 
355  template<class View, bool Perm>
356  forceinline size_t
358  x.cancel(home,*this, PC_INT_BND);
359  y.cancel(home,*this, PC_INT_BND);
360  if (Perm)
361  z.cancel(home,*this, PC_INT_BND);
362  (void) Propagator::dispose(home);
363  return sizeof(*this);
364  }
365 
366  template<class View, bool Perm>
367  Actor* Sorted<View,Perm>::copy(Space& home, bool share) {
368  return new (home) Sorted<View,Perm>(home, share, *this);
369  }
370 
371  template<class View, bool Perm>
373  return PropCost::linear(PropCost::LO, x.size());
374  }
375 
376  template<class View, bool Perm>
377  ExecStatus
379  int n = x.size();
380  bool secondpass = false;
381  bool nofix = false;
382  int dropfst = 0;
383 
384  bool subsumed = false;
385  bool array_subs = false;
386  bool match_fixed = false;
387 
388  // normalization of x and y
389  if (!normalize(home, y, x, nofix))
390  return ES_FAILED;
391 
392  // create sigma sorting
393  sort_sigma<View,Perm>(home,x,z);
394 
395  bool noperm_bc = false;
396  if (!array_assigned<View,Perm>
397  (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc))
398  return ES_FAILED;
399 
400  if (array_subs)
401  return home.ES_SUBSUMED(*this);
402 
403  sort_sigma<View,Perm>(home,x,z);
404 
405  // in this case check_subsumptions is guaranteed to find
406  // the xs ordered by sigma
407 
408  if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst))
409  return ES_FAILED;
410 
411  if (subsumed)
412  return home.ES_SUBSUMED(*this);
413 
414  if (Perm) {
415  // dropping possibly yields inconsistent indices on permutation variables
416  if (dropfst) {
417  reachable = w[dropfst - 1].max();
418  bool unreachable = true;
419  for (int i = x.size(); unreachable && i-- ; ) {
420  unreachable &= (reachable < x[i].min());
421  }
422 
423  if (unreachable) {
424  x.drop_fst(dropfst, home, *this, PC_INT_BND);
425  y.drop_fst(dropfst, home, *this, PC_INT_BND);
426  z.drop_fst(dropfst, home, *this, PC_INT_BND);
427  } else {
428  dropfst = 0;
429  }
430  }
431 
432  n = x.size();
433 
434  if (n < 2) {
435  if (x[0].max() < y[0].min() || y[0].max() < x[0].min())
436  return ES_FAILED;
437  if (Perm) {
438  GECODE_ME_CHECK(z[0].eq(home, w.size() - 1));
439  }
440  GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0])));
441  }
442 
443  // check whether shifting the permutation variables
444  // is necessary after dropping x and y vars
445  // highest reachable index
446  int valid = n - 1;
447  int index = 0;
448  int shift = 0;
449 
450  for (int i = n; i--; ){
451  if (z[i].max() > index)
452  index = z[i].max();
453  if (index > valid)
454  shift = index - valid;
455  }
456 
457  if (shift) {
458  ViewArray<OffsetView> ox(home,n), oy(home,n), oz(home,n);
459 
460  for (int i = n; i--; ) {
461  GECODE_ME_CHECK(z[i].gq(home, shift));
462 
463  oz[i] = OffsetView(z[i], -shift);
464  ox[i] = OffsetView(x[i], 0);
465  oy[i] = OffsetView(y[i], 0);
466  }
467 
468  GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm>
469  (home,*this,ox,oy,oz,secondpass,nofix,match_fixed)));
470 
471  if (secondpass) {
472  GECODE_ES_CHECK((bounds_propagation<OffsetView,Perm>
473  (home,*this,ox,oy,oz,secondpass,nofix,match_fixed)));
474  }
475  } else {
476  GECODE_ES_CHECK((bounds_propagation<View,Perm>
477  (home,*this,x,y,z,secondpass,nofix,match_fixed)));
478 
479  if (secondpass) {
480  GECODE_ES_CHECK((bounds_propagation<View,Perm>
481  (home,*this,x,y,z,secondpass,nofix,match_fixed)));
482  }
483  }
484  } else {
485  // dropping has no consequences
486  if (dropfst) {
487  x.drop_fst(dropfst, home, *this, PC_INT_BND);
488  y.drop_fst(dropfst, home, *this, PC_INT_BND);
489  }
490 
491  n = x.size();
492 
493  if (n < 2) {
494  if (x[0].max() < y[0].min() || y[0].max() < x[0].min())
495  return ES_FAILED;
496  GECODE_REWRITE(*this,(Rel::EqBnd<View,View>::post(home(*this), x[0], y[0])));
497  }
498 
499  GECODE_ES_CHECK((bounds_propagation<View,Perm>
500  (home, *this, x, y, z,secondpass, nofix, match_fixed)));
501  // no second pass possible if there are no permvars
502  }
503 
504  if (!normalize(home, y, x, nofix))
505  return ES_FAILED;
506 
507  Region r(home);
508  int* tau = r.alloc<int>(n);
509  if (match_fixed) {
510  // sorting is determined
511  // sigma and tau coincide
512  for (int i = x.size(); i--; ) {
513  int pi = z[i].val();
514  tau[pi] = i;
515  }
516  } else {
517  for (int i = n; i--; ) {
518  tau[i] = i;
519  }
520  }
521 
522  sort_tau<View,Perm>(x,z,tau);
523  // recreate consistency for already assigned subparts
524  // in order of the upper bounds starting at the end of the array
525  bool xbassigned = true;
526  for (int i = x.size(); i--; ) {
527  if (x[tau[i]].assigned() && xbassigned) {
528  GECODE_ME_CHECK(y[i].eq(home, x[tau[i]].val()));
529  } else {
530  xbassigned = false;
531  }
532  }
533 
534  subsumed = true;
535  array_subs = false;
536  noperm_bc = false;
537 
538  // creating sorting anew
539  sort_sigma<View,Perm>(home,x,z);
540 
541  if (Perm) {
542  for (int i = 0; i < x.size() - 1; i++) {
543  // special case of subsccs of size2 for the lower bounds
544  // two x variables are in the same scc of size 2
545  if (z[i].min() == z[i+1].min() &&
546  z[i].max() == z[i+1].max() &&
547  z[i].size() == 2 && z[i].range()) {
548  if (x[i].min() < x[i+1].min()) {
549  ModEvent me = y[z[i].min()].gq(home, x[i].min());
550  GECODE_ME_CHECK(me);
551  nofix |= (me_modified(me) &&
552  y[z[i].min()].min() != x[i].min());
553 
554  me = y[z[i+1].max()].gq(home, x[i+1].min());
555  GECODE_ME_CHECK(me);
556  nofix |= (me_modified(me) &&
557  y[z[i+1].max()].min() != x[i+1].min());
558  }
559  }
560  }
561  }
562 
563  // check assigned
564  // should be sorted
565  bool xassigned = true;
566  for (int i = 0; i < x.size(); i++) {
567  if (x[i].assigned() && xassigned) {
568  GECODE_ME_CHECK(y[i].eq(home,x[i].val()));
569  } else {
570  xassigned = false;
571  }
572  }
573 
574  // sorted check bounds
575  // final check that variables are consitent with least and greatest possible
576  // values
577  int tlb = std::min(x[0].min(), y[0].min());
578  int tub = std::max(x[x.size() - 1].max(), y[y.size() - 1].max());
579  for (int i = x.size(); i--; ) {
580  ModEvent me = y[i].lq(home, tub);
581  GECODE_ME_CHECK(me);
582  nofix |= me_modified(me) && (y[i].max() != tub);
583 
584  me = y[i].gq(home, tlb);
585  GECODE_ME_CHECK(me);
586  nofix |= me_modified(me) && (y[i].min() != tlb);
587 
588  me = x[i].lq(home, tub);
589  GECODE_ME_CHECK(me);
590  nofix |= me_modified(me) && (x[i].max() != tub);
591 
592  me = x[i].gq(home, tlb);
593  GECODE_ME_CHECK(me);
594  nofix |= me_modified(me) && (x[i].min() != tlb);
595  }
596 
597  if (!array_assigned<View,Perm>
598  (home, x, y, z, array_subs, match_fixed, nofix, noperm_bc))
599  return ES_FAILED;
600 
601  if (array_subs)
602  return home.ES_SUBSUMED(*this);
603 
604  if (!check_subsumption<View,Perm>(x,y,z,subsumed,dropfst))
605  return ES_FAILED;
606 
607  if (subsumed)
608  return home.ES_SUBSUMED(*this);
609 
610  return nofix ? ES_NOFIX : ES_FIX;
611  }
612 
613  template<class View, bool Perm>
614  ExecStatus
616  post(Home home,
618  int n = x0.size();
619  if (n < 2) {
620  if ((x0[0].max() < y0[0].min()) || (y0[0].max() < x0[0].min()))
621  return ES_FAILED;
622  GECODE_ES_CHECK((Rel::EqBnd<View,View>::post(home,x0[0],y0[0])));
623  if (Perm) {
624  GECODE_ME_CHECK(z0[0].eq(home,0));
625  }
626  } else {
627  if (Perm) {
628  ViewArray<View> z(home,n);
629  for (int i=n; i--; ) {
630  z[i]=z0[i];
631  GECODE_ME_CHECK(z[i].gq(home,0));
632  GECODE_ME_CHECK(z[i].lq(home,n-1));
633  }
635  }
636  new (home) Sorted<View,Perm>(home,x0,y0,z0);
637  }
638  return ES_OK;
639  }
640 
641 }}}
642 
643 // STATISTICS: int-prop
644 
645 
646