From 0152168fb7ca3733caaa451b6ea6be49d41e1718 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 17 Jul 2018 14:00:18 -0700 Subject: [PATCH] add C# sat code samples in ortools/sat/samples; remove old code_samples_sat.* files --- examples/cpp/code_samples_sat.cc | 575 ------------------ .../dotnet/csharp-netfx/code_samples_sat.cs | 404 ------------ ortools/sat/samples/binpacking_problem.cc | 5 +- ortools/sat/samples/binpacking_problem.cs | 128 ++++ ortools/sat/samples/binpacking_problem.py | 4 +- ortools/sat/samples/bool_or_sample.cc | 1 - ortools/sat/samples/bool_or_sample.cs | 30 + ortools/sat/samples/code_sample.cc | 1 - ortools/sat/samples/code_sample.cs | 31 + ortools/sat/samples/interval_sample.cc | 5 +- ortools/sat/samples/interval_sample.cs | 35 ++ ortools/sat/samples/literal_sample.cc | 1 - ortools/sat/samples/literal_sample.cs | 29 + .../sat/samples/optional_interval_sample.cc | 5 +- .../sat/samples/optional_interval_sample.cs | 36 ++ ortools/sat/samples/rabbits_and_pheasants.cc | 1 - ortools/sat/samples/rabbits_and_pheasants.cs | 46 ++ ortools/sat/samples/reified_sample.cc | 1 - ortools/sat/samples/reified_sample.cs | 42 ++ ortools/sat/samples/simple_solve.cc | 1 - ortools/sat/samples/simple_solve.cs | 48 ++ ortools/sat/samples/solve_all_solutions.cs | 77 +++ .../solve_with_intermediate_solutions.cc | 1 - .../solve_with_intermediate_solutions.cs | 81 +++ ortools/sat/samples/solve_with_time_limit.cs | 52 ++ 25 files changed, 641 insertions(+), 999 deletions(-) delete mode 100644 examples/cpp/code_samples_sat.cc delete mode 100644 examples/dotnet/csharp-netfx/code_samples_sat.cs create mode 100644 ortools/sat/samples/binpacking_problem.cs create mode 100644 ortools/sat/samples/bool_or_sample.cs create mode 100644 ortools/sat/samples/code_sample.cs create mode 100644 ortools/sat/samples/interval_sample.cs create mode 100644 ortools/sat/samples/literal_sample.cs create mode 100644 ortools/sat/samples/optional_interval_sample.cs create mode 100644 ortools/sat/samples/rabbits_and_pheasants.cs create mode 100644 ortools/sat/samples/reified_sample.cs create mode 100644 ortools/sat/samples/simple_solve.cs create mode 100644 ortools/sat/samples/solve_all_solutions.cs create mode 100644 ortools/sat/samples/solve_with_intermediate_solutions.cs create mode 100644 ortools/sat/samples/solve_with_time_limit.cs diff --git a/examples/cpp/code_samples_sat.cc b/examples/cpp/code_samples_sat.cc deleted file mode 100644 index d6d4635bbb..0000000000 --- a/examples/cpp/code_samples_sat.cc +++ /dev/null @@ -1,575 +0,0 @@ -// 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 CodeSample() { - CpModelProto cp_model; - - auto new_boolean_variable = [&cp_model]() { - const int index = cp_model.variables_size(); - IntegerVariableProto* const var = cp_model.add_variables(); - var->add_domain(0); - var->add_domain(1); - return index; - }; - - const int x = new_boolean_variable(); - LOG(INFO) << x; -} - -void LiteralSample() { - CpModelProto cp_model; - - auto new_boolean_variable = [&cp_model]() { - const int index = cp_model.variables_size(); - IntegerVariableProto* const var = cp_model.add_variables(); - var->add_domain(0); - var->add_domain(1); - return index; - }; - - const int x = new_boolean_variable(); - const int not_x = NegatedRef(x); - LOG(INFO) << "x = " << x << ", not(x) = " << not_x; -} - -void BoolOrSample() { - CpModelProto cp_model; - - auto new_boolean_variable = [&cp_model]() { - const int index = cp_model.variables_size(); - IntegerVariableProto* const var = cp_model.add_variables(); - var->add_domain(0); - var->add_domain(1); - return index; - }; - - auto add_bool_or = [&cp_model](const std::vector& literals) { - BoolArgumentProto* const bool_or = - cp_model.add_constraints()->mutable_bool_or(); - for (const int lit : literals) { - bool_or->add_literals(lit); - } - }; - - const int x = new_boolean_variable(); - const int y = new_boolean_variable(); - add_bool_or({x, NegatedRef(y)}); -} - -void ReifiedSample() { - CpModelProto cp_model; - - auto new_boolean_variable = [&cp_model]() { - const int index = cp_model.variables_size(); - IntegerVariableProto* const var = cp_model.add_variables(); - var->add_domain(0); - var->add_domain(1); - return index; - }; - - auto add_bool_or = [&cp_model](const std::vector& literals) { - BoolArgumentProto* const bool_or = - cp_model.add_constraints()->mutable_bool_or(); - for (const int lit : literals) { - bool_or->add_literals(lit); - } - }; - - auto add_reified_bool_and = [&cp_model](const std::vector& literals, - const int literal) { - ConstraintProto* const ct = cp_model.add_constraints(); - ct->add_enforcement_literal(literal); - for (const int lit : literals) { - ct->mutable_bool_and()->add_literals(lit); - } - }; - - const int x = new_boolean_variable(); - const int y = new_boolean_variable(); - const int b = new_boolean_variable(); - - // First version using a half-reified bool and. - add_reified_bool_and({x, NegatedRef(y)}, b); - - // Second version using bool or. - add_bool_or({NegatedRef(b), x}); - add_bool_or({NegatedRef(b), NegatedRef(y)}); -} - -void RabbitsAndPheasants() { - CpModelProto cp_model; - - // Trivial model with just one variable and no constraint. - 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_linear_constraint = [&cp_model](const std::vector& vars, - const std::vector& coeffs, - int64 lb, int64 ub) { - LinearConstraintProto* const lin = - cp_model.add_constraints()->mutable_linear(); - for (const int v : vars) { - lin->add_vars(v); - } - for (const int64 c : coeffs) { - lin->add_coeffs(c); - } - lin->add_domain(lb); - lin->add_domain(ub); - }; - - // Creates variables. - const int r = new_variable(0, 100); - const int p = new_variable(0, 100); - - // 20 heads. - add_linear_constraint({r, p}, {1, 1}, 20, 20); - // 56 legs. - add_linear_constraint({r, p}, {4, 2}, 56, 56); - - // Solving part. - Model model; - LOG(INFO) << CpModelStats(cp_model); - const CpSolverResponse response = SolveCpModel(cp_model, &model); - LOG(INFO) << CpSolverResponseStats(response); - - if (response.status() == CpSolverStatus::FEASIBLE) { - // Get the value of x in the solution. - LOG(INFO) << response.solution(r) << " rabbits, and " - << response.solution(p) << " pheasants"; - } -} - -void BinpackingProblem() { - // Data. - const int kBinCapacity = 100; - const int kSlackCapacity = 20; - const int kNumBins = 10; - - const std::vector> items = { - {20, 12}, {15, 12}, {30, 8}, {45, 5}}; - const int num_items = items.size(); - - // Model. - CpModelProto cp_model; - - // Helpers. - 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_linear_constraint = [&cp_model](const std::vector& vars, - const std::vector& coeffs, - int64 lb, int64 ub) { - LinearConstraintProto* const lin = - cp_model.add_constraints()->mutable_linear(); - for (const int v : vars) { - lin->add_vars(v); - } - for (const int64 c : coeffs) { - lin->add_coeffs(c); - } - lin->add_domain(lb); - lin->add_domain(ub); - }; - - auto add_reified_variable_bounds = [&cp_model](int var, int64 lb, int64 ub, - int lit) { - ConstraintProto* const ct = cp_model.add_constraints(); - ct->add_enforcement_literal(lit); - LinearConstraintProto* const lin = ct->mutable_linear(); - lin->add_vars(var); - lin->add_coeffs(1); - lin->add_domain(lb); - lin->add_domain(ub); - }; - - auto maximize = [&cp_model](const std::vector& vars) { - CpObjectiveProto* const obj = cp_model.mutable_objective(); - for (const int v : vars) { - obj->add_vars(v); - obj->add_coeffs(-1); // Maximize. - } - obj->set_scaling_factor(-1.0); // Maximize. - }; - - // Main variables. - std::vector> x(num_items); - for (int i = 0; i < num_items; ++i) { - const int num_copies = items[i][1]; - for (int b = 0; b < kNumBins; ++b) { - x[i].push_back(new_variable(0, num_copies)); - } - } - - // Load variables. - std::vector load(kNumBins); - for (int b = 0; b < kNumBins; ++b) { - load[b] = new_variable(0, kBinCapacity); - } - - // Slack variables. - std::vector slack(kNumBins); - for (int b = 0; b < kNumBins; ++b) { - slack[b] = new_variable(0, 1); - } - - // Links load and x. - for (int b = 0; b < kNumBins; ++b) { - std::vector vars; - std::vector coeffs; - vars.push_back(load[b]); - coeffs.push_back(-1); - for (int i = 0; i < num_items; ++i) { - vars.push_back(x[i][b]); - coeffs.push_back(items[i][0]); - } - add_linear_constraint(vars, coeffs, 0, 0); - } - - // Place all items. - for (int i = 0; i < num_items; ++i) { - std::vector vars; - std::vector coeffs; - for (int b = 0; b < kNumBins; ++b) { - vars.push_back(x[i][b]); - coeffs.push_back(1); - } - add_linear_constraint(vars, coeffs, items[i][1], items[i][1]); - } - - // Links load and slack through an equivalence relation. - const int safe_capacity = kBinCapacity - kSlackCapacity; - for (int b = 0; b < kNumBins; ++b) { - // slack[b] => load[b] <= safe_capacity. - add_reified_variable_bounds(load[b], kint64min, safe_capacity, slack[b]); - // not(slack[b]) => load[b] > safe_capacity. - add_reified_variable_bounds(load[b], safe_capacity + 1, kint64max, - NegatedRef(slack[b])); - } - - // Maximize sum of slacks. - maximize(slack); - - // Solving part. - Model model; - LOG(INFO) << CpModelStats(cp_model); - const CpSolverResponse response = SolveCpModel(cp_model, &model); - LOG(INFO) << CpSolverResponseStats(response); -} - -void IntervalSample() { - CpModelProto cp_model; - const int kHorizon = 100; - - 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 new_constant = [&cp_model, &new_variable](int64 v) { - return new_variable(v, v); - }; - - auto new_interval = [&cp_model](int start, int duration, int end) { - const int index = cp_model.constraints_size(); - IntervalConstraintProto* const interval = - cp_model.add_constraints()->mutable_interval(); - interval->set_start(start); - interval->set_size(duration); - interval->set_end(end); - return index; - }; - - const int start_var = new_variable(0, kHorizon); - const int duration_var = new_constant(10); - const int end_var = new_variable(0, kHorizon); - const int interval_var = new_interval(start_var, duration_var, end_var); - LOG(INFO) << "start_var = " << start_var - << ", duration_var = " << duration_var << ", end_var = " << end_var - << ", interval_var = " << interval_var; -} - -void OptionalIntervalSample() { - CpModelProto cp_model; - const int kHorizon = 100; - - 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 new_constant = [&cp_model, &new_variable](int64 v) { - return new_variable(v, v); - }; - - auto new_optional_interval = [&cp_model](int start, int duration, int end, - int presence) { - const int index = cp_model.constraints_size(); - ConstraintProto* const ct = cp_model.add_constraints(); - ct->add_enforcement_literal(presence); - IntervalConstraintProto* const interval = ct->mutable_interval(); - interval->set_start(start); - interval->set_size(duration); - interval->set_end(end); - return index; - }; - - const int start_var = new_variable(0, kHorizon); - const int duration_var = new_constant(10); - const int end_var = new_variable(0, kHorizon); - const int presence_var = new_variable(0, 1); - const int interval_var = - new_optional_interval(start_var, duration_var, end_var, presence_var); - LOG(INFO) << "start_var = " << start_var - << ", duration_var = " << duration_var << ", end_var = " << end_var - << ", presence_var = " << presence_var - << ", interval_var = " << interval_var; -} - -void SimpleSolve() { - CpModelProto cp_model; - - // Trivial model with just one variable and no constraint. - 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; - }; - - const int x = new_variable(0, 3); - - // Solving part. - Model model; - LOG(INFO) << CpModelStats(cp_model); - const CpSolverResponse response = SolveCpModel(cp_model, &model); - LOG(INFO) << CpSolverResponseStats(response); - - if (response.status() == CpSolverStatus::FEASIBLE) { - // Get the value of x in the solution. - const int64 value_x = response.solution(x); - LOG(INFO) << "x = " << value_x; - } -} - -void SolveWithTimeLimit() { - CpModelProto cp_model; - - // Trivial model with just one variable and no constraint. - 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; - }; - - const int x = new_variable(0, 3); - - // Solving part. - Model model; - - // Sets a time limit of 10 seconds. - SatParameters parameters; - parameters.set_max_time_in_seconds(10.0); - model.Add(NewSatParameters(parameters)); - - // Solve. - LOG(INFO) << CpModelStats(cp_model); - const CpSolverResponse response = SolveCpModel(cp_model, &model); - LOG(INFO) << CpSolverResponseStats(response); - - if (response.status() == CpSolverStatus::FEASIBLE) { - // Get the value of x in the solution. - const int64 value_x = response.solution(x); - LOG(INFO) << "value_x = " << value_x; - } -} - -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() { - LOG(INFO) << "--- CodeSample ---"; - operations_research::sat::CodeSample(); - LOG(INFO) << "--- LiteralSample ---"; - operations_research::sat::LiteralSample(); - LOG(INFO) << "--- BoolOrSample ---"; - operations_research::sat::BoolOrSample(); - LOG(INFO) << "--- ReifiedSample ---"; - operations_research::sat::ReifiedSample(); - LOG(INFO) << "--- RabbitsAndPheasants ---"; - operations_research::sat::RabbitsAndPheasants(); - LOG(INFO) << "--- BinpackingProblem ---"; - operations_research::sat::BinpackingProblem(); - LOG(INFO) << "--- IntervalSample ---"; - operations_research::sat::IntervalSample(); - LOG(INFO) << "--- OptionalIntervalSample ---"; - operations_research::sat::OptionalIntervalSample(); - LOG(INFO) << "--- SimpleSolve ---"; - operations_research::sat::SimpleSolve(); - LOG(INFO) << "--- SolveWithTimeLimit ---"; - operations_research::sat::SolveWithTimeLimit(); - LOG(INFO) << "--- MinimalSatPrintIntermediateSolutions ---"; - operations_research::sat::MinimalSatPrintIntermediateSolutions(); - LOG(INFO) << "--- MinimalSatSearchForAllSolutions ---"; - operations_research::sat::MinimalSatSearchForAllSolutions(); - - return EXIT_SUCCESS; -} diff --git a/examples/dotnet/csharp-netfx/code_samples_sat.cs b/examples/dotnet/csharp-netfx/code_samples_sat.cs deleted file mode 100644 index a9f4be6838..0000000000 --- a/examples/dotnet/csharp-netfx/code_samples_sat.cs +++ /dev/null @@ -1,404 +0,0 @@ -// 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. - -using System; -using Google.OrTools.Sat; - -public class VarArraySolutionPrinter : CpSolverSolutionCallback -{ - public VarArraySolutionPrinter(IntVar[] variables) - { - variables_ = variables; - } - - public override void OnSolutionCallback() - { - { - Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", - solution_count_, WallTime())); - foreach (IntVar v in variables_) - { - Console.WriteLine( - String.Format(" {0} = {1}", v.ShortString(), Value(v))); - } - solution_count_++; - } - } - - public int SolutionCount() - { - return solution_count_; - } - - private int solution_count_; - private IntVar[] variables_; -} - -public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback -{ - public VarArraySolutionPrinterWithObjective(IntVar[] variables) - { - variables_ = variables; - } - - public override void OnSolutionCallback() - { - { - Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", - solution_count_, WallTime())); - Console.WriteLine( - String.Format(" objective value = {0}", ObjectiveValue())); - foreach (IntVar v in variables_) - { - Console.WriteLine( - String.Format(" {0} = {1}", v.ShortString(), Value(v))); - } - solution_count_++; - } - } - - public int SolutionCount() - { - return solution_count_; - } - - private int solution_count_; - private IntVar[] variables_; -} - - -public class CodeSamplesSat -{ - static void CodeSample() - { - // Creates the model. - CpModel model = new CpModel(); - // Creates the Boolean variable. - IntVar x = model.NewBoolVar("x"); - } - - static void LiteralSample() - { - CpModel model = new CpModel(); - IntVar x = model.NewBoolVar("x"); - ILiteral not_x = x.Not(); - } - - static void BoolOrSample() - { - CpModel model = new CpModel(); - IntVar x = model.NewBoolVar("x"); - IntVar y = model.NewBoolVar("y"); - model.AddBoolOr(new ILiteral[] {x, y.Not()}); - } - - static void ReifiedSample() - { - CpModel model = new CpModel(); - - IntVar x = model.NewBoolVar("x"); - IntVar y = model.NewBoolVar("y"); - IntVar b = model.NewBoolVar("b"); - - // First version using a half-reified bool and. - model.AddBoolAnd(new ILiteral[] {x, y.Not()}).OnlyEnforceIf(b); - - // Second version using implications. - model.AddImplication(b, x); - model.AddImplication(b, y.Not()); - - // Third version using bool or. - model.AddBoolOr(new ILiteral[] {b.Not(), x}); - model.AddBoolOr(new ILiteral[] {b.Not(), y.Not()}); - } - - static void RabbitsAndPheasants() - { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - IntVar r = model.NewIntVar(0, 100, "r"); - IntVar p = model.NewIntVar(0, 100, "p"); - // 20 heads. - model.Add(r + p == 20); - // 56 legs. - model.Add(4 * r + 2 * p == 56); - - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - CpSolverStatus status = solver.Solve(model); - - if (status == CpSolverStatus.Feasible) - { - Console.WriteLine(solver.Value(r) + " rabbits, and " + - solver.Value(p) + " pheasants"); - } - } - - static void BinpackingProblem() - { - // Data. - int bin_capacity = 100; - int slack_capacity = 20; - int num_bins = 10; - - int[,] items = new int[,] { {20, 12}, {15, 12}, {30, 8}, {45, 5} }; - int num_items = items.GetLength(0); - - // Model. - CpModel model = new CpModel(); - - // Main variables. - IntVar[,] x = new IntVar[num_items, num_bins]; - for (int i = 0; i < num_items; ++i) - { - int num_copies = items[i, 1]; - for (int b = 0; b < num_bins; ++b) - { - x[i, b] = model.NewIntVar(0, num_copies, String.Format("x_{0}_{1}", i, b)); - } - } - - // Load variables. - IntVar[] load = new IntVar[num_bins]; - for (int b = 0; b < num_bins; ++b) - { - load[b] = model.NewIntVar(0, bin_capacity, String.Format("load_{0}", b)); - } - - // Slack variables. - IntVar[] slacks = new IntVar[num_bins]; - for (int b = 0; b < num_bins; ++b) - { - slacks[b] = model.NewBoolVar(String.Format("slack_{0}", b)); - } - - // Links load and x. - int[] sizes = new int[num_items]; - for (int i = 0; i < num_items; ++i) { - sizes[i] = items[i, 0]; - } - for (int b = 0; b < num_bins; ++b) - { - IntVar[] tmp = new IntVar[num_items]; - for (int i = 0; i < num_items; ++i) - { - tmp[i] = x[i, b]; - } - model.Add(load[b] == tmp.ScalProd(sizes)); - } - - // Place all items. - for (int i = 0; i < num_items; ++i) - { - IntVar[] tmp = new IntVar[num_bins]; - for (int b = 0; b < num_bins; ++b) - { - tmp[b] = x[i, b]; - } - model.Add(tmp.Sum() == items[i, 1]); - } - - // Links load and slack. - int safe_capacity = bin_capacity - slack_capacity; - for (int b = 0; b < num_bins; ++b) - { - // slack[b] => load[b] <= safe_capacity. - model.Add(load[b] <= safe_capacity).OnlyEnforceIf(slacks[b]); - // not(slack[b]) => load[b] > safe_capacity. - model.Add(load[b] > safe_capacity).OnlyEnforceIf(slacks[b].Not()); - } - - // Maximize sum of slacks. - model.Maximize(slacks.Sum()); - - // Solves and prints out the solution. - CpSolver solver = new CpSolver(); - CpSolverStatus status = solver.Solve(model); - Console.WriteLine(String.Format("Solve status: {0}", status)); - if (status == CpSolverStatus.Optimal) { - Console.WriteLine(String.Format("Optimal objective value: {0}", - solver.ObjectiveValue)); - for (int b = 0; b < num_bins; ++b) - { - Console.WriteLine(String.Format("load_{0} = {1}", - b, solver.Value(load[b]))); - for (int i = 0; i < num_items; ++i) - { - Console.WriteLine(string.Format(" item_{0}_{1} = {2}", - i, b, solver.Value(x[i, b]))); - } - } - } - Console.WriteLine("Statistics"); - Console.WriteLine( - String.Format(" - conflicts : {0}", solver.NumConflicts())); - Console.WriteLine( - String.Format(" - branches : {0}", solver.NumBranches())); - Console.WriteLine( - String.Format(" - wall time : {0} s", solver.WallTime())); - } - - static void IntervalSample() - { - CpModel model = new CpModel(); - int horizon = 100; - IntVar start_var = model.NewIntVar(0, horizon, "start"); - // C# code supports IntVar or integer constants in intervals. - int duration = 10; - IntVar end_var = model.NewIntVar(0, horizon, "end"); - IntervalVar interval = - model.NewIntervalVar(start_var, duration, end_var, "interval"); - } - - static void OptionalIntervalSample() - { - CpModel model = new CpModel(); - int horizon = 100; - IntVar start_var = model.NewIntVar(0, horizon, "start"); - // C# code supports IntVar or integer constants in intervals. - int duration = 10; - IntVar end_var = model.NewIntVar(0, horizon, "end"); - IntVar presence_var = model.NewBoolVar("presence"); - IntervalVar interval = model.NewOptionalIntervalVar( - start_var, duration, end_var, presence_var, "interval"); - } - - static void MinimalCpSat() - { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; - - IntVar x = model.NewIntVar(0, num_vals - 1, "x"); - IntVar y = model.NewIntVar(0, num_vals - 1, "y"); - IntVar z = model.NewIntVar(0, num_vals - 1, "z"); - // Creates the constraints. - model.Add(x != y); - - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - CpSolverStatus status = solver.Solve(model); - - if (status == CpSolverStatus.Feasible) - { - Console.WriteLine("x = " + solver.Value(x)); - Console.WriteLine("y = " + solver.Value(y)); - Console.WriteLine("z = " + solver.Value(z)); - } - } - - static void MinimalCpSatWithTimeLimit() - { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; - - IntVar x = model.NewIntVar(0, num_vals - 1, "x"); - IntVar y = model.NewIntVar(0, num_vals - 1, "y"); - IntVar z = model.NewIntVar(0, num_vals - 1, "z"); - // Creates the constraints. - model.Add(x != y); - - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - - // Adds a time limit. Parameters are stored as strings in the solver. - solver.StringParameters = "max_time_in_seconds:10.0" ; - - CpSolverStatus status = solver.Solve(model); - - if (status == CpSolverStatus.Feasible) - { - Console.WriteLine("x = " + solver.Value(x)); - Console.WriteLine("y = " + solver.Value(y)); - Console.WriteLine("z = " + solver.Value(z)); - } - } - - static void MinimalCpSatPrintIntermediateSolutions() - { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; - - IntVar x = model.NewIntVar(0, num_vals - 1, "x"); - IntVar y = model.NewIntVar(0, num_vals - 1, "y"); - IntVar z = model.NewIntVar(0, num_vals - 1, "z"); - // Creates the constraints. - model.Add(x != y); - // Create the objective. - model.Maximize(x + 2 * y + 3 * z); - - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - VarArraySolutionPrinterWithObjective cb = - new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); - solver.SearchAllSolutions(model, cb); - Console.WriteLine(String.Format("Number of solutions found: {0}", - cb.SolutionCount())); - } - - static void MinimalCpSatAllSolutions() - { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; - - IntVar x = model.NewIntVar(0, num_vals - 1, "x"); - IntVar y = model.NewIntVar(0, num_vals - 1, "y"); - IntVar z = model.NewIntVar(0, num_vals - 1, "z"); - // Creates the constraints. - model.Add(x != y); - - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] {x, y, z}); - solver.SearchAllSolutions(model, cb); - Console.WriteLine(String.Format("Number of solutions found: {0}", - cb.SolutionCount())); - } - - static void Main() - { - Console.WriteLine("--- CodeSample ---"); - CodeSample(); - Console.WriteLine("--- LiteralSample ---"); - LiteralSample(); - Console.WriteLine("--- BoolOrSample ---"); - BoolOrSample(); - Console.WriteLine("--- ReifiedSample ---"); - ReifiedSample(); - Console.WriteLine("--- RabbitsAndPheasants ---"); - RabbitsAndPheasants(); - Console.WriteLine("--- BinpackingProblem ---"); - BinpackingProblem(); - Console.WriteLine("--- IntervalSample ---"); - IntervalSample(); - Console.WriteLine("--- OptionalIntervalSample ---"); - OptionalIntervalSample(); - Console.WriteLine("--- MinimalCpSat ---"); - MinimalCpSat(); - Console.WriteLine("--- MinimalCpSatWithTimeLimit ---"); - MinimalCpSatWithTimeLimit(); - Console.WriteLine("--- MinimalCpSatPrintIntermediateSolutions ---"); - MinimalCpSatPrintIntermediateSolutions(); - Console.WriteLine("--- MinimalCpSatAllSolutions ---"); - MinimalCpSatAllSolutions(); - } -} diff --git a/ortools/sat/samples/binpacking_problem.cc b/ortools/sat/samples/binpacking_problem.cc index 2df5309c75..2bdada3623 100644 --- a/ortools/sat/samples/binpacking_problem.cc +++ b/ortools/sat/samples/binpacking_problem.cc @@ -15,7 +15,6 @@ #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 { @@ -24,10 +23,10 @@ void BinpackingProblem() { // Data. const int kBinCapacity = 100; const int kSlackCapacity = 20; - const int kNumBins = 10; + const int kNumBins = 5; const std::vector> items = { - {20, 12}, {15, 12}, {30, 8}, {45, 5}}; + {20, 6}, {15, 6}, {30, 4}, {45, 3}}; const int num_items = items.size(); // Model. diff --git a/ortools/sat/samples/binpacking_problem.cs b/ortools/sat/samples/binpacking_problem.cs new file mode 100644 index 0000000000..34ef511e76 --- /dev/null +++ b/ortools/sat/samples/binpacking_problem.cs @@ -0,0 +1,128 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void BinpackingProblem() + { + // Data. + int bin_capacity = 100; + int slack_capacity = 20; + int num_bins = 10; + + int[,] items = new int[,] { {20, 12}, {15, 12}, {30, 8}, {45, 5} }; + int num_items = items.GetLength(0); + + // Model. + CpModel model = new CpModel(); + + // Main variables. + IntVar[,] x = new IntVar[num_items, num_bins]; + for (int i = 0; i < num_items; ++i) + { + int num_copies = items[i, 1]; + for (int b = 0; b < num_bins; ++b) + { + x[i, b] = model.NewIntVar(0, num_copies, String.Format("x_{0}_{1}", i, b)); + } + } + + // Load variables. + IntVar[] load = new IntVar[num_bins]; + for (int b = 0; b < num_bins; ++b) + { + load[b] = model.NewIntVar(0, bin_capacity, String.Format("load_{0}", b)); + } + + // Slack variables. + IntVar[] slacks = new IntVar[num_bins]; + for (int b = 0; b < num_bins; ++b) + { + slacks[b] = model.NewBoolVar(String.Format("slack_{0}", b)); + } + + // Links load and x. + int[] sizes = new int[num_items]; + for (int i = 0; i < num_items; ++i) { + sizes[i] = items[i, 0]; + } + for (int b = 0; b < num_bins; ++b) + { + IntVar[] tmp = new IntVar[num_items]; + for (int i = 0; i < num_items; ++i) + { + tmp[i] = x[i, b]; + } + model.Add(load[b] == tmp.ScalProd(sizes)); + } + + // Place all items. + for (int i = 0; i < num_items; ++i) + { + IntVar[] tmp = new IntVar[num_bins]; + for (int b = 0; b < num_bins; ++b) + { + tmp[b] = x[i, b]; + } + model.Add(tmp.Sum() == items[i, 1]); + } + + // Links load and slack. + int safe_capacity = bin_capacity - slack_capacity; + for (int b = 0; b < num_bins; ++b) + { + // slack[b] => load[b] <= safe_capacity. + model.Add(load[b] <= safe_capacity).OnlyEnforceIf(slacks[b]); + // not(slack[b]) => load[b] > safe_capacity. + model.Add(load[b] > safe_capacity).OnlyEnforceIf(slacks[b].Not()); + } + + // Maximize sum of slacks. + model.Maximize(slacks.Sum()); + + Console.WriteLine(model.Model); + + // Solves and prints out the solution. + CpSolver solver = new CpSolver(); + CpSolverStatus status = solver.Solve(model); + Console.WriteLine(String.Format("Solve status: {0}", status)); + if (status == CpSolverStatus.Optimal) { + Console.WriteLine(String.Format("Optimal objective value: {0}", + solver.ObjectiveValue)); + for (int b = 0; b < num_bins; ++b) + { + Console.WriteLine(String.Format("load_{0} = {1}", + b, solver.Value(load[b]))); + for (int i = 0; i < num_items; ++i) + { + Console.WriteLine(string.Format(" item_{0}_{1} = {2}", + i, b, solver.Value(x[i, b]))); + } + } + } + Console.WriteLine("Statistics"); + Console.WriteLine(String.Format(" - conflicts : {0}", + solver.NumConflicts())); + Console.WriteLine(String.Format(" - branches : {0}", + solver.NumBranches())); + Console.WriteLine(String.Format(" - wall time : {0} s", + } + + static void Main() + { + BinpackingProblem(); + } +} diff --git a/ortools/sat/samples/binpacking_problem.py b/ortools/sat/samples/binpacking_problem.py index 41abb8595a..79e92036d9 100644 --- a/ortools/sat/samples/binpacking_problem.py +++ b/ortools/sat/samples/binpacking_problem.py @@ -24,10 +24,10 @@ def BinpackingProblem(): # Data. bin_capacity = 100 slack_capacity = 20 - num_bins = 10 + num_bins = 5 all_bins = range(num_bins) - items = [(20, 12), (15, 12), (30, 8), (45, 5)] + items = [(20, 6), (15, 6), (30, 4), (45, 3)] num_items = len(items) all_items = range(num_items) diff --git a/ortools/sat/samples/bool_or_sample.cc b/ortools/sat/samples/bool_or_sample.cc index 06c98a1a14..9d55d8519b 100644 --- a/ortools/sat/samples/bool_or_sample.cc +++ b/ortools/sat/samples/bool_or_sample.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/bool_or_sample.cs b/ortools/sat/samples/bool_or_sample.cs new file mode 100644 index 0000000000..5145517ae8 --- /dev/null +++ b/ortools/sat/samples/bool_or_sample.cs @@ -0,0 +1,30 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void BoolOrSample() + { + CpModel model = new CpModel(); + IntVar x = model.NewBoolVar("x"); + IntVar y = model.newBoolVar("y"); + model.AddBoolOr(new ILiteral[] {x, y.Not()}); + } + + static void Main() { + BoolOrSample(); + } +} diff --git a/ortools/sat/samples/code_sample.cc b/ortools/sat/samples/code_sample.cc index 473a9e6bac..c39b7b2d4f 100644 --- a/ortools/sat/samples/code_sample.cc +++ b/ortools/sat/samples/code_sample.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/code_sample.cs b/ortools/sat/samples/code_sample.cs new file mode 100644 index 0000000000..78f54739b7 --- /dev/null +++ b/ortools/sat/samples/code_sample.cs @@ -0,0 +1,31 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void CodeSample() + { + // Creates the model. + CpModel model = new CpModel(); + // Creates the Boolean variable. + IntVar x = model.NewBoolVar("x"); + } + + static void Main() + { + CodeSample(); + } +} diff --git a/ortools/sat/samples/interval_sample.cc b/ortools/sat/samples/interval_sample.cc index f969b07549..f8eed5f10b 100644 --- a/ortools/sat/samples/interval_sample.cc +++ b/ortools/sat/samples/interval_sample.cc @@ -15,7 +15,6 @@ #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 { @@ -33,9 +32,7 @@ void IntervalSample() { return index; }; - auto new_constant = [&cp_model, &new_variable](int64 v) { - return new_variable(v, v); - }; + auto new_constant = [&new_variable](int64 v) { return new_variable(v, v); }; auto new_interval = [&cp_model](int start, int duration, int end) { const int index = cp_model.constraints_size(); diff --git a/ortools/sat/samples/interval_sample.cs b/ortools/sat/samples/interval_sample.cs new file mode 100644 index 0000000000..790ba5cc8d --- /dev/null +++ b/ortools/sat/samples/interval_sample.cs @@ -0,0 +1,35 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void IntervalSample() + { + CpModel model = new CpModel(); + int horizon = 100; + IntVar start_var = model.NewIntVar(0, horizon, "start"); + // C# code supports IntVar or integer constants in intervals. + int duration = 10; + IntVar end_var = model.NewIntVar(0, horizon, "end"); + IntervalVar interval = + model.NewIntervalVar(start_var, duration, end_var, "interval"); + } + + static void Main() + { + IntervalSample(); + } +} diff --git a/ortools/sat/samples/literal_sample.cc b/ortools/sat/samples/literal_sample.cc index 8fa35f8346..2d3c99529a 100644 --- a/ortools/sat/samples/literal_sample.cc +++ b/ortools/sat/samples/literal_sample.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/literal_sample.cs b/ortools/sat/samples/literal_sample.cs new file mode 100644 index 0000000000..98d855d247 --- /dev/null +++ b/ortools/sat/samples/literal_sample.cs @@ -0,0 +1,29 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void LiteralSample() + { + CpModel model = new CpModel(); + IntVar x = model.NewBoolVar("x"); + ILiteral not_x = x.Not(); + } + + static void Main() { + LiteralSample(); + } +} diff --git a/ortools/sat/samples/optional_interval_sample.cc b/ortools/sat/samples/optional_interval_sample.cc index 7a8507a120..08b8d0a6f6 100644 --- a/ortools/sat/samples/optional_interval_sample.cc +++ b/ortools/sat/samples/optional_interval_sample.cc @@ -15,7 +15,6 @@ #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 { @@ -33,9 +32,7 @@ void OptionalIntervalSample() { return index; }; - auto new_constant = [&cp_model, &new_variable](int64 v) { - return new_variable(v, v); - }; + auto new_constant = [&new_variable](int64 v) { return new_variable(v, v); }; auto new_optional_interval = [&cp_model](int start, int duration, int end, int presence) { diff --git a/ortools/sat/samples/optional_interval_sample.cs b/ortools/sat/samples/optional_interval_sample.cs new file mode 100644 index 0000000000..33df4e82e2 --- /dev/null +++ b/ortools/sat/samples/optional_interval_sample.cs @@ -0,0 +1,36 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void OptionalIntervalSample() + { + CpModel model = new CpModel(); + int horizon = 100; + IntVar start_var = model.NewIntVar(0, horizon, "start"); + // C# code supports IntVar or integer constants in intervals. + int duration = 10; + IntVar end_var = model.NewIntVar(0, horizon, "end"); + IntVar presence_var = model.NewBoolVar("presence"); + IntervalVar interval = model.NewOptionalIntervalVar( + start_var, duration, end_var, presence_var, "interval"); + } + + static void Main() + { + OptionalIntervalSample(); + } +} diff --git a/ortools/sat/samples/rabbits_and_pheasants.cc b/ortools/sat/samples/rabbits_and_pheasants.cc index 5f12fb4971..003a4d465f 100644 --- a/ortools/sat/samples/rabbits_and_pheasants.cc +++ b/ortools/sat/samples/rabbits_and_pheasants.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/rabbits_and_pheasants.cs b/ortools/sat/samples/rabbits_and_pheasants.cs new file mode 100644 index 0000000000..1b9023c64f --- /dev/null +++ b/ortools/sat/samples/rabbits_and_pheasants.cs @@ -0,0 +1,46 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void RabbitsAndPheasants() + { + // Creates the model. + CpModel model = new CpModel(); + // Creates the variables. + IntVar r = model.NewIntVar(0, 100, "r"); + IntVar p = model.NewIntVar(0, 100, "p"); + // 20 heads. + model.Add(r + p == 20); + // 56 legs. + model.Add(4 * r + 2 * p == 56); + + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + CpSolverStatus status = solver.Solve(model); + + if (status == CpSolverStatus.Feasible) + { + Console.WriteLine(solver.Value(r) + " rabbits, and " + + solver.Value(p) + " pheasants"); + } + } + + static void Main() + { + RabbitsAndPheasants(); + } +} diff --git a/ortools/sat/samples/reified_sample.cc b/ortools/sat/samples/reified_sample.cc index 12242b1189..df198d940d 100644 --- a/ortools/sat/samples/reified_sample.cc +++ b/ortools/sat/samples/reified_sample.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/reified_sample.cs b/ortools/sat/samples/reified_sample.cs new file mode 100644 index 0000000000..a4468a322f --- /dev/null +++ b/ortools/sat/samples/reified_sample.cs @@ -0,0 +1,42 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void ReifiedSample() + { + CpModel model = new CpModel(); + + IntVar x = model.NewBoolVar("x"); + IntVar y = model.NewBoolVar("y"); + IntVar b = model.NewBoolVar("b"); + + // First version using a half-reified bool and. + model.AddBoolAnd(new ILiteral[] {x, y.Not()}).OnlyEnforceIf(b); + + // Second version using implications. + model.AddImplication(b, x); + model.AddImplication(b, y.Not()); + + // Third version using bool or. + model.AddBoolOr(new ILiteral[] {b.Not(), x}); + model.AddBoolOr(new ILiteral[] {b.Not(), y.Not()}); + } + + static void Main() { + ReifiedSample(); + } +} diff --git a/ortools/sat/samples/simple_solve.cc b/ortools/sat/samples/simple_solve.cc index 36443eb59d..efe1e26f7e 100644 --- a/ortools/sat/samples/simple_solve.cc +++ b/ortools/sat/samples/simple_solve.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/simple_solve.cs b/ortools/sat/samples/simple_solve.cs new file mode 100644 index 0000000000..06cc80826c --- /dev/null +++ b/ortools/sat/samples/simple_solve.cs @@ -0,0 +1,48 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void SimpleSolve() + { + // Creates the model. + CpModel model = new CpModel(); + // Creates the variables. + int num_vals = 3; + + IntVar x = model.NewIntVar(0, num_vals - 1, "x"); + IntVar y = model.NewIntVar(0, num_vals - 1, "y"); + IntVar z = model.NewIntVar(0, num_vals - 1, "z"); + // Creates the constraints. + model.Add(x != y); + + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + CpSolverStatus status = solver.Solve(model); + + if (status == CpSolverStatus.Feasible) + { + Console.WriteLine("x = " + solver.Value(x)); + Console.WriteLine("y = " + solver.Value(y)); + Console.WriteLine("z = " + solver.Value(z)); + } + } + + static void Main() + { + SimpleSolve(); + } +} diff --git a/ortools/sat/samples/solve_all_solutions.cs b/ortools/sat/samples/solve_all_solutions.cs new file mode 100644 index 0000000000..8e988739ed --- /dev/null +++ b/ortools/sat/samples/solve_all_solutions.cs @@ -0,0 +1,77 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class VarArraySolutionPrinter : CpSolverSolutionCallback +{ + public VarArraySolutionPrinter(IntVar[] variables) + { + variables_ = variables; + } + + public override void OnSolutionCallback() + { + { + Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", + solution_count_, WallTime())); + foreach (IntVar v in variables_) + { + Console.WriteLine( + String.Format(" {0} = {1}", v.ShortString(), Value(v))); + } + solution_count_++; + } + } + + public int SolutionCount() + { + return solution_count_; + } + + private int solution_count_; + private IntVar[] variables_; +} + + +public class CodeSamplesSat +{ + static void MinimalCpSatAllSolutions() + { + // Creates the model. + CpModel model = new CpModel(); + // Creates the variables. + int num_vals = 3; + + IntVar x = model.NewIntVar(0, num_vals - 1, "x"); + IntVar y = model.NewIntVar(0, num_vals - 1, "y"); + IntVar z = model.NewIntVar(0, num_vals - 1, "z"); + + // Adds a different constraint. + model.Add(x != y); + + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + VarArraySolutionPrinter cb = + new VarArraySolutionPrinter(new IntVar[] {x, y, z}); + solver.SearchAllSolutions(model, cb); + Console.WriteLine(String.Format("Number of solutions found: {0}", + cb.SolutionCount())); + } + + static void Main() + { + MinimalCpSatAllSolutions(); + } +} diff --git a/ortools/sat/samples/solve_with_intermediate_solutions.cc b/ortools/sat/samples/solve_with_intermediate_solutions.cc index 9bdc7e0c4f..9a2bc3c234 100644 --- a/ortools/sat/samples/solve_with_intermediate_solutions.cc +++ b/ortools/sat/samples/solve_with_intermediate_solutions.cc @@ -15,7 +15,6 @@ #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 { diff --git a/ortools/sat/samples/solve_with_intermediate_solutions.cs b/ortools/sat/samples/solve_with_intermediate_solutions.cs new file mode 100644 index 0000000000..9af2a7d776 --- /dev/null +++ b/ortools/sat/samples/solve_with_intermediate_solutions.cs @@ -0,0 +1,81 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback +{ + public VarArraySolutionPrinterWithObjective(IntVar[] variables) + { + variables_ = variables; + } + + public override void OnSolutionCallback() + { + { + Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", + solution_count_, WallTime())); + Console.WriteLine( + String.Format(" objective value = {0}", ObjectiveValue())); + foreach (IntVar v in variables_) + { + Console.WriteLine( + String.Format(" {0} = {1}", v.ShortString(), Value(v))); + } + solution_count_++; + } + } + + public int SolutionCount() + { + return solution_count_; + } + + private int solution_count_; + private IntVar[] variables_; +} + +public class CodeSamplesSat +{ + static void MinimalCpSatPrintIntermediateSolutions() + { + // Creates the model. + CpModel model = new CpModel(); + // Creates the variables. + int num_vals = 3; + + IntVar x = model.NewIntVar(0, num_vals - 1, 'x'); + IntVar y = model.NewIntVar(0, num_vals - 1, 'y'); + IntVar z = model.NewIntVar(0, num_vals - 1, 'z'); + + // Adds a different constraint. + model.Add(x != y); + + // Maximizes a linear combination of variables. + model.Maximize(x + 2 * y + 3 * z); + + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + VarArraySolutionPrinterWithObjective cb = + new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); + solver.SearchAllSolutions(model, cb); + Console.WriteLine(String.Format('Number of solutions found: {0}', + cb.SolutionCount())); + } + + static void Main() + { + MinimalCpSatPrintIntermediateSolutions(); + } +} diff --git a/ortools/sat/samples/solve_with_time_limit.cs b/ortools/sat/samples/solve_with_time_limit.cs new file mode 100644 index 0000000000..e7b7c99a99 --- /dev/null +++ b/ortools/sat/samples/solve_with_time_limit.cs @@ -0,0 +1,52 @@ +// 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. + +using System; +using Google.OrTools.Sat; + +public class CodeSamplesSat +{ + static void MinimalCpSatWithTimeLimit() + { + // Creates the model. + CpModel model = new CpModel(); + // Creates the variables. + int num_vals = 3; + + IntVar x = model.NewIntVar(0, num_vals - 1, "x"); + IntVar y = model.NewIntVar(0, num_vals - 1, "y"); + IntVar z = model.NewIntVar(0, num_vals - 1, "z"); + // Adds a different constraint. + model.Add(x != y); + + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + + // Adds a time limit. Parameters are stored as strings in the solver. + solver.StringParameters = "max_time_in_seconds:10.0" ; + + CpSolverStatus status = solver.Solve(model); + + if (status == CpSolverStatus.Feasible) + { + Console.WriteLine("x = " + solver.Value(x)); + Console.WriteLine("y = " + solver.Value(y)); + Console.WriteLine("z = " + solver.Value(z)); + } + } + + static void Main() + { + MinimalCpSatWithTimeLimit(); + } +}