From e3eb35132b7df8b96b3a0c8909fb1e15af256e71 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 21 Apr 2022 16:28:13 +0200 Subject: [PATCH] [CP-SAT] add more CpModel C++ methods; fix #3248; fix #3251; specify restrictions in cp_model.proto --- ortools/sat/cp_model.h | 37 ++++++++++++++++++------------------- ortools/sat/cp_model.proto | 4 ++++ ortools/sat/timetable.cc | 12 ++++++------ 3 files changed, 28 insertions(+), 25 deletions(-) diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index 622019b01f..4fb8603279 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -19,15 +19,15 @@ * print out the solution. * \code CpModelBuilder cp_model; - Domain all_animals(0, 20); - IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits"); - IntVar pheasants = cp_model.NewIntVar(all_animals).WithName("pheasants"); + const Domain all_animals(0, 20); + const IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits"); + const IntVar pheasants = cp_model.NewIntVar(all_animals).WithName("pheasants"); cp_model.AddEquality(rabbits + pheasants, 20); cp_model.AddEquality(4 * rabbits + 2 * pheasants, 56); const CpSolverResponse response = Solve(cp_model.Build()); - if (response.status() == CpSolverStatus::FEASIBLE) { + if (response.status() == CpSolverStatus::OPTIMAL) { LOG(INFO) << SolutionIntegerValue(response, rabbits) << " rabbits, and " << SolutionIntegerValue(response, pheasants) << " pheasants."; @@ -314,13 +314,7 @@ std::ostream& operator<<(std::ostream& os, const LinearExpr& e); /** * A dedicated container for linear expressions with double coefficients. - * - * This class helps building and manipulating linear expressions. - * Note that Not(x) will be silently transformed into 1 - x when added to the - * linear expression. - * - * Furthermore, static methods allows sums and scalar products, with or without - * an additional constant. + * This is currently only usable to define a floating point objective. * * Usage: * \code @@ -531,7 +525,7 @@ class Constraint { * (controlled by a literal l) and its negation (controlled by the negation of * l). * - * Important: as of September 2018, only a few constraint support enforcement: + * [Important] currently, only a few constraints support enforcement: * - bool_or, bool_and, linear: fully supported. * - interval: only support a single enforcement literal. * - other: no support (but can be added on a per-demand basis). @@ -777,7 +771,7 @@ class CpModelBuilder { /// Adds the constraint that at least one of the literals must be true. Constraint AddBoolOr(absl::Span literals); - /// Same as AddBoolOr. Sum literals >= 1. + /// Same as AddBoolOr(). Sum literals >= 1. Constraint AddAtLeastOne(absl::Span literals); /// At most one literal is true. Sum literals <= 1. @@ -797,6 +791,12 @@ class CpModelBuilder { return AddBoolOr({a.Not(), b}); } + /// Adds implication: if all lhs vars are true then all rhs vars must be true. + Constraint AddImplication(absl::Span lhs, + absl::Span rhs) { + return AddBoolAnd(rhs).OnlyEnforceIf(lhs); + } + /// Adds left == right. Constraint AddEquality(const LinearExpr& left, const LinearExpr& right); @@ -1029,15 +1029,15 @@ class CpModelBuilder { /// Adds a linear minimization objective. void Minimize(const LinearExpr& expr); - /// Adds a linear minimization objective after rescaling of the double - /// coefficients. + /// Adds a linear floating point minimization objective. + /// Note that the coefficients will be internally scaled to integer. void Minimize(const DoubleLinearExpr& expr); /// Adds a linear maximization objective. void Maximize(const LinearExpr& expr); - /// Adds a linear maximization objective after rescaling of the double - /// coefficients. + /// Adds a linear floating point maximization objective. + /// Note that the coefficients will be internally scaled to integer. void Maximize(const DoubleLinearExpr& expr); /// Adds a decision strategy on a list of integer variables. @@ -1070,8 +1070,7 @@ class CpModelBuilder { /// Remove all assumptions from the model. void ClearAssumptions(); - const CpModelProto& Build() const { return Proto(); } - + const CpModelProto& Build() const { return cp_model_; } const CpModelProto& Proto() const { return cp_model_; } CpModelProto* MutableProto() { return &cp_model_; } diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 6b8ac4b2a1..59db9f96c1 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -150,6 +150,10 @@ message NoOverlap2DConstraintProto { // a capacity. Note that intervals are interpreted as [start, end) and as // such intervals like [2,3) and [3,4) do not overlap for the point of view of // this constraint. Moreover, intervals of size zero are ignored. +// +// All demands must not contain any negative value in their domains. This is +// checked at validation. The capacity can currently contains negative values, +// but it will be propagated to >= 0 right away. message CumulativeConstraintProto { LinearExpressionProto capacity = 1; repeated int32 intervals = 2; diff --git a/ortools/sat/timetable.cc b/ortools/sat/timetable.cc index ad99a27e17..6f1149e95d 100644 --- a/ortools/sat/timetable.cc +++ b/ortools/sat/timetable.cc @@ -366,7 +366,7 @@ bool TimeTablingPerTask::BuildProfile() { profile_.clear(); // Start and height of the highest profile rectangle. - profile_max_height_ = kMinIntegerValue; + profile_max_height_ = 0; IntegerValue max_height_start = kMinIntegerValue; // Add a sentinel to simplify the algorithm. @@ -435,8 +435,7 @@ void TimeTablingPerTask::ReverseProfile() { bool TimeTablingPerTask::SweepAllTasks() { // Tasks with a lower or equal demand will not be pushed. - const IntegerValue demand_threshold( - CapSub(CapacityMax().value(), profile_max_height_.value())); + const IntegerValue demand_threshold = CapacityMax() - profile_max_height_; // TODO(user): On some problem, a big chunk of the time is spend just checking // these conditions below because it requires indirect memory access to fetch @@ -562,6 +561,10 @@ bool TimeTablingPerTask::UpdateStartingTime(int task_id, IntegerValue left, IntegerValue right) { helper_->ClearReason(); AddProfileReason(task_id, left, right); + if (capacity_.var != kNoIntegerVariable) { + helper_->MutableIntegerReason()->push_back( + integer_trail_->UpperBoundAsLiteral(capacity_.var)); + } // State of the task to be pushed. helper_->AddEndMinReason(task_id, left + 1); @@ -655,9 +658,6 @@ bool TimeTablingPerTask::IncreaseCapacity(IntegerValue time, if (capacity_.var == kNoIntegerVariable) { return helper_->ReportConflict(); } - - helper_->MutableIntegerReason()->push_back( - integer_trail_->UpperBoundAsLiteral(capacity_.var)); return helper_->PushIntegerLiteral(capacity_.GreaterOrEqual(new_min)); }