From fb309a252737fe4fb69051df3638dcad35d4d02c Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 1 Aug 2018 10:17:48 -0700 Subject: [PATCH] [API Change] Remove support for optional int vars in reservoir, use parallel array of boolean literals to indicate presence --- ortools/dotnet/OrTools/sat/CpModel.cs | 25 +++--- ortools/sat/cp_model.proto | 11 ++- ortools/sat/cp_model_checker.cc | 13 ++- ortools/sat/cp_model_expand.cc | 115 +++++++++++++++++--------- ortools/sat/python/cp_model.py | 18 +++- 5 files changed, 127 insertions(+), 55 deletions(-) diff --git a/ortools/dotnet/OrTools/sat/CpModel.cs b/ortools/dotnet/OrTools/sat/CpModel.cs index 7a79762e79..932f8cb6b1 100644 --- a/ortools/dotnet/OrTools/sat/CpModel.cs +++ b/ortools/dotnet/OrTools/sat/CpModel.cs @@ -490,9 +490,9 @@ public class CpModel return ct; } - public Constraint AddReservoirConstraint(IEnumerable times, - IEnumerable demands, - long min_level, long max_level) + public Constraint AddReservoirConstraint(IEnumerable times, + IEnumerable demands, + long min_level, long max_level) { Constraint ct = new Constraint(model_); ReservoirConstraintProto res = new ReservoirConstraintProto(); @@ -500,18 +500,19 @@ public class CpModel { res.Times.Add(var.Index); } - foreach (long d in demands) + foreach (I d in demands) { - res.Demands.Add(d); + res.Demands.Add(Convert.ToInt64(d)); } ct.Proto.Reservoir = res; return ct; } - public Constraint AddReservoirConstraint(IEnumerable times, - IEnumerable demands, - long min_level, long max_level) + public Constraint AddReservoirConstraint(IEnumerable times, + IEnumerable demands, + IEnumerable actives, + long min_level, long max_level) { Constraint ct = new Constraint(model_); ReservoirConstraintProto res = new ReservoirConstraintProto(); @@ -519,9 +520,13 @@ public class CpModel { res.Times.Add(var.Index); } - foreach (int d in demands) + foreach (I d in demands) { - res.Demands.Add(d); + res.Demands.Add(Convert.ToInt64(d)); + } + foreach (IntVar var in actives) + { + res.Actives.Add(var.Index); } ct.Proto.Reservoir = res; diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 03ac6e28e8..2918f59410 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -143,18 +143,23 @@ message CumulativeConstraintProto { // Maintain a reservoir level within bounds. The water level starts at 0, and at // any time >= 0, it must be within min_level, and max_level. Furthermore, this // constraints expect all times variables to be >= 0. -// If the variable times[i] is assigned a value t, then the current level -// changes by demands[i] (which is constant) at the time t. +// If the variable actives[i] is true, and if the variable times[i] is assigned +// a value t, then the current level changes by demands[i] (which is constant) +// at the time t. // // Note that level min can be > 0, or level max can be < 0. It just forces // some demands to be executed at time 0 to make sure that we are within those // bounds with the executed demands. Therefore, at any time t >= 0: -// sum(demands[i] if times[i] <= t) in [min_level, max_level] +// sum(demands[i] * actives[i] if times[i] <= t) in [min_level, max_level] +// The array of boolean variables 'actives', if defined, indicates which actions +// are actually performed. If this array is not defined, then it is assumed that +// all actions will be performed. message ReservoirConstraintProto { int64 min_level = 1; int64 max_level = 2; repeated int32 times = 3; repeated int64 demands = 4; + repeated int32 actives = 5; } // The circuit constraint is defined on a graph where the arc presence are diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 0918bf7213..7ee9fa19ff 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -195,6 +195,14 @@ std::string ValidateReservoirConstraint(const CpModelProto& model, ProtobufDebugString(ct); } } + if (ct.reservoir().actives_size() > 0 && + ct.reservoir().actives_size() != ct.reservoir().times_size()) { + return "Wrong array length of actives variables"; + } + if (ct.reservoir().demands_size() > 0 && + ct.reservoir().demands_size() != ct.reservoir().times_size()) { + return "Wrong array length of demands variables"; + } return ""; } @@ -683,13 +691,16 @@ class ConstraintChecker { const int64 max_level = ct.reservoir().max_level(); std::map deltas; deltas[0] = 0; + const bool has_active_variables = ct.reservoir().actives_size() > 0; for (int i = 0; i < num_variables; i++) { const int64 time = Value(ct.reservoir().times(i)); if (time < 0) { VLOG(1) << "reservoir times(" << i << ") is negative."; return false; } - deltas[time] += ct.reservoir().demands(i); + if (!has_active_variables || Value(ct.reservoir().actives(i)) == 1) { + deltas[time] += ct.reservoir().demands(i); + } } int64 current_level = 0; for (const auto& delta : deltas) { diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 92f989527e..88074d76f7 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -30,6 +30,7 @@ struct ExpansionHelper { CpModelProto expanded_proto; std::unordered_map, int> precedence_cache; std::map statistics; + static const int kAlwaysTrue = kint32min; // a => b. void AddImplication(int a, int b) { @@ -57,35 +58,33 @@ struct ExpansionHelper { int AddBoolVar() { return AddIntVar(0, 1); } - int VariableIsOptional(int index) const { - return expanded_proto.variables(index).enforcement_literal_size() > 0; + void AddBoolOr(const std::vector& literals) { + BoolArgumentProto* const bool_or = + expanded_proto.add_constraints()->mutable_bool_or(); + for (const int lit : literals) { + bool_or->add_literals(lit); + } } - int VariableEnforcementLiteral(int index) const { - DCHECK(VariableIsOptional(index)); - return expanded_proto.variables(index).enforcement_literal(0); - } - - // lesseq_0 <=> (x <= 0 && x performed). - void AddReifiedLesssOrEqualThanZero(int lesseq_0, int x) { + // lesseq_0 <=> (x <= 0 && lit is true). + void AddReifiedLessOrEqualThanZero(int lesseq_0, int x, int lit) { AddImplyInDomain(lesseq_0, x, kint64min, 0); - AddImplyInDomain(NegatedRef(lesseq_0), x, 1, kint64max); - if (VariableIsOptional(x)) { - AddImplication(lesseq_0, VariableEnforcementLiteral(x)); + if (lit == kAlwaysTrue) { + AddImplyInDomain(NegatedRef(lesseq_0), x, 1, kint64max); + } else { + // conjunction <=> lit && not(lesseq_0). + const int conjunction = AddBoolVar(); + AddImplication(conjunction, lit); + AddImplication(conjunction, NegatedRef(lesseq_0)); + AddBoolOr({NegatedRef(lit), lesseq_0, conjunction}); + + AddImplyInDomain(conjunction, x, 1, kint64max); } } - // x_lesseq_y <=> (x <= y && x enforced && y enforced). - void AddReifiedPrecedence(int x_lesseq_y, int x, int y) { - // x_lesseq_y => x enforced && y enforced - if (VariableIsOptional(x)) { - AddImplication(x_lesseq_y, VariableEnforcementLiteral(x)); - } - if (VariableIsOptional(y)) { - AddImplication(x_lesseq_y, VariableEnforcementLiteral(y)); - } - - // x_lesseq_y => (x <= y) + // x_lesseq_y <=> (x <= y && l_x is true && l_y is true). + void AddReifiedPrecedence(int x_lesseq_y, int x, int y, int l_x, int l_y) { + // x_lesseq_y => (x <= y) && l_x is true && l_y is true. ConstraintProto* const lesseq = expanded_proto.add_constraints(); lesseq->add_enforcement_literal(x_lesseq_y); lesseq->mutable_linear()->add_vars(x); @@ -94,16 +93,41 @@ struct ExpansionHelper { lesseq->mutable_linear()->add_coeffs(1); lesseq->mutable_linear()->add_domain(0); lesseq->mutable_linear()->add_domain(kint64max); + if (l_x != kAlwaysTrue) { + AddImplication(x_lesseq_y, l_x); + } + if (l_y != kAlwaysTrue) { + AddImplication(x_lesseq_y, l_y); + } - // Not(x_lesseq_y) => (x > y) + // Not(x_lesseq_y) && l_x && l_y => (x > y) ConstraintProto* const greater = expanded_proto.add_constraints(); - greater->add_enforcement_literal(NegatedRef(x_lesseq_y)); greater->mutable_linear()->add_vars(x); greater->mutable_linear()->add_vars(y); greater->mutable_linear()->add_coeffs(-1); greater->mutable_linear()->add_coeffs(1); greater->mutable_linear()->add_domain(kint64min); greater->mutable_linear()->add_domain(-1); + // Manages enforcement literal. + if (l_x == kAlwaysTrue && l_y == kAlwaysTrue) { + greater->add_enforcement_literal(NegatedRef(x_lesseq_y)); + } else { + // conjunction <=> l_x && l_y && not(x_lesseq_y). + const int conjunction = AddBoolVar(); + std::vector literals = {conjunction, x_lesseq_y}; + AddImplication(conjunction, NegatedRef(x_lesseq_y)); + if (l_x != kAlwaysTrue) { + AddImplication(conjunction, l_x); + literals.push_back(NegatedRef(l_x)); + } + if (l_y != kAlwaysTrue) { + AddImplication(conjunction, l_y); + literals.push_back(NegatedRef(l_y)); + } + AddBoolOr(literals); + + greater->add_enforcement_literal(conjunction); + } } }; @@ -112,6 +136,19 @@ void ExpandReservoir(ConstraintProto* ct, ExpansionHelper* helper) { const int num_variables = reservoir.times_size(); CpModelProto& expanded_proto = helper->expanded_proto; + auto is_optional = [&expanded_proto, &reservoir](int index) { + if (reservoir.actives_size() == 0) return false; + const int literal = reservoir.actives(index); + const int ref = PositiveRef(literal); + const IntegerVariableProto& var_proto = expanded_proto.variables(ref); + return var_proto.domain_size() != 2 || + var_proto.domain(0) != var_proto.domain(1); + }; + auto active = [&reservoir, &helper](int index) { + if (reservoir.actives_size() == 0) return helper->kAlwaysTrue; + return reservoir.actives(index); + }; + int num_positives = 0; int num_negatives = 0; for (const int64 demand : reservoir.demands()) { @@ -136,21 +173,21 @@ void ExpandReservoir(ConstraintProto* ct, ExpansionHelper* helper) { helper->precedence_cache[p] = i_lesseq_j; const int j_lesseq_i = helper->AddBoolVar(); helper->precedence_cache[rev_p] = j_lesseq_i; - helper->AddReifiedPrecedence(i_lesseq_j, time_i, time_j); - helper->AddReifiedPrecedence(j_lesseq_i, time_j, time_i); + helper->AddReifiedPrecedence(i_lesseq_j, time_i, time_j, active(i), + active(j)); + helper->AddReifiedPrecedence(j_lesseq_i, time_j, time_i, active(j), + active(i)); // Consistency. This is redundant but should improves performance. auto* const bool_or = expanded_proto.add_constraints()->mutable_bool_or(); bool_or->add_literals(i_lesseq_j); bool_or->add_literals(j_lesseq_i); - if (helper->VariableIsOptional(time_i)) { - bool_or->add_literals( - NegatedRef(helper->VariableEnforcementLiteral(time_i))); + if (is_optional(i)) { + bool_or->add_literals(NegatedRef(reservoir.actives(i))); } - if (helper->VariableIsOptional(time_j)) { - bool_or->add_literals( - NegatedRef(helper->VariableEnforcementLiteral(time_j))); + if (is_optional(j)) { + bool_or->add_literals(NegatedRef(reservoir.actives(j))); } } } @@ -176,9 +213,8 @@ void ExpandReservoir(ConstraintProto* ct, ExpansionHelper* helper) { CapSub(reservoir.min_level(), demand_i)); level->mutable_linear()->add_domain( CapSub(reservoir.max_level(), demand_i)); - if (helper->VariableIsOptional(time_i)) { - level->add_enforcement_literal( - helper->VariableEnforcementLiteral(time_i)); + if (is_optional(i)) { + level->add_enforcement_literal(reservoir.actives(i)); } } } else { @@ -187,11 +223,10 @@ void ExpandReservoir(ConstraintProto* ct, ExpansionHelper* helper) { int64 fixed_demand = 0; auto* const sum = expanded_proto.add_constraints()->mutable_linear(); for (int i = 0; i < num_variables; ++i) { - const int time = reservoir.times(i); const int64 demand = reservoir.demands(i); if (demand == 0) continue; - if (helper->VariableIsOptional(time)) { - sum->add_vars(helper->VariableEnforcementLiteral(time)); + if (is_optional(i)) { + sum->add_vars(reservoir.actives(i)); sum->add_coeffs(demand); } else { fixed_demand += demand; @@ -209,7 +244,7 @@ void ExpandReservoir(ConstraintProto* ct, ExpansionHelper* helper) { for (int i = 0; i < num_variables; ++i) { const int time_i = reservoir.times(i); const int lesseq_0 = helper->AddBoolVar(); - helper->AddReifiedLesssOrEqualThanZero(lesseq_0, time_i); + helper->AddReifiedLessOrEqualThanZero(lesseq_0, time_i, active(i)); initial_ct->add_vars(lesseq_0); initial_ct->add_coeffs(reservoir.demands(i)); } diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py index 2ca7b9afae..8d1c225402 100644 --- a/ortools/sat/python/cp_model.py +++ b/ortools/sat/python/cp_model.py @@ -437,7 +437,11 @@ class Constraint(object): self.__constraint = constraints.add() def OnlyEnforceIf(self, boolvar): - self.__constraint.enforcement_literal.append(boolvar.Index()) + if isinstance(boolvar, numbers.Integral) and boolvar == 1: + # Always true. Do nothing. + pass + else: + self.__constraint.enforcement_literal.append(boolvar.Index()) def Index(self): return self.__index @@ -725,6 +729,18 @@ class CpModel(object): model_ct.reservoir.max_level = max_level return ct + def AddReservoirConstraintWithActive(self, times, demands, actives, min_level, + max_level): + """Adds Reservoir(times, demands, actives, min_level, max_level).""" + ct = Constraint(self.__model.constraints) + model_ct = self.__model.constraints[ct.Index()] + model_ct.reservoir.times.extend([self.GetOrMakeIndex(x) for x in times]) + model_ct.reservoir.demands.extend(demands) + model_ct.reservoir.actives.extend(actives) + model_ct.reservoir.min_level = min_level + model_ct.reservoir.max_level = max_level + return ct + def AddMapDomain(self, var, bool_var_array, offset=0): """Creates var == i + offset <=> bool_var_array[i] == true for all i."""