always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[API Change] Remove support for optional int vars in reservoir, use parallel array of boolean literals to indicate presence

Browse Source
This commit is contained in:
Laurent Perron
2018-08-01 10:17:48 -07:00
parent 3e013bb5be
commit fb309a2527
5 changed files with 127 additions and 55 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
ortools/dotnet/OrTools/sat/CpModel.cs
View File

@@ -490,9 +490,9 @@ public class CpModel
return ct;
}
public Constraint AddReservoirConstraint(IEnumerable<IntVar> times,
IEnumerable<long> demands,
long min_level, long max_level)
public Constraint AddReservoirConstraint<I>(IEnumerable<IntVar> times,
IEnumerable<I> 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<IntVar> times,
IEnumerable<int> demands,
long min_level, long max_level)
public Constraint AddReservoirConstraint<I>(IEnumerable<IntVar> times,
IEnumerable<I> demands,
IEnumerable<IntVar> 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;

11
ortools/sat/cp_model.proto
View File

@@ -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

13
ortools/sat/cp_model_checker.cc
View File

@@ -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<int64, int64> 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) {

115
ortools/sat/cp_model_expand.cc
View File

@@ -30,6 +30,7 @@ struct ExpansionHelper {
CpModelProto expanded_proto;
std::unordered_map<std::pair<int, int>, int> precedence_cache;
std::map<std::string, int> 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<int>& 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<int> 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));
}

18
ortools/sat/python/cp_model.py
View File

@@ -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."""