// Copyright 2010-2018 Google LLC // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at // // http://www.apache.org/licenses/LICENSE-2.0 // // Unless required by applicable law or agreed to in writing, software // distributed under the License is distributed on an "AS IS" BASIS, // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. // See the License for the specific language governing permissions and // limitations under the License. // Solve the Slitherlink problem: // see https://en.wikipedia.org/wiki/Slitherlink #include #include #include "absl/strings/str_format.h" #include "ortools/sat/cp_model.h" #include "ortools/sat/model.h" const std::vector> tiny = {{3, 3, 1}}; const std::vector> small = { {3, 2, -1, 3}, {-1, -1, -1, 2}, {3, -1, -1, -1}, {3, -1, 3, 1}}; const std::vector> medium = { {-1, 0, -1, 1, -1, -1, 1, -1}, {-1, 3, -1, -1, 2, 3, -1, 2}, {-1, -1, 0, -1, -1, -1, -1, 0}, {-1, 3, -1, -1, 0, -1, -1, -1}, {-1, -1, -1, 3, -1, -1, 0, -1}, {1, -1, -1, -1, -1, 3, -1, -1}, {3, -1, 1, 3, -1, -1, 3, -1}, {-1, 0, -1, -1, 3, -1, 3, -1}}; const std::vector> big = { {3, -1, -1, -1, 2, -1, 1, -1, 1, 2}, {1, -1, 0, -1, 3, -1, 2, 0, -1, -1}, {-1, 3, -1, -1, -1, -1, -1, -1, 3, -1}, {2, 0, -1, 3, -1, 2, 3, -1, -1, -1}, {-1, -1, -1, 1, 1, 1, -1, -1, 3, 3}, {2, 3, -1, -1, 2, 2, 3, -1, -1, -1}, {-1, -1, -1, 1, 2, -1, 2, -1, 3, 3}, {-1, 2, -1, -1, -1, -1, -1, -1, 2, -1}, {-1, -1, 1, 1, -1, 2, -1, 1, -1, 3}, {3, 3, -1, 1, -1, 2, -1, -1, -1, 2}}; namespace operations_research { namespace sat { void PrintSolution(const std::vector> &data, const std::vector> &h_arcs, const std::vector> &v_arcs) { const int num_rows = data.size(); const int num_columns = data[0].size(); for (int i = 0; i < num_rows; ++i) { std::string first_line; std::string second_line; std::string third_line; for (int j = 0; j < num_columns; ++j) { const bool h_arc = h_arcs[i][j]; const bool v_arc = v_arcs[j][i]; const int sum = data[i][j]; first_line += h_arc ? " -----" : " "; second_line += v_arc ? "|" : " "; second_line += sum == -1 ? " " : absl::StrFormat(" %d ", sum).c_str(); third_line += v_arc ? "| " : " "; } const bool termination = v_arcs[num_columns][i]; second_line += termination == 1 ? "|" : " "; third_line += termination == 1 ? "|" : " "; std::cout << first_line << std::endl; std::cout << third_line << std::endl; std::cout << second_line << std::endl; std::cout << third_line << std::endl; } std::string last_line; for (int j = 0; j < num_columns; ++j) { const bool h_arc = h_arcs[num_rows][j]; last_line += h_arc ? " -----" : " "; } std::cout << last_line << std::endl; } void SlitherLink(const std::vector> &data) { const int num_rows = data.size(); const int num_columns = data[0].size(); const int num_nodes = (num_rows + 1) * (num_columns + 1); const int num_horizontal_arcs = num_columns * (num_rows + 1); const int num_vertical_arcs = (num_rows) * (num_columns + 1); auto undirected_horizontal_arc = [=](int x, int y) { CHECK_LT(x, num_columns); CHECK_LT(y, num_rows + 1); return x + (num_columns * y); }; auto undirected_vertical_arc = [=](int x, int y) { CHECK_LT(x, num_columns + 1); CHECK_LT(y, num_rows); return x + (num_columns + 1) * y; }; auto node_index = [=](int x, int y) { CHECK_LT(x, num_columns + 1); CHECK_LT(y, num_rows + 1); return x + y * (num_columns + 1); }; CpModelBuilder builder; std::vector horizontal_arcs; for (int arc = 0; arc < 2 * num_horizontal_arcs; ++arc) { horizontal_arcs.push_back(builder.NewBoolVar()); } std::vector vertical_arcs; for (int arc = 0; arc < 2 * num_vertical_arcs; ++arc) { vertical_arcs.push_back(builder.NewBoolVar()); } CircuitConstraint circuit = builder.AddCircuitConstraint(); // Horizontal arcs. for (int x = 0; x < num_columns; ++x) { for (int y = 0; y < num_rows + 1; ++y) { const int arc = undirected_horizontal_arc(x, y); circuit.AddArc(node_index(x, y), node_index(x + 1, y), horizontal_arcs[2 * arc]); circuit.AddArc(node_index(x + 1, y), node_index(x, y), horizontal_arcs[2 * arc + 1]); } } // Vertical arcs. for (int x = 0; x < num_columns + 1; ++x) { for (int y = 0; y < num_rows; ++y) { const int arc = undirected_vertical_arc(x, y); circuit.AddArc(node_index(x, y), node_index(x, y + 1), vertical_arcs[2 * arc]); circuit.AddArc(node_index(x, y + 1), node_index(x, y), vertical_arcs[2 * arc + 1]); } } // Self loops. std::vector self_nodes(num_nodes); for (int x = 0; x < num_columns + 1; ++x) { for (int y = 0; y < num_rows + 1; ++y) { const int node = node_index(x, y); const BoolVar self_node = builder.NewBoolVar(); circuit.AddArc(node, node, self_node); self_nodes[node] = self_node; } } for (int x = 0; x < num_columns; ++x) { for (int y = 0; y < num_rows; ++y) { if (data[y][x] == -1) continue; std::vector neighbors; const int top_arc = undirected_horizontal_arc(x, y); neighbors.push_back(horizontal_arcs[2 * top_arc]); neighbors.push_back(horizontal_arcs[2 * top_arc + 1]); const int bottom_arc = undirected_horizontal_arc(x, y + 1); neighbors.push_back(horizontal_arcs[2 * bottom_arc]); neighbors.push_back(horizontal_arcs[2 * bottom_arc + 1]); const int left_arc = undirected_vertical_arc(x, y); neighbors.push_back(vertical_arcs[2 * left_arc]); neighbors.push_back(vertical_arcs[2 * left_arc + 1]); const int right_arc = undirected_vertical_arc(x + 1, y); neighbors.push_back(vertical_arcs[2 * right_arc]); neighbors.push_back(vertical_arcs[2 * right_arc + 1]); builder.AddEquality(LinearExpr::BooleanSum(neighbors), data[y][x]); } } // Special rule on corners: value == 3 implies 2 corner arcs used. if (data[0][0] == 3) { const int h_arc = undirected_horizontal_arc(0, 0); builder.AddBoolOr( {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]}); const int v_arc = undirected_vertical_arc(0, 0); builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]}); } if (data[0][num_columns - 1] == 3) { const int h_arc = undirected_horizontal_arc(num_columns - 1, 0); builder.AddBoolOr( {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]}); const int v_arc = undirected_vertical_arc(num_columns, 0); builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]}); } if (data[num_rows - 1][0] == 3) { const int h_arc = undirected_horizontal_arc(0, num_rows); builder.AddBoolOr( {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]}); const int v_arc = undirected_vertical_arc(0, num_rows - 1); builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]}); } if (data[num_rows - 1][num_columns - 1] == 3) { const int h_arc = undirected_horizontal_arc(num_columns - 1, num_rows); builder.AddBoolOr( {horizontal_arcs[2 * h_arc], horizontal_arcs[2 * h_arc + 1]}); const int v_arc = undirected_vertical_arc(num_columns, num_rows - 1); builder.AddBoolOr({vertical_arcs[2 * v_arc], vertical_arcs[2 * v_arc + 1]}); } // Topology rule: Border arcs are oriented in one direction. for (int x = 0; x < num_columns; ++x) { const int top_arc = undirected_horizontal_arc(x, 0); builder.AddEquality(horizontal_arcs[2 * top_arc + 1], 0); const int bottom_arc = undirected_horizontal_arc(x, num_rows); builder.AddEquality(horizontal_arcs[2 * bottom_arc], 0); } for (int y = 0; y < num_rows; ++y) { const int left_arc = undirected_vertical_arc(0, y); builder.AddEquality(vertical_arcs[2 * left_arc], 0); const int right_arc = undirected_vertical_arc(num_columns, y); builder.AddEquality(vertical_arcs[2 * right_arc + 1], 0); } const CpSolverResponse response = Solve(builder.Build()); std::vector> h_arcs(num_rows + 1); for (int y = 0; y < num_rows + 1; ++y) { for (int x = 0; x < num_columns; ++x) { const int arc = undirected_horizontal_arc(x, y); h_arcs[y].push_back( SolutionBooleanValue(response, horizontal_arcs[2 * arc]) || SolutionBooleanValue(response, horizontal_arcs[2 * arc + 1])); } } std::vector> v_arcs(num_columns + 1); for (int y = 0; y < num_rows; ++y) { for (int x = 0; x < num_columns + 1; ++x) { const int arc = undirected_vertical_arc(x, y); v_arcs[x].push_back( SolutionBooleanValue(response, vertical_arcs[2 * arc]) || SolutionBooleanValue(response, vertical_arcs[2 * arc + 1])); } } PrintSolution(data, h_arcs, v_arcs); LOG(INFO) << CpSolverResponseStats(response); } } // namespace sat } // namespace operations_research int main() { std::cout << "Tiny problem" << std::endl; operations_research::sat::SlitherLink(tiny); std::cout << "Small problem" << std::endl; operations_research::sat::SlitherLink(small); std::cout << "Medium problem" << std::endl; operations_research::sat::SlitherLink(medium); std::cout << "Big problem" << std::endl; operations_research::sat::SlitherLink(big); return EXIT_SUCCESS; }