1 /*++
2 Copyright (c) 2017 Arie Gurfinkel
3
4 Module Name:
5
6 min_cut.cpp
7
8 Abstract:
9 min cut solver
10
11 Author:
12 Bernhard Gleiss
13
14 Revision History:
15
16
17 --*/
18 #include "util/min_cut.h"
19 #include "util/trace.h"
20
min_cut()21 min_cut::min_cut() {
22 // push back two empty vectors for source and sink
23 m_edges.push_back(edge_vector());
24 m_edges.push_back(edge_vector());
25 }
26
new_node()27 unsigned min_cut::new_node() {
28 m_edges.push_back(edge_vector());
29 return m_edges.size() - 1;
30 }
31
add_edge(unsigned int i,unsigned int j,unsigned capacity)32 void min_cut::add_edge(unsigned int i, unsigned int j, unsigned capacity) {
33 m_edges.reserve(i + 1);
34 m_edges[i].push_back(edge(j, capacity));
35 TRACE("spacer.mincut", tout << "adding edge (" << i << "," << j << ")\n";);
36 }
37
compute_min_cut(unsigned_vector & cut_nodes)38 void min_cut::compute_min_cut(unsigned_vector& cut_nodes) {
39 if (m_edges.size() == 2) {
40 return;
41 }
42
43 m_d.resize(m_edges.size());
44 m_pred.resize(m_edges.size());
45
46 // compute initial distances and number of nodes
47 compute_initial_distances();
48
49 unsigned i = 0;
50
51 while (m_d[0] < m_edges.size()) {
52 unsigned j = get_admissible_edge(i);
53
54 if (j < m_edges.size()) {
55 // advance(i)
56 m_pred[j] = i;
57 i = j;
58
59 // if i is the sink, augment path
60 if (i == 1) {
61 augment_path();
62 i = 0;
63 }
64 }
65 else {
66 // retreat
67 compute_distance(i);
68 if (i != 0) {
69 i = m_pred[i];
70 }
71 }
72 }
73
74 // split nodes into reachable and unreachable ones
75 bool_vector reachable(m_edges.size());
76 compute_reachable_nodes(reachable);
77
78 // find all edges between reachable and unreachable nodes and
79 // for each such edge, add corresponding lemma to unsat-core
80 compute_cut_and_add_lemmas(reachable, cut_nodes);
81 }
82
compute_initial_distances()83 void min_cut::compute_initial_distances() {
84 unsigned_vector todo;
85 bool_vector visited(m_edges.size());
86
87 todo.push_back(0); // start at the source, since we do postorder traversel
88
89 while (!todo.empty()) {
90 unsigned current = todo.back();
91
92 // if we haven't already visited current
93 if (!visited[current]) {
94 bool exists_unvisited_parent = false;
95
96 // add unprocessed parents to stack for DFS. If there is at least
97 // one unprocessed parent, don't compute the result
98 // for current now, but wait until those unprocessed parents are processed
99 for (auto const& edge : m_edges[current]) {
100 unsigned parent = edge.node;
101
102 // if we haven't visited the current parent yet
103 if (!visited[parent]) {
104 // add it to the stack
105 todo.push_back(parent);
106 exists_unvisited_parent = true;
107 }
108 }
109
110 // if we already visited all parents, we can visit current too
111 if (!exists_unvisited_parent) {
112 visited[current] = true;
113 todo.pop_back();
114
115 compute_distance(current); // I.H. all parent distances are already computed
116 }
117 }
118 else {
119 todo.pop_back();
120 }
121 }
122 }
123
get_admissible_edge(unsigned i)124 unsigned min_cut::get_admissible_edge(unsigned i) {
125 for (const auto& edge : m_edges[i]) {
126 if (edge.weight > 0 && m_d[i] == m_d[edge.node] + 1) {
127 return edge.node;
128 }
129 }
130 return m_edges.size(); // no element found
131 }
132
augment_path()133 void min_cut::augment_path() {
134 // find bottleneck capacity
135 unsigned max = std::numeric_limits<unsigned int>::max();
136 unsigned k = 1;
137 while (k != 0) {
138 unsigned l = m_pred[k];
139 for (const auto& edge : m_edges[l]) {
140 if (edge.node == k) {
141 max = std::min(max, edge.weight);
142 }
143 }
144 k = l;
145 }
146
147 k = 1;
148 while (k != 0) {
149 unsigned l = m_pred[k];
150
151 // decrease capacity
152 for (auto& edge : m_edges[l]) {
153 if (edge.node == k) {
154 edge.weight -= max;
155 }
156 }
157 // increase reverse flow
158 bool already_exists = false;
159 for (auto& edge : m_edges[k]) {
160 if (edge.node == l) {
161 already_exists = true;
162 edge.weight += max;
163 }
164 }
165 if (!already_exists) {
166 m_edges[k].push_back(edge(1, max));
167 }
168 k = l;
169 }
170 }
171
compute_distance(unsigned i)172 void min_cut::compute_distance(unsigned i) {
173 if (i == 1) { // sink node
174 m_d[1] = 0;
175 }
176 else {
177 unsigned min = std::numeric_limits<unsigned int>::max();
178
179 // find edge (i,j) with positive residual capacity and smallest distance
180 for (const auto& edge : m_edges[i]) {
181 if (edge.weight > 0) {
182 min = std::min(min, m_d[edge.node] + 1);
183 }
184 }
185 m_d[i] = min;
186 }
187 }
188
compute_reachable_nodes(bool_vector & reachable)189 void min_cut::compute_reachable_nodes(bool_vector& reachable) {
190 unsigned_vector todo;
191
192 todo.push_back(0);
193 while (!todo.empty()) {
194 unsigned current = todo.back();
195 todo.pop_back();
196
197 if (!reachable[current]) {
198 reachable[current] = true;
199
200 for (const auto& edge : m_edges[current]) {
201 if (edge.weight > 0) {
202 todo.push_back(edge.node);
203 }
204 }
205 }
206 }
207 }
208
compute_cut_and_add_lemmas(bool_vector & reachable,unsigned_vector & cut_nodes)209 void min_cut::compute_cut_and_add_lemmas(bool_vector& reachable, unsigned_vector& cut_nodes) {
210 unsigned_vector todo;
211 bool_vector visited(m_edges.size());
212
213 todo.push_back(0);
214 while (!todo.empty()) {
215 unsigned current = todo.back();
216 todo.pop_back();
217
218 if (!visited[current]) {
219 visited[current] = true;
220
221 for (const auto& edge : m_edges[current]) {
222 unsigned successor = edge.node;
223 if (reachable[successor]) {
224 todo.push_back(successor);
225 }
226 else {
227 cut_nodes.push_back(successor);
228 }
229 }
230 }
231 }
232 }
233