1 // Copyright 2010-2021 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13
14 // Solve the Slitherlink problem:
15 // see https://en.wikipedia.org/wiki/Slitherlink
16
17 #include <string>
18 #include <vector>
19
20 #include "absl/strings/str_format.h"
21 #include "ortools/sat/cp_model.h"
22 #include "ortools/sat/model.h"
23
24 const std::vector<std::vector<int> > tiny = {{3, 3, 1}};
25
26 const std::vector<std::vector<int> > small = {
27 {3, 2, -1, 3}, {-1, -1, -1, 2}, {3, -1, -1, -1}, {3, -1, 3, 1}};
28
29 const std::vector<std::vector<int> > medium = {
30 {-1, 0, -1, 1, -1, -1, 1, -1}, {-1, 3, -1, -1, 2, 3, -1, 2},
31 {-1, -1, 0, -1, -1, -1, -1, 0}, {-1, 3, -1, -1, 0, -1, -1, -1},
32 {-1, -1, -1, 3, -1, -1, 0, -1}, {1, -1, -1, -1, -1, 3, -1, -1},
33 {3, -1, 1, 3, -1, -1, 3, -1}, {-1, 0, -1, -1, 3, -1, 3, -1}};
34
35 const std::vector<std::vector<int> > big = {
36 {3, -1, -1, -1, 2, -1, 1, -1, 1, 2},
37 {1, -1, 0, -1, 3, -1, 2, 0, -1, -1},
38 {-1, 3, -1, -1, -1, -1, -1, -1, 3, -1},
39 {2, 0, -1, 3, -1, 2, 3, -1, -1, -1},
40 {-1, -1, -1, 1, 1, 1, -1, -1, 3, 3},
41 {2, 3, -1, -1, 2, 2, 3, -1, -1, -1},
42 {-1, -1, -1, 1, 2, -1, 2, -1, 3, 3},
43 {-1, 2, -1, -1, -1, -1, -1, -1, 2, -1},
44 {-1, -1, 1, 1, -1, 2, -1, 1, -1, 3},
45 {3, 3, -1, 1, -1, 2, -1, -1, -1, 2}};
46
47 namespace operations_research {
48 namespace sat {
49
PrintSolution(const std::vector<std::vector<int>> & data,const std::vector<std::vector<bool>> & h_arcs,const std::vector<std::vector<bool>> & v_arcs)50 void PrintSolution(const std::vector<std::vector<int> >& data,
51 const std::vector<std::vector<bool> >& h_arcs,
52 const std::vector<std::vector<bool> >& v_arcs) {
53 const int num_rows = data.size();
54 const int num_columns = data[0].size();
55
56 for (int i = 0; i < num_rows; ++i) {
57 std::string first_line;
58 std::string second_line;
59 std::string third_line;
60 for (int j = 0; j < num_columns; ++j) {
61 const bool h_arc = h_arcs[i][j];
62 const bool v_arc = v_arcs[j][i];
63 const int sum = data[i][j];
64 first_line += h_arc ? " -----" : " ";
65 second_line += v_arc ? "|" : " ";
66 second_line +=
67 sum == -1 ? " " : absl::StrFormat(" %d ", sum).c_str();
68 third_line += v_arc ? "| " : " ";
69 }
70 const bool termination = v_arcs[num_columns][i];
71 second_line += termination == 1 ? "|" : " ";
72 third_line += termination == 1 ? "|" : " ";
73 std::cout << first_line << std::endl;
74 std::cout << third_line << std::endl;
75 std::cout << second_line << std::endl;
76 std::cout << third_line << std::endl;
77 }
78 std::string last_line;
79 for (int j = 0; j < num_columns; ++j) {
80 const bool h_arc = h_arcs[num_rows][j];
81 last_line += h_arc ? " -----" : " ";
82 }
83 std::cout << last_line << std::endl;
84 }
85
SlitherLink(const std::vector<std::vector<int>> & data)86 void SlitherLink(const std::vector<std::vector<int> >& data) {
87 const int num_rows = data.size();
88 const int num_columns = data[0].size();
89
90 const int num_nodes = (num_rows + 1) * (num_columns + 1);
91 const int num_horizontal_arcs = num_columns * (num_rows + 1);
92 const int num_vertical_arcs = (num_rows) * (num_columns + 1);
93
94 auto undirected_horizontal_arc = [=](int x, int y) {
95 CHECK_LT(x, num_columns);
96 CHECK_LT(y, num_rows + 1);
97 return x + (num_columns * y);
98 };
99
100 auto undirected_vertical_arc = [=](int x, int y) {
101 CHECK_LT(x, num_columns + 1);
102 CHECK_LT(y, num_rows);
103 return x + (num_columns + 1) * y;
104 };
105
106 auto node_index = [=](int x, int y) {
107 CHECK_LT(x, num_columns + 1);
108 CHECK_LT(y, num_rows + 1);
109 return x + y * (num_columns + 1);
110 };
111
112 CpModelBuilder builder;
113
114 std::vector<BoolVar> horizontal_arcs;
115 for (int arc = 0; arc < 2 * num_horizontal_arcs; ++arc) {
116 horizontal_arcs.push_back(builder.NewBoolVar());
117 }
118 std::vector<BoolVar> vertical_arcs;
119 for (int arc = 0; arc < 2 * num_vertical_arcs; ++arc) {
120 vertical_arcs.push_back(builder.NewBoolVar());
121 }
122
123 CircuitConstraint circuit = builder.AddCircuitConstraint();
124 // Horizontal arcs.
125 for (int x = 0; x < num_columns; ++x) {
126 for (int y = 0; y < num_rows + 1; ++y) {
127 const int arc = undirected_horizontal_arc(x, y);
128 circuit.AddArc(node_index(x, y), node_index(x + 1, y),
129 horizontal_arcs[2 * arc]);
130 circuit.AddArc(node_index(x + 1, y), node_index(x, y),
131 horizontal_arcs[2 * arc + 1]);
132 }
133 }
134 // Vertical arcs.
135 for (int x = 0; x < num_columns + 1; ++x) {
136 for (int y = 0; y < num_rows; ++y) {
137 const int arc = undirected_vertical_arc(x, y);
138 circuit.AddArc(node_index(x, y), node_index(x, y + 1),
139 vertical_arcs[2 * arc]);
140 circuit.AddArc(node_index(x, y + 1), node_index(x, y),
141 vertical_arcs[2 * arc + 1]);
142 }
143 }
144 // Self loops.
145 std::vector<BoolVar> self_nodes(num_nodes);
146 for (int x = 0; x < num_columns + 1; ++x) {
147 for (int y = 0; y < num_rows + 1; ++y) {
148 const int node = node_index(x, y);
149 const BoolVar self_node = builder.NewBoolVar();
150 circuit.AddArc(node, node, self_node);
151 self_nodes[node] = self_node;
152 }
153 }
154
155 for (int x = 0; x < num_columns; ++x) {
156 for (int y = 0; y < num_rows; ++y) {
157 if (data[y][x] == -1) continue;
158 std::vector<BoolVar> neighbors;
159 const int top_arc = undirected_horizontal_arc(x, y);
160 neighbors.push_back(horizontal_arcs[2 * top_arc]);
161 neighbors.push_back(horizontal_arcs[2 * top_arc + 1]);
162 const int bottom_arc = undirected_horizontal_arc(x, y + 1);
163 neighbors.push_back(horizontal_arcs[2 * bottom_arc]);
164 neighbors.push_back(horizontal_arcs[2 * bottom_arc + 1]);
165 const int left_arc = undirected_vertical_arc(x, y);
166 neighbors.push_back(vertical_arcs[2 * left_arc]);
167 neighbors.push_back(vertical_arcs[2 * left_arc + 1]);
168 const int right_arc = undirected_vertical_arc(x + 1, y);
169 neighbors.push_back(vertical_arcs[2 * right_arc]);
170 neighbors.push_back(vertical_arcs[2 * right_arc + 1]);
171 builder.AddEquality(LinearExpr::Sum(neighbors), data[y][x]);
172 }
173 }
174
175 // Special rule on corners: value == 3 implies 2 corner arcs used.
176 if (data[0][0] == 3) {
177 const int h_arc = undirected_horizontal_arc(0, 0);
178 builder.AddBoolOr(
179 {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]});
180 const int v_arc = undirected_vertical_arc(0, 0);
181 builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]});
182 }
183 if (data[0][num_columns - 1] == 3) {
184 const int h_arc = undirected_horizontal_arc(num_columns - 1, 0);
185 builder.AddBoolOr(
186 {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]});
187 const int v_arc = undirected_vertical_arc(num_columns, 0);
188 builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]});
189 }
190 if (data[num_rows - 1][0] == 3) {
191 const int h_arc = undirected_horizontal_arc(0, num_rows);
192 builder.AddBoolOr(
193 {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]});
194 const int v_arc = undirected_vertical_arc(0, num_rows - 1);
195 builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]});
196 }
197 if (data[num_rows - 1][num_columns - 1] == 3) {
198 const int h_arc = undirected_horizontal_arc(num_columns - 1, num_rows);
199 builder.AddBoolOr(
200 {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]});
201 const int v_arc = undirected_vertical_arc(num_columns, num_rows - 1);
202 builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]});
203 }
204
205 // Topology rule: Border arcs are oriented in one direction.
206 for (int x = 0; x < num_columns; ++x) {
207 const int top_arc = undirected_horizontal_arc(x, 0);
208 builder.AddEquality(horizontal_arcs[2 * top_arc + 1], 0);
209 const int bottom_arc = undirected_horizontal_arc(x, num_rows);
210 builder.AddEquality(horizontal_arcs[2 * bottom_arc], 0);
211 }
212
213 for (int y = 0; y < num_rows; ++y) {
214 const int left_arc = undirected_vertical_arc(0, y);
215 builder.AddEquality(vertical_arcs[2 * left_arc], 0);
216 const int right_arc = undirected_vertical_arc(num_columns, y);
217 builder.AddEquality(vertical_arcs[2 * right_arc + 1], 0);
218 }
219
220 const CpSolverResponse response = Solve(builder.Build());
221
222 std::vector<std::vector<bool> > h_arcs(num_rows + 1);
223 for (int y = 0; y < num_rows + 1; ++y) {
224 for (int x = 0; x < num_columns; ++x) {
225 const int arc = undirected_horizontal_arc(x, y);
226 h_arcs[y].push_back(
227 SolutionBooleanValue(response, horizontal_arcs[2 * arc]) ||
228 SolutionBooleanValue(response, horizontal_arcs[2 * arc + 1]));
229 }
230 }
231
232 std::vector<std::vector<bool> > v_arcs(num_columns + 1);
233 for (int y = 0; y < num_rows; ++y) {
234 for (int x = 0; x < num_columns + 1; ++x) {
235 const int arc = undirected_vertical_arc(x, y);
236 v_arcs[x].push_back(
237 SolutionBooleanValue(response, vertical_arcs[2 * arc]) ||
238 SolutionBooleanValue(response, vertical_arcs[2 * arc + 1]));
239 }
240 }
241
242 PrintSolution(data, h_arcs, v_arcs);
243 LOG(INFO) << CpSolverResponseStats(response);
244 }
245
246 } // namespace sat
247 } // namespace operations_research
248
main()249 int main() {
250 std::cout << "Tiny problem" << std::endl;
251 operations_research::sat::SlitherLink(tiny);
252 std::cout << "Small problem" << std::endl;
253 operations_research::sat::SlitherLink(small);
254 std::cout << "Medium problem" << std::endl;
255 operations_research::sat::SlitherLink(medium);
256 std::cout << "Big problem" << std::endl;
257 operations_research::sat::SlitherLink(big);
258 return EXIT_SUCCESS;
259 }
260