From 1186dc6196ce53614503f267af3cf414bc1c64bc Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 3 Nov 2020 14:01:06 +0100 Subject: [PATCH] minor polish; update c# code in CP-SAT cookbook --- ortools/constraint_solver/constraint_solver.h | 5 +- ortools/flatzinc/fz.cc | 2 - ortools/flatzinc/mznlib/BUILD | 2 +- ortools/linear_solver/linear_solver.proto | 3 - ortools/sat/README.md | 5 +- ortools/sat/doc/README.md | 54 +-- ortools/sat/doc/boolean_logic.md | 68 +-- ortools/sat/doc/channeling.md | 267 +++++------ ortools/sat/doc/integer_arithmetic.md | 282 ++++++------ ortools/sat/doc/model.md | 85 ++-- ortools/sat/doc/scheduling.md | 416 +++++++++--------- ortools/sat/doc/solver.md | 300 ++++++------- 12 files changed, 772 insertions(+), 717 deletions(-) diff --git a/ortools/constraint_solver/constraint_solver.h b/ortools/constraint_solver/constraint_solver.h index f91e414e7b..cb14d809f1 100644 --- a/ortools/constraint_solver/constraint_solver.h +++ b/ortools/constraint_solver/constraint_solver.h @@ -2200,10 +2200,9 @@ class Solver { /// Creates a search limit that constrains the running time. RegularLimit* MakeTimeLimit(absl::Duration time); - #if !defined(SWIG) ABSL_DEPRECATED("Use the version taking absl::Duration() as argument") -#endif +#endif // !defined(SWIG) RegularLimit* MakeTimeLimit(int64 time_in_ms) { return MakeTimeLimit(time_in_ms == kint64max ? absl::InfiniteDuration() @@ -2234,7 +2233,7 @@ class Solver { #if !defined(SWIG) ABSL_DEPRECATED("Use other MakeLimit() versions") -#endif +#endif // !defined(SWIG) RegularLimit* MakeLimit(int64 time, int64 branches, int64 failures, int64 solutions, bool smart_time_check = false, bool cumulative = false); diff --git a/ortools/flatzinc/fz.cc b/ortools/flatzinc/fz.cc index 41465f26c8..fd2499a3df 100644 --- a/ortools/flatzinc/fz.cc +++ b/ortools/flatzinc/fz.cc @@ -55,8 +55,6 @@ ABSL_FLAG(std::string, params, "", "SatParameters as a text proto."); ABSL_DECLARE_FLAG(bool, log_prefix); -using operations_research::ThreadPool; - namespace operations_research { namespace fz { diff --git a/ortools/flatzinc/mznlib/BUILD b/ortools/flatzinc/mznlib/BUILD index 3fc1bee5db..cc602503ca 100644 --- a/ortools/flatzinc/mznlib/BUILD +++ b/ortools/flatzinc/mznlib/BUILD @@ -10,6 +10,6 @@ package(default_visibility = ["//visibility:public"]) # Definition files (.mzn). filegroup( - name = "minizinc_sat_files", + name = "minizinc_files", srcs = glob(["*.mzn"]), ) diff --git a/ortools/linear_solver/linear_solver.proto b/ortools/linear_solver/linear_solver.proto index 3d403a7cde..c6c6d1ae4f 100644 --- a/ortools/linear_solver/linear_solver.proto +++ b/ortools/linear_solver/linear_solver.proto @@ -297,9 +297,6 @@ message MPModelProto { // To support 'unspecified' double value in proto3, the simplest is to wrap // any double value in a nested message (has_XXX works for message fields). -// We don't use google/protobuf/wrappers.proto because depending on it makes -// the following android integration test fail: -// http://sponge/c4bce1fd-41bd-4d0b-b4ca-fc04d4d64621 message OptionalDouble { optional double value = 1; } diff --git a/ortools/sat/README.md b/ortools/sat/README.md index 598625057f..0db74d738f 100644 --- a/ortools/sat/README.md +++ b/ortools/sat/README.md @@ -5,7 +5,7 @@ clause learning. It is built on top of an efficient SAT/max-SAT solver whose code is also in this directory. To begin, skim -[cp_model.proto](../sat/cp_model.proto) to +[cp_model.proto](../cp_model.proto) to understand how optimization problems can be modeled using the solver. You can then solve a model with the functions in [cp_model_solver.h](../sat/cp_model_solver.h). @@ -20,7 +20,7 @@ then solve a model with the functions in The optimization model description and related utilities: -* [cp_model.proto](../sat/cp_model.proto): +* [cp_model.proto](../cp_model.proto): Proto describing a general Constraint Programming model. * [cp_model_utils.h](../sat/cp_model_utils.h): Utilities to manipulate and create a cp_model.proto. @@ -117,7 +117,6 @@ Scheduling constraints: Propagation algorithms for the disjunctive scheduling constraint. * [cumulative.h](../sat/cumulative.h), [timetable.h](../sat/timetable.h), - [overload_checker.h](../sat/overload_checker.h), [timetable_edgefinding.h](../sat/timetable_edgefinding.h): Propagation algorithms for the cumulative scheduling constraint. * [cumulative_energy.h](../sat/cumulative_energy.h): diff --git a/ortools/sat/doc/README.md b/ortools/sat/doc/README.md index 13a702f21f..a0f37555e7 100644 --- a/ortools/sat/doc/README.md +++ b/ortools/sat/doc/README.md @@ -14,7 +14,7 @@ * [Java code samples](#java-code-samples) * [C# code samples](#c-code-samples-1) - + @@ -70,7 +70,7 @@ def SimpleSatProgram(): solver = cp_model.CpSolver() status = solver.Solve(model) - if status == cp_model.FEASIBLE: + if status == cp_model.OPTIMAL: print('x = %i' % solver.Value(x)) print('y = %i' % solver.Value(y)) print('z = %i' % solver.Value(z)) @@ -109,7 +109,7 @@ void SimpleSatProgram() { const CpSolverResponse response = Solve(cp_model.Build()); LOG(INFO) << CpSolverResponseStats(response); - if (response.status() == CpSolverStatus::FEASIBLE) { + if (response.status() == CpSolverStatus::OPTIMAL) { // Get the value of x in the solution. LOG(INFO) << "x = " << SolutionIntegerValue(response, x); LOG(INFO) << "y = " << SolutionIntegerValue(response, y); @@ -184,31 +184,31 @@ using Google.OrTools.Sat; public class SimpleSatProgram { - static void Main() - { - // 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) + static void Main() { - Console.WriteLine("x = " + solver.Value(x)); - Console.WriteLine("y = " + solver.Value(y)); - Console.WriteLine("z = " + solver.Value(z)); + // 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.Optimal) + { + Console.WriteLine("x = " + solver.Value(x)); + Console.WriteLine("y = " + solver.Value(y)); + Console.WriteLine("z = " + solver.Value(z)); + } } - } } ``` diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index 3dd4eac3d7..ca65a456ae 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -26,7 +26,7 @@ * [Product of two Boolean Variables](#product-of-two-boolean-variables) * [Python code](#python-code-3) - + @@ -122,12 +122,14 @@ public class LiteralSampleSat { using System; using Google.OrTools.Sat; -public class LiteralSampleSat { - static void Main() { - CpModel model = new CpModel(); - IntVar x = model.NewBoolVar("x"); - ILiteral not_x = x.Not(); - } +public class LiteralSampleSat +{ + static void Main() + { + CpModel model = new CpModel(); + IntVar x = model.NewBoolVar("x"); + ILiteral not_x = x.Not(); + } } ``` @@ -196,6 +198,8 @@ int main() { ### Java code ```java +package com.google.ortools.sat.samples; + import com.google.ortools.sat.CpModel; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; @@ -220,15 +224,17 @@ public class BoolOrSampleSat { using System; using Google.OrTools.Sat; -public class BoolOrSampleSat { - static void Main() { - CpModel model = new CpModel(); +public class BoolOrSampleSat +{ + static void Main() + { + CpModel model = new CpModel(); - IntVar x = model.NewBoolVar("x"); - IntVar y = model.NewBoolVar("y"); + IntVar x = model.NewBoolVar("x"); + IntVar y = model.NewBoolVar("y"); - model.AddBoolOr(new ILiteral[] { x, y.Not() }); - } + model.AddBoolOr(new ILiteral[] { x, y.Not() }); + } } ``` @@ -324,6 +330,8 @@ int main() { ### Java code ```java +package com.google.ortools.sat.samples; + import com.google.ortools.sat.CpModel; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.Literal; @@ -369,25 +377,27 @@ public class ReifiedSampleSat { using System; using Google.OrTools.Sat; -public class ReifiedSampleSat { - static void Main() { - CpModel model = new CpModel(); +public class ReifiedSampleSat +{ + static void Main() + { + CpModel model = new CpModel(); - IntVar x = model.NewBoolVar("x"); - IntVar y = model.NewBoolVar("y"); - IntVar b = model.NewBoolVar("b"); + 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); + // 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()); + // 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()}); - } + // Third version using bool or. + model.AddBoolOr(new ILiteral[] { b.Not(), x }); + model.AddBoolOr(new ILiteral[] { b.Not(), y.Not() }); + } } ``` diff --git a/ortools/sat/doc/channeling.md b/ortools/sat/doc/channeling.md index 9b75847122..066d6cd293 100644 --- a/ortools/sat/doc/channeling.md +++ b/ortools/sat/doc/channeling.md @@ -17,7 +17,7 @@ * [Java code](#java-code-1) * [C# code](#c-code-3) - + @@ -254,60 +254,64 @@ using System; using Google.OrTools.Sat; using Google.OrTools.Util; -public class VarArraySolutionPrinter : CpSolverSolutionCallback { - public VarArraySolutionPrinter(IntVar[] variables) { - variables_ = variables; - } - - public override void OnSolutionCallback() { +public class VarArraySolutionPrinter : CpSolverSolutionCallback +{ + public VarArraySolutionPrinter(IntVar[] variables) { - foreach (IntVar v in variables_) { - Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v))); - } - Console.WriteLine(); + variables_ = variables; } - } - private IntVar[] variables_; + public override void OnSolutionCallback() + { + { + foreach (IntVar v in variables_) + { + Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v))); + } + Console.WriteLine(); + } + } + + private IntVar[] variables_; } -public class ChannelingSampleSat { - static void Main() { - // Create the CP-SAT model. - CpModel model = new CpModel(); +public class ChannelingSampleSat +{ + static void Main() + { + // Create the CP-SAT model. + CpModel model = new CpModel(); - // Declare our two primary variables. - IntVar x = model.NewIntVar(0, 10, "x"); - IntVar y = model.NewIntVar(0, 10, "y"); + // Declare our two primary variables. + IntVar x = model.NewIntVar(0, 10, "x"); + IntVar y = model.NewIntVar(0, 10, "y"); - // Declare our intermediate boolean variable. - IntVar b = model.NewBoolVar("b"); + // Declare our intermediate boolean variable. + IntVar b = model.NewBoolVar("b"); - // Implement b == (x >= 5). - model.Add(x >= 5).OnlyEnforceIf(b); - model.Add(x < 5).OnlyEnforceIf(b.Not()); + // Implement b == (x >= 5). + model.Add(x >= 5).OnlyEnforceIf(b); + model.Add(x < 5).OnlyEnforceIf(b.Not()); - // Create our two half-reified constraints. - // First, b implies (y == 10 - x). - model.Add(y == 10 - x).OnlyEnforceIf(b); - // Second, not(b) implies y == 0. - model.Add(y == 0).OnlyEnforceIf(b.Not()); + // Create our two half-reified constraints. + // First, b implies (y == 10 - x). + model.Add(y == 10 - x).OnlyEnforceIf(b); + // Second, not(b) implies y == 0. + model.Add(y == 0).OnlyEnforceIf(b.Not()); - // Search for x values in increasing order. - model.AddDecisionStrategy(new IntVar[] { x }, - DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst, - DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue); + // Search for x values in increasing order. + model.AddDecisionStrategy(new IntVar[] { x }, DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst, + DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue); - // Create the solver. - CpSolver solver = new CpSolver(); + // Create the solver. + CpSolver solver = new CpSolver(); - // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Force solver to follow the decision strategy exactly. + solver.StringParameters = "search_branching:FIXED_SEARCH"; - VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] {x, y, b}); - solver.SearchAllSolutions(model, cb); - } + VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, b }); + solver.SearchAllSolutions(model, cb); + } } ``` @@ -504,6 +508,8 @@ int main() { ### Java code ```java +package com.google.ortools.sat.samples; + import com.google.ortools.sat.CpSolverStatus; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; @@ -609,91 +615,106 @@ public class BinPackingProblemSat { using System; using Google.OrTools.Sat; -public class BinPackingProblemSat { - static void Main() { - // Data. - int bin_capacity = 100; - int slack_capacity = 20; - int num_bins = 5; +public class BinPackingProblemSat +{ + static void Main() + { + // Data. + int bin_capacity = 100; + int slack_capacity = 20; + int num_bins = 5; - int[,] items = new int[,] { { 20, 6 }, { 15, 6 }, { 30, 4 }, { 45, 3 } }; - int num_items = items.GetLength(0); + int[,] items = new int[,] { { 20, 6 }, { 15, 6 }, { 30, 4 }, { 45, 3 } }; + int num_items = items.GetLength(0); - // Model. - CpModel model = new CpModel(); + // 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(LinearExpr.Sum(tmp) == 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(LinearExpr.Sum(slacks)); - - // 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]))); + // 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] == LinearExpr.ScalProd(tmp, 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(LinearExpr.Sum(tmp) == 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(LinearExpr.Sum(slacks)); + + // 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())); } - 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())); - } } ``` diff --git a/ortools/sat/doc/integer_arithmetic.md b/ortools/sat/doc/integer_arithmetic.md index 354246dbbb..8a622e594b 100644 --- a/ortools/sat/doc/integer_arithmetic.md +++ b/ortools/sat/doc/integer_arithmetic.md @@ -33,7 +33,7 @@ * [Java code](#java-code-2) * [C# code](#c-code-5) - + @@ -172,7 +172,7 @@ def RabbitsAndPheasantsSat(): solver = cp_model.CpSolver() status = solver.Solve(model) - if status == cp_model.FEASIBLE: + if status == cp_model.OPTIMAL: print('%i rabbits and %i pheasants' % (solver.Value(r), solver.Value(p))) @@ -200,7 +200,7 @@ void RabbitsAndPheasantsSat() { const CpSolverResponse response = Solve(cp_model.Build()); - if (response.status() == CpSolverStatus::FEASIBLE) { + if (response.status() == CpSolverStatus::OPTIMAL) { // Get the value of x in the solution. LOG(INFO) << SolutionIntegerValue(response, rabbits) << " rabbits, and " << SolutionIntegerValue(response, pheasants) << " pheasants"; @@ -263,28 +263,29 @@ public class RabbitsAndPheasantsSat { using System; using Google.OrTools.Sat; -public class RabbitsAndPheasantsSat { - static void Main() { - // 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) +public class RabbitsAndPheasantsSat +{ + static void Main() { - Console.WriteLine(solver.Value(r) + " rabbits, and " + - solver.Value(p) + " pheasants"); + // 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.Optimal) + { + Console.WriteLine(solver.Value(r) + " rabbits, and " + solver.Value(p) + " pheasants"); + } } - } } ``` @@ -579,76 +580,79 @@ using System; using Google.OrTools.Sat; using Google.OrTools.Util; -public class VarArraySolutionPrinter : CpSolverSolutionCallback { - public VarArraySolutionPrinter(IntVar[] variables) { - variables_ = variables; - } - - public override void OnSolutionCallback() { +public class VarArraySolutionPrinter : CpSolverSolutionCallback +{ + public VarArraySolutionPrinter(IntVar[] variables) { - foreach (IntVar v in variables_) { - Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v))); - } - Console.WriteLine(); + variables_ = variables; } - } - private IntVar[] variables_; + public override void OnSolutionCallback() + { + { + foreach (IntVar v in variables_) + { + Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v))); + } + Console.WriteLine(); + } + } + + private IntVar[] variables_; } -public class EarlinessTardinessCostSampleSat { - static void Main() { - long earliness_date = 5; - long earliness_cost = 8; - long lateness_date = 15; - long lateness_cost = 12; +public class EarlinessTardinessCostSampleSat +{ + static void Main() + { + long earliness_date = 5; + long earliness_cost = 8; + long lateness_date = 15; + long lateness_cost = 12; - // Create the CP-SAT model. - CpModel model = new CpModel(); + // Create the CP-SAT model. + CpModel model = new CpModel(); - // Declare our primary variable. - IntVar x = model.NewIntVar(0, 20, "x"); + // Declare our primary variable. + IntVar x = model.NewIntVar(0, 20, "x"); - // Create the expression variable and implement the piecewise linear - // function. - // - // \ / - // \______/ - // ed ld - // - long large_constant = 1000; - IntVar expr = model.NewIntVar(0, large_constant, "expr"); + // Create the expression variable and implement the piecewise linear + // function. + // + // \ / + // \______/ + // ed ld + // + long large_constant = 1000; + IntVar expr = model.NewIntVar(0, large_constant, "expr"); - // First segment. - IntVar s1 = model.NewIntVar(-large_constant, large_constant, "s1"); - model.Add(s1 == earliness_cost * (earliness_date - x)); + // First segment. + IntVar s1 = model.NewIntVar(-large_constant, large_constant, "s1"); + model.Add(s1 == earliness_cost * (earliness_date - x)); - // Second segment. - IntVar s2 = model.NewConstant(0); + // Second segment. + IntVar s2 = model.NewConstant(0); - // Third segment. - IntVar s3 = model.NewIntVar(-large_constant, large_constant, "s3"); - model.Add(s3 == lateness_cost * (x - lateness_date)); + // Third segment. + IntVar s3 = model.NewIntVar(-large_constant, large_constant, "s3"); + model.Add(s3 == lateness_cost * (x - lateness_date)); - // Link together expr and x through s1, s2, and s3. - model.AddMaxEquality(expr, new IntVar[] {s1, s2, s3}); + // Link together expr and x through s1, s2, and s3. + model.AddMaxEquality(expr, new IntVar[] { s1, s2, s3 }); - // Search for x values in increasing order. - model.AddDecisionStrategy( - new IntVar[] {x}, - DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst, - DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue); + // Search for x values in increasing order. + model.AddDecisionStrategy(new IntVar[] { x }, DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst, + DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue); - // Create the solver. - CpSolver solver = new CpSolver(); + // Create the solver. + CpSolver solver = new CpSolver(); - // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Force solver to follow the decision strategy exactly. + solver.StringParameters = "search_branching:FIXED_SEARCH"; - VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] {x, expr}); - solver.SearchAllSolutions(model, cb); - } + VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, expr }); + solver.SearchAllSolutions(model, cb); + } } ``` @@ -947,82 +951,82 @@ using System; using Google.OrTools.Sat; using Google.OrTools.Util; -public class VarArraySolutionPrinter : CpSolverSolutionCallback { - public VarArraySolutionPrinter(IntVar[] variables) { - variables_ = variables; - } - - public override void OnSolutionCallback() { +public class VarArraySolutionPrinter : CpSolverSolutionCallback +{ + public VarArraySolutionPrinter(IntVar[] variables) { - foreach (IntVar v in variables_) { - Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v))); - } - Console.WriteLine(); + variables_ = variables; } - } - private IntVar[] variables_; + public override void OnSolutionCallback() + { + { + foreach (IntVar v in variables_) + { + Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v))); + } + Console.WriteLine(); + } + } + + private IntVar[] variables_; } -public class StepFunctionSampleSat { - static void Main() { - // Create the CP-SAT model. - CpModel model = new CpModel(); +public class StepFunctionSampleSat +{ + static void Main() + { + // Create the CP-SAT model. + CpModel model = new CpModel(); - // Declare our primary variable. - IntVar x = model.NewIntVar(0, 20, "x"); + // Declare our primary variable. + IntVar x = model.NewIntVar(0, 20, "x"); - // Create the expression variable and implement the step function - // Note it is not defined for var == 2. - // - // - 3 - // -- -- --------- 2 - // 1 - // -- --- 0 - // 0 ================ 20 - // - IntVar expr = model.NewIntVar(0, 3, "expr"); + // Create the expression variable and implement the step function + // Note it is not defined for var == 2. + // + // - 3 + // -- -- --------- 2 + // 1 + // -- --- 0 + // 0 ================ 20 + // + IntVar expr = model.NewIntVar(0, 3, "expr"); - // expr == 0 on [5, 6] U [8, 10] - ILiteral b0 = model.NewBoolVar("b0"); - model.AddLinearExpressionInDomain( - x, - Domain.FromValues(new long[] { 5, 6, 8, 9, 10 })).OnlyEnforceIf(b0); - model.Add(expr == 0).OnlyEnforceIf(b0); + // expr == 0 on [5, 6] U [8, 10] + ILiteral b0 = model.NewBoolVar("b0"); + model.AddLinearExpressionInDomain(x, Domain.FromValues(new long[] { 5, 6, 8, 9, 10 })).OnlyEnforceIf(b0); + model.Add(expr == 0).OnlyEnforceIf(b0); - // expr == 2 on [0, 1] U [3, 4] U [11, 20] - ILiteral b2 = model.NewBoolVar("b2"); - model.AddLinearExpressionInDomain( - x, - Domain.FromIntervals( - new long[][] {new long[] {0, 1}, - new long[] {3, 4}, - new long[] {11, 20}})).OnlyEnforceIf(b2); - model.Add(expr == 2).OnlyEnforceIf(b2); + // expr == 2 on [0, 1] U [3, 4] U [11, 20] + ILiteral b2 = model.NewBoolVar("b2"); + model + .AddLinearExpressionInDomain( + x, + Domain.FromIntervals(new long[][] { new long[] { 0, 1 }, new long[] { 3, 4 }, new long[] { 11, 20 } })) + .OnlyEnforceIf(b2); + model.Add(expr == 2).OnlyEnforceIf(b2); - // expr == 3 when x == 7 - ILiteral b3 = model.NewBoolVar("b3"); - model.Add(x == 7).OnlyEnforceIf(b3); - model.Add(expr == 3).OnlyEnforceIf(b3); + // expr == 3 when x == 7 + ILiteral b3 = model.NewBoolVar("b3"); + model.Add(x == 7).OnlyEnforceIf(b3); + model.Add(expr == 3).OnlyEnforceIf(b3); - // At least one bi is true. (we could use a sum == 1). - model.AddBoolOr(new ILiteral[] { b0, b2, b3 }); + // At least one bi is true. (we could use a sum == 1). + model.AddBoolOr(new ILiteral[] { b0, b2, b3 }); - // Search for x values in increasing order. - model.AddDecisionStrategy( - new IntVar[] { x }, - DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst, - DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue); + // Search for x values in increasing order. + model.AddDecisionStrategy(new IntVar[] { x }, DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst, + DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue); - // Create the solver. - CpSolver solver = new CpSolver(); + // Create the solver. + CpSolver solver = new CpSolver(); - // Force solver to follow the decision strategy exactly. - solver.StringParameters = "search_branching:FIXED_SEARCH"; + // Force solver to follow the decision strategy exactly. + solver.StringParameters = "search_branching:FIXED_SEARCH"; - VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] { x, expr }); - solver.SearchAllSolutions(model, cb); - } + VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, expr }); + solver.SearchAllSolutions(model, cb); + } } ``` diff --git a/ortools/sat/doc/model.md b/ortools/sat/doc/model.md index 8be72152f8..6c8adc4371 100644 --- a/ortools/sat/doc/model.md +++ b/ortools/sat/doc/model.md @@ -13,7 +13,7 @@ * [Java code](#java-code) * [C# code](#c-code-1) - + @@ -246,56 +246,61 @@ public class SolutionHintingSampleSat { using System; using Google.OrTools.Sat; -public class VarArraySolutionPrinter : CpSolverSolutionCallback { - public VarArraySolutionPrinter(IntVar[] variables) { - variables_ = variables; - } - - public override void OnSolutionCallback() { +public class VarArraySolutionPrinter : CpSolverSolutionCallback +{ + public VarArraySolutionPrinter(IntVar[] variables) { - 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_++; + variables_ = variables; } - } - public int SolutionCount() { - return solution_count_; - } + 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_++; + } + } - private int solution_count_; - private IntVar[] variables_; + public int SolutionCount() + { + return solution_count_; + } + + private int solution_count_; + private IntVar[] variables_; } -public class SolutionHintingSampleSat { - static void Main() { - // Creates the model. - CpModel model = new CpModel(); +public class SolutionHintingSampleSat +{ + static void Main() + { + // Creates the model. + CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; + // 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"); + 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 the constraints. + model.Add(x != y); - // Solution hinting: x <- 1, y <- 2 - model.AddHint(x, 1); - model.AddHint(y, 2); + // Solution hinting: x <- 1, y <- 2 + model.AddHint(x, 1); + model.AddHint(y, 2); - model.Maximize(LinearExpr.ScalProd(new IntVar[] {x, y, z}, new int[] {1, 2, 3})); + model.Maximize(LinearExpr.ScalProd(new IntVar[] { x, y, z }, new int[] { 1, 2, 3 })); - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] { x, y, z }); - CpSolverStatus status = solver.SolveWithSolutionCallback(model, cb); - } + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); + CpSolverStatus status = solver.SolveWithSolutionCallback(model, cb); + } } ``` diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md index fe059f03be..b9674cabd3 100644 --- a/ortools/sat/doc/scheduling.md +++ b/ortools/sat/doc/scheduling.md @@ -36,7 +36,7 @@ * [Convex hull of a set of intervals](#convex-hull-of-a-set-of-intervals) * [Reservoir constraint](#reservoir-constraint) - + @@ -156,17 +156,18 @@ public class IntervalSampleSat { using System; using Google.OrTools.Sat; -public class IntervalSampleSat { - static void Main() { - 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"); - } +public class IntervalSampleSat +{ + static void Main() + { + 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"); + } } ``` @@ -284,18 +285,19 @@ public class OptionalIntervalSampleSat { using System; using Google.OrTools.Sat; -public class OptionalIntervalSampleSat { - static void Main() { - 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"); - } +public class OptionalIntervalSampleSat +{ + static void Main() + { + 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"); + } } ``` @@ -529,58 +531,57 @@ public class NoOverlapSampleSat { using System; using Google.OrTools.Sat; -public class NoOverlapSampleSat { - static void Main() { - CpModel model = new CpModel(); - // Three weeks. - int horizon = 21; +public class NoOverlapSampleSat +{ + static void Main() + { + CpModel model = new CpModel(); + // Three weeks. + int horizon = 21; - // Task 0, duration 2. - IntVar start_0 = model.NewIntVar(0, horizon, "start_0"); - int duration_0 = 2; - IntVar end_0 = model.NewIntVar(0, horizon, "end_0"); - IntervalVar task_0 = - model.NewIntervalVar(start_0, duration_0, end_0, "task_0"); + // Task 0, duration 2. + IntVar start_0 = model.NewIntVar(0, horizon, "start_0"); + int duration_0 = 2; + IntVar end_0 = model.NewIntVar(0, horizon, "end_0"); + IntervalVar task_0 = model.NewIntervalVar(start_0, duration_0, end_0, "task_0"); - // Task 1, duration 4. - IntVar start_1 = model.NewIntVar(0, horizon, "start_1"); - int duration_1 = 4; - IntVar end_1 = model.NewIntVar(0, horizon, "end_1"); - IntervalVar task_1 = - model.NewIntervalVar(start_1, duration_1, end_1, "task_1"); + // Task 1, duration 4. + IntVar start_1 = model.NewIntVar(0, horizon, "start_1"); + int duration_1 = 4; + IntVar end_1 = model.NewIntVar(0, horizon, "end_1"); + IntervalVar task_1 = model.NewIntervalVar(start_1, duration_1, end_1, "task_1"); - // Task 2, duration 3. - IntVar start_2 = model.NewIntVar(0, horizon, "start_2"); - int duration_2 = 3; - IntVar end_2 = model.NewIntVar(0, horizon, "end_2"); - IntervalVar task_2 = - model.NewIntervalVar(start_2, duration_2, end_2, "task_2"); + // Task 2, duration 3. + IntVar start_2 = model.NewIntVar(0, horizon, "start_2"); + int duration_2 = 3; + IntVar end_2 = model.NewIntVar(0, horizon, "end_2"); + IntervalVar task_2 = model.NewIntervalVar(start_2, duration_2, end_2, "task_2"); - // Weekends. - IntervalVar weekend_0 = model.NewIntervalVar(5, 2, 7, "weekend_0"); - IntervalVar weekend_1 = model.NewIntervalVar(12, 2, 14, "weekend_1"); - IntervalVar weekend_2 = model.NewIntervalVar(19, 2, 21, "weekend_2"); + // Weekends. + IntervalVar weekend_0 = model.NewIntervalVar(5, 2, 7, "weekend_0"); + IntervalVar weekend_1 = model.NewIntervalVar(12, 2, 14, "weekend_1"); + IntervalVar weekend_2 = model.NewIntervalVar(19, 2, 21, "weekend_2"); - // No Overlap constraint. - model.AddNoOverlap(new IntervalVar[] {task_0, task_1, task_2, weekend_0, - weekend_1, weekend_2}); + // No Overlap constraint. + model.AddNoOverlap(new IntervalVar[] { task_0, task_1, task_2, weekend_0, weekend_1, weekend_2 }); - // Makespan objective. - IntVar obj = model.NewIntVar(0, horizon, "makespan"); - model.AddMaxEquality(obj, new IntVar[] {end_0, end_1, end_2}); - model.Minimize(obj); + // Makespan objective. + IntVar obj = model.NewIntVar(0, horizon, "makespan"); + model.AddMaxEquality(obj, new IntVar[] { end_0, end_1, end_2 }); + model.Minimize(obj); - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - CpSolverStatus status = solver.Solve(model); + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + CpSolverStatus status = solver.Solve(model); - if (status == CpSolverStatus.Optimal) { - Console.WriteLine("Optimal Schedule Length: " + solver.ObjectiveValue); - Console.WriteLine("Task 0 starts at " + solver.Value(start_0)); - Console.WriteLine("Task 1 starts at " + solver.Value(start_1)); - Console.WriteLine("Task 2 starts at " + solver.Value(start_2)); + if (status == CpSolverStatus.Optimal) + { + Console.WriteLine("Optimal Schedule Length: " + solver.ObjectiveValue); + Console.WriteLine("Task 0 starts at " + solver.Value(start_0)); + Console.WriteLine("Task 1 starts at " + solver.Value(start_1)); + Console.WriteLine("Task 2 starts at " + solver.Value(start_2)); + } } - } } ``` @@ -1079,144 +1080,159 @@ using System; using System.Collections.Generic; using Google.OrTools.Sat; -public class RankingSampleSat { - static void RankTasks(CpModel model, - IntVar[] starts, - ILiteral[] presences, - IntVar[] ranks) { - int num_tasks = starts.Length; +public class RankingSampleSat +{ + static void RankTasks(CpModel model, IntVar[] starts, ILiteral[] presences, IntVar[] ranks) + { + int num_tasks = starts.Length; - // Creates precedence variables between pairs of intervals. - ILiteral[,] precedences = new ILiteral[num_tasks, num_tasks]; - for (int i = 0; i < num_tasks; ++i) { - for (int j = 0; j < num_tasks; ++j) { - if (i == j) { - precedences[i, i] = presences[i]; - } else { - IntVar prec = model.NewBoolVar(String.Format("{0} before {1}", i, j)); - precedences[i, j] = prec; - model.Add(starts[i] < starts[j]).OnlyEnforceIf(prec); + // Creates precedence variables between pairs of intervals. + ILiteral[,] precedences = new ILiteral[num_tasks, num_tasks]; + for (int i = 0; i < num_tasks; ++i) + { + for (int j = 0; j < num_tasks; ++j) + { + if (i == j) + { + precedences[i, i] = presences[i]; + } + else + { + IntVar prec = model.NewBoolVar(String.Format("{0} before {1}", i, j)); + precedences[i, j] = prec; + model.Add(starts[i] < starts[j]).OnlyEnforceIf(prec); + } + } } - } - } - // Treats optional intervals. - for (int i = 0; i < num_tasks - 1; ++i) { - for (int j = i + 1; j < num_tasks; ++j) { - List tmp_array = new List(); - tmp_array.Add(precedences[i, j]); - tmp_array.Add(precedences[j, i]); - tmp_array.Add(presences[i].Not()); - // Makes sure that if i is not performed, all precedences are false. - model.AddImplication(presences[i].Not(), precedences[i, j].Not()); - model.AddImplication(presences[i].Not(), precedences[j, i].Not()); - tmp_array.Add(presences[j].Not()); - // Makes sure that if j is not performed, all precedences are false. - model.AddImplication(presences[j].Not(), precedences[i, j].Not()); - model.AddImplication(presences[j].Not(), precedences[j, i].Not()); - // The following bool_or will enforce that for any two intervals: - // i precedes j or j precedes i or at least one interval is not - // performed. - model.AddBoolOr(tmp_array); - // Redundant constraint: it propagates early that at most one precedence - // is true. - model.AddImplication(precedences[i, j], precedences[j, i].Not()); - model.AddImplication(precedences[j, i], precedences[i, j].Not()); - } - } - - // Links precedences and ranks. - for (int i = 0; i < num_tasks; ++i) { - IntVar[] tmp_array = new IntVar[num_tasks]; - for (int j = 0; j < num_tasks; ++j) { - tmp_array[j] = (IntVar)precedences[j, i]; - } - model.Add(ranks[i] == LinearExpr.Sum(tmp_array) - 1); - } - } - - static void Main() { - CpModel model = new CpModel(); - // Three weeks. - int horizon = 100; - int num_tasks = 4; - - IntVar[] starts = new IntVar[num_tasks]; - IntVar[] ends = new IntVar[num_tasks]; - IntervalVar[] intervals = new IntervalVar[num_tasks]; - ILiteral[] presences = new ILiteral[num_tasks]; - IntVar[] ranks = new IntVar[num_tasks]; - - IntVar true_var = model.NewConstant(1); - - // Creates intervals, half of them are optional. - for (int t = 0; t < num_tasks; ++t) { - starts[t] = model.NewIntVar(0, horizon, String.Format("start_{0}", t)); - int duration = t + 1; - ends[t] = model.NewIntVar(0, horizon, String.Format("end_{0}", t)); - if (t < num_tasks / 2) { - intervals[t] = model.NewIntervalVar(starts[t], duration, ends[t], - String.Format("interval_{0}", t)); - presences[t] = true_var; - } else { - presences[t] = model.NewBoolVar(String.Format("presence_{0}", t)); - intervals[t] = model.NewOptionalIntervalVar( - starts[t], duration, ends[t], presences[t], - String.Format("o_interval_{0}", t)); - } - - // Ranks = -1 if and only if the tasks is not performed. - ranks[t] = - model.NewIntVar(-1, num_tasks - 1, String.Format("rank_{0}", t)); - } - - // Adds NoOverlap constraint. - model.AddNoOverlap(intervals); - - // Adds ranking constraint. - RankTasks(model, starts, presences, ranks); - - // Adds a constraint on ranks. - model.Add(ranks[0] < ranks[1]); - - // Creates makespan variable. - IntVar makespan = model.NewIntVar(0, horizon, "makespan"); - for (int t = 0; t < num_tasks; ++t) { - model.Add(ends[t] <= makespan).OnlyEnforceIf(presences[t]); - } - // Minimizes makespan - fixed gain per tasks performed. - // As the fixed cost is less that the duration of the last interval, - // the solver will not perform the last interval. - IntVar[] presences_as_int_vars = new IntVar[num_tasks]; - for (int t = 0; t < num_tasks; ++t) { - presences_as_int_vars[t] = (IntVar)presences[t]; - } - model.Minimize(2 * makespan - 7 * LinearExpr.Sum(presences_as_int_vars)); - - // Creates a solver and solves the model. - CpSolver solver = new CpSolver(); - CpSolverStatus status = solver.Solve(model); - - if (status == CpSolverStatus.Optimal) { - Console.WriteLine(String.Format("Optimal cost: {0}", - solver.ObjectiveValue)); - Console.WriteLine(String.Format("Makespan: {0}", solver.Value(makespan))); - for (int t = 0; t < num_tasks; ++t) { - if (solver.BooleanValue(presences[t])) { - Console.WriteLine(String.Format( - "Task {0} starts at {1} with rank {2}", - t, solver.Value(starts[t]), solver.Value(ranks[t]))); - } else { - Console.WriteLine(String.Format( - "Task {0} in not performed and ranked at {1}", t, - solver.Value(ranks[t]))); + // Treats optional intervals. + for (int i = 0; i < num_tasks - 1; ++i) + { + for (int j = i + 1; j < num_tasks; ++j) + { + List tmp_array = new List(); + tmp_array.Add(precedences[i, j]); + tmp_array.Add(precedences[j, i]); + tmp_array.Add(presences[i].Not()); + // Makes sure that if i is not performed, all precedences are false. + model.AddImplication(presences[i].Not(), precedences[i, j].Not()); + model.AddImplication(presences[i].Not(), precedences[j, i].Not()); + tmp_array.Add(presences[j].Not()); + // Makes sure that if j is not performed, all precedences are false. + model.AddImplication(presences[j].Not(), precedences[i, j].Not()); + model.AddImplication(presences[j].Not(), precedences[j, i].Not()); + // The following bool_or will enforce that for any two intervals: + // i precedes j or j precedes i or at least one interval is not + // performed. + model.AddBoolOr(tmp_array); + // Redundant constraint: it propagates early that at most one precedence + // is true. + model.AddImplication(precedences[i, j], precedences[j, i].Not()); + model.AddImplication(precedences[j, i], precedences[i, j].Not()); + } + } + + // Links precedences and ranks. + for (int i = 0; i < num_tasks; ++i) + { + IntVar[] tmp_array = new IntVar[num_tasks]; + for (int j = 0; j < num_tasks; ++j) + { + tmp_array[j] = (IntVar)precedences[j, i]; + } + model.Add(ranks[i] == LinearExpr.Sum(tmp_array) - 1); + } + } + + static void Main() + { + CpModel model = new CpModel(); + // Three weeks. + int horizon = 100; + int num_tasks = 4; + + IntVar[] starts = new IntVar[num_tasks]; + IntVar[] ends = new IntVar[num_tasks]; + IntervalVar[] intervals = new IntervalVar[num_tasks]; + ILiteral[] presences = new ILiteral[num_tasks]; + IntVar[] ranks = new IntVar[num_tasks]; + + IntVar true_var = model.NewConstant(1); + + // Creates intervals, half of them are optional. + for (int t = 0; t < num_tasks; ++t) + { + starts[t] = model.NewIntVar(0, horizon, String.Format("start_{0}", t)); + int duration = t + 1; + ends[t] = model.NewIntVar(0, horizon, String.Format("end_{0}", t)); + if (t < num_tasks / 2) + { + intervals[t] = model.NewIntervalVar(starts[t], duration, ends[t], String.Format("interval_{0}", t)); + presences[t] = true_var; + } + else + { + presences[t] = model.NewBoolVar(String.Format("presence_{0}", t)); + intervals[t] = model.NewOptionalIntervalVar(starts[t], duration, ends[t], presences[t], + String.Format("o_interval_{0}", t)); + } + + // Ranks = -1 if and only if the tasks is not performed. + ranks[t] = model.NewIntVar(-1, num_tasks - 1, String.Format("rank_{0}", t)); + } + + // Adds NoOverlap constraint. + model.AddNoOverlap(intervals); + + // Adds ranking constraint. + RankTasks(model, starts, presences, ranks); + + // Adds a constraint on ranks. + model.Add(ranks[0] < ranks[1]); + + // Creates makespan variable. + IntVar makespan = model.NewIntVar(0, horizon, "makespan"); + for (int t = 0; t < num_tasks; ++t) + { + model.Add(ends[t] <= makespan).OnlyEnforceIf(presences[t]); + } + // Minimizes makespan - fixed gain per tasks performed. + // As the fixed cost is less that the duration of the last interval, + // the solver will not perform the last interval. + IntVar[] presences_as_int_vars = new IntVar[num_tasks]; + for (int t = 0; t < num_tasks; ++t) + { + presences_as_int_vars[t] = (IntVar)presences[t]; + } + model.Minimize(2 * makespan - 7 * LinearExpr.Sum(presences_as_int_vars)); + + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + CpSolverStatus status = solver.Solve(model); + + if (status == CpSolverStatus.Optimal) + { + Console.WriteLine(String.Format("Optimal cost: {0}", solver.ObjectiveValue)); + Console.WriteLine(String.Format("Makespan: {0}", solver.Value(makespan))); + for (int t = 0; t < num_tasks; ++t) + { + if (solver.BooleanValue(presences[t])) + { + Console.WriteLine(String.Format("Task {0} starts at {1} with rank {2}", t, solver.Value(starts[t]), + solver.Value(ranks[t]))); + } + else + { + Console.WriteLine( + String.Format("Task {0} in not performed and ranked at {1}", t, solver.Value(ranks[t]))); + } + } + } + else + { + Console.WriteLine(String.Format("Solver exited with nonoptimal status: {0}", status)); } - } - } else { - Console.WriteLine( - String.Format("Solver exited with nonoptimal status: {0}", status)); } - } } ``` diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md index d3951fb76a..0e8d61f0a7 100644 --- a/ortools/sat/doc/solver.md +++ b/ortools/sat/doc/solver.md @@ -27,7 +27,7 @@ * [Java code](#java-code-2) * [C# code](#c-code-5) - + @@ -69,7 +69,7 @@ def SolveWithTimeLimitSampleSat(): status = solver.Solve(model) - if status == cp_model.FEASIBLE: + if status == cp_model.OPTIMAL: print('x = %i' % solver.Value(x)) print('y = %i' % solver.Value(y)) print('z = %i' % solver.Value(z)) @@ -110,7 +110,7 @@ void SolveWithTimeLimitSampleSat() { const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model); LOG(INFO) << CpSolverResponseStats(response); - if (response.status() == CpSolverStatus::FEASIBLE) { + if (response.status() == CpSolverStatus::OPTIMAL) { LOG(INFO) << " x = " << SolutionIntegerValue(response, x); LOG(INFO) << " y = " << SolutionIntegerValue(response, y); LOG(INFO) << " z = " << SolutionIntegerValue(response, z); @@ -176,33 +176,36 @@ Parameters must be passed as string to the solver. using System; using Google.OrTools.Sat; -public class SolveWithTimeLimitSampleSat { - static void Main() { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; +public class SolveWithTimeLimitSampleSat +{ + static void Main() + { + // 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); + 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(); + // 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"; + // 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); + CpSolverStatus status = solver.Solve(model); - if (status == CpSolverStatus.Optimal) { - Console.WriteLine("x = " + solver.Value(x)); - Console.WriteLine("y = " + solver.Value(y)); - Console.WriteLine("z = " + solver.Value(z)); + if (status == CpSolverStatus.Optimal) + { + Console.WriteLine("x = " + solver.Value(x)); + Console.WriteLine("y = " + solver.Value(y)); + Console.WriteLine("z = " + solver.Value(z)); + } } - } } ``` @@ -394,60 +397,60 @@ public class SolveAndPrintIntermediateSolutionsSampleSat { 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_) +public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback +{ + public VarArraySolutionPrinterWithObjective(IntVar[] variables) { - Console.WriteLine( - String.Format(" {0} = {1}", v.ShortString(), Value(v))); + variables_ = variables; } - solution_count_++; - } - public int SolutionCount() { - return solution_count_; - } + 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_++; + } - private int solution_count_; - private IntVar[] variables_; + public int SolutionCount() + { + return solution_count_; + } + + private int solution_count_; + private IntVar[] variables_; } -public class SolveAndPrintIntermediateSolutionsSampleSat { - static void Main() { - // Creates the model. - CpModel model = new CpModel(); +public class SolveAndPrintIntermediateSolutionsSampleSat +{ + static void Main() + { + // Creates the model. + CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; + // 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"); + 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); + // Adds a different constraint. + model.Add(x != y); - // Maximizes a linear combination of variables. - model.Maximize(x + 2 * y + 3 * z); + // 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.SolveWithSolutionCallback(model, cb); + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + VarArraySolutionPrinterWithObjective cb = new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z }); + solver.SolveWithSolutionCallback(model, cb); - Console.WriteLine(String.Format("Number of solutions found: {0}", - cb.SolutionCount())); - } + Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); + } } ``` @@ -640,56 +643,58 @@ As in Python, CpSolver.SearchAllSolutions() must be called. using System; using Google.OrTools.Sat; -public class VarArraySolutionPrinter : CpSolverSolutionCallback { - public VarArraySolutionPrinter(IntVar[] variables) { - variables_ = variables; - } - - public override void OnSolutionCallback() { +public class VarArraySolutionPrinter : CpSolverSolutionCallback +{ + public VarArraySolutionPrinter(IntVar[] variables) { - 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_++; + variables_ = variables; } - } - public int SolutionCount() { - return solution_count_; - } + 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_++; + } + } - private int solution_count_; - private IntVar[] variables_; + public int SolutionCount() + { + return solution_count_; + } + + private int solution_count_; + private IntVar[] variables_; } -public class SearchForAllSolutionsSampleSat { - static void Main() { - // Creates the model. - CpModel model = new CpModel(); +public class SearchForAllSolutionsSampleSat +{ + static void Main() + { + // Creates the model. + CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; + // 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"); + 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); + // 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); + // 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())); - } + Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); + } } ``` @@ -902,56 +907,57 @@ CpSolverSolutionCallback.OnSolutionCallback(). using System; using Google.OrTools.Sat; -public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { - public VarArraySolutionPrinterWithLimit(IntVar[] variables, int solution_limit) { - variables_ = variables; - solution_limit_ = solution_limit; - } - - public override void OnSolutionCallback() { - Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", - solution_count_, WallTime())); - foreach (IntVar v in variables_) +public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback +{ + public VarArraySolutionPrinterWithLimit(IntVar[] variables, int solution_limit) { - Console.WriteLine( - String.Format(" {0} = {1}", v.ShortString(), Value(v))); + variables_ = variables; + solution_limit_ = solution_limit; } - solution_count_++; - if (solution_count_ >= solution_limit_) { - Console.WriteLine( - String.Format("Stopping search after {0} solutions", - solution_limit_)); - StopSearch(); + + 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_++; + if (solution_count_ >= solution_limit_) + { + Console.WriteLine(String.Format("Stopping search after {0} solutions", solution_limit_)); + StopSearch(); + } } - } - public int SolutionCount() { - return solution_count_; - } + public int SolutionCount() + { + return solution_count_; + } - private int solution_count_; - private IntVar[] variables_; - private int solution_limit_; + private int solution_count_; + private IntVar[] variables_; + private int solution_limit_; } -public class StopAfterNSolutionsSampleSat { - static void Main() { - // Creates the model. - CpModel model = new CpModel(); - // Creates the variables. - int num_vals = 3; +public class StopAfterNSolutionsSampleSat +{ + static void Main() + { + // 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"); + 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 a solver and solves the model. - CpSolver solver = new CpSolver(); - VarArraySolutionPrinterWithLimit cb = - new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5); - solver.SearchAllSolutions(model, cb); - Console.WriteLine(String.Format("Number of solutions found: {0}", - cb.SolutionCount())); - } + // Creates a solver and solves the model. + CpSolver solver = new CpSolver(); + VarArraySolutionPrinterWithLimit cb = new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5); + solver.SearchAllSolutions(model, cb); + Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); + } } ```