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

refactor code

Browse Source
This commit is contained in:
Laurent Perron
2020-09-14 22:23:17 +02:00
parent 5ba2d9aa2a
commit 7d413479f6
17 changed files with 407 additions and 430 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/sat/BUILD
View File

@@ -7,6 +7,8 @@ package(
default_visibility = ["//visibility:public"],
)
COPTS=["-std=c++17"]
proto_library(
name = "sat_parameters_proto",
srcs = ["sat_parameters.proto"],

2
ortools/sat/cumulative.h
View File

@@ -37,7 +37,7 @@ namespace sat {
// the sum of the demands of all the tasks that overlap any time point cannot
// exceed the capacity of the resource.
//
// This constraint assumes that an interval can be optional or have a duration
// This constraint assumes that an interval can be optional or have a size
// of zero. The demands and the capacity can be any non-negative number.
//
// Optimization: If one already have an helper constructed from the interval

38
ortools/sat/cumulative_energy.cc
View File

@@ -48,38 +48,36 @@ void AddCumulativeOverloadChecker(const std::vector<AffineExpression>& demands,
const int num_tasks = helper->NumTasks();
CHECK_EQ(demands.size(), num_tasks);
for (int t = 0; t < num_tasks; ++t) {
// TODO(user): Remove once helper->Durations()[t] is an expression.
const AffineExpression duration =
helper->DurationVars()[t] == kNoIntegerVariable ||
integer_trail->IsFixed(helper->DurationVars()[t])
? AffineExpression(helper->DurationMin(t))
: AffineExpression(helper->DurationVars()[t]);
// TODO(user): Remove once helper->Sizes()[t] is an expression.
const AffineExpression size =
helper->SizeVars()[t] == kNoIntegerVariable ||
integer_trail->IsFixed(helper->SizeVars()[t])
? AffineExpression(helper->SizeMin(t))
: AffineExpression(helper->SizeVars()[t]);
const AffineExpression demand = demands[t];
if (demand.var == kNoIntegerVariable &&
duration.var == kNoIntegerVariable) {
if (demand.var == kNoIntegerVariable && size.var == kNoIntegerVariable) {
CHECK_GE(demand.constant, 0);
CHECK_GE(duration.constant, 0);
energies.emplace_back(demand.constant * duration.constant);
CHECK_GE(size.constant, 0);
energies.emplace_back(demand.constant * size.constant);
} else if (demand.var == kNoIntegerVariable) {
CHECK_GE(demand.constant, 0);
energies.push_back(duration);
energies.push_back(size);
energies.back().coeff *= demand.constant;
energies.back().constant *= demand.constant;
} else if (duration.var == kNoIntegerVariable) {
CHECK_GE(duration.constant, 0);
} else if (size.var == kNoIntegerVariable) {
CHECK_GE(size.constant, 0);
energies.push_back(demand);
energies.back().coeff *= duration.constant;
energies.back().constant *= duration.constant;
energies.back().coeff *= size.constant;
energies.back().constant *= size.constant;
} else {
// The case where both demand and duration are variable should be rare.
// The case where both demand and size are variable should be rare.
//
// TODO(user): Handle when needed by creating an intermediate product
// variable equal to demand * duration. Note that because of the affine
// variable equal to demand * size. Note that because of the affine
// expression, we do need some custom code for this.
LOG(INFO)
<< "Overload checker with variable demand and varialbe duration "
"is currently not implemented. Skipping.";
LOG(INFO) << "Overload checker with variable demand and variable size "
"is currently not implemented. Skipping.";
return;
}
}

2
ortools/sat/cumulative_energy.h
View File

@@ -33,7 +33,7 @@ namespace sat {
// The schedule never uses more than capacity units of energy at a given time.
//
// This is mathematically equivalent to making a model with energy(task)
// different tasks with demand and duration 1, but is much more efficient,
// different tasks with demand and size 1, but is much more efficient,
// since it uses O(|tasks|) variables instead of O(sum_{task} |energy(task)|).
void AddCumulativeEnergyConstraint(std::vector<AffineExpression> energies,
AffineExpression capacity,

466
ortools/sat/cuts.cc
View File

@@ -1149,9 +1149,11 @@ bool CoverCutHelper::TrySimpleKnapsack(
terms_.clear();
IntegerValue rhs = base_ct.ub;
IntegerValue sum_of_diff(0);
IntegerValue max_base_magnitude(0);
for (int i = 0; i < base_size; ++i) {
const IntegerValue coeff = base_ct.coeffs[i];
const IntegerValue positive_coeff = IntTypeAbs(coeff);
max_base_magnitude = std::max(max_base_magnitude, positive_coeff);
const IntegerValue bound_diff = upper_bounds[i] - lower_bounds[i];
if (!AddProductTo(positive_coeff, bound_diff, &sum_of_diff)) {
return false;
@@ -1214,11 +1216,6 @@ bool CoverCutHelper::TrySimpleKnapsack(
// distance from upper bound first.
//
// We compute the cut at the same time.
//
// TODO(user): the cut rhs might be tightened slightly using FloorRatio(rhs,
// max_coeff) instead of -1. But I have no occurrence of this on the Miplib
// for now. Note that this require a non-binary variable otherwise it will
// always be -1.
terms_.resize(new_size);
std::sort(terms_.begin(), terms_.end(), [](const Term& a, const Term& b) {
if (a.positive_coeff == b.positive_coeff) {
@@ -1248,29 +1245,66 @@ bool CoverCutHelper::TrySimpleKnapsack(
}
}
// Basic Lifting. A move in activity of 1 in the cut correspond to a move of
// max_coeff in the original constraint. So we can basically lift all
// variables with a coefficient greater or equal to max_coeff. If the coeff
// is >= 2 * max_coeff, we can even use a coeff of 2, etc...
// In case the max_coeff variable is not binary, it might be possible to
// tighten the cut a bit more.
//
// Note(user): I never observed this on the miplib so far.
if (max_coeff == 0) return true;
if (max_coeff < -rhs) {
const IntegerValue m = FloorRatio(-rhs, max_coeff);
rhs += max_coeff * m;
cut_.ub -= m;
}
// Lift all at once the variables not used in the cover.
//
// We have a cut of the form sum_i X_i <= b that we will lift into
// sum_i scaling X_i + sum f(base_coeff_j) X_j <= b * scaling.
//
// Using the super additivity of f() and how we construct it,
// we know that: sum_j base_coeff_j X_j <= N * max_coeff + (max_coeff - slack)
// implies that: sum_j f(base_coeff_j) X_j <= N * scaling.
//
// 1/ cut > b -(N+1) => original sum + (N+1) * max_coeff >= rhs + slack
// 2/ rewrite 1/ as : scaling * cut >= scaling * b - scaling * N => ...
// 3/ lift > N * scaling => lift_sum > N * max_coeff + (max_coeff - slack)
// And adding 2/ + 3/ we prove what we want:
// cut * scaling + lift > b * scaling => original_sum + lift_sum > rhs.
const IntegerValue slack = -rhs;
const IntegerValue remainder = max_coeff - slack;
const IntegerValue max_scaling(std::min(
IntegerValue(60), FloorRatio(kMaxIntegerValue, max_base_magnitude)));
const auto f = GetSuperAdditiveRoundingFunction(remainder, max_coeff,
IntegerValue(1), max_scaling);
const IntegerValue scaling = f(max_coeff);
if (scaling > 1) {
for (int i = 0; i < cut_.coeffs.size(); ++i) cut_.coeffs[i] *= scaling;
cut_.ub *= scaling;
}
num_lifting_ = 0;
for (int i = 0; i < base_size; ++i) {
if (in_cut_[i]) continue;
const IntegerValue positive_coeff = IntTypeAbs(base_ct.coeffs[i]);
if (positive_coeff < max_coeff) continue;
const IntegerValue new_coeff = f(positive_coeff);
if (new_coeff == 0) continue;
++num_lifting_;
const IntegerValue f = FloorRatio(positive_coeff, max_coeff);
if (base_ct.coeffs[i] > 0) { // Add f * (X - LB)
cut_.coeffs.push_back(IntegerValue(f));
if (base_ct.coeffs[i] > 0) {
// Add new_coeff * (X - LB)
cut_.coeffs.push_back(new_coeff);
cut_.vars.push_back(base_ct.vars[i]);
cut_.ub += lower_bounds[i] * f;
} else { // Add f * (UB - X)
cut_.coeffs.push_back(IntegerValue(-f));
cut_.ub += lower_bounds[i] * new_coeff;
} else {
// Add new_coeff * (UB - X)
cut_.coeffs.push_back(-new_coeff);
cut_.vars.push_back(base_ct.vars[i]);
cut_.ub -= upper_bounds[i] * f;
cut_.ub -= upper_bounds[i] * new_coeff;
}
}
if (scaling > 1) DivideByGCD(&cut_);
return true;
}
@@ -1927,18 +1961,32 @@ CutGenerator CreateLinMaxCutGenerator(
return result;
}
void AddLiteralToCut(const Literal l, IntegerEncoder* encoder, Model* model,
CutGenerator* cutgen) {
if (encoder->GetLiteralView(l) == kNoIntegerVariable &&
encoder->GetLiteralView(l.Negated()) == kNoIntegerVariable) {
model->Add(NewIntegerVariableFromLiteral(l));
}
const IntegerVariable direct_view = encoder->GetLiteralView(l);
if (direct_view != kNoIntegerVariable) {
cutgen->vars.push_back(direct_view);
} else {
cutgen->vars.push_back(encoder->GetLiteralView(l.Negated()));
DCHECK_NE(cutgen->vars.back(), kNoIntegerVariable);
void AddIntegerVariableFromIntervals(SchedulingConstraintHelper* helper,
Model* model,
std::vector<IntegerVariable>* vars) {
vars->insert(vars->end(), helper->StartVars().begin(),
helper->StartVars().end());
vars->insert(vars->end(), helper->SizeVars().begin(),
helper->SizeVars().end());
vars->insert(vars->end(), helper->EndVars().begin(), helper->EndVars().end());
IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
for (int t = 0; t < helper->NumTasks(); ++t) {
if (helper->IsOptional(t) && !helper->IsAbsent(t) &&
!helper->IsPresent(t)) {
const Literal l = helper->PresenceLiteral(t);
if (encoder->GetLiteralView(l) == kNoIntegerVariable &&
encoder->GetLiteralView(l.Negated()) == kNoIntegerVariable) {
model->Add(NewIntegerVariableFromLiteral(l));
}
const IntegerVariable direct_view = encoder->GetLiteralView(l);
if (direct_view != kNoIntegerVariable) {
vars->push_back(direct_view);
} else {
vars->push_back(encoder->GetLiteralView(l.Negated()));
DCHECK_NE(vars->back(), kNoIntegerVariable);
}
}
}
}
@@ -1948,146 +1996,100 @@ CutGenerator CreateCumulativeCutGenerator(
Model* model) {
CutGenerator result;
SchedulingConstraintHelper* helper =
new SchedulingConstraintHelper(intervals, model);
model->TakeOwnership(helper);
result.vars = demands;
IntervalsRepository* intervals_repo =
model->GetOrCreate<IntervalsRepository>();
IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
for (const IntervalVariable interval : intervals) {
result.vars.push_back(intervals_repo->StartVar(interval));
result.vars.push_back(intervals_repo->EndVar(interval));
result.vars.push_back(intervals_repo->SizeVar(interval));
if (intervals_repo->IsOptional(interval)) {
const Literal l = intervals_repo->IsPresentLiteral(interval);
AddLiteralToCut(l, encoder, model, &result);
}
}
result.vars.push_back(capacity);
AddIntegerVariableFromIntervals(helper, model, &result.vars);
Trail* trail = model->GetOrCreate<Trail>();
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
result.generate_cuts = [intervals, capacity, demands, trail, integer_trail,
intervals_repo,
model](const gtl::ITIVector<IntegerVariable, double>&
lp_values,
LinearConstraintManager* manager) {
if (model->GetOrCreate<Trail>()->CurrentDecisionLevel() > 0) return;
result.generate_cuts =
[capacity, demands, trail, integer_trail, helper, model](
const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
if (trail->CurrentDecisionLevel() > 0) return;
IntegerValue min_of_starts = kMaxIntegerValue;
IntegerValue max_of_ends = kMinIntegerValue;
IntegerValue min_of_starts = kMaxIntegerValue;
IntegerValue max_of_ends = kMinIntegerValue;
std::vector<IntegerVariable> size_variables;
std::vector<IntegerVariable> demand_variables;
std::vector<Literal> presence_literals;
IntegerValue fixed_contribution(0);
std::vector<int> active_intervals;
IntegerValue fixed_contribution(0);
for (int i = 0; i < intervals.size(); ++i) {
const IntervalVariable interval = intervals[i];
const Literal presence = intervals_repo->IsOptional(interval)
? intervals_repo->IsPresentLiteral(interval)
: Literal(kTrueLiteralIndex);
const VariablesAssignment& assignment = trail->Assignment();
if (presence.Index() != kTrueLiteralIndex &&
assignment.LiteralIsAssigned(presence) &&
assignment.LiteralIsFalse(presence)) {
continue;
}
for (int i = 0; i < helper->NumTasks(); ++i) {
if (helper->IsAbsent(i)) continue;
const IntegerVariable start_var = intervals_repo->StartVar(interval);
const IntegerVariable end_var = intervals_repo->EndVar(interval);
min_of_starts = std::min(min_of_starts, helper->StartMin(i));
max_of_ends = std::max(max_of_ends, helper->EndMax(i));
const IntegerValue start_min =
integer_trail->LevelZeroLowerBound(start_var);
const IntegerValue end_max = integer_trail->LevelZeroUpperBound(end_var);
if (start_min < min_of_starts) {
min_of_starts = start_min;
}
if (end_max > max_of_ends) {
max_of_ends = end_max;
}
const IntegerVariable size_var = intervals_repo->SizeVar(interval);
const IntegerVariable demand_var = demands[i];
const bool size_is_fixed = integer_trail->IsFixedAtLevelZero(size_var);
const bool demand_is_fixed =
integer_trail->IsFixedAtLevelZero(demand_var);
const bool is_optional = presence.Index() != kTrueLiteralIndex &&
!assignment.LiteralIsAssigned(presence);
if (!is_optional && size_is_fixed && demand_is_fixed) {
fixed_contribution += integer_trail->LevelZeroLowerBound(size_var) *
integer_trail->LevelZeroLowerBound(demand_var);
} else {
size_variables.push_back(size_var);
demand_variables.push_back(demand_var);
presence_literals.push_back(presence);
}
}
if (size_variables.empty() && integer_trail->IsFixedAtLevelZero(capacity)) {
// Everything is fixed, and the span is already computed.
VLOG(2) << "Fixed";
return;
}
bool cut_generated = true;
LinearConstraintBuilder cut(model, kMinIntegerValue, -fixed_contribution);
VLOG(2) << "Capacity: [" << integer_trail->LevelZeroLowerBound(capacity)
<< ".." << integer_trail->LevelZeroUpperBound(capacity) << "]";
VLOG(2) << "Span: " << max_of_ends - min_of_starts;
VLOG(2) << "Fixed contribution: " << fixed_contribution;
cut.AddTerm(capacity, min_of_starts - max_of_ends);
for (int i = 0; i < size_variables.size(); ++i) {
const Literal presence = presence_literals[i];
const VariablesAssignment& assignment = trail->Assignment();
if (presence.Index() != kTrueLiteralIndex &&
assignment.LiteralIsAssigned(presence) &&
assignment.LiteralIsFalse(presence)) {
continue;
}
const IntegerVariable size_var = size_variables[i];
const IntegerVariable demand_var = demand_variables[i];
const bool size_is_fixed = integer_trail->IsFixedAtLevelZero(size_var);
const bool demand_is_fixed =
integer_trail->IsFixedAtLevelZero(demand_var);
VLOG(2) << "Task: " << i;
VLOG(2) << " size: [" << integer_trail->LevelZeroLowerBound(size_var)
<< ".." << integer_trail->LevelZeroUpperBound(size_var) << "]";
VLOG(2) << " demand: [" << integer_trail->LevelZeroLowerBound(demand_var)
<< ".." << integer_trail->LevelZeroUpperBound(demand_var) << "]";
if (presence.Index() == kTrueLiteralIndex ||
(assignment.LiteralIsAssigned(presence) &&
assignment.LiteralIsTrue(presence))) {
// Interval is performed.
if (size_is_fixed) {
cut.AddTerm(demand_var, integer_trail->LevelZeroLowerBound(size_var));
} else if (demand_is_fixed) {
cut.AddTerm(size_var, integer_trail->LevelZeroLowerBound(demand_var));
} else if (lp_values[size_var] *
integer_trail->LevelZeroLowerBound(demand_var) >=
lp_values[demand_var] *
integer_trail->LevelZeroLowerBound(size_var)) {
cut.AddTerm(size_var, integer_trail->LevelZeroLowerBound(demand_var));
} else {
cut.AddTerm(demand_var, integer_trail->LevelZeroLowerBound(size_var));
const IntegerVariable demand_var = demands[i];
const bool size_is_fixed = helper->SizeIsFixed(i);
const bool demand_is_fixed = integer_trail->IsFixed(demand_var);
const bool is_optional = helper->IsOptional(i);
if (!is_optional && size_is_fixed && demand_is_fixed) {
fixed_contribution +=
helper->SizeMin(i) * integer_trail->LowerBound(demand_var);
} else {
active_intervals.push_back(i);
}
}
} else {
// Interval is optional.
cut_generated &= cut.AddLiteralTerm(
presence, integer_trail->LevelZeroLowerBound(size_var) *
integer_trail->LevelZeroLowerBound(demand_var));
if (!cut_generated) break;
}
}
if (cut_generated) {
// Violation of the cut is checked by AddCut so we don't check
// it here.
manager->AddCut(cut.Build(), "CumulativeEnergy", lp_values);
}
};
if (active_intervals.empty() && integer_trail->IsFixed(capacity)) {
// Everything is fixed, and the span is already computed.
VLOG(2) << "Fixed";
return;
}
const IntegerValue span = max_of_ends - min_of_starts;
bool cut_generated = true;
LinearConstraintBuilder cut(model, kMinIntegerValue,
-fixed_contribution);
VLOG(2) << "Capacity: [" << integer_trail->LowerBound(capacity) << ".."
<< integer_trail->UpperBound(capacity) << "]";
VLOG(2) << "Span: " << span;
VLOG(2) << "Fixed contribution: " << fixed_contribution;
cut.AddTerm(capacity, -span);
for (const int i : active_intervals) {
const IntegerVariable size_var = helper->SizeVar(i);
const IntegerVariable demand_var = demands[i];
const IntegerValue demand_min = integer_trail->LowerBound(demand_var);
const IntegerValue demand_max = integer_trail->UpperBound(demand_var);
const IntegerValue size_min = helper->SizeMin(i);
const IntegerValue size_max = helper->SizeMax(i);
VLOG(2) << "Task: " << i;
VLOG(2) << " size: [" << size_min << ".." << size_max << "]";
VLOG(2) << " demand: [" << demand_min << ".." << demand_max << "]";
if (helper->IsPresent(i)) {
// Interval is performed.
if (helper->SizeIsFixed(i)) {
cut.AddTerm(demand_var, size_min);
} else if (integer_trail->IsFixed(demand_var)) {
cut.AddTerm(size_var, demand_min);
} else if (lp_values[size_var] * demand_min >=
lp_values[demand_var] * size_min) {
cut.AddTerm(size_var, demand_min);
} else {
cut.AddTerm(demand_var, size_min);
}
} else {
// Interval is optional.
cut_generated &= cut.AddLiteralTerm(helper->PresenceLiteral(i),
size_min * demand_min);
if (!cut_generated) break;
}
}
if (cut_generated) {
// Violation of the cut is checked by AddCut so we don't check
// it here.
manager->AddCut(cut.Build(), "CumulativeEnergy", lp_values);
}
};
return result;
}
@@ -2097,49 +2099,38 @@ CutGenerator CreateOverlappingCumulativeCutGenerator(
Model* model) {
CutGenerator result;
SchedulingConstraintHelper* helper =
new SchedulingConstraintHelper(intervals, model);
model->TakeOwnership(helper);
result.vars = demands;
IntervalsRepository* intervals_repo =
model->GetOrCreate<IntervalsRepository>();
IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
for (const IntervalVariable interval : intervals) {
result.vars.push_back(intervals_repo->StartVar(interval));
result.vars.push_back(intervals_repo->EndVar(interval));
result.vars.push_back(intervals_repo->SizeVar(interval));
if (intervals_repo->IsOptional(interval)) {
const Literal l = intervals_repo->IsPresentLiteral(interval);
AddLiteralToCut(l, encoder, model, &result);
}
}
result.vars.push_back(capacity);
AddIntegerVariableFromIntervals(helper, model, &result.vars);
struct Event {
int interval_index;
IntegerValue time;
bool positive;
IntegerVariable demand;
Literal presence_literal;
};
Trail* trail = model->GetOrCreate<Trail>();
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
result.generate_cuts =
[intervals, capacity, demands, trail, integer_trail, intervals_repo,
model](const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
if (model->GetOrCreate<Trail>()->CurrentDecisionLevel() > 0) return;
[helper, capacity, demands, trail, integer_trail, model](
const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
if (trail->CurrentDecisionLevel() > 0) return;
std::vector<Event> events;
// Iterate through the intervals. If start_max < end_min, the demand is
// mandatory.
for (int i = 0; i < intervals.size(); ++i) {
const IntervalVariable interval = intervals[i];
const IntegerVariable start_var = intervals_repo->StartVar(interval);
const IntegerVariable end_var = intervals_repo->EndVar(interval);
for (int i = 0; i < helper->NumTasks(); ++i) {
if (helper->IsAbsent(i)) continue;
const IntegerValue start_max =
integer_trail->LevelZeroUpperBound(start_var);
const IntegerValue end_min =
integer_trail->LevelZeroLowerBound(end_var);
const IntegerValue start_max = helper->StartMax(i);
const IntegerValue end_min = helper->EndMin(i);
if (start_max >= end_min) continue;
@@ -2148,9 +2139,7 @@ CutGenerator CreateOverlappingCumulativeCutGenerator(
e1.time = start_max;
e1.demand = demands[i];
e1.positive = true;
e1.presence_literal = intervals_repo->IsOptional(interval)
? intervals_repo->IsPresentLiteral(interval)
: Literal(kTrueLiteralIndex);
Event e2 = e1;
e2.time = end_min;
e2.positive = false;
@@ -2187,12 +2176,12 @@ CutGenerator CreateOverlappingCumulativeCutGenerator(
IntegerValue(0));
cut.AddTerm(capacity, IntegerValue(-1));
for (const Event& cut_event : cut_events) {
if (cut_event.presence_literal == Literal(kTrueLiteralIndex)) {
if (helper->IsPresent(cut_event.interval_index)) {
cut.AddTerm(cut_event.demand, IntegerValue(1));
} else {
cut_generated &= cut.AddLiteralTerm(
cut_event.presence_literal,
integer_trail->LevelZeroLowerBound(cut_event.demand));
helper->PresenceLiteral(cut_event.interval_index),
integer_trail->LowerBound(cut_event.demand));
if (!cut_generated) break;
}
}
@@ -2222,23 +2211,16 @@ CutGenerator CreateNoOverlapCutGenerator(
const std::vector<IntervalVariable>& intervals, Model* model) {
CutGenerator result;
IntervalsRepository* intervals_repo =
model->GetOrCreate<IntervalsRepository>();
IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
for (const IntervalVariable interval : intervals) {
result.vars.push_back(intervals_repo->StartVar(interval));
result.vars.push_back(intervals_repo->EndVar(interval));
result.vars.push_back(intervals_repo->SizeVar(interval));
if (intervals_repo->IsOptional(interval)) {
AddLiteralToCut(intervals_repo->IsPresentLiteral(interval), encoder,
model, &result);
}
}
SchedulingConstraintHelper* helper =
new SchedulingConstraintHelper(intervals, model);
model->TakeOwnership(helper);
AddIntegerVariableFromIntervals(helper, model, &result.vars);
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
Trail* trail = model->GetOrCreate<Trail>();
result.generate_cuts =
[intervals, trail, integer_trail, intervals_repo, model](
[trail, helper, model](
const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
if (trail->CurrentDecisionLevel() > 0) return;
@@ -2246,76 +2228,44 @@ CutGenerator CreateNoOverlapCutGenerator(
IntegerValue min_of_starts = kMaxIntegerValue;
IntegerValue max_of_ends = kMinIntegerValue;
std::vector<IntegerVariable> size_variables;
std::vector<Literal> presence_literals;
std::vector<int> active_intervals;
IntegerValue fixed_contribution(0);
IntegerValue max_contribution(0);
const VariablesAssignment& assignment = trail->Assignment();
for (int i = 0; i < helper->NumTasks(); ++i) {
if (helper->IsAbsent(i)) continue;
for (int i = 0; i < intervals.size(); ++i) {
const IntervalVariable interval = intervals[i];
const Literal presence =
intervals_repo->IsOptional(interval)
? intervals_repo->IsPresentLiteral(interval)
: Literal(kTrueLiteralIndex);
if (presence.Index() != kTrueLiteralIndex &&
assignment.LiteralIsAssigned(presence) &&
assignment.LiteralIsFalse(presence)) {
continue;
}
min_of_starts = std::min(min_of_starts, helper->StartMin(i));
max_of_ends = std::max(max_of_ends, helper->EndMax(i));
const IntegerVariable start_var = intervals_repo->StartVar(interval);
const IntegerVariable end_var = intervals_repo->EndVar(interval);
const IntegerValue start_min =
integer_trail->LevelZeroLowerBound(start_var);
const IntegerValue end_max =
integer_trail->LevelZeroUpperBound(end_var);
if (start_min < min_of_starts) {
min_of_starts = start_min;
}
if (end_max > max_of_ends) {
max_of_ends = end_max;
}
const IntegerVariable size_var = intervals_repo->SizeVar(interval);
const bool size_is_fixed =
integer_trail->IsFixedAtLevelZero(size_var);
const bool is_optional = presence.Index() != kTrueLiteralIndex &&
!assignment.LiteralIsAssigned(presence);
if (!is_optional && size_is_fixed) {
fixed_contribution += integer_trail->LevelZeroLowerBound(size_var);
if (helper->IsPresent(i) && helper->SizeIsFixed(i)) {
fixed_contribution += helper->SizeMin(i);
} else {
size_variables.push_back(size_var);
presence_literals.push_back(presence);
active_intervals.push_back(i);
}
max_contribution += integer_trail->LevelZeroUpperBound(size_var);
max_contribution += helper->SizeMax(i);
}
const IntegerValue span = max_of_ends - min_of_starts;
// If everything fits, there is nothing to do.
if (max_contribution <= max_of_ends - min_of_starts) return;
if (max_contribution <= span) return;
// If infeasible, the solver will find it.
if (fixed_contribution > max_of_ends - min_of_starts) return;
// there is no point creating a cut since the propagation should make it
// always satisfied
if (size_variables.empty()) return;
if (fixed_contribution > span) return;
// There is no point creating a cut since the propagation should make it
// always satisfied.
if (active_intervals.empty()) return;
bool cut_generated = true;
LinearConstraintBuilder cut(
model, IntegerValue(0),
max_of_ends - min_of_starts - fixed_contribution);
LinearConstraintBuilder cut(model, IntegerValue(0),
span - fixed_contribution);
for (int i = 0; i < size_variables.size(); ++i) {
const Literal presence = presence_literals[i];
const IntegerVariable size_var = size_variables[i];
if (presence.Index() == kTrueLiteralIndex ||
(assignment.LiteralIsAssigned(presence) &&
assignment.LiteralIsTrue(presence))) {
cut.AddTerm(size_var, IntegerValue(1));
for (const int i : active_intervals) {
if (helper->IsPresent(i)) {
cut.AddTerm(helper->SizeVar(i), IntegerValue(1));
} else {
cut_generated &= cut.AddLiteralTerm(
presence, integer_trail->LevelZeroLowerBound(size_var));
cut_generated &= cut.AddLiteralTerm(helper->PresenceLiteral(i),
helper->SizeMin(i));
if (!cut_generated) break;
}
}

13
ortools/sat/cuts.h
View File

@@ -466,11 +466,11 @@ CutGenerator CreateLinMaxCutGenerator(
// capacity.
//
// If an interval is optional, it contributes
//. min_demand * min_duration * presence_literal
// min_demand * min_size * presence_literal
// amount of total energy.
//
// If an interval is performed, it contributes either min_demand * duration or
// demand * min_duration. We choose the most violated formulation.
// If an interval is performed, it contributes either min_demand * size or
// demand * min_size. We choose the most violated formulation.
//
// The maximum energy is capacity * span of intervals at level 0.
CutGenerator CreateCumulativeCutGenerator(
@@ -493,15 +493,16 @@ CutGenerator CreateOverlappingCumulativeCutGenerator(
const std::vector<IntervalVariable>& intervals,
const IntegerVariable capacity, const std::vector<IntegerVariable>& demands,
Model* model);
// For a given set of intervals, we first compute the min and max of all
// intervals. Then we create a cut that indicates that all intervals must fit
// in that span.
//
// If an interval is optional, it contributes min_duration * presence_literal
// If an interval is optional, it contributes min_size * presence_literal
// amount of demand to the mandatory demands sum. So the final cut is generated
// as follows:
// sum(durations of always present intervals)
// + sum(presence_literal * min_of_duration) <= span of all intervals.
// sum(sizes of always present intervals)
// + sum(presence_literal * min_of_size) <= span of all intervals.
CutGenerator CreateNoOverlapCutGenerator(
const std::vector<IntervalVariable>& intervals, Model* model);

12
ortools/sat/diffn.cc
View File

@@ -39,9 +39,9 @@ void AddCumulativeRelaxation(const std::vector<IntervalVariable>& x_intervals,
int64 min_starts = kint64max;
int64 max_ends = kint64min;
for (int box = 0; box < y->NumTasks(); ++box) {
IntegerVariable s_var = y->DurationVars()[box];
IntegerVariable s_var = y->SizeVars()[box];
if (s_var == kNoIntegerVariable || integer_trail->IsFixed(s_var)) {
sizes.push_back(AffineExpression(y->DurationMin(box)));
sizes.push_back(AffineExpression(y->SizeMin(box)));
} else {
sizes.push_back(AffineExpression(s_var));
}
@@ -144,7 +144,7 @@ bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
cached_areas_.resize(num_boxes);
cached_dimensions_.resize(num_boxes);
for (int box = 0; box < num_boxes; ++box) {
cached_areas_[box] = x_.DurationMin(box) * y_.DurationMin(box);
cached_areas_[box] = x_.SizeMin(box) * y_.SizeMin(box);
if (cached_areas_[box] == 0) continue;
// TODO(user): Also consider shifted end max.
@@ -216,9 +216,9 @@ bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
IntegerValue sum_of_areas = cached_areas_[box];
const auto add_box_energy_in_rectangle_reason = [&](int b) {
x_.AddEnergyAfterReason(b, x_.DurationMin(b), area.x_min);
x_.AddEnergyAfterReason(b, x_.SizeMin(b), area.x_min);
x_.AddEndMaxReason(b, area.x_max);
y_.AddEnergyAfterReason(b, y_.DurationMin(b), area.y_min);
y_.AddEnergyAfterReason(b, y_.SizeMin(b), area.y_min);
y_.AddEndMaxReason(b, area.y_max);
};
@@ -298,7 +298,7 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
active_boxes_.clear();
events_time_.clear();
for (int box = 0; box < x.NumTasks(); ++box) {
if (!strict_ && (x.DurationMin(box) == 0 || y.DurationMin(box) == 0)) {
if (!strict_ && (x.SizeMin(box) == 0 || y.SizeMin(box) == 0)) {
continue;
}

82
ortools/sat/disjunctive.cc
View File

@@ -175,7 +175,7 @@ void TaskSet::AddEntry(const Entry& e) {
void TaskSet::AddShiftedStartMinEntry(const SchedulingConstraintHelper& helper,
int t) {
const IntegerValue dmin = helper.DurationMin(t);
const IntegerValue dmin = helper.SizeMin(t);
AddEntry({t, std::max(helper.StartMin(t), helper.EndMin(t) - dmin), dmin});
}
@@ -207,9 +207,9 @@ IntegerValue TaskSet::ComputeEndMin() const {
const Entry& e = sorted_tasks_[i];
if (e.start_min >= end_min) {
optimized_restart_ = i;
end_min = e.start_min + e.duration_min;
end_min = e.start_min + e.size_min;
} else {
end_min += e.duration_min;
end_min += e.size_min;
}
}
return end_min;
@@ -239,9 +239,9 @@ IntegerValue TaskSet::ComputeEndMin(int task_to_ignore,
if (e.start_min >= end_min) {
*critical_index = i;
if (!ignored) optimized_restart_ = i;
end_min = e.start_min + e.duration_min;
end_min = e.start_min + e.size_min;
} else {
end_min += e.duration_min;
end_min += e.size_min;
}
}
return end_min;
@@ -255,11 +255,11 @@ bool DisjunctiveWithTwoItems::Propagate() {
// Note that this propagation also take care of the "overload checker" part.
// It also propagates as much as possible, even in the presence of task with
// variable durations.
// variable sizes.
//
// TODO(user): For optional interval whose presense in unknown and without
// TODO(user): For optional interval whose presence in unknown and without
// optional variable, the end-min may not be propagated to at least (start_min
// + duration_min). Consider that into the computation so we may decide the
// + size_min). Consider that into the computation so we may decide the
// interval forced absence? Same for the start-max.
int task_before = 0;
int task_after = 1;
@@ -366,11 +366,10 @@ bool CombinedDisjunctive<time_direction>::Propagate() {
if (helper_->IsPresent(task_index)) {
task_is_added_[task_index] = true;
const IntegerValue shifted_smin = helper_->ShiftedStartMin(task_index);
const IntegerValue duration_min = helper_->DurationMin(task_index);
const IntegerValue size_min = helper_->SizeMin(task_index);
for (const int d_index : task_to_disjunctives_[task_index]) {
// TODO(user): AddEntry() and ComputeEndMin() could be combined.
task_sets_[d_index].AddEntry(
{task_index, shifted_smin, duration_min});
task_sets_[d_index].AddEntry({task_index, shifted_smin, size_min});
end_mins_[d_index] = task_sets_[d_index].ComputeEndMin();
max_of_end_min = std::max(max_of_end_min, end_mins_[d_index]);
}
@@ -430,8 +429,7 @@ bool CombinedDisjunctive<time_direction>::Propagate() {
const int ct = sorted_tasks[i].task;
if (ct == t) continue;
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
window_start);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min, window_start);
helper_->AddStartMaxReason(ct, end_min - 1);
}
helper_->AddEndMinReason(t, end_min);
@@ -445,10 +443,10 @@ bool CombinedDisjunctive<time_direction>::Propagate() {
// not happen if its start is not optional).
if (task_is_added_[t]) {
const IntegerValue shifted_smin = helper_->ShiftedStartMin(t);
const IntegerValue duration_min = helper_->DurationMin(t);
const IntegerValue size_min = helper_->SizeMin(t);
for (const int d_index : task_to_disjunctives_[t]) {
task_sets_[d_index].NotifyEntryIsNowLastIfPresent(
{t, shifted_smin, duration_min});
{t, shifted_smin, size_min});
end_mins_[d_index] = task_sets_[d_index].ComputeEndMin();
max_of_end_min = std::max(max_of_end_min, end_mins_[d_index]);
}
@@ -482,7 +480,7 @@ bool DisjunctiveOverloadChecker::Propagate() {
const IntegerValue start_min = task_time.time;
if (start_min < window_end) {
window_.push_back(task_time);
window_end += helper_->DurationMin(task);
window_end += helper_->SizeMin(task);
if (window_end > helper_->EndMax(task)) {
relevant_size = window_.size();
relevant_end = window_end;
@@ -501,7 +499,7 @@ bool DisjunctiveOverloadChecker::Propagate() {
// Start of the next window.
window_.clear();
window_.push_back(task_time);
window_end = start_min + helper_->DurationMin(task);
window_end = start_min + helper_->SizeMin(task);
relevant_size = 0;
}
@@ -551,10 +549,10 @@ bool DisjunctiveOverloadChecker::PropagateSubwindow(
DCHECK_NE(task_to_event_[current_task], -1);
{
const int current_event = task_to_event_[current_task];
const IntegerValue energy_min = helper_->DurationMin(current_task);
const IntegerValue energy_min = helper_->SizeMin(current_task);
if (helper_->IsPresent(current_task)) {
// TODO(user,user): Add max energy deduction for variable
// durations by putting the energy_max here and modifying the code
// sizes by putting the energy_max here and modifying the code
// dealing with the optional envelope greater than current_end below.
theta_tree_.AddOrUpdateEvent(current_event, window_[current_event].time,
energy_min, energy_min);
@@ -598,11 +596,10 @@ bool DisjunctiveOverloadChecker::PropagateSubwindow(
current_end, &critical_event, &optional_event, &available_energy);
const int optional_task = window_[optional_event].task_index;
const IntegerValue optional_duration_min =
helper_->DurationMin(optional_task);
const IntegerValue optional_size_min = helper_->SizeMin(optional_task);
const IntegerValue window_start = window_[critical_event].time;
const IntegerValue window_end =
current_end + optional_duration_min - available_energy - 1;
current_end + optional_size_min - available_energy - 1;
for (int event = critical_event; event < window_size; event++) {
const IntegerValue energy_min = theta_tree_.EnergyMin(event);
if (energy_min > 0) {
@@ -613,7 +610,7 @@ bool DisjunctiveOverloadChecker::PropagateSubwindow(
}
}
helper_->AddEnergyAfterReason(optional_task, optional_duration_min,
helper_->AddEnergyAfterReason(optional_task, optional_size_min,
window_start);
helper_->AddEndMaxReason(optional_task, window_end);
@@ -658,24 +655,24 @@ bool DisjunctiveDetectablePrecedences::Propagate() {
if (helper_->IsAbsent(task)) continue;
const IntegerValue shifted_smin = task_time.time;
const IntegerValue duration_min = helper_->DurationMin(task);
const IntegerValue size_min = helper_->SizeMin(task);
// Tricky: Because we use the up to date version of duration_min (that might
// Tricky: Because we use the up to date version of size_min (that might
// have increased in one of the PropagateSubwindow() call) and the cached
// shifted_smin which didn't change, we cannot do shifted_smin +
// duration_min which might be higher than the actual end_min_if_present.
// size_min which might be higher than the actual end_min_if_present.
// So we use the updated value instead.
//
// Note that we have the same problem below when window_end might be higher
// that it is actually, but that is fine since we will just decompose less.
const IntegerValue end_min_if_present =
std::max(helper_->EndMin(task), helper_->StartMin(task) + duration_min);
std::max(helper_->EndMin(task), helper_->StartMin(task) + size_min);
// Note that we use the real StartMin() here, as this is the one we will
// push.
if (helper_->StartMin(task) < window_end) {
task_by_increasing_end_min_.push_back({task, end_min_if_present});
window_end = std::max(window_end, shifted_smin) + duration_min;
window_end = std::max(window_end, shifted_smin) + size_min;
continue;
}
@@ -773,8 +770,7 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow() {
helper_->AddReasonForBeingBefore(t, blocking_task);
return helper_->ReportConflict();
}
DCHECK_LT(start_max,
helper_->ShiftedStartMin(t) + helper_->DurationMin(t))
DCHECK_LT(start_max, helper_->ShiftedStartMin(t) + helper_->SizeMin(t))
<< " task should have mandatory part: "
<< helper_->TaskDebugString(t);
DCHECK(to_propagate_.empty());
@@ -819,14 +815,14 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow() {
// - StartMax(ct) < EndMin(t) for the detectable precedence.
// - StartMin(ct) >= window_start for the value of task_set_end_min.
const IntegerValue end_min_if_present =
helper_->ShiftedStartMin(t) + helper_->DurationMin(t);
helper_->ShiftedStartMin(t) + helper_->SizeMin(t);
const IntegerValue window_start =
sorted_tasks[critical_index].start_min;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
DCHECK_NE(ct, t);
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
window_start);
helper_->AddStartMaxReason(ct, end_min_if_present - 1);
}
@@ -878,7 +874,7 @@ bool DisjunctivePrecedences::Propagate() {
const IntegerValue start_min = task_time.time;
if (start_min < window_end) {
window_.push_back(task_time);
window_end += helper_->DurationMin(task);
window_end += helper_->SizeMin(task);
continue;
}
@@ -889,7 +885,7 @@ bool DisjunctivePrecedences::Propagate() {
// Start of the next window.
window_.clear();
window_.push_back(task_time);
window_end = start_min + helper_->DurationMin(task);
window_end = start_min + helper_->SizeMin(task);
}
if (window_.size() > 1 && !PropagateSubwindow()) {
return false;
@@ -920,7 +916,7 @@ bool DisjunctivePrecedences::PropagateSubwindow() {
// The task are actually in sorted order, so we do not need to call
// task_set_.Sort(). This property is DCHECKed.
task_set_.AddUnsortedEntry({task_time.task_index, task_time.time,
helper_->DurationMin(task_time.task_index)});
helper_->SizeMin(task_time.task_index)});
}
DCHECK_GE(task_set_.SortedTasks().size(), 2);
if (integer_trail_->IsCurrentlyIgnored(var)) continue;
@@ -944,7 +940,7 @@ bool DisjunctivePrecedences::PropagateSubwindow() {
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
const int ct = sorted_tasks[i].task;
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
window_start);
precedences_->AddPrecedenceReason(task_to_arc_index_[ct], min_offset,
helper_->MutableLiteralReason(),
@@ -1003,10 +999,10 @@ bool DisjunctiveNotLast::Propagate() {
const IntegerValue start_min = task_time.time;
if (start_min_window_.empty()) {
start_min_window_.push_back(task_time);
window_end = start_min + helper_->DurationMin(task);
window_end = start_min + helper_->SizeMin(task);
} else if (start_min < window_end) {
start_min_window_.push_back(task_time);
window_end += helper_->DurationMin(task);
window_end += helper_->SizeMin(task);
} else {
break;
}
@@ -1083,7 +1079,7 @@ bool DisjunctiveNotLast::PropagateSubwindow() {
const int task_index = to_insert.task_index;
DCHECK(helper_->IsPresent(task_index));
task_set_.AddEntry({task_index, helper_->ShiftedStartMin(task_index),
helper_->DurationMin(task_index)});
helper_->SizeMin(task_index)});
++queue_index;
}
@@ -1128,7 +1124,7 @@ bool DisjunctiveNotLast::PropagateSubwindow() {
const int ct = sorted_tasks[i].task;
if (ct == t) continue;
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
window_start);
helper_->AddStartMaxReason(ct, largest_ct_start_max);
}
@@ -1167,7 +1163,7 @@ bool DisjunctiveEdgeFinding::Propagate() {
// because we might be able to push it if it is smaller than window end.
if (helper_->StartMin(task) < window_end) {
window_.push_back(task_time);
window_end += helper_->DurationMin(task);
window_end += helper_->SizeMin(task);
continue;
}
@@ -1180,7 +1176,7 @@ bool DisjunctiveEdgeFinding::Propagate() {
// Start of the next window.
window_.clear();
window_.push_back(task_time);
window_end = task_time.time + helper_->DurationMin(task);
window_end = task_time.time + helper_->SizeMin(task);
}
if (window_.size() > 2 && !PropagateSubwindow(window_end)) {
return false;
@@ -1233,7 +1229,7 @@ bool DisjunctiveEdgeFinding::PropagateSubwindow(IntegerValue window_end_min) {
for (int event = 0; event < window_size; ++event) {
const TaskTime task_time = window_[event];
const int task = task_time.task_index;
const IntegerValue energy_min = helper_->DurationMin(task);
const IntegerValue energy_min = helper_->SizeMin(task);
event_size_.push_back(energy_min);
if (is_gray_[task]) {
theta_tree_.AddOrUpdateOptionalEvent(event, task_time.time, energy_min);

12
ortools/sat/disjunctive.h
View File

@@ -50,7 +50,7 @@ std::function<void(Model*)> DisjunctiveWithBooleanPrecedences(
const std::vector<IntervalVariable>& vars);
// Helper class to compute the end-min of a set of tasks given their start-min
// and duration-min. In Petr Vilim's PhD "Global Constraints in Scheduling",
// and size-min. In Petr Vilim's PhD "Global Constraints in Scheduling",
// this corresponds to his Theta-tree except that we use a O(n) implementation
// for most of the function here, not a O(log(n)) one.
class TaskSet {
@@ -60,7 +60,7 @@ class TaskSet {
struct Entry {
int task;
IntegerValue start_min;
IntegerValue duration_min;
IntegerValue size_min;
// Note that the tie-breaking is not important here.
bool operator<(Entry other) const { return start_min < other.start_min; }
@@ -74,8 +74,8 @@ class TaskSet {
void AddEntry(const Entry& e);
void RemoveEntryWithIndex(int index);
// Same as AddEntry({t, helper->ShiftedStartMin(t), helper->DurationMin(t)}).
// This is a minor optimization to not call DurationMin(t) twice.
// Same as AddEntry({t, helper->ShiftedStartMin(t), helper->SizeMin(t)}).
// This is a minor optimization to not call SizeMin(t) twice.
void AddShiftedStartMinEntry(const SchedulingConstraintHelper& helper, int t);
// Advanced usage, if the entry is present, this assumes that its start_min is
@@ -101,7 +101,7 @@ class TaskSet {
// SortedTasks().
//
// A reason for the min end is:
// - The duration-min of all the critical tasks.
// - The size-min of all the critical tasks.
// - The fact that all critical tasks have a start-min greater or equal to the
// first of them, that is SortedTasks()[critical_index].start_min.
//
@@ -179,7 +179,7 @@ class DisjunctiveDetectablePrecedences : public PropagatorInterface {
TaskSet task_set_;
};
// Singleton model class wich is just a SchedulingConstraintHelper will all
// Singleton model class which is just a SchedulingConstraintHelper will all
// the intervals.
class AllIntervalsHelper : public SchedulingConstraintHelper {
public:

36
ortools/sat/intervals.cc
View File

@@ -59,8 +59,8 @@ SchedulingConstraintHelper::SchedulingConstraintHelper(
end_vars_.clear();
minus_end_vars_.clear();
minus_start_vars_.clear();
duration_vars_.clear();
fixed_durations_.clear();
size_vars_.clear();
fixed_sizes_.clear();
reason_for_presence_.clear();
for (const IntervalVariable i : tasks) {
if (repository->IsOptional(i)) {
@@ -69,11 +69,11 @@ SchedulingConstraintHelper::SchedulingConstraintHelper(
reason_for_presence_.push_back(kNoLiteralIndex);
}
if (repository->SizeVar(i) == kNoIntegerVariable) {
duration_vars_.push_back(kNoIntegerVariable);
fixed_durations_.push_back(repository->MinSize(i));
size_vars_.push_back(kNoIntegerVariable);
fixed_sizes_.push_back(repository->MinSize(i));
} else {
duration_vars_.push_back(repository->SizeVar(i));
fixed_durations_.push_back(IntegerValue(0));
size_vars_.push_back(repository->SizeVar(i));
fixed_sizes_.push_back(IntegerValue(0));
}
start_vars_.push_back(repository->StartVar(i));
end_vars_.push_back(repository->EndVar(i));
@@ -102,8 +102,8 @@ void SchedulingConstraintHelper::ResetFromSubset(
end_vars_.resize(num_tasks);
minus_end_vars_.resize(num_tasks);
minus_start_vars_.resize(num_tasks);
duration_vars_.resize(num_tasks);
fixed_durations_.resize(num_tasks);
size_vars_.resize(num_tasks);
fixed_sizes_.resize(num_tasks);
reason_for_presence_.resize(num_tasks);
for (int i = 0; i < num_tasks; ++i) {
const int t = tasks[i];
@@ -111,8 +111,8 @@ void SchedulingConstraintHelper::ResetFromSubset(
end_vars_[i] = other.end_vars_[t];
minus_end_vars_[i] = other.minus_end_vars_[t];
minus_start_vars_[i] = other.minus_start_vars_[t];
duration_vars_[i] = other.duration_vars_[t];
fixed_durations_[i] = other.fixed_durations_[t];
size_vars_[i] = other.size_vars_[t];
fixed_sizes_[i] = other.fixed_sizes_[t];
reason_for_presence_[i] = other.reason_for_presence_[t];
}
@@ -231,14 +231,14 @@ void SchedulingConstraintHelper::AddReasonForBeingBefore(int before,
// When this happen it is because we used the "Shifted" end min instead.
// TODO(user): This is pretty rare, but we could also relax the reason a bit.
if (StartMax(before) >= EndMin(after)) {
CHECK_LT(StartMax(before), StartMin(after) + DurationMin(after));
CHECK_LT(StartMax(before), StartMin(after) + SizeMin(after));
integer_reason_.push_back(
integer_trail_->UpperBoundAsLiteral(start_vars_[before]));
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(start_vars_[after]));
if (duration_vars_[after] != kNoIntegerVariable) {
if (size_vars_[after] != kNoIntegerVariable) {
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(duration_vars_[after]));
integer_trail_->LowerBoundAsLiteral(size_vars_[after]));
}
return;
}
@@ -263,9 +263,9 @@ void SchedulingConstraintHelper::AddReasonForBeingBefore(int before,
{end_min_lit.var, start_max_lit.var}, &integer_reason_);
}
bool SchedulingConstraintHelper::PushIntegerLiteral(IntegerLiteral bound) {
bool SchedulingConstraintHelper::PushIntegerLiteral(IntegerLiteral lit) {
CHECK(other_helper_ == nullptr);
return integer_trail_->Enqueue(bound, literal_reason_, integer_reason_);
return integer_trail_->Enqueue(lit, literal_reason_, integer_reason_);
}
bool SchedulingConstraintHelper::PushIntegerLiteralIfTaskPresent(
@@ -354,8 +354,8 @@ void SchedulingConstraintHelper::WatchAllTasks(int id,
if (watch_end_max) {
watcher->WatchUpperBound(end_vars_[t], id);
}
if (duration_vars_[t] != kNoIntegerVariable) {
watcher->WatchLowerBound(duration_vars_[t], id);
if (size_vars_[t] != kNoIntegerVariable) {
watcher->WatchLowerBound(size_vars_[t], id);
}
if (!IsPresent(t) && !IsAbsent(t)) {
watcher->WatchLiteral(Literal(reason_for_presence_[t]), id);
@@ -386,7 +386,7 @@ void SchedulingConstraintHelper::ImportOtherReasons(
std::string SchedulingConstraintHelper::TaskDebugString(int t) const {
return absl::StrCat("t=", t, " is_present=", IsPresent(t),
" min_duration=", DurationMin(t).value(), " start=[",
" min_size=", SizeMin(t).value(), " start=[",
StartMin(t).value(), ",", StartMax(t).value(), "]",
" end=[", EndMin(t).value(), ",", EndMax(t).value(), "]");
}

108
ortools/sat/intervals.h
View File

@@ -161,37 +161,38 @@ class SchedulingConstraintHelper {
void SetTimeDirection(bool is_forward);
// Helpers for the current bounds on the current task time window.
// [(duration-min) ... (duration-min)]
// [ (size-min) ... (size-min) ]
// ^ ^ ^ ^
// start-min end-min start-max end-max
//
// Note that for tasks with variable durations, we don't necessarily have
// duration-min between the XXX-min and XXX-max value.
IntegerValue DurationMin(int t) const;
IntegerValue DurationMax(int t) const;
// Note that for tasks with variable sizes, we don't necessarily have
// size-min between the XXX-min and XXX-max value.
IntegerValue SizeMin(int t) const;
IntegerValue SizeMax(int t) const;
IntegerValue StartMin(int t) const;
IntegerValue StartMax(int t) const;
IntegerValue EndMin(int t) const;
IntegerValue EndMax(int t) const;
// In the presense of tasks with a variable duration, we do not necessarily
// have start_min + duration_min = end_min, we can instead have a situation
// In the presence of tasks with a variable size, we do not necessarily
// have start_min + size_min = end_min, we can instead have a situation
// like:
// | |<- duration-min ->|
// | |<--- size-min --->|
// ^ ^ ^
// start-min | end-min
// |
// We define the "shifted start min" to be the right most time such that
// we known that we must have min-duration "energy" to the right of it if the
// we known that we must have min-size "energy" to the right of it if the
// task is present. Using it in our scheduling propagators allows to propagate
// more in the presence of tasks with variable duration (or optional task
// where we also do not necessarily have start_min + duration_min = end_min.
// more in the presence of tasks with variable size (or optional task
// where we also do not necessarily have start_min + size_min = end_min.
//
// To explain this shifted start min, one must use the AddEnergyAfterReason().
IntegerValue ShiftedStartMin(int t) const;
bool StartIsFixed(int t) const;
bool EndIsFixed(int t) const;
bool SizeIsFixed(int t) const;
// Returns true if the corresponding fact is known for sure. A normal task is
// always present. For optional task for which the presence is still unknown,
@@ -218,8 +219,8 @@ class SchedulingConstraintHelper {
// Functions to clear and then set the current reason.
void ClearReason();
void AddPresenceReason(int t);
void AddDurationMinReason(int t);
void AddDurationMinReason(int t, IntegerValue lower_bound);
void AddSizeMinReason(int t);
void AddSizeMinReason(int t, IntegerValue lower_bound);
void AddStartMinReason(int t, IntegerValue lower_bound);
void AddStartMaxReason(int t, IntegerValue upper_bound);
void AddEndMinReason(int t, IntegerValue lower_bound);
@@ -249,20 +250,23 @@ class SchedulingConstraintHelper {
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_min_start);
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_max_end);
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t);
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral bound);
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit);
ABSL_MUST_USE_RESULT bool ReportConflict();
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(
int t, IntegerLiteral bound);
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t,
IntegerLiteral lit);
// Returns the underlying integer variables.
const std::vector<IntegerVariable>& StartVars() const { return start_vars_; }
const std::vector<IntegerVariable>& EndVars() const { return end_vars_; }
const std::vector<IntegerVariable>& DurationVars() const {
return duration_vars_;
const std::vector<IntegerVariable>& SizeVars() const { return size_vars_; }
IntegerVariable SizeVar(int index) const { return size_vars_[index]; }
Literal PresenceLiteral(int index) const {
DCHECK(IsOptional(index));
return Literal(reason_for_presence_[index]);
}
// Registers the given propagator id to be called if any of the tasks
// in this class change. Note that we do not watch duration max though.
// in this class change. Note that we do not watch size max though.
void WatchAllTasks(int id, GenericLiteralWatcher* watcher,
bool watch_start_max = true,
bool watch_end_max = true) const;
@@ -313,8 +317,8 @@ class SchedulingConstraintHelper {
// The vectors are indexed by the task index t.
std::vector<IntegerVariable> start_vars_;
std::vector<IntegerVariable> end_vars_;
std::vector<IntegerVariable> duration_vars_;
std::vector<IntegerValue> fixed_durations_;
std::vector<IntegerVariable> size_vars_;
std::vector<IntegerValue> fixed_sizes_;
std::vector<LiteralIndex> reason_for_presence_;
// The negation of the start/end variable so that SetTimeDirection()
@@ -347,16 +351,22 @@ class SchedulingConstraintHelper {
// SchedulingConstraintHelper inlined functions.
// =============================================================================
inline IntegerValue SchedulingConstraintHelper::DurationMin(int t) const {
return duration_vars_[t] == kNoIntegerVariable
? fixed_durations_[t]
: integer_trail_->LowerBound(duration_vars_[t]);
inline IntegerValue SchedulingConstraintHelper::SizeMin(int t) const {
return size_vars_[t] == kNoIntegerVariable
? fixed_sizes_[t]
: integer_trail_->LowerBound(size_vars_[t]);
}
inline IntegerValue SchedulingConstraintHelper::DurationMax(int t) const {
return duration_vars_[t] == kNoIntegerVariable
? fixed_durations_[t]
: integer_trail_->UpperBound(duration_vars_[t]);
inline IntegerValue SchedulingConstraintHelper::SizeMax(int t) const {
return size_vars_[t] == kNoIntegerVariable
? fixed_sizes_[t]
: integer_trail_->UpperBound(size_vars_[t]);
}
inline bool SchedulingConstraintHelper::SizeIsFixed(int t) const {
return size_vars_[t] == kNoIntegerVariable
? true
: integer_trail_->IsFixed(size_vars_[t]);
}
inline IntegerValue SchedulingConstraintHelper::StartMin(int t) const {
@@ -375,9 +385,9 @@ inline IntegerValue SchedulingConstraintHelper::EndMax(int t) const {
return integer_trail_->UpperBound(end_vars_[t]);
}
// for optional interval, we don't necessarily have start + duration = end.
// for optional interval, we don't necessarily have start + size = end.
inline IntegerValue SchedulingConstraintHelper::ShiftedStartMin(int t) const {
return std::max(StartMin(t), EndMin(t) - DurationMin(t));
return std::max(StartMin(t), EndMin(t) - SizeMin(t));
}
inline bool SchedulingConstraintHelper::StartIsFixed(int t) const {
@@ -419,21 +429,21 @@ inline void SchedulingConstraintHelper::AddPresenceReason(int t) {
}
}
inline void SchedulingConstraintHelper::AddDurationMinReason(int t) {
inline void SchedulingConstraintHelper::AddSizeMinReason(int t) {
AddOtherReason(t);
if (duration_vars_[t] != kNoIntegerVariable) {
if (size_vars_[t] != kNoIntegerVariable) {
integer_reason_.push_back(
integer_trail_->LowerBoundAsLiteral(duration_vars_[t]));
integer_trail_->LowerBoundAsLiteral(size_vars_[t]));
}
}
inline void SchedulingConstraintHelper::AddDurationMinReason(
inline void SchedulingConstraintHelper::AddSizeMinReason(
int t, IntegerValue lower_bound) {
AddOtherReason(t);
if (duration_vars_[t] != kNoIntegerVariable) {
DCHECK_GE(DurationMin(t), lower_bound);
if (size_vars_[t] != kNoIntegerVariable) {
DCHECK_GE(SizeMin(t), lower_bound);
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(duration_vars_[t], lower_bound));
IntegerLiteral::GreaterOrEqual(size_vars_[t], lower_bound));
}
}
@@ -458,15 +468,15 @@ inline void SchedulingConstraintHelper::AddEndMinReason(
AddOtherReason(t);
if (EndMin(t) < lower_bound) {
// This might happen if we used for the end_min the max between end_min
// and start_min + duration_min. That is, the end_min assuming the task is
// and start_min + size_min. That is, the end_min assuming the task is
// present.
const IntegerValue duration_min = DurationMin(t);
if (duration_vars_[t] != kNoIntegerVariable) {
const IntegerValue size_min = SizeMin(t);
if (size_vars_[t] != kNoIntegerVariable) {
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(duration_vars_[t], duration_min));
IntegerLiteral::GreaterOrEqual(size_vars_[t], size_min));
}
integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(
start_vars_[t], lower_bound - duration_min));
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(start_vars_[t], lower_bound - size_min));
return;
}
integer_reason_.push_back(
@@ -491,9 +501,9 @@ inline void SchedulingConstraintHelper::AddEnergyAfterReason(
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(end_vars_[t], time + energy_min));
}
if (duration_vars_[t] != kNoIntegerVariable) {
if (size_vars_[t] != kNoIntegerVariable) {
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(duration_vars_[t], energy_min));
IntegerLiteral::GreaterOrEqual(size_vars_[t], energy_min));
}
}
@@ -632,7 +642,7 @@ inline std::function<void(Model*)> IntervalWithAlternatives(
IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
std::vector<Literal> presences;
std::vector<IntegerValue> durations;
std::vector<IntegerValue> sizes;
// Create an "exactly one executed" constraint on the alternatives.
std::vector<LiteralWithCoeff> sat_ct;
@@ -649,10 +659,10 @@ inline std::function<void(Model*)> IntervalWithAlternatives(
// Generalize to an "int_var_element" constraint.
CHECK_EQ(intervals->SizeVar(member), kNoIntegerVariable);
presences.push_back(is_present);
durations.push_back(intervals->MinSize(member));
sizes.push_back(intervals->MinSize(member));
}
if (intervals->SizeVar(master) != kNoIntegerVariable) {
model->Add(IsOneOf(intervals->SizeVar(master), presences, durations));
model->Add(IsOneOf(intervals->SizeVar(master), presences, sizes));
}
model->Add(BooleanLinearConstraint(1, 1, &sat_ct));

19
ortools/sat/linear_constraint_manager.cc
View File

@@ -56,7 +56,10 @@ LinearConstraintManager::~LinearConstraintManager() {
VLOG(2) << "num_coeff_strenghtening: " << num_coeff_strenghtening_;
}
if (sat_parameters_.log_search_progress() && num_cuts_ > 0) {
LOG(INFO) << "Total cuts added: " << num_cuts_;
LOG(INFO) << "Total cuts added: " << num_cuts_ << " (out of "
<< num_add_cut_calls_ << " calls) worker: '" << model_->Name()
<< "'";
LOG(INFO) << "Num simplifications: " << num_simplifications_;
for (const auto& entry : type_to_num_cuts_) {
LOG(INFO) << "Added " << entry.second << " cuts of type '" << entry.first
<< "'.";
@@ -78,7 +81,6 @@ bool LinearConstraintManager::MaybeRemoveSomeInactiveConstraints(
const glop::RowIndex num_rows(lp_constraints_.size());
const glop::ColIndex num_cols =
solution_state->statuses.size() - RowToColIndex(num_rows);
int new_size = 0;
for (int i = 0; i < num_rows; ++i) {
const ConstraintIndex constraint_index = lp_constraints_[i];
@@ -205,6 +207,7 @@ bool LinearConstraintManager::AddCut(
LinearConstraint ct, std::string type_name,
const gtl::ITIVector<IntegerVariable, double>& lp_solution,
std::string extra_info) {
++num_add_cut_calls_;
if (ct.vars.empty()) return false;
const double activity = ComputeActivity(ct, lp_solution);
@@ -439,6 +442,7 @@ bool LinearConstraintManager::ChangeLp(
glop::BasisState* solution_state) {
VLOG(3) << "Enter ChangeLP, scan " << constraint_infos_.size()
<< " constraints";
const double saved_dtime = dtime_;
std::vector<ConstraintIndex> new_constraints;
std::vector<double> new_constraints_efficacies;
std::vector<double> new_constraints_orthogonalities;
@@ -448,13 +452,16 @@ bool LinearConstraintManager::ChangeLp(
last_simplification_timestamp_ = integer_trail_.num_level_zero_enqueues();
// We keep any constraints that is already present, and otherwise, we add the
// ones that are currently not satisfied by at least "tolerance".
// ones that are currently not satisfied by at least "tolerance" to the set
// of potential new constraints.
bool rescale_active_count = false;
const double tolerance = 1e-6;
for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
// Inprocessing of the constraint.
if (simplify_constraints &&
SimplifyConstraint(&constraint_infos_[i].constraint)) {
++num_simplifications_;
// Note that the canonicalization shouldn't be needed since the order
// of the variable is not changed by the simplification, and we only
// reduce the coefficients at both end of the spectrum.
@@ -477,6 +484,10 @@ bool LinearConstraintManager::ChangeLp(
if (constraint_infos_[i].is_in_lp) continue;
// ComputeActivity() often represent the bulk of the time spent in
// ChangeLP().
dtime_ += 1.7e-9 *
static_cast<double>(constraint_infos_[i].constraint.vars.size());
const double activity =
ComputeActivity(constraint_infos_[i].constraint, lp_solution);
const double lb_violation =
@@ -657,6 +668,8 @@ bool LinearConstraintManager::ChangeLp(
PermanentlyRemoveSomeConstraints();
}
time_limit_->AdvanceDeterministicTime(dtime_ - saved_dtime);
// The LP changed only if we added new constraints or if some constraints
// already inside changed (simplification or tighter bounds).
if (current_lp_is_changed_) {

5
ortools/sat/linear_constraint_manager.h
View File

@@ -180,18 +180,23 @@ class LinearConstraintManager {
// constraints.
absl::flat_hash_map<size_t, ConstraintIndex> equiv_constraints_;
int64 num_simplifications_ = 0;
int64 num_merged_constraints_ = 0;
int64 num_shortened_constraints_ = 0;
int64 num_splitted_constraints_ = 0;
int64 num_coeff_strenghtening_ = 0;
int64 num_cuts_ = 0;
int64 num_add_cut_calls_ = 0;
std::map<std::string, int> type_to_num_cuts_;
bool objective_is_defined_ = false;
bool objective_norm_computed_ = false;
double objective_l2_norm_ = 0.0;
// Total deterministic time spent in this class.
double dtime_ = 0.0;
// Dense representation of the objective coeffs indexed by positive variables
// indices. It contains 0.0 where the variables does not appear in the
// objective.

12
ortools/sat/linear_relaxation.cc
View File

@@ -452,8 +452,7 @@ void TryToLinearizeConstraint(const CpModelProto& model_proto,
const IntegerVariable size = mapping->Integer(ct.interval().size());
const IntegerVariable end = mapping->Integer(ct.interval().end());
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
const bool size_is_fixed =
integer_trail->LowerBound(size) == integer_trail->UpperBound(size);
const bool size_is_fixed = integer_trail->IsFixed(size);
const IntegerValue rhs =
size_is_fixed ? -integer_trail->LowerBound(size) : IntegerValue(0);
LinearConstraintBuilder lc(model, rhs, rhs);
@@ -463,12 +462,13 @@ void TryToLinearizeConstraint(const CpModelProto& model_proto,
}
lc.AddTerm(end, IntegerValue(-1));
if (HasEnforcementLiteral(ct)) {
LinearConstraint tmp_lc = lc.Build();
LinearExpression expr;
expr.coeffs = lc.Build().coeffs;
expr.vars = lc.Build().vars;
expr.coeffs = tmp_lc.coeffs;
expr.vars = tmp_lc.vars;
AppendEnforcedLinearExpression(
mapping->Literals(ct.enforcement_literal()), expr, rhs, rhs, *model,
relaxation);
mapping->Literals(ct.enforcement_literal()), expr, tmp_lc.ub,
tmp_lc.ub, *model, relaxation);
} else {
relaxation->linear_constraints.push_back(lc.Build());
}

2
ortools/sat/samples/BUILD
View File

@@ -1,5 +1,7 @@
load(":code_samples.bzl", "code_sample_cc")
COPTS=["-std=c++17"]
code_sample_cc(sample = "assignment_sat")
code_sample_cc(sample = "binpacking_problem_sat")

14
ortools/sat/timetable.cc
View File

@@ -196,7 +196,7 @@ bool TimeTablingPerTask::SweepAllTasks(bool is_forward) {
// 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
// the demand/duration/presence/start ...
// the demand/size/presence/start ...
for (int i = num_tasks - 1; i >= 0; --i) {
const int t = tasks[i];
if (helper_->IsAbsent(t) ||
@@ -220,9 +220,9 @@ bool TimeTablingPerTask::SweepAllTasks(bool is_forward) {
continue;
}
// Skip if duration is zero.
if (helper_->DurationMin(t) == 0) {
if (helper_->DurationMax(t) == 0) {
// Skip if size is zero.
if (helper_->SizeMin(t) == 0) {
if (helper_->SizeMax(t) == 0) {
std::swap(tasks[i], tasks[--num_tasks]);
}
continue;
@@ -236,7 +236,7 @@ bool TimeTablingPerTask::SweepAllTasks(bool is_forward) {
bool TimeTablingPerTask::SweepTask(int task_id) {
const IntegerValue start_max = helper_->StartMax(task_id);
const IntegerValue duration_min = helper_->DurationMin(task_id);
const IntegerValue size_min = helper_->SizeMin(task_id);
const IntegerValue initial_start_min = helper_->StartMin(task_id);
const IntegerValue initial_end_min = helper_->EndMin(task_id);
@@ -292,7 +292,7 @@ bool TimeTablingPerTask::SweepTask(int task_id) {
}
}
new_end_min = std::max(new_end_min, new_start_min + duration_min);
new_end_min = std::max(new_end_min, new_start_min + size_min);
limit = std::min(start_max, new_end_min);
if (profile_[rec_id].start < initial_end_min) {
@@ -337,7 +337,7 @@ bool TimeTablingPerTask::UpdateStartingTime(int task_id, IntegerValue left,
// State of the task to be pushed.
helper_->AddEndMinReason(task_id, left + 1);
helper_->AddDurationMinReason(task_id, IntegerValue(1));
helper_->AddSizeMinReason(task_id, IntegerValue(1));
if (demands_[task_id].var != kNoIntegerVariable) {
helper_->MutableIntegerReason()->push_back(
integer_trail_->LowerBoundAsLiteral(demands_[task_id].var));

12
ortools/sat/timetable_edgefinding.cc
View File

@@ -165,9 +165,9 @@ bool TimeTableEdgeFinding::TimeTableEdgeFindingPass() {
const IntegerValue start_max = helper_->StartMax(t);
const IntegerValue end_min = helper_->EndMin(t);
if (start_max >= end_min) {
size_free_[t] = helper_->DurationMin(t);
size_free_[t] = helper_->SizeMin(t);
} else {
size_free_[t] = helper_->DurationMin(t) + start_max - end_min;
size_free_[t] = helper_->SizeMin(t) + start_max - end_min;
}
energy_free_[t] = size_free_[t] * DemandMin(t);
}
@@ -321,7 +321,7 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin,
integer_trail_->LowerBoundAsLiteral(demands_[task_index].var));
}
helper_->AddStartMinReason(task_index, begin);
helper_->AddDurationMinReason(task_index);
helper_->AddSizeMinReason(task_index);
// Task contributing to the energy in the interval.
for (int t = 0; t < num_tasks_; ++t) {
@@ -342,11 +342,11 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin,
// could relax the reason more.
//
// TODO(user): This reason might not be enough in the presence of variable
// duration intervals where StartMax and EndMin give rise to more energy
// that just using duration min and these bounds. Fix.
// size intervals where StartMax and EndMin give rise to more energy
// that just using size min and these bounds. Fix.
helper_->AddStartMinReason(t, std::min(begin, helper_->StartMin(t)));
helper_->AddEndMaxReason(t, std::max(end, helper_->EndMax(t)));
helper_->AddDurationMinReason(t);
helper_->AddSizeMinReason(t);
helper_->AddPresenceReason(t);
}