From eea1ae01b0ce93062f110a40661373300d242ebd Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 10 Nov 2016 18:05:44 +0100 Subject: [PATCH] speedup linear inequations in sat --- src/sat/integer.h | 5 +++ src/sat/integer_expr.cc | 29 +++++++++---- src/sat/integer_expr.h | 1 + src/sat/overload_checker.cc | 85 +++++++++++++++++++++++-------------- src/sat/overload_checker.h | 3 +- 5 files changed, 81 insertions(+), 42 deletions(-) diff --git a/src/sat/integer.h b/src/sat/integer.h index 9b730c68a9..b4d8230b9e 100644 --- a/src/sat/integer.h +++ b/src/sat/integer.h @@ -467,6 +467,11 @@ class IntegerTrail : public SatPropagator { return false; } + // Returns true if the variable lower bound is still the one from level zero. + bool VariableLowerBoundIsFixed(IntegerVariable var) const { + return vars_[var.value()].current_trail_index < vars_.size(); + } + private: // Does the work of MergeReasonInto() when queue_ is already initialized. void MergeReasonIntoInternal(std::vector* output) const; diff --git a/src/sat/integer_expr.cc b/src/sat/integer_expr.cc index 624c48f415..b92d13b498 100644 --- a/src/sat/integer_expr.cc +++ b/src/sat/integer_expr.cc @@ -44,8 +44,15 @@ IntegerSumLE::IntegerSumLE(LiteralIndex reified_literal, void IntegerSumLE::FillIntegerReason() { integer_reason_.clear(); - for (const IntegerVariable& var : vars_) { - integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var)); + index_in_integer_reason_.resize(vars_.size(), -1); + for (int i = 0; i < vars_.size(); ++i) { + const IntegerVariable var = vars_[i]; + if (integer_trail_->VariableLowerBoundIsFixed(var)) { + index_in_integer_reason_[i] = -1; + } else { + index_in_integer_reason_[i] = integer_reason_.size(); + integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var)); + } } } @@ -98,10 +105,14 @@ bool IntegerSumLE::Propagate() { if (new_ub < integer_trail_->UpperBound(vars_[i])) { if (integer_reason_.empty()) FillIntegerReason(); - // We need to remove the entry i temporarily. - const IntegerLiteral saved = integer_reason_[i]; - std::swap(integer_reason_[i], integer_reason_.back()); - integer_reason_.pop_back(); + // We need to remove the entry index from the reason temporarily. + IntegerLiteral saved; + const int index = index_in_integer_reason_[i]; + if (index >= 0) { + saved = integer_reason_[index]; + std::swap(integer_reason_[index], integer_reason_.back()); + integer_reason_.pop_back(); + } if (!integer_trail_->Enqueue( IntegerLiteral::LowerOrEqual(vars_[i], new_ub), literal_reason_, @@ -111,8 +122,10 @@ bool IntegerSumLE::Propagate() { // Restore integer_reason_. Note that this is not needed if we returned // false above. - integer_reason_.push_back(saved); - std::swap(integer_reason_[i], integer_reason_.back()); + if (index >= 0) { + integer_reason_.push_back(saved); + std::swap(integer_reason_[index], integer_reason_.back()); + } } } diff --git a/src/sat/integer_expr.h b/src/sat/integer_expr.h index 72fa98f52f..690dd3fe38 100644 --- a/src/sat/integer_expr.h +++ b/src/sat/integer_expr.h @@ -70,6 +70,7 @@ class IntegerSumLE : public PropagatorInterface { std::vector literal_reason_; std::vector integer_reason_; + std::vector index_in_integer_reason_; DISALLOW_COPY_AND_ASSIGN(IntegerSumLE); }; diff --git a/src/sat/overload_checker.cc b/src/sat/overload_checker.cc index 37c090a6f2..8aca405dc8 100644 --- a/src/sat/overload_checker.cc +++ b/src/sat/overload_checker.cc @@ -38,9 +38,13 @@ OverloadChecker::OverloadChecker( end_vars_[t] = intervals_repository->EndVar(i); duration_vars_[t] = intervals_repository->SizeVar(i); } - // Allocate space for the sorted tasks. + // Initialize the data for the sorted tasks. by_start_min_.reserve(num_tasks_); by_end_max_.reserve(num_tasks_); + for (int t = 0; t < num_tasks_; ++t) { + by_start_min_.push_back(TaskTime(t, IntegerValue(0))); + by_end_max_.push_back(TaskTime(t, IntegerValue(0))); + } task_to_index_in_start_min_.resize(num_tasks_); } @@ -78,22 +82,33 @@ void OverloadChecker::RegisterWith(GenericLiteralWatcher* watcher) { } } -bool OverloadChecker::Propagate() { - // Sort the tasks by start min and end max. - by_start_min_.clear(); - by_end_max_.clear(); - for (int t = 0; t < num_tasks_; t++) { - // Tasks with no energy have no impact in the algorithm and are not - // considered in the remainder of this function. - if (DurationMin(t) > 0 && DemandMin(t) > 0) { - by_start_min_.push_back(TaskTime(t, StartMin(t))); - by_end_max_.push_back(TaskTime(t, EndMax(t))); - } - } - std::sort(by_start_min_.begin(), by_start_min_.end()); - std::sort(by_end_max_.begin(), by_end_max_.end()); +namespace { +IntegerValue CeilOfDivision(IntegerValue a, IntegerValue b) { + return (a + b - 1) / b; +} +} // namespace - // Link each unskipped task to its position in by_start_min_. +bool OverloadChecker::Propagate() { + // Sort the tasks by start-min and end-max. Note that we reuse the current + // order because it is often already sorted. + for (const bool start_min_or_end_max : {true, false}) { + bool already_sorted = true; + IntegerValue prev = kMinIntegerValue; + std::vector& to_sort = + start_min_or_end_max ? by_start_min_ : by_end_max_; + for (TaskTime& ref : to_sort) { + const IntegerValue value = + start_min_or_end_max ? StartMin(ref.task_id) : EndMax(ref.task_id); + ref.time = value; + if (already_sorted) { + if (value < prev) already_sorted = false; + prev = value; + } + } + if (!already_sorted) std::sort(to_sort.begin(), to_sort.end()); + } + + // Link each task to its position in by_start_min_. for (int i = 0; i < by_start_min_.size(); ++i) { task_to_index_in_start_min_[by_start_min_[i].task_id] = i; } @@ -107,25 +122,28 @@ bool OverloadChecker::Propagate() { // Build the left cuts and check for a possible overload. for (int i = 0; i < by_end_max_.size(); ++i) { const int task_id = by_end_max_[i].task_id; - const int leaf_id = task_to_index_in_start_min_[task_id]; - // Compute the energy and envelope of the task. - const IntegerValue energy = DurationMin(task_id) * DemandMin(task_id); - const IntegerValue envelope = StartMin(task_id) * capacity_max + energy; - - DCHECK_GT(energy, kMinIntegerValue); - DCHECK_GT(envelope, kMinIntegerValue); + // Tasks with no energy have no impact in the algorithm. Skip them. + if (DurationMin(task_id) == 0 || DemandMin(task_id) == 0) continue; // Insert the task in the Theta-tree. This will compute the envelope of the // left-cut ending with task task_id where the left-cut of task_id is the // set of all tasks having a maximum ending time that is lower or equal than // the maximum ending time of task_id. - InsertTaskInThetaTree(task_id, leaf_id, energy, envelope); + { + // Compute the energy and envelope of the task. + // TODO(user): This code will not work for negative start_min. + // TODO(user): Deal with integer overflow. + const int leaf_id = task_to_index_in_start_min_[task_id]; + const IntegerValue energy = DurationMin(task_id) * DemandMin(task_id); + const IntegerValue envelope = StartMin(task_id) * capacity_max + energy; + InsertTaskInThetaTree(task_id, leaf_id, energy, envelope); + } // Compute the minimum capacity required to provide the left-cut with enough // energy. The minimum capacity is ceil(envelopes_[i] / EndMax(task_id)). - IntegerValue new_capacity_min = node_envelopes_[1] / EndMax(task_id); - if (node_envelopes_[1] % EndMax(task_id) != 0) new_capacity_min++; + const IntegerValue new_capacity_min = + CeilOfDivision(node_envelopes_[1], by_end_max_[i].time); // Do not explain if the minimum capacity does not increase. if (new_capacity_min <= integer_trail_->LowerBound(capacity_var_)) continue; @@ -135,14 +153,15 @@ bool OverloadChecker::Propagate() { // Compute the bounds of the task interval responsible for the value of the // root envelope. const IntegerValue interval_end = by_end_max_[i].time; - const int interval_start_index = LeftMostInvolvedLeaf(); - const IntegerValue interval_start = - by_start_min_[interval_start_index].time; - + const int interval_start_leaf = LeftMostInvolvedLeaf(); + const IntegerValue interval_start = by_start_min_[interval_start_leaf].time; for (int j = 0; j <= i; ++j) { const int t = by_end_max_[j].task_id; + // Do not consider tasks that are not contained in the task interval. - if (task_to_index_in_start_min_[t] < interval_start_index) continue; + if (task_to_index_in_start_min_[t] < interval_start_leaf) continue; + if (DurationMin(t) == 0 || DemandMin(t) == 0) continue; + // Add the task to the explanation. reason_.push_back( IntegerLiteral::GreaterOrEqual(start_vars_[t], interval_start)); @@ -171,6 +190,8 @@ bool OverloadChecker::Propagate() { void OverloadChecker::InsertTaskInThetaTree(int task_id, int leaf_id, IntegerValue energy, IntegerValue envelope) { + DCHECK_GT(energy, kMinIntegerValue); + DCHECK_GT(envelope, kMinIntegerValue); const int leaf_node = first_leaf_ + leaf_id; DCHECK_LT(leaf_node, node_energies_.size()); node_energies_[leaf_node] = energy; @@ -180,7 +201,7 @@ void OverloadChecker::InsertTaskInThetaTree(int task_id, int leaf_id, DCHECK_LT(parent, first_leaf_); const int left = parent * 2; const int right = left + 1; - node_energies_[parent] = node_energies_[left] + node_energies_[right]; + node_energies_[parent] += energy; node_envelopes_[parent] = std::max( node_envelopes_[left] + node_energies_[right], node_envelopes_[right]); parent = parent / 2; diff --git a/src/sat/overload_checker.h b/src/sat/overload_checker.h index 513a5a855d..dcc74fc119 100644 --- a/src/sat/overload_checker.h +++ b/src/sat/overload_checker.h @@ -64,10 +64,9 @@ class OverloadChecker : public PropagatorInterface { private: struct TaskTime { /* const */ int task_id; - /* const */ IntegerValue time; + IntegerValue time; TaskTime(int task_id, IntegerValue time) : task_id(task_id), time(time) {} bool operator<(TaskTime other) const { return time < other.time; } - bool operator>(TaskTime other) const { return time > other.time; } }; // Inserts the task task_id to the leaf leaf_id with the given energy and