From 46a78c021dc6b5b500217f58c6d9fe435c19973e Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Sat, 24 Nov 2018 23:06:05 +0100 Subject: [PATCH] golomb -> golomb_sat --- examples/cpp/CMakeLists.txt | 4 +- examples/cpp/golomb.cc | 104 ----------------------------- examples/cpp/golomb_sat.cc | 129 ++++++++++++++++++++++++++++++++++++ makefiles/Makefile.cpp.mk | 2 +- 4 files changed, 132 insertions(+), 107 deletions(-) delete mode 100644 examples/cpp/golomb.cc create mode 100644 examples/cpp/golomb_sat.cc diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt index d0e72984a8..bec87afdc3 100644 --- a/examples/cpp/CMakeLists.txt +++ b/examples/cpp/CMakeLists.txt @@ -25,7 +25,7 @@ foreach(EXECUTABLE dobble_ls flow_api frequency_assignment_problem - golomb + golomb_sat integer_programming jobshop_sat knapsack @@ -68,7 +68,7 @@ foreach(TEST #dobble_ls # Too long flow_api #frequency_assignment_problem - golomb + golomb_sat integer_programming #jobshop_sat knapsack diff --git a/examples/cpp/golomb.cc b/examples/cpp/golomb.cc deleted file mode 100644 index d051852d89..0000000000 --- a/examples/cpp/golomb.cc +++ /dev/null @@ -1,104 +0,0 @@ -// 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. - -// -// Golomb ruler problem -// -// find minimal ruler so that the differences between ticks are unique. -// -// First solutions: -// 0, 1 -// 0, 1, 3 -// 0, 1, 4, 6 -// 0, 1, 4, 9, 11 -// 0, 1, 4, 10, 12, 17 -// 0, 1, 4, 10, 18, 23, 25 - -#include - -#include "ortools/base/commandlineflags.h" -#include "ortools/base/integral_types.h" -#include "ortools/base/logging.h" -#include "ortools/base/stringprintf.h" -#include "ortools/constraint_solver/constraint_solver.h" - -DEFINE_bool(print, false, "If true, print the minimal solution."); -DEFINE_int32( - size, 0, - "Size of the problem. If equal to 0, will test several increasing sizes."); - -static const int kBestSolutions[] = {0, 1, 3, 6, 11, 17, 25, 34, 44, 55, 72, 85, - // just for the optimistics ones, the rest: - 106, 127, 151, 177, 199, 216, 246}; - -static const int kKnownSolutions = 19; - -namespace operations_research { - -void GolombRuler(int size) { - CHECK_GE(size, 1); - Solver s("golomb"); - - // model - std::vector ticks(size); - ticks[0] = s.MakeIntConst(0); // X(0) = 0 - const int64 max = 1 + size * size * size; - for (int i = 1; i < size; ++i) { - ticks[i] = s.MakeIntVar(1, max, StringPrintf("X%02d", i)); - } - std::vector diffs; - for (int i = 0; i < size; ++i) { - for (int j = i + 1; j < size; ++j) { - IntVar* const diff = s.MakeDifference(ticks[j], ticks[i])->Var(); - diffs.push_back(diff); - diff->SetMin(1); - } - } - s.AddConstraint(s.MakeAllDifferent(diffs)); - - OptimizeVar* const length = s.MakeMinimize(ticks[size - 1], 1); - SolutionCollector* const collector = s.MakeLastSolutionCollector(); - collector->Add(ticks); - DecisionBuilder* const db = s.MakePhase(ticks, Solver::CHOOSE_FIRST_UNBOUND, - Solver::ASSIGN_MIN_VALUE); - s.Solve(db, collector, length); // go! - CHECK_EQ(collector->solution_count(), 1); - const int64 result = collector->Value(0, ticks[size - 1]); - const int num_failures = collector->failures(0); - printf("N = %d, optimal length = %d (fails:%d)\n", size, - static_cast(result), num_failures); - if (size - 1 < kKnownSolutions) { - CHECK_EQ(result, kBestSolutions[size - 1]); - } - if (FLAGS_print) { - for (int i = 0; i < size; ++i) { - const int64 tick = collector->Value(0, ticks[i]); - printf("%d ", static_cast(tick)); - } - printf("\n"); - } -} - -} // namespace operations_research - -int main(int argc, char** argv) { - gflags::ParseCommandLineFlags(&argc, &argv, true); - if (FLAGS_size != 0) { - operations_research::GolombRuler(FLAGS_size); - } else { - for (int n = 1; n < 11; ++n) { - operations_research::GolombRuler(n); - } - } - return EXIT_SUCCESS; -} diff --git a/examples/cpp/golomb_sat.cc b/examples/cpp/golomb_sat.cc new file mode 100644 index 0000000000..278575a80d --- /dev/null +++ b/examples/cpp/golomb_sat.cc @@ -0,0 +1,129 @@ +// 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. + +// +// Golomb ruler problem +// +// find minimal ruler so that the differences between ticks are unique. +// +// First solutions: +// 0, 1 +// 0, 1, 3 +// 0, 1, 4, 6 +// 0, 1, 4, 9, 11 +// 0, 1, 4, 10, 12, 17 +// 0, 1, 4, 10, 18, 23, 25 + +#include + +#include "google/protobuf/text_format.h" +#include "ortools/base/commandlineflags.h" +#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" +#include "ortools/base/stringprintf.h" +#include "ortools/sat/cp_model.h" +#include "ortools/sat/model.h" + +DEFINE_bool(print, false, "If true, print the minimal solution."); +DEFINE_int32( + size, 0, + "Size of the problem. If equal to 0, will test several increasing sizes."); +DEFINE_string(params, "", "Sat parameters."); + +static const int kBestSolutions[] = {0, 1, 3, 6, 11, 17, 25, 34, 44, 55, 72, 85, + // just for the optimistics ones, the rest: + 106, 127, 151, 177, 199, 216, 246}; + +static const int kKnownSolutions = 19; + +namespace operations_research { +namespace sat { + +void GolombRuler(int size) { + CHECK_GE(size, 1); + CpModelBuilder cp_model; + + std::vector ticks(size); + ticks[0] = cp_model.NewConstant(0); + const int64 max = size * size; + Domain domain(1, max); + for (int i = 1; i < size; ++i) { + ticks[i] = cp_model.NewIntVar(domain); + } + std::vector diffs; + for (int i = 0; i < size; ++i) { + for (int j = i + 1; j < size; ++j) { + const IntVar diff = cp_model.NewIntVar(domain); + cp_model.AddEquality(LinearExpr::Sum({diff, ticks[i]}), ticks[j]); + diffs.push_back(diff); + } + } + + cp_model.AddAllDifferent(diffs); + + // Symmetry breaking. + if (size > 2) { + cp_model.AddLessThan(diffs.front(), diffs.back()); + } + + // Objective. + cp_model.Minimize(ticks.back()); + + // Search strategy. + cp_model.AddDecisionStrategy(ticks, DecisionStrategyProto::CHOOSE_FIRST, + DecisionStrategyProto::SELECT_MIN_VALUE); + + Model model; + SatParameters parameters; + parameters.set_search_branching(SatParameters::FIXED_SEARCH); + // Parse the --params flag. + if (!FLAGS_params.empty()) { + CHECK(google::protobuf::TextFormat::MergeFromString(FLAGS_params, + ¶meters)) + << FLAGS_params; + } + model.Add(NewSatParameters(parameters)); + const CpSolverResponse response = SolveWithModel(cp_model, &model); + + if (response.status() == CpSolverStatus::OPTIMAL) { + const int64 result = SolutionIntegerValue(response, ticks.back()); + const int64 num_failures = response.num_conflicts(); + printf("N = %d, optimal length = %lld (conflicts:%lld, time=%f s)\n", size, result, + num_failures, response.wall_time()); + if (size - 1 < kKnownSolutions) { + CHECK_EQ(result, kBestSolutions[size - 1]); + } + if (FLAGS_print) { + for (int i = 0; i < size; ++i) { + const int64 tick = SolutionIntegerValue(response, ticks[i]); + printf("%d ", static_cast(tick)); + } + printf("\n"); + } + } +} + +} // namespace sat +} // namespace operations_research + +int main(int argc, char** argv) { + gflags::ParseCommandLineFlags(&argc, &argv, true); + if (FLAGS_size != 0) { + operations_research::sat::GolombRuler(FLAGS_size); + } else { + for (int n = 1; n < 11; ++n) { + operations_research::sat::GolombRuler(n); + } + } + return EXIT_SUCCESS; +} diff --git a/makefiles/Makefile.cpp.mk b/makefiles/Makefile.cpp.mk index d6f220fc7d..77397f2892 100755 --- a/makefiles/Makefile.cpp.mk +++ b/makefiles/Makefile.cpp.mk @@ -421,7 +421,7 @@ test_cc_cpp: \ SOURCE=examples/cpp/dimacs_assignment.cc \ ARGS=examples/data/dimacs/assignment/small.asn $(MAKE) run \ - SOURCE=examples/cpp/golomb.cc \ + SOURCE=examples/cpp/golomb_sat.cc \ ARGS="--size=5" $(MAKE) run \ SOURCE=examples/cpp/jobshop_sat.cc \