From bf87fd8ad4ca3bb4707da0164e63422cb403f61b Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 30 Jan 2025 12:45:02 +0100 Subject: [PATCH] [CP-SAT] more minor improvements --- ortools/sat/2d_rectangle_presolve.cc | 1 + ortools/sat/disjunctive.cc | 15 ++++++-- ortools/sat/integer.cc | 14 ++----- ortools/sat/integer.h | 7 +++- ortools/sat/intervals.cc | 7 ++++ ortools/sat/scheduling_helpers.cc | 56 ++++++++++++---------------- ortools/sat/scheduling_helpers.h | 30 ++++++++++----- ortools/sat/timetable.cc | 3 +- ortools/sat/timetable_edgefinding.cc | 2 +- 9 files changed, 74 insertions(+), 61 deletions(-) diff --git a/ortools/sat/2d_rectangle_presolve.cc b/ortools/sat/2d_rectangle_presolve.cc index 07ca6be0d4..ebc940b3c0 100644 --- a/ortools/sat/2d_rectangle_presolve.cc +++ b/ortools/sat/2d_rectangle_presolve.cc @@ -111,6 +111,7 @@ bool PresolveFixed2dRectangles( // The whole rectangle was outside of the domain, remove it. std::swap(rectangle, (*fixed_boxes)[fixed_boxes->size() - 1]); fixed_boxes->resize(fixed_boxes->size() - 1); + changed = true; continue; } else { new_size++; diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index bc0823d813..a72b3ac18f 100644 --- a/ortools/sat/disjunctive.cc +++ b/ortools/sat/disjunctive.cc @@ -871,18 +871,19 @@ bool DisjunctiveDetectablePrecedences::Propagate() { const auto by_shifted_smin = helper_->TaskByIncreasingShiftedStartMin(); int rank = -1; IntegerValue window_end = kMinIntegerValue; + int* const ranks = ranks_.data(); for (const auto [task, presence_lit, start_min] : by_shifted_smin) { if (!helper_->IsPresent(presence_lit)) { - ranks_[task] = -1; + ranks[task] = -1; continue; } const IntegerValue size_min = helper_->SizeMin(task); if (start_min < window_end) { - ranks_[task] = rank; + ranks[task] = rank; window_end += size_min; } else { - ranks_[task] = ++rank; + ranks[task] = ++rank; window_end = start_min + size_min; } } @@ -1329,9 +1330,15 @@ bool DisjunctivePrecedences::PropagateSubwindow() { int DisjunctivePrecedences::RegisterWith(GenericLiteralWatcher* watcher) { // This propagator reach the fixed point in one go. + // Maybe not in corner cases, but since it is expansive, it is okay not to + // run it again right away + // + // Note also that technically, we don't need to be waked up if only the upper + // bound of the task changes, but this require to use more memory and the gain + // is unclear as this runs with the highest priority. const int id = watcher->Register(this); helper_->SetTimeDirection(time_direction_); - helper_->WatchAllTasks(id, /*watch_max_side=*/false); + helper_->WatchAllTasks(id); return id; } diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 20a30a562a..32015e3c85 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -2119,10 +2119,7 @@ void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) { const Literal literal = (*trail)[propagation_trail_index_++]; if (literal.Index() >= literal_limit) continue; for (const auto entry : literal_to_watcher_[literal]) { - if (!in_queue_[entry.id]) { - in_queue_[entry.id] = true; - queue_by_priority_[id_to_priority_[entry.id]].push_back(entry.id); - } + CallOnNextPropagate(entry.id); if (entry.watch_index >= 0) { id_to_watch_indices_[entry.id].push_back(entry.watch_index); } @@ -2134,10 +2131,7 @@ void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) { for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) { if (var.value() >= var_limit) continue; for (const auto entry : var_to_watcher_[var]) { - if (!in_queue_[entry.id]) { - in_queue_[entry.id] = true; - queue_by_priority_[id_to_priority_[entry.id]].push_back(entry.id); - } + CallOnNextPropagate(entry.id); if (entry.watch_index >= 0) { id_to_watch_indices_[entry.id].push_back(entry.watch_index); } @@ -2161,9 +2155,7 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) { const int level = trail->CurrentDecisionLevel(); if (level == 0) { for (const int id : propagator_ids_to_call_at_level_zero_) { - if (in_queue_[id]) continue; - in_queue_[id] = true; - queue_by_priority_[id_to_priority_[id]].push_back(id); + CallOnNextPropagate(id); } } diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 91d22b090c..24ff2e3524 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -787,6 +787,7 @@ class IntegerTrail final : public SatPropagator { void AddAllGreaterThanConstantReason(absl::Span exprs, IntegerValue target_min, std::vector* indices) const { + int64_t num_processed = 0; for (const AffineExpression& expr : exprs) { if (expr.IsConstant()) { DCHECK_GE(expr.constant, target_min); @@ -794,6 +795,10 @@ class IntegerTrail final : public SatPropagator { } DCHECK_NE(expr.var, kNoIntegerVariable); + // On large routing problems, we can spend a lot of time in this loop. + // We check the time limit every 5 processed expressions. + if (++num_processed % 5 == 0 && time_limit_->LimitReached()) return; + // Skip if we already have an explanation for expr >= target_min. Note // that we already do that while processing the returned indices, so this // mainly save a FindLowestTrailIndexThatExplainBound() call per skipped @@ -897,7 +902,7 @@ class IntegerTrail final : public SatPropagator { // Returns some debugging info. std::string DebugString(); - // Used internally to return the next conlict number. + // Used internally to return the next conflict number. int64_t NextConflictId(); // Information for each integer variable about its current lower bound and diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index d04f6c2d80..ff5ec85852 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -214,6 +214,12 @@ SchedulingConstraintHelper* IntervalsRepository::GetOrCreateHelper( std::vector sizes; std::vector reason_for_presence; + const int num_variables = variables.size(); + starts.reserve(num_variables); + ends.reserve(num_variables); + sizes.reserve(num_variables); + reason_for_presence.reserve(num_variables); + for (const IntervalVariable i : variables) { if (IsOptional(i)) { reason_for_presence.push_back(PresenceLiteral(i).Index()); @@ -224,6 +230,7 @@ SchedulingConstraintHelper* IntervalsRepository::GetOrCreateHelper( starts.push_back(Start(i)); ends.push_back(End(i)); } + SchedulingConstraintHelper* helper = new SchedulingConstraintHelper( std::move(starts), std::move(ends), std::move(sizes), std::move(reason_for_presence), model_); diff --git a/ortools/sat/scheduling_helpers.cc b/ortools/sat/scheduling_helpers.cc index 78e995e93b..c391a957f2 100644 --- a/ortools/sat/scheduling_helpers.cc +++ b/ortools/sat/scheduling_helpers.cc @@ -20,7 +20,6 @@ #include #include -#include "absl/container/flat_hash_map.h" #include "absl/log/check.h" #include "absl/meta/type_traits.h" #include "absl/strings/str_cat.h" @@ -47,8 +46,8 @@ SchedulingConstraintHelper::SchedulingConstraintHelper( std::vector sizes, std::vector reason_for_presence, Model* model) : model_(model), - trail_(model->GetOrCreate()), sat_solver_(model->GetOrCreate()), + assignment_(sat_solver_->Assignment()), integer_trail_(model->GetOrCreate()), watcher_(model->GetOrCreate()), precedence_relations_(model->GetOrCreate()), @@ -64,15 +63,17 @@ SchedulingConstraintHelper::SchedulingConstraintHelper( cached_negated_end_max_(new IntegerValue[capacity_]), cached_shifted_start_min_(new IntegerValue[capacity_]), cached_negated_shifted_end_max_(new IntegerValue[capacity_]) { - minus_ends_.clear(); - minus_starts_.clear(); DCHECK_EQ(starts_.size(), ends_.size()); DCHECK_EQ(starts_.size(), sizes_.size()); DCHECK_EQ(starts_.size(), reason_for_presence_.size()); + minus_starts_.clear(); + minus_starts_.reserve(starts_.size()); + minus_ends_.clear(); + minus_ends_.reserve(starts_.size()); for (int i = 0; i < starts_.size(); ++i) { - minus_ends_.push_back(ends_[i].Negated()); minus_starts_.push_back(starts_[i].Negated()); + minus_ends_.push_back(ends_[i].Negated()); } InitSortedVectors(); @@ -84,8 +85,8 @@ SchedulingConstraintHelper::SchedulingConstraintHelper( SchedulingConstraintHelper::SchedulingConstraintHelper(int num_tasks, Model* model) : model_(model), - trail_(model->GetOrCreate()), sat_solver_(model->GetOrCreate()), + assignment_(sat_solver_->Assignment()), integer_trail_(model->GetOrCreate()), precedence_relations_(model->GetOrCreate()), capacity_(num_tasks), @@ -120,6 +121,16 @@ void SchedulingConstraintHelper::RegisterWith(GenericLiteralWatcher* watcher) { watcher->WatchIntegerVariable(sizes_[t].var, id, t); watcher->WatchIntegerVariable(starts_[t].var, id, t); watcher->WatchIntegerVariable(ends_[t].var, id, t); + + // This class do not need to be waked up on presence change, since this is + // not cached. However given that we can have many propagators that use the + // same helper, it is nicer to only register this one, and wake up all + // propagator through it rather than registering all of them individually. + // Note that IncrementalPropagate() will do nothing if this is the only + // change except waking up registered propagators. + if (!IsPresent(t) && !IsAbsent(t)) { + watcher_->WatchLiteral(Literal(reason_for_presence_[t]), id); + } } watcher->SetPropagatorPriority(id, 0); } @@ -352,7 +363,7 @@ IntegerValue SchedulingConstraintHelper::GetCurrentMinDistanceBetweenTasks( bool SchedulingConstraintHelper::PropagatePrecedence(int a, int b) { CHECK(IsPresent(a)); CHECK(IsPresent(b)); - CHECK_EQ(trail_->CurrentDecisionLevel(), 0); + CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); const AffineExpression before = ends_[a]; const AffineExpression after = starts_[b]; @@ -370,7 +381,7 @@ bool SchedulingConstraintHelper::PropagatePrecedence(int a, int b) { AddWeightedSumLowerOrEqual({}, {before.var, after.var}, {int64_t{1}, int64_t{-1}}, -offset.value(), model_); - if (model_->GetOrCreate()->ModelIsUnsat()) return false; + if (sat_solver_->ModelIsUnsat()) return false; } return true; } @@ -609,30 +620,11 @@ bool SchedulingConstraintHelper::ReportConflict() { return integer_trail_->ReportConflict(literal_reason_, integer_reason_); } -void SchedulingConstraintHelper::WatchAllTasks(int id, bool watch_max_side) { - // In all cases, we watch presence literals since this class is not waked up - // when those changes. - const int num_tasks = starts_.size(); - for (int t = 0; t < num_tasks; ++t) { - if (!IsPresent(t) && !IsAbsent(t)) { - watcher_->WatchLiteral(Literal(reason_for_presence_[t]), id); - } - } - - // If everything is watched, it is slighlty more efficient to enqueue the - // propagator when the helper Propagate() is called. This result in less - // entries in our watched lists. - if (watch_max_side) { - propagator_ids_.push_back(id); - return; - } - - // We only watch "min" side. - for (int t = 0; t < num_tasks; ++t) { - watcher_->WatchLowerBound(starts_[t], id); - watcher_->WatchLowerBound(ends_[t], id); - watcher_->WatchLowerBound(sizes_[t], id); - } +void SchedulingConstraintHelper::WatchAllTasks(int id) { + // It is more efficient to enqueue the propagator + // when the helper Propagate() is called. This result in less entries in our + // watched lists. + propagator_ids_.push_back(id); } void SchedulingConstraintHelper::AddOtherReason(int t) { diff --git a/ortools/sat/scheduling_helpers.h b/ortools/sat/scheduling_helpers.h index 1612fb795c..0ecd1f8404 100644 --- a/ortools/sat/scheduling_helpers.h +++ b/ortools/sat/scheduling_helpers.h @@ -318,7 +318,7 @@ class SchedulingConstraintHelper : public PropagatorInterface { // Registers the given propagator id to be called if any of the tasks // in this class change. Note that we do not watch size max though. - void WatchAllTasks(int id, bool watch_max_side = true); + void WatchAllTasks(int id); // Manages the other helper (used by the diffn constraint). // @@ -349,7 +349,9 @@ class SchedulingConstraintHelper : public PropagatorInterface { // not handle this correctly. bool InPropagationLoop() const { return integer_trail_->InPropagationLoop(); } - int CurrentDecisionLevel() const { return trail_->CurrentDecisionLevel(); } + int CurrentDecisionLevel() const { + return sat_solver_->CurrentDecisionLevel(); + } private: // Tricky: when a task is optional, it is possible it size min is negative, @@ -384,8 +386,8 @@ class SchedulingConstraintHelper : public PropagatorInterface { void ImportOtherReasons(); Model* model_; - Trail* trail_; SatSolver* sat_solver_; + const VariablesAssignment& assignment_; IntegerTrail* integer_trail_; GenericLiteralWatcher* watcher_; PrecedenceRelations* precedence_relations_; @@ -610,17 +612,25 @@ inline bool SchedulingConstraintHelper::SizeIsFixed(int t) const { } inline bool SchedulingConstraintHelper::IsOptional(int t) const { - return reason_for_presence_[t] != kNoLiteralIndex; + DCHECK_GE(t, 0); + DCHECK_LT(t, reason_for_presence_.size()); + return reason_for_presence_.data()[t] != kNoLiteralIndex; } inline bool SchedulingConstraintHelper::IsPresent(int t) const { - if (reason_for_presence_[t] == kNoLiteralIndex) return true; - return trail_->Assignment().LiteralIsTrue(Literal(reason_for_presence_[t])); + DCHECK_GE(t, 0); + DCHECK_LT(t, reason_for_presence_.size()); + const LiteralIndex lit = reason_for_presence_.data()[t]; + if (lit == kNoLiteralIndex) return true; + return assignment_.LiteralIsTrue(Literal(lit)); } inline bool SchedulingConstraintHelper::IsAbsent(int t) const { - if (reason_for_presence_[t] == kNoLiteralIndex) return false; - return trail_->Assignment().LiteralIsFalse(Literal(reason_for_presence_[t])); + DCHECK_GE(t, 0); + DCHECK_LT(t, reason_for_presence_.size()); + const LiteralIndex lit = reason_for_presence_.data()[t]; + if (lit == kNoLiteralIndex) return false; + return assignment_.LiteralIsFalse(Literal(lit)); } inline bool SchedulingConstraintHelper::IsOptional(LiteralIndex lit) const { @@ -629,12 +639,12 @@ inline bool SchedulingConstraintHelper::IsOptional(LiteralIndex lit) const { inline bool SchedulingConstraintHelper::IsPresent(LiteralIndex lit) const { if (lit == kNoLiteralIndex) return true; - return trail_->Assignment().LiteralIsTrue(Literal(lit)); + return assignment_.LiteralIsTrue(Literal(lit)); } inline bool SchedulingConstraintHelper::IsAbsent(LiteralIndex lit) const { if (lit == kNoLiteralIndex) return false; - return trail_->Assignment().LiteralIsFalse(Literal(lit)); + return assignment_.LiteralIsFalse(Literal(lit)); } inline void SchedulingConstraintHelper::ClearReason() { diff --git a/ortools/sat/timetable.cc b/ortools/sat/timetable.cc index 84d6adf08c..b8d194297b 100644 --- a/ortools/sat/timetable.cc +++ b/ortools/sat/timetable.cc @@ -21,7 +21,6 @@ #include "absl/types/span.h" #include "ortools/sat/integer.h" #include "ortools/sat/integer_base.h" -#include "ortools/sat/intervals.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/scheduling_helpers.h" @@ -344,7 +343,7 @@ TimeTablingPerTask::TimeTablingPerTask(AffineExpression capacity, void TimeTablingPerTask::RegisterWith(GenericLiteralWatcher* watcher) { const int id = watcher->Register(this); - helper_->WatchAllTasks(id, watcher); + helper_->WatchAllTasks(id); watcher->WatchUpperBound(capacity_.var, id); for (int t = 0; t < num_tasks_; t++) { watcher->WatchLowerBound(demands_->Demands()[t], id); diff --git a/ortools/sat/timetable_edgefinding.cc b/ortools/sat/timetable_edgefinding.cc index f9ee14890f..00f2081402 100644 --- a/ortools/sat/timetable_edgefinding.cc +++ b/ortools/sat/timetable_edgefinding.cc @@ -49,7 +49,7 @@ TimeTableEdgeFinding::TimeTableEdgeFinding(AffineExpression capacity, void TimeTableEdgeFinding::RegisterWith(GenericLiteralWatcher* watcher) { const int id = watcher->Register(this); watcher->WatchUpperBound(capacity_, id); - helper_->WatchAllTasks(id, watcher); + helper_->WatchAllTasks(id); for (int t = 0; t < num_tasks_; t++) { watcher->WatchLowerBound(demands_->Demands()[t], id); }