TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
PathZdd.hpp
1 /*
2  * TdZdd: a Top-down/Breadth-first Decision Diagram Manipulation Framework
3  * by Hiroaki Iwashita <iwashita@erato.ist.hokudai.ac.jp>
4  * Copyright (c) 2014 ERATO MINATO Project
5  *
6  * Permission is hereby granted, free of charge, to any person obtaining a
7  * copy of this software and associated documentation files (the "Software"),
8  * to deal in the Software without restriction, including without limitation
9  * the rights to use, copy, modify, merge, publish, distribute, sublicense,
10  * and/or sell copies of the Software, and to permit persons to whom the
11  * Software is furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be included in
14  * all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21  * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
22  * DEALINGS IN THE SOFTWARE.
23  */
24 
25 #pragma once
26 
27 #include <vector>
28 
29 #include "../DdSpec.hpp"
30 #include "../util/Graph.hpp"
31 
32 namespace tdzdd {
33 
34 enum SimpathBasedImplType {
35  Path, Cycle
36 };
37 
38 template<typename S, SimpathBasedImplType type, bool hamilton = false>
39 class SimpathBasedImpl: public tdzdd::PodArrayDdSpec<S,int16_t,2> {
40 public:
41  typedef int16_t Mate;
42 
43 private:
44  Graph const& graph;
45  int const m;
46  int const n;
47  int const mateArraySize_;
48  std::vector<Mate> initialMate;
49 
50  bool const lookahead;
51 
52  enum Takable {
53  NO, YES, HIT
54  };
55 
56  void shiftMate(Mate* mate, int v0, int vv0) const {
57  int const d = vv0 - v0;
58  if (d > 0) {
59  std::memmove(mate, mate + d, (mateArraySize_ - d) * sizeof(*mate));
60  for (int k = mateArraySize_ - d; k < mateArraySize_; ++k) {
61  mate[k] = initialMate[vv0 + k];
62  }
63  }
64  }
65 
66  Takable takable(Mate const* mate, Graph::EdgeInfo const& e) const {
67  int const w1 = mate[e.v1 - e.v0];
68  int const w2 = mate[e.v2 - e.v0];
69 
70  if (w1 == 0) return NO;
71  if (e.v1final && w1 == e.v1) return NO;
72 
73  if (w2 == 0) return NO;
74  if (e.v2final && w2 == e.v2) return NO;
75 
76  switch (type) {
77  case Path:
78  if (w1 == e.v2) return NO;
79 
80  if (w1 < 0 && w2 < 0) {
81  if (w1 != w2) return NO;
82  if (!e.allColorsSeen) return YES;
83 
84  bool clean = true;
85  for (int k = 0; k < mateArraySize_; ++k) {
86  if (e.v0 + k == e.v1) continue;
87  if (e.v0 + k == e.v2) continue;
88  int w = mate[k];
89  if (w < 0) return YES;
90  if (w != 0 && (hamilton || w != e.v0 + k)) clean = false;
91  }
92  return clean ? HIT : NO;
93  }
94  break;
95  case Cycle:
96  if (w1 == e.v2) {
97  assert(w2 == e.v1);
98 
99  for (int k = 1; k < mateArraySize_; ++k) {
100  if (e.v0 + k == e.v1) continue;
101  if (e.v0 + k == e.v2) continue;
102  int w = mate[k];
103  if (w != 0 && (hamilton || w != e.v0 + k)) return NO;
104  }
105  return HIT;
106  }
107  break;
108  }
109 
110  return YES;
111  }
112 
113  bool leavable(Mate const* mate, Graph::EdgeInfo const& e) const {
114  int const w1 = mate[e.v1 - e.v0];
115  int const w2 = mate[e.v2 - e.v0];
116 
117  if (hamilton) {
118  if (e.v1final && w1 != 0) return false;
119  if (e.v2final && w2 != 0) return false;
120  if (e.v1final2 && w1 == e.v1) return false;
121  if (e.v2final2 && w2 == e.v2) return false;
122  }
123  else {
124  if (e.v1final && w1 != 0 && w1 != e.v1) return false;
125  if (e.v2final && w2 != 0 && w2 != e.v2) return false;
126  }
127 
128  return true;
129  }
130 
131 public:
132  SimpathBasedImpl(Graph const& graph, bool lookahead)
133  : graph(graph), m(graph.vertexSize()), n(graph.edgeSize()),
134  mateArraySize_(graph.maxFrontierSize()),
135  initialMate(m + mateArraySize_), lookahead(lookahead) {
136  this->setArraySize(mateArraySize_);
137 
138  for (int v = 1; v <= m; ++v) {
139  int c = graph.colorNumber(v);
140  initialMate[v] = (c > 0) ? -c : v;
141  }
142 
143  for (int v = m + 1; v < m + mateArraySize_; ++v) {
144  initialMate[v] = 0;
145  }
146  }
147 
148  int mateArraySize() const {
149  return mateArraySize_;
150  }
151 
152  int getRoot(Mate* mate) const {
153  int const v0 = graph.edgeInfo(0).v0;
154 
155  for (int k = 0; k < mateArraySize_; ++k) {
156  mate[k] = initialMate[v0 + k];
157  }
158 
159  return n;
160  }
161 
162  int getChild(Mate* mate, int level, int take) const {
163  assert(1 <= level && level <= n);
164  int i = n - level;
165  Graph::EdgeInfo const& e = graph.edgeInfo(i);
166  assert(e.v1 <= e.v2);
167 
168  if (take) {
169  switch (takable(mate, e)) {
170  case NO:
171  return 0;
172  case HIT:
173  return -1;
174  case YES:
175  break;
176  }
177 
178  int w1 = mate[e.v1 - e.v0];
179  int w2 = mate[e.v2 - e.v0];
180  if (w1 > 0) mate[w1 - e.v0] = w2;
181  if (w2 > 0) mate[w2 - e.v0] = w1;
182  if (e.v1final || w1 != e.v1) mate[e.v1 - e.v0] = 0;
183  if (e.v2final || w2 != e.v2) mate[e.v2 - e.v0] = 0;
184  }
185  else {
186  if (!leavable(mate, e)) return 0;
187 
188  Mate& w1 = mate[e.v1 - e.v0];
189  Mate& w2 = mate[e.v2 - e.v0];
190  if (e.v1final || (e.v1final2 && w1 == e.v1)) w1 = 0;
191  if (e.v2final || (e.v2final2 && w2 == e.v2)) w2 = 0;
192  }
193 
194  if (++i == n) return 0;
195  shiftMate(mate, e.v0, graph.edgeInfo(i).v0);
196 
197  while (lookahead) {
198  Graph::EdgeInfo const& e = graph.edgeInfo(i);
199  assert(e.v1 <= e.v2);
200 
201  if (takable(mate, e) != NO) break;
202  if (!leavable(mate, e)) return 0;
203  if (++i == n) return 0;
204 
205  Mate& w1 = mate[e.v1 - e.v0];
206  Mate& w2 = mate[e.v2 - e.v0];
207  if (e.v1final || (e.v1final2 && w1 == e.v1)) w1 = 0;
208  if (e.v2final || (e.v2final2 && w2 == e.v2)) w2 = 0;
209 
210  shiftMate(mate, e.v0, graph.edgeInfo(i).v0);
211  }
212 
213  assert(i < n);
214  return n - i;
215  }
216 };
217 
218 struct PathZdd: public SimpathBasedImpl<PathZdd,Path,false> {
219  PathZdd(Graph const& graph, bool lookahead = true)
220  : SimpathBasedImpl<PathZdd,Path,false>(graph, lookahead) {
221  }
222 };
223 
224 struct HamiltonPathZdd: public SimpathBasedImpl<HamiltonPathZdd,Path,true> {
225  HamiltonPathZdd(Graph const& graph, bool lookahead = true)
226  : SimpathBasedImpl<HamiltonPathZdd,Path,true>(graph, lookahead) {
227  }
228 };
229 
230 struct CycleZdd: public SimpathBasedImpl<CycleZdd,Cycle,false> {
231  CycleZdd(Graph const& graph, bool lookahead = true)
232  : SimpathBasedImpl<CycleZdd,Cycle,false>(graph, lookahead) {
233  }
234 };
235 
236 struct HamiltonCycleZdd: public SimpathBasedImpl<HamiltonCycleZdd,Cycle,true> {
237  HamiltonCycleZdd(Graph const& graph, bool lookahead = true)
238  : SimpathBasedImpl<HamiltonCycleZdd,Cycle,true>(graph, lookahead) {
239  }
240 };
241 
242 } // namespace tdzdd
Abstract class of DD specifications using POD array states.
Definition: DdSpec.hpp:373