this repo has no description
dekker.one
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 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34namespace Gecode { namespace Int { namespace Circuit {
35
36 template<class View, class Offset>
37 forceinline
38 Base<View,Offset>::Base(Home home, ViewArray<View>& x, Offset& o0)
39 : NaryPropagator<View,Int::PC_INT_DOM>(home,x),
40 start(0), y(home,x), o(o0) {
41 home.notice(*this,AP_WEAKLY);
42 }
43
44 template<class View, class Offset>
45 forceinline
46 Base<View,Offset>::Base(Space& home, Base<View,Offset>& p)
47 : NaryPropagator<View,Int::PC_INT_DOM>(home,p), start(p.start) {
48 o.update(p.o);
49 y.update(home,p.y);
50 }
51
52 /// Information required for non-recursive checking for a single scc
53 template<class View>
54 class NodeInfo {
55 public:
56 int min, low, pre;
57 Int::ViewValues<View> v;
58 };
59
60 /// Information for performing a recorded tell
61 template<class View>
62 class TellInfo {
63 public:
64 View x; int n;
65 };
66
67 template<class View, class Offset>
68 ExecStatus
69 Base<View,Offset>::connected(Space& home) {
70 int n = x.size();
71
72 /// First non-assigned node reachable from start
73 {
74 int v = start;
75 /// Number of nodes not yet visited
76 int m = n;
77 while (x[v].assigned()) {
78 m--;
79 v = o(x[v]).val();
80 // Reached start node again, check whether all nodes have been visited
81 if (start == v)
82 return (m == 0) ? home.ES_SUBSUMED(*this) : ES_FAILED;
83 }
84 start = v;
85 }
86
87 /// Information needed for checking scc's
88 Region r;
89 typedef typename Offset::ViewType OView;
90 NodeInfo<OView>* si = r.alloc<NodeInfo<OView> >(n);
91 unsigned int n_edges = 0;
92 for (int i=0; i<n; i++) {
93 n_edges += x[i].size();
94 si[i].pre=-1;
95 }
96
97 // Stack to remember which nodes have not been processed completely
98 Support::StaticStack<int,Region> next(r,n);
99
100 // Array to remember which mandatory tells need to be done
101 TellInfo<OView>* eq = r.alloc<TellInfo<OView> >(n);
102 int n_eq = 0;
103
104 // Array to remember which edges need to be pruned
105 TellInfo<OView>* nq = r.alloc<TellInfo<OView> >(n_edges);
106 int n_nq = 0;
107
108 /*
109 * Check whether there is a single strongly connected component.
110 * This is a downstripped version of Tarjan's algorithm as
111 * the computation of sccs proper is not needed. In addition, it
112 * checks a mandatory condition for a graph to be Hamiltonian
113 * (due to Mats Carlsson).
114 *
115 * To quote Mats: Suppose you do a depth-first search of the graph.
116 * In that search, the root node will have a number of child subtrees
117 * T1, ..., Tn. By construction, if i<j then there is no edge from
118 * Ti to Tj. The necessary condition for Hamiltonianicity is that
119 * there be an edge from Ti+1 to Ti, for 0 < i < n.
120 *
121 * In addition, we do the following: if there is only a single edge
122 * from Ti+1 to Ti, then it must be mandatory and the variable must
123 * be assigned to that value.
124 *
125 * The same holds true for a back edge from T0 to the root node.
126 *
127 * Then, all edges that reach from Ti+k+1 to Ti can be pruned.
128 *
129 */
130
131 {
132 // Start always at node start
133 int i = start;
134 // Counter for scc
135 int cnt = 0;
136 // Smallest preorder number of last subtree (initially, the root node)
137 int subtree_min = 0;
138 // Largest preorder number of last subtree (initially, the root node)
139 int subtree_max = 0;
140 // Number of back edges into last subtree or root
141 int back = 0;
142 start:
143 si[i].min = si[i].pre = si[i].low = cnt++;
144 si[i].v.init(o(x[i]));
145 do {
146 if (si[si[i].v.val()].pre < 0) {
147 next.push(i);
148 i=si[i].v.val();
149 goto start;
150 } else if ((subtree_min <= si[si[i].v.val()].pre) &&
151 (si[si[i].v.val()].pre <= subtree_max)) {
152 back++;
153 eq[n_eq].x = o(x[i]);
154 eq[n_eq].n = si[i].v.val();
155 } else if (si[si[i].v.val()].pre < subtree_min) {
156 nq[n_nq].x = o(x[i]);
157 nq[n_nq].n = si[i].v.val();
158 n_nq++;
159 }
160 cont:
161 if (si[si[i].v.val()].low < si[i].min)
162 si[i].min = si[si[i].v.val()].low;
163 ++si[i].v;
164 } while (si[i].v());
165 if (si[i].min < si[i].low) {
166 si[i].low = si[i].min;
167 } else if (i != start) {
168 // If it is not the first node visited, there is more than one SCC
169 return ES_FAILED;
170 }
171 if (!next.empty()) {
172 i=next.pop();
173 if (i == start) {
174 // No back edge
175 if (back == 0)
176 return ES_FAILED;
177 // Exactly one back edge, make it mandatory (keep topmost entry)
178 if (back == 1)
179 n_eq++;
180 back = 0;
181 subtree_min = subtree_max+1;
182 subtree_max = cnt-1;
183 }
184 goto cont;
185 }
186
187 // Whether all nodes have been visited
188 if (cnt != n)
189 return ES_FAILED;
190
191 /*
192 * Whether there is more than one subtree
193 *
194 * This propagation rule is taken from: Kathryn Glenn Francis,
195 * Peter Stuckey, Explaining Circuit Propagation,
196 * Constraints (2014) 19:1-29.
197 *
198 */
199 if (subtree_min > 1) {
200 for (Int::ViewValues<OView> v(o(x[start])); v(); ++v)
201 if (si[v.val()].pre < subtree_min) {
202 nq[n_nq].x = o(x[v.val()]);
203 nq[n_nq].n = v.val();
204 n_nq++;
205 }
206 }
207
208 ExecStatus es = ES_FIX;
209 // Assign all mandatory edges
210 while (n_eq-- > 0) {
211 ModEvent me = eq[n_eq].x.eq(home,eq[n_eq].n);
212 if (me_failed(me))
213 return ES_FAILED;
214 if (me_modified(me))
215 es = ES_NOFIX;
216 }
217
218 // Remove all edges that would require a non-simple cycle
219 while (n_nq-- > 0) {
220 ModEvent me = nq[n_nq].x.nq(home,nq[n_nq].n);
221 if (me_failed(me))
222 return ES_FAILED;
223 if (me_modified(me))
224 es = ES_NOFIX;
225 }
226
227 // Move start to different node for next run
228 start = o(x[start]).min();
229
230 return es;
231 }
232 }
233
234 template<class View, class Offset>
235 ExecStatus
236 Base<View,Offset>::path(Space& home) {
237 // Prunes that partial assigned paths are not completed to cycles
238
239 int n=x.size();
240
241 Region r;
242
243 // The path starting at assigned x[i] ends at x[end[j]] which is
244 // not assigned.
245 int* end = r.alloc<int>(n);
246 for (int i=0; i<n; i++)
247 end[i]=-1;
248
249 // A stack that records all indices i such that end[i] != -1
250 Support::StaticStack<int,Region> tell(r,n);
251
252 typedef typename Offset::ViewType OView;
253 for (int i=0; i<y.size(); i++) {
254 assert(!y[i].assigned());
255 // Non-assigned views serve as starting points for assigned paths
256 Int::ViewValues<OView> v(o(y[i]));
257 // Try all connected values
258 do {
259 int j0=v.val();
260 // Starting point for not yet followed assigned path found
261 if (x[j0].assigned() && (end[j0] < 0)) {
262 // Follow assigned path until non-assigned view:
263 // all assigned view on the paths can be skipped, as
264 // if x[i] is assigned to j, then x[j] will only have
265 // x[i] as predecessor due to propagating distinct.
266 int j = j0;
267 do {
268 j=o(x[j]).val();
269 } while (x[j].assigned());
270 // Now there cannot be a cycle from x[j] to x[v.val()]!
271 // However, the tell cannot be done here as j might be
272 // equal to i and might hence kill the iterator v!
273 end[j0]=j; tell.push(j0);
274 }
275 ++v;
276 } while (v());
277 }
278
279 // Now do the tells based on the end information
280 while (!tell.empty()) {
281 int i = tell.pop();
282 assert(end[i] >= 0);
283 GECODE_ME_CHECK(o(x[end[i]]).nq(home,i));
284 }
285 return ES_NOFIX;
286 }
287
288 template<class View, class Offset>
289 forceinline size_t
290 Base<View,Offset>::dispose(Space& home) {
291 home.ignore(*this,AP_WEAKLY);
292 (void) NaryPropagator<View,Int::PC_INT_DOM>::dispose(home);
293 return sizeof(*this);
294 }
295
296}}}
297
298// STATISTICS: int-prop
299