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

speedup linear inequations in sat

Browse Source
This commit is contained in:
Laurent Perron
2016-11-10 18:05:44 +01:00
parent 56f5307c63
commit eea1ae01b0
5 changed files with 81 additions and 42 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/sat/integer.h
View File

@@ -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<Literal>* output) const;

29
src/sat/integer_expr.cc
View File

@@ -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());
}
}
}

1
src/sat/integer_expr.h
View File

@@ -70,6 +70,7 @@ class IntegerSumLE : public PropagatorInterface {
std::vector<Literal> literal_reason_;
std::vector<IntegerLiteral> integer_reason_;
std::vector<int> index_in_integer_reason_;
DISALLOW_COPY_AND_ASSIGN(IntegerSumLE);
};

85
src/sat/overload_checker.cc
View File

@@ -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<TaskTime>& 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;

3
src/sat/overload_checker.h
View File

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