Generated on Sat Jan 20 2018 22:21:14 for Gecode by doxygen 1.8.13
base.hpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Christian Schulte <schulte@gecode.org>
5  *
6  * Copyright:
7  * Christian Schulte, 2007
8  *
9  * Last modified:
10  * $Date: 2016-04-19 17:19:45 +0200 (Tue, 19 Apr 2016) $ by $Author: schulte $
11  * $Revision: 14967 $
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 namespace Gecode { namespace Int { namespace Circuit {
39 
40  template<class View, class Offset>
43  : NaryPropagator<View,Int::PC_INT_DOM>(home,x),
44  start(0), y(home,x), o(o0) {
45  home.notice(*this,AP_WEAKLY);
46  }
47 
48  template<class View, class Offset>
52  o.update(p.o);
53  y.update(home,share,p.y);
54  }
55 
57  template<class View>
58  class NodeInfo {
59  public:
60  int min, low, pre;
62  };
63 
65  template<class View>
66  class TellInfo {
67  public:
68  View x; int n;
69  };
70 
71  template<class View, class Offset>
74  int n = x.size();
75 
77  {
78  int v = start;
80  int m = n;
81  while (x[v].assigned()) {
82  m--;
83  v = o(x[v]).val();
84  // Reached start node again, check whether all nodes have been visited
85  if (start == v)
86  return (m == 0) ? home.ES_SUBSUMED(*this) : ES_FAILED;
87  }
88  start = v;
89  }
90 
92  Region r(home);
93  typedef typename Offset::ViewType OView;
95  unsigned int n_edges = 0;
96  for (int i=n; i--; ) {
97  n_edges += x[i].size();
98  si[i].pre=-1;
99  }
100 
101  // Stack to remember which nodes have not been processed completely
103 
104  // Array to remember which mandatory tells need to be done
106  int n_eq = 0;
107 
108  // Array to remember which edges need to be pruned
109  TellInfo<OView>* nq = r.alloc<TellInfo<OView> >(n_edges);
110  int n_nq = 0;
111 
112  /*
113  * Check whether there is a single strongly connected component.
114  * This is a downstripped version of Tarjan's algorithm as
115  * the computation of sccs proper is not needed. In addition, it
116  * checks a mandatory condition for a graph to be Hamiltonian
117  * (due to Mats Carlsson).
118  *
119  * To quote Mats: Suppose you do a depth-first search of the graph.
120  * In that search, the root node will have a number of child subtrees
121  * T1, ..., Tn. By construction, if i<j then there is no edge from
122  * Ti to Tj. The necessary condition for Hamiltonianicity is that
123  * there be an edge from Ti+1 to Ti, for 0 < i < n.
124  *
125  * In addition, we do the following: if there is only a single edge
126  * from Ti+1 to Ti, then it must be mandatory and the variable must
127  * be assigned to that value.
128  *
129  * The same holds true for a back edge from T0 to the root node.
130  *
131  * Then, all edges that reach from Ti+k+1 to Ti can be pruned.
132  *
133  */
134 
135  {
136  // Start always at node start
137  int i = start;
138  // Counter for scc
139  int cnt = 0;
140  // Smallest preorder number of last subtree (initially, the root node)
141  int subtree_min = 0;
142  // Largest preorder number of last subtree (initially, the root node)
143  int subtree_max = 0;
144  // Number of back edges into last subtree or root
145  int back = 0;
146  start:
147  si[i].min = si[i].pre = si[i].low = cnt++;
148  si[i].v.init(o(x[i]));
149  do {
150  if (si[si[i].v.val()].pre < 0) {
151  next.push(i);
152  i=si[i].v.val();
153  goto start;
154  } else if ((subtree_min <= si[si[i].v.val()].pre) &&
155  (si[si[i].v.val()].pre <= subtree_max)) {
156  back++;
157  eq[n_eq].x = o(x[i]);
158  eq[n_eq].n = si[i].v.val();
159  } else if (si[si[i].v.val()].pre < subtree_min) {
160  nq[n_nq].x = o(x[i]);
161  nq[n_nq].n = si[i].v.val();
162  n_nq++;
163  }
164  cont:
165  if (si[si[i].v.val()].low < si[i].min)
166  si[i].min = si[si[i].v.val()].low;
167  ++si[i].v;
168  } while (si[i].v());
169  if (si[i].min < si[i].low) {
170  si[i].low = si[i].min;
171  } else if (i != start) {
172  // If it is not the first node visited, there is more than one SCC
173  return ES_FAILED;
174  }
175  if (!next.empty()) {
176  i=next.pop();
177  if (i == start) {
178  // No back edge
179  if (back == 0)
180  return ES_FAILED;
181  // Exactly one back edge, make it mandatory (keep topmost entry)
182  if (back == 1)
183  n_eq++;
184  back = 0;
185  subtree_min = subtree_max+1;
186  subtree_max = cnt-1;
187  }
188  goto cont;
189  }
190 
191  // Whether all nodes have been visited
192  if (cnt != n)
193  return ES_FAILED;
194 
195  /*
196  * Whether there is more than one subtree
197  *
198  * This propagation rule is taken from: Kathryn Glenn Francis,
199  * Peter Stuckey, Explaining Circuit Propagation,
200  * Constraints (2014) 19:1-29.
201  *
202  */
203  if (subtree_min > 1) {
204  for (Int::ViewValues<OView> v(o(x[start])); v(); ++v)
205  if (si[v.val()].pre < subtree_min) {
206  nq[n_nq].x = o(x[v.val()]);
207  nq[n_nq].n = v.val();
208  n_nq++;
209  }
210  }
211 
212  ExecStatus es = ES_FIX;
213  // Assign all mandatory edges
214  while (n_eq-- > 0) {
215  ModEvent me = eq[n_eq].x.eq(home,eq[n_eq].n);
216  if (me_failed(me))
217  return ES_FAILED;
218  if (me_modified(me))
219  es = ES_NOFIX;
220  }
221 
222  // Remove all edges that would require a non-simple cycle
223  while (n_nq-- > 0) {
224  ModEvent me = nq[n_nq].x.nq(home,nq[n_nq].n);
225  if (me_failed(me))
226  return ES_FAILED;
227  if (me_modified(me))
228  es = ES_NOFIX;
229  }
230 
231  // Move start to different node for next run
232  start = o(x[start]).min();
233 
234  return es;
235  }
236  }
237 
238  template<class View, class Offset>
239  ExecStatus
241  // Prunes that partial assigned paths are not completed to cycles
242 
243  int n=x.size();
244 
245  Region r(home);
246 
247  // The path starting at assigned x[i] ends at x[end[j]] which is
248  // not assigned.
249  int* end = r.alloc<int>(n);
250  for (int i=n; i--; )
251  end[i]=-1;
252 
253  // A stack that records all indices i such that end[i] != -1
255 
256  typedef typename Offset::ViewType OView;
257  for (int i=y.size(); i--; ) {
258  assert(!y[i].assigned());
259  // Non-assigned views serve as starting points for assigned paths
261  // Try all connected values
262  do {
263  int j0=v.val();
264  // Starting point for not yet followed assigned path found
265  if (x[j0].assigned() && (end[j0] < 0)) {
266  // Follow assigned path until non-assigned view:
267  // all assigned view on the paths can be skipped, as
268  // if x[i] is assigned to j, then x[j] will only have
269  // x[i] as predecessor due to propagating distinct.
270  int j = j0;
271  do {
272  j=o(x[j]).val();
273  } while (x[j].assigned());
274  // Now there cannot be a cycle from x[j] to x[v.val()]!
275  // However, the tell cannot be done here as j might be
276  // equal to i and might hence kill the iterator v!
277  end[j0]=j; tell.push(j0);
278  }
279  ++v;
280  } while (v());
281  }
282 
283  // Now do the tells based on the end information
284  while (!tell.empty()) {
285  int i = tell.pop();
286  assert(end[i] >= 0);
287  GECODE_ME_CHECK(o(x[end[i]]).nq(home,i));
288  }
289  return ES_NOFIX;
290  }
291 
292  template<class View, class Offset>
293  forceinline size_t
295  home.ignore(*this,AP_WEAKLY);
297  return sizeof(*this);
298  }
299 
300 }}}
301 
302 // STATISTICS: int-prop
303 
void push(const T &x)
Push element x on top of stack.
const SetInstr * si[]
Definition: mm-set.cpp:4340
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3614
Offset o
Offset transformation.
Definition: circuit.hh:67
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:326
ExecStatus path(Space &home)
Ensure path property: prune edges that could give too small cycles.
Definition: base.hpp:240
bool empty(void) const
Test whether stack is empty.
int ModEvent
Type for modification events.
Definition: core.hpp:142
ViewArray< View > x
Array of views.
Definition: propagator.hpp:152
ExecStatus connected(Space &home)
Check whether the view value graph is strongly connected.
Definition: base.hpp:73
Handle to region.
Definition: region.hpp:61
Value iterator for integer views.
Definition: view.hpp:94
Propagation has computed fixpoint.
Definition: core.hpp:545
Computation spaces.
Definition: core.hpp:1748
int val(void) const
Return current value.
int start
Remember where to start the next time the propagator runs.
Definition: circuit.hh:63
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Execution has resulted in failure.
Definition: core.hpp:542
const Gecode::PropCond PC_INT_DOM
Propagate when domain changes.
Definition: var-type.hpp:100
n-ary propagator
Definition: propagator.hpp:149
ViewArray< View > y
Array for performing value propagation for distinct.
Definition: circuit.hh:65
Offset integer view.
Definition: view.hpp:422
void update(const Offset &o)
Update during cloning.
Definition: view.hpp:637
View arrays.
Definition: array.hpp:234
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:56
void notice(Actor &a, ActorProperty p, bool duplicate=false)
Notice actor property.
Definition: core.hpp:3321
Converter with fixed offset.
Definition: view.hpp:617
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:784
const int v[7]
Definition: distinct.cpp:263
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:71
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:784
void ignore(Actor &a, ActorProperty p, bool duplicate=false)
Ignore actor property.
Definition: core.hpp:4141
Base(Space &home, bool share, Base &p)
Constructor for cloning p.
ExecStatus
Definition: core.hpp:540
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:47
#define forceinline
Definition: config.hpp:173
Stack with fixed number of elements.
bool me_modified(ModEvent me)
Check whether modification event me describes variable modification.
Definition: modevent.hpp:63
T pop(void)
Pop topmost element from stack and return it.
Post propagator for SetVar x
Definition: set.hh:784
Propagation has not computed fixpoint.
Definition: core.hpp:543
Information required for non-recursive checking for a single scc.
Definition: base.hpp:58
Gecode toplevel namespace
Int::ViewValues< View > v
Definition: base.hpp:61
Home class for posting propagators
Definition: core.hpp:922
Base-class for circuit propagator.
Definition: circuit.hh:59
bool me_failed(ModEvent me)
Check whether modification event me is failed.
Definition: modevent.hpp:58
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: base.hpp:294
Information for performing a recorded tell.
Definition: base.hpp:66