From 99d9475b0ed309fac3d09ad2d4df5e23c1564622 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 6 Jun 2022 11:05:46 +0200 Subject: [PATCH] [CP-SAT] use linearized expression in ttef; add probing_max_lp --- ortools/sat/BUILD.bazel | 1 + ortools/sat/cp_model_lns.cc | 2 +- ortools/sat/cp_model_search.cc | 4 ++ ortools/sat/cumulative.cc | 8 ++-- ortools/sat/timetable_edgefinding.cc | 59 +++++++++++++++++++++------- ortools/sat/timetable_edgefinding.h | 7 +++- 6 files changed, 60 insertions(+), 21 deletions(-) diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 9ec5a602e2..c8c58108a1 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -907,6 +907,7 @@ cc_library( srcs = ["timetable_edgefinding.cc"], hdrs = ["timetable_edgefinding.h"], deps = [ + ":implied_bounds", ":integer", ":intervals", ":sat_base", diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc index d0811173e0..ee791cf580 100644 --- a/ortools/sat/cp_model_lns.cc +++ b/ortools/sat/cp_model_lns.cc @@ -625,7 +625,7 @@ void ProcessDemandListFromCumulativeConstraint( unique_starts.push_back(demand.start); } } - CHECK(std::is_sorted(unique_starts.begin(), unique_starts.end())); + DCHECK(std::is_sorted(unique_starts.begin(), unique_starts.end())); const int num_points = unique_starts.size(); // Split the capacity in 2 and dispatch all demands on the 2 parts. diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 35f474303d..5bc32eff69 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -504,6 +504,9 @@ std::vector GetDiverseSetOfParameters( new_params.set_use_hard_precedences_in_cumulative_constraint(true); } strategies["probing"] = new_params; + + new_params.set_linearization_level(2); + strategies["probing_max_lp"] = new_params; } // Search variation. @@ -605,6 +608,7 @@ std::vector GetDiverseSetOfParameters( names.push_back("quick_restart_no_lp"); names.push_back("lb_tree_search"); names.push_back("probing"); + if (base_params.num_workers() > 16) names.push_back("probing_max_lp"); #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP) if (absl::GetFlag(FLAGS_cp_model_use_max_hs)) names.push_back("max_hs"); #endif // !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP) diff --git a/ortools/sat/cumulative.cc b/ortools/sat/cumulative.cc index b3ce923da0..cac0341684 100644 --- a/ortools/sat/cumulative.cc +++ b/ortools/sat/cumulative.cc @@ -244,8 +244,8 @@ std::function Cumulative( // rule. It increases the minimum of the start variables and decreases the // maximum of the end variables, if (parameters.use_timetable_edge_finding_in_cumulative_constraint()) { - TimeTableEdgeFinding* time_table_edge_finding = - new TimeTableEdgeFinding(demands, capacity, helper, integer_trail); + TimeTableEdgeFinding* time_table_edge_finding = new TimeTableEdgeFinding( + demands, capacity, helper, integer_trail, model); time_table_edge_finding->RegisterWith(watcher); model->TakeOwnership(time_table_edge_finding); } @@ -316,8 +316,8 @@ std::function CumulativeTimeDecomposition( model->Add(ReifiedBoolAnd(consume_condition, consume)); - // TODO(user): this is needed because we currently can't create a - // boolean variable if the model is unsat. + // this is needed because we currently can't create a boolean variable + // if the model is unsat. if (sat_solver->IsModelUnsat()) return; literals_with_coeff.push_back( diff --git a/ortools/sat/timetable_edgefinding.cc b/ortools/sat/timetable_edgefinding.cc index 09f38a6607..69e0ae94d7 100644 --- a/ortools/sat/timetable_edgefinding.cc +++ b/ortools/sat/timetable_edgefinding.cc @@ -19,6 +19,7 @@ #include "ortools/base/iterator_adaptors.h" #include "ortools/base/logging.h" +#include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" #include "ortools/sat/intervals.h" #include "ortools/util/strong_integers.h" @@ -28,7 +29,8 @@ namespace sat { TimeTableEdgeFinding::TimeTableEdgeFinding( const std::vector& demands, AffineExpression capacity, - SchedulingConstraintHelper* helper, IntegerTrail* integer_trail) + SchedulingConstraintHelper* helper, IntegerTrail* integer_trail, + Model* model) : num_tasks_(helper->NumTasks()), demands_(demands), capacity_(capacity), @@ -41,6 +43,12 @@ TimeTableEdgeFinding::TimeTableEdgeFinding( // Energy of free parts. size_free_.resize(num_tasks_); energy_free_.resize(num_tasks_); + + // Try to linearize the energy. + energies_.resize(num_tasks_); + for (int t = 0; t < num_tasks_; t++) { + energies_[t] = TryToLinearizeProduct(helper->Sizes()[t], demands[t], model); + } } void TimeTableEdgeFinding::RegisterWith(GenericLiteralWatcher* watcher) { @@ -156,12 +164,27 @@ bool TimeTableEdgeFinding::TimeTableEdgeFindingPass() { // If the task has no mandatory part, then its free part is the task itself. const IntegerValue start_max = helper_->StartMax(t); const IntegerValue end_min = helper_->EndMin(t); + const IntegerValue demand_min = DemandMin(t); + IntegerValue mandatory_energy(0); + if (start_max >= end_min) { size_free_[t] = helper_->SizeMin(t); } else { size_free_[t] = helper_->SizeMin(t) + start_max - end_min; + mandatory_energy = (end_min - start_max) * demand_min; } - energy_free_[t] = size_free_[t] * DemandMin(t); + const IntegerValue min_energy_of_product = helper_->SizeMin(t) * demand_min; + const IntegerValue min_linear_energy = + energies_[t].has_value() ? energies_[t].value().Min(*integer_trail_) + : IntegerValue(0); + CHECK_EQ(size_free_[t] * DemandMin(t) + mandatory_energy, + min_energy_of_product); + // if (min_linear_energy > min_energy_of_product) { + // LOG(INFO) << "linear: " << min_linear_energy.value() + // << " vs product: " << min_energy_of_product.value(); + // } + energy_free_[t] = + std::max(min_linear_energy, min_energy_of_product) - mandatory_energy; } BuildTimeTable(); @@ -294,6 +317,23 @@ bool TimeTableEdgeFinding::TimeTableEdgeFindingPass() { return true; } +void TimeTableEdgeFinding::AddEnergyReason(int task_index) { + if (energies_[task_index].has_value()) { + for (const IntegerVariable var : energies_[task_index].value().vars) { + helper_->MutableIntegerReason()->push_back( + integer_trail_->LowerBoundAsLiteral(var)); + } + } else { + // Variables of the task to be pushed. We do not need the end max for this + // task and we only need for it to begin in the time window. + if (demands_[task_index].var != kNoIntegerVariable) { + helper_->MutableIntegerReason()->push_back( + integer_trail_->LowerBoundAsLiteral(demands_[task_index].var)); + } + helper_->AddSizeMinReason(task_index); + } +} + bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin, IntegerValue end, int task_index, IntegerValue new_start) { @@ -306,14 +346,8 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin, integer_trail_->UpperBoundAsLiteral(capacity_.var)); } - // Variables of the task to be pushed. We do not need the end max for this - // task and we only need for it to begin in the time window. - if (demands_[task_index].var != kNoIntegerVariable) { - mutable_reason->push_back( - integer_trail_->LowerBoundAsLiteral(demands_[task_index].var)); - } helper_->AddStartMinReason(task_index, begin); - helper_->AddSizeMinReason(task_index); + AddEnergyReason(task_index); // Task contributing to the energy in the interval. for (int t = 0; t < num_tasks_; ++t) { @@ -322,11 +356,6 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin, if (helper_->EndMax(t) <= begin) continue; if (helper_->StartMin(t) >= end) continue; - if (demands_[t].var != kNoIntegerVariable) { - mutable_reason->push_back( - integer_trail_->LowerBoundAsLiteral(demands_[t].var)); - } - // We need the reason for the energy contribution of this interval into // [begin, end]. // @@ -338,8 +367,8 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin, // 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_->AddSizeMinReason(t); helper_->AddPresenceReason(t); + AddEnergyReason(t); } return helper_->IncreaseStartMin(task_index, new_start); diff --git a/ortools/sat/timetable_edgefinding.h b/ortools/sat/timetable_edgefinding.h index 099a52f6f7..45392654c3 100644 --- a/ortools/sat/timetable_edgefinding.h +++ b/ortools/sat/timetable_edgefinding.h @@ -63,7 +63,7 @@ class TimeTableEdgeFinding : public PropagatorInterface { TimeTableEdgeFinding(const std::vector& demands, AffineExpression capacity, SchedulingConstraintHelper* helper, - IntegerTrail* integer_trail); + IntegerTrail* integer_trail, Model* model); bool Propagate() final; @@ -87,6 +87,9 @@ class TimeTableEdgeFinding : public PropagatorInterface { bool IncreaseStartMin(IntegerValue begin, IntegerValue end, int task_index, IntegerValue new_start); + // Add the minimum energy reason of a task. + void AddEnergyReason(int task_index); + IntegerValue DemandMin(int task_index) const { return integer_trail_->LowerBound(demands_[task_index]); } @@ -106,6 +109,8 @@ class TimeTableEdgeFinding : public PropagatorInterface { SchedulingConstraintHelper* helper_; IntegerTrail* integer_trail_; + std::vector> energies_; + // Start (resp. end) of the compulsory parts used to build the profile. std::vector scp_; std::vector ecp_;