From ca579c649f8fa841f36b048ba6a55bddbcd7bac1 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 30 May 2018 10:03:49 -0700 Subject: [PATCH] add code samples in C++ for sat --- examples/cpp/code_samples_sat.cc | 145 +++++++++++++++++++++++++++++++ makefiles/Makefile.cpp.mk | 6 ++ 2 files changed, 151 insertions(+) create mode 100644 examples/cpp/code_samples_sat.cc diff --git a/examples/cpp/code_samples_sat.cc b/examples/cpp/code_samples_sat.cc new file mode 100644 index 0000000000..1412465900 --- /dev/null +++ b/examples/cpp/code_samples_sat.cc @@ -0,0 +1,145 @@ +// Copyright 2010-2017 Google +// 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. + +#include "ortools/base/commandlineflags.h" +#include "ortools/base/logging.h" +#include "ortools/base/timer.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/sat/cp_model_utils.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_parameters.pb.h" + +namespace operations_research { +namespace sat { +void MinimalSatPrintIntermediateSolutions() { + + CpModelProto cp_model; + + auto new_variable = [&cp_model](int64 lb, int64 ub) { + CHECK_LE(lb, ub); + const int index = cp_model.variables_size(); + IntegerVariableProto* const var = cp_model.add_variables(); + var->add_domain(lb); + var->add_domain(ub); + return index; + }; + + auto add_different = [&cp_model](const int left_var, const int right_var) { + LinearConstraintProto* const lin = + cp_model.add_constraints()->mutable_linear(); + lin->add_vars(left_var); + lin->add_coeffs(1); + lin->add_vars(right_var); + lin->add_coeffs(-1); + lin->add_domain(kint64min); + lin->add_domain(-1); + lin->add_domain(1); + lin->add_domain(kint64max); + }; + + auto maximize = [&cp_model](const std::vector& vars, + const std::vector& coeffs) { + CpObjectiveProto* const obj = cp_model.mutable_objective(); + for (const int v : vars) { + obj->add_vars(v); + } + for (const int64 c : coeffs) { + obj->add_coeffs(-c); // Maximize. + } + obj->set_scaling_factor(-1.0); // Maximize. + }; + + const int kNumVals = 3; + const int x = new_variable(0, kNumVals - 1); + const int y = new_variable(0, kNumVals - 1); + const int z = new_variable(0, kNumVals - 1); + + add_different(x, y); + + maximize({x, y, z}, {1, 2, 3}); + + + Model model; + int num_solutions = 0; + model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) { + LOG(INFO) << "Solution " << num_solutions; + LOG(INFO) << " objective value = " << r.objective_value(); + LOG(INFO) << " x = " << r.solution(x); + LOG(INFO) << " y = " << r.solution(y); + LOG(INFO) << " z = " << r.solution(z); + num_solutions++; + })); + const CpSolverResponse response = SolveCpModel(cp_model, &model); + LOG(INFO) << "Number of solutions found: " << num_solutions; +} + +void MinimalSatSearchForAllSolutions() { + CpModelProto cp_model; + + auto new_variable = [&cp_model](int64 lb, int64 ub) { + CHECK_LE(lb, ub); + const int index = cp_model.variables_size(); + IntegerVariableProto* const var = cp_model.add_variables(); + var->add_domain(lb); + var->add_domain(ub); + return index; + }; + + auto add_different = [&cp_model](const int left_var, const int right_var) { + LinearConstraintProto* const lin = + cp_model.add_constraints()->mutable_linear(); + lin->add_vars(left_var); + lin->add_coeffs(1); + lin->add_vars(right_var); + lin->add_coeffs(-1); + lin->add_domain(kint64min); + lin->add_domain(-1); + lin->add_domain(1); + lin->add_domain(kint64max); + }; + + const int kNumVals = 3; + const int x = new_variable(0, kNumVals - 1); + const int y = new_variable(0, kNumVals - 1); + const int z = new_variable(0, kNumVals - 1); + + add_different(x, y); + + Model model; + + // Tell the solver to enumerate all solutions. + SatParameters parameters; + parameters.set_enumerate_all_solutions(true); + model.Add(NewSatParameters(parameters)); + + int num_solutions = 0; + model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) { + LOG(INFO) << "Solution " << num_solutions; + LOG(INFO) << " x = " << r.solution(x); + LOG(INFO) << " y = " << r.solution(y); + LOG(INFO) << " z = " << r.solution(z); + num_solutions++; + })); + const CpSolverResponse response = SolveCpModel(cp_model, &model); + LOG(INFO) << "Number of solutions found: " << num_solutions; +} + +} // namespace sat +} // namespace operations_research + +int main(int argc, char** argv) { + operations_research::sat::MinimalSatPrintIntermediateSolutions(); + operations_research::sat::MinimalSatSearchForAllSolutions(); + return EXIT_SUCCESS; +} diff --git a/makefiles/Makefile.cpp.mk b/makefiles/Makefile.cpp.mk index e88bc479c8..b9903ac780 100755 --- a/makefiles/Makefile.cpp.mk +++ b/makefiles/Makefile.cpp.mk @@ -495,6 +495,12 @@ $(OBJ_DIR)/costas_array.$O: $(EX_DIR)/cpp/costas_array.cc $(SRC_DIR)/ortools/con $(BIN_DIR)/costas_array$E: $(OR_TOOLS_LIBS) $(OBJ_DIR)/costas_array.$O $(CCC) $(CFLAGS) $(OBJ_DIR)/costas_array.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LDFLAGS) $(EXE_OUT)$(BIN_DIR)$Scostas_array$E +$(OBJ_DIR)/code_samples_sat.$O: $(EX_DIR)/cpp/code_samples_sat.cc $(SAT_DEPS) + $(CCC) $(CFLAGS) -c $(EX_DIR)$Scpp/code_samples_sat.cc $(OBJ_OUT)$(OBJ_DIR)$Scode_samples_sat.$O + +$(BIN_DIR)/code_samples_sat$E: $(OR_TOOLS_LIBS) $(OBJ_DIR)/code_samples_sat.$O + $(CCC) $(CFLAGS) $(OBJ_DIR)/code_samples_sat.$O $(OR_TOOLS_LNK) $(OR_TOOLS_LDFLAGS) $(EXE_OUT)$(BIN_DIR)$Scode_samples_sat$E + $(OBJ_DIR)/cryptarithm.$O: $(EX_DIR)/cpp/cryptarithm.cc $(SRC_DIR)/ortools/constraint_solver/constraint_solver.h $(CCC) $(CFLAGS) -c $(EX_DIR)$Scpp/cryptarithm.cc $(OBJ_OUT)$(OBJ_DIR)$Scryptarithm.$O