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

sync ortools/sat with main

Browse Source
This commit is contained in:
Laurent Perron
2024-04-08 11:52:13 +02:00
committed by Corentin Le Molgat
parent af1f701ca9
commit 870edf6f7b
1 changed files with 232 additions and 223 deletions
Download Patch File Download Diff File Expand all files Collapse all files

455
ortools/sat/linear_propagation.cc
View File

@@ -470,28 +470,29 @@ void LinearPropagator::OnVariableChange(IntegerVariable var, IntegerValue lb,
}
bool LinearPropagator::Propagate() {
id_scanned_at_least_once_.ClearAndResize(in_queue_.size());
// Initial addition.
// We will clear modified_vars_ on exit.
//
// We will clear modified_vars_ on exit since everything we propagate here
// is handled by PropagateOneConstraint().
for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= var_to_constraint_ids_.size()) continue;
SetPropagatedBy(var, -1);
AddWatchedToQueue(var, /*push_delayed_right_away=*/false);
OnVariableChange(var, integer_trail_->LowerBound(var), -1);
}
for (const int id : tmp_delayed_) {
AddToQueueIfNeeded(id);
}
tmp_delayed_.clear();
// Cleanup.
num_terms_for_dtime_update_ = 0;
const auto cleanup = ::absl::MakeCleanup([this]() {
time_limit_->AdvanceDeterministicTime(
static_cast<double>(num_terms_for_dtime_update_) * 1e-9);
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
});
// We abort this propagator as soon as a Boolean is propagated, so that we
// always finish the Boolean propagation first. This can happen when we push a
// bound that has associated Booleans or push enforcement to false. The idea
// is to resume from our current state when we are called again. Note however
// that we have to clear the propagated_by_ info (as done above) has other
// propagator might have pushed the same variable further.
//
// Empty FIFO queue.
// that we have to clear the propagated_by_ info has other propagator might
// have pushed the same variable further.
//
// TODO(user): More than the propagation speed, I think it is important to
// have proper explanation, so if A pushes B, but later on the queue we have C
@@ -512,28 +513,63 @@ bool LinearPropagator::Propagate() {
// - 2 * Y + Z + T <= 11 ==> Y <= 5, Z <= 11, T <= 11 (1)
// - Z + Y >= 6 ==> Z >= 1
// - (1) again to push T <= 10 and reach the propagation fixed point.
bool result = true;
num_terms_for_dtime_update_ = 0;
const int saved_index = trail_->Index();
while (!propagation_queue_.empty()) {
const int id = propagation_queue_.Pop();
in_queue_[id] = false;
if (!PropagateOneConstraint(id)) {
result = false;
break;
Bitset64<int>::View in_queue = in_queue_.view();
while (true) {
// We always process the whole queue in FIFO order.
// Note that the order really only matter for infeasible constraint so it
// shouldn't have a big impact.
const int saved_index = trail_->Index();
while (!propagation_queue_.empty()) {
const int id = propagation_queue_.front();
propagation_queue_.pop_front();
in_queue.Clear(id);
const auto [slack, num_to_push] = AnalyzeConstraint(id);
if (slack < 0) {
// This is either a conflict or an enforcement propagation.
// We do it right away.
if (!PropagateInfeasibleConstraint(id, slack)) return false;
// We abort after the first pushed boolean. We could abort later too,
// it is unclear what works best.
//
// TODO(user): Maybe we should "update" explanation if we have a shorter
// one to be less reliant on the propagation order.
if (trail_->Index() > saved_index) {
++num_bool_aborts_;
return true;
}
} else if (num_to_push > 0) {
// Note that the last constraint added in to_propagate_ should never
// be "skipped" and have any variable marked as var_will_change_.
const auto vars = GetVariables(infos_[id]);
const auto coeffs = GetCoeffs(infos_[id]);
for (int i = 0; i < num_to_push; ++i) {
const IntegerVariable var = vars[i];
const IntegerValue coeff = coeffs[i];
const IntegerValue div = slack / coeff;
const IntegerValue new_ub = integer_trail_->LowerBound(var) + div;
order_.Register(id, NegationOf(var), -new_ub);
}
}
}
const int next_id = order_.NextId();
if (next_id == -1) break;
// We can probably save the AnalyzeConstraint() cost, but then we only do
// that when the constraint propagate, and the context might have change
// since we computed it above.
if (!PropagateOneConstraint(next_id)) return false;
// TODO(user): This do not seems always good, especially since we pushed
// Boolean with a really small explanation, maybe we want to push more of
// these rather than go back to pure-binary propagation.
if (trail_->Index() > saved_index) {
++num_bool_aborts_;
break;
return true;
}
}
// Clean-up modified_vars_ to do as little as possible on the next call.
time_limit_->AdvanceDeterministicTime(
static_cast<double>(num_terms_for_dtime_update_) * 1e-9);
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
return result;
return true;
}
// Adds a new constraint to the propagator.
@@ -570,7 +606,6 @@ bool LinearPropagator::AddConstraint(
}
id_to_propagation_count_.push_back(0);
id_propagated_something_.push_back(false);
variables_buffer_.insert(variables_buffer_.end(), vars.begin(), vars.end());
coeffs_buffer_.insert(coeffs_buffer_.end(), coeffs.begin(), coeffs.end());
CanonicalizeConstraint(id);
@@ -590,8 +625,7 @@ bool LinearPropagator::AddConstraint(
// Initialize watchers.
// Initialy we want everything to be propagated at least once.
in_queue_.push_back(false);
propagation_queue_.IncreaseSize(in_queue_.size());
in_queue_.resize(in_queue_.size() + 1);
if (!enforcement_literals.empty()) {
infos_.back().enf_status =
@@ -634,6 +668,7 @@ bool LinearPropagator::AddConstraint(
infos_.back().enf_status = static_cast<int>(EnforcementStatus::IS_ENFORCED);
}
order_.Resize(var_to_constraint_ids_.size(), in_queue_.size());
for (const IntegerVariable var : GetVariables(infos_[id])) {
// Transposed graph to know which constraint to wake up.
if (var >= var_to_constraint_ids_.size()) {
@@ -643,6 +678,8 @@ bool LinearPropagator::AddConstraint(
propagated_by_.resize(size, -1);
propagated_by_was_set_.Resize(IntegerVariable(size));
is_watched_.resize(size, false);
order_.Resize(size, in_queue_.size());
}
// TODO(user): Shall we decide on some ordering here? maybe big coeff first
@@ -661,10 +698,12 @@ bool LinearPropagator::AddConstraint(
// Propagate this new constraint.
// TODO(user): Do we want to do that?
num_terms_for_dtime_update_ = 0;
const bool result = PropagateOneConstraint(id);
time_limit_->AdvanceDeterministicTime(
static_cast<double>(num_terms_for_dtime_update_) * 1e-9);
return result;
const auto cleanup = ::absl::MakeCleanup([this]() {
time_limit_->AdvanceDeterministicTime(
static_cast<double>(num_terms_for_dtime_update_) * 1e-9);
});
if (!PropagateOneConstraint(id)) return false;
return true;
}
absl::Span<IntegerValue> LinearPropagator::GetCoeffs(
@@ -690,27 +729,26 @@ void LinearPropagator::CanonicalizeConstraint(int id) {
vars[i] = NegationOf(vars[i]);
}
}
// Note that we DO NOT support having both var and NegationOf(var) in a
// constraint, that would break the algo.
if (DEBUG_MODE) {
absl::flat_hash_set<IntegerVariable> no_dup;
for (const IntegerVariable var : GetVariables(info)) {
auto [_, inserted] = no_dup.insert(PositiveVariable(var));
CHECK(inserted);
}
}
}
// TODO(user): template everything for the case info.all_coeffs_are_one ?
bool LinearPropagator::PropagateOneConstraint(int id) {
// This is here for development purpose, it is a bit too slow to check by
// default though, even VLOG_IS_ON(1) so we disable it.
if (/* DISABLES CODE */ (false)) {
++num_scanned_;
if (id < id_scanned_at_least_once_.size()) {
if (id_scanned_at_least_once_[id]) {
++num_extra_scans_;
} else {
id_scanned_at_least_once_.Set(id);
}
}
}
std::pair<IntegerValue, int> LinearPropagator::AnalyzeConstraint(int id) {
++num_scanned_;
// Skip constraint not enforced or that cannot propagate if false.
ConstraintInfo& info = infos_[id];
const EnforcementStatus enf_status = EnforcementStatus(info.enf_status);
if (DEBUG_MODE) {
if (DEBUG_MODE && enforcement_propagator_->PropagationIsDone(*trail_)) {
const EnforcementStatus debug_status =
enforcement_propagator_->DebugStatus(info.enf_id);
if (enf_status != debug_status) {
@@ -732,11 +770,11 @@ bool LinearPropagator::PropagateOneConstraint(int id) {
if (enf_status == EnforcementStatus::IS_FALSE) {
// We mark this constraint as in the queue but will never inspect it
// again until we backtrack over this time.
in_queue_[id] = true;
in_queue_.Set(id);
unenforced_constraints_.push_back(id);
}
++num_ignored_;
return true;
return {0, 0};
}
// Compute the slack and max_variations_ of each variables.
@@ -747,13 +785,14 @@ bool LinearPropagator::PropagateOneConstraint(int id) {
bool first_change = true;
num_terms_for_dtime_update_ += info.rev_size;
IntegerValue* max_variations = max_variations_.data();
const IntegerValue* lower_bounds = integer_trail_->LowerBoundsData();
if (info.all_coeffs_are_one) {
// TODO(user): Avoid duplication?
for (int i = 0; i < info.rev_size;) {
const IntegerVariable var = vars[i];
const IntegerValue lb = integer_trail_->LowerBound(var);
const IntegerValue ub = integer_trail_->UpperBound(var);
if (lb == ub) {
const IntegerValue lb = lower_bounds[var.value()];
const IntegerValue diff = -lower_bounds[NegationOf(var).value()] - lb;
if (diff == 0) {
if (first_change) {
// Note that we can save at most one state per fixed var. Also at
// level zero we don't save anything.
@@ -766,8 +805,8 @@ bool LinearPropagator::PropagateOneConstraint(int id) {
info.rev_rhs -= lb;
} else {
implied_lb += lb;
max_variations[i] = (ub - lb);
max_variation = std::max(max_variation, max_variations[i]);
max_variations[i] = diff;
max_variation = std::max(max_variation, diff);
++i;
}
}
@@ -776,9 +815,9 @@ bool LinearPropagator::PropagateOneConstraint(int id) {
for (int i = 0; i < info.rev_size;) {
const IntegerVariable var = vars[i];
const IntegerValue coeff = coeffs[i];
const IntegerValue lb = integer_trail_->LowerBound(var);
const IntegerValue ub = integer_trail_->UpperBound(var);
if (lb == ub) {
const IntegerValue lb = lower_bounds[var.value()];
const IntegerValue diff = -lower_bounds[NegationOf(var).value()] - lb;
if (diff == 0) {
if (first_change) {
// Note that we can save at most one state per fixed var. Also at
// level zero we don't save anything.
@@ -792,49 +831,93 @@ bool LinearPropagator::PropagateOneConstraint(int id) {
info.rev_rhs -= coeff * lb;
} else {
implied_lb += coeff * lb;
max_variations[i] = (ub - lb) * coeff;
max_variations[i] = diff * coeff;
max_variation = std::max(max_variation, max_variations[i]);
++i;
}
}
}
// What we call slack here is the "room" between the implied_lb and the rhs.
// Note that we use slack in other context in this file too.
const IntegerValue slack = info.rev_rhs - implied_lb;
// Negative slack means the constraint is false.
if (max_variation <= slack) return true;
id_propagated_something_[id] = true;
if (slack < 0) {
// Fill integer reason.
integer_reason_.clear();
reason_coeffs_.clear();
// Note that if max_variation > slack, we are sure to propagate something
// except if the constraint is enforced and the slack is non-negative.
if (slack < 0 || max_variation <= slack) return {slack, 0};
if (enf_status == EnforcementStatus::IS_ENFORCED) {
// Swap the variable(s) that will be pushed at the beginning.
int num_to_push = 0;
const auto coeffs = GetCoeffs(info);
for (int i = 0; i < info.initial_size; ++i) {
const IntegerVariable var = vars[i];
if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
reason_coeffs_.push_back(coeffs[i]);
}
for (int i = 0; i < info.rev_size; ++i) {
if (max_variations[i] <= slack) continue;
std::swap(vars[i], vars[num_to_push]);
std::swap(coeffs[i], coeffs[num_to_push]);
++num_to_push;
}
return {slack, num_to_push};
}
return {slack, 0};
}
// Relax it.
integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs_,
&integer_reason_);
++num_enforcement_pushes_;
return enforcement_propagator_->PropagateWhenFalse(info.enf_id, {},
integer_reason_);
bool LinearPropagator::PropagateInfeasibleConstraint(int id,
IntegerValue slack) {
DCHECK_LT(slack, 0);
const ConstraintInfo& info = infos_[id];
const auto vars = GetVariables(info);
const auto coeffs = GetCoeffs(info);
// Fill integer reason.
integer_reason_.clear();
reason_coeffs_.clear();
for (int i = 0; i < info.initial_size; ++i) {
const IntegerVariable var = vars[i];
if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
reason_coeffs_.push_back(coeffs[i]);
}
}
// Relax it.
integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs_,
&integer_reason_);
++num_enforcement_pushes_;
return enforcement_propagator_->PropagateWhenFalse(info.enf_id, {},
integer_reason_);
}
bool LinearPropagator::PropagateOneConstraint(int id) {
const auto [slack, num_to_push] = AnalyzeConstraint(id);
if (slack < 0) return PropagateInfeasibleConstraint(id, slack);
if (num_to_push == 0) return true;
DCHECK_GT(num_to_push, 0);
DCHECK_GE(slack, 0);
const ConstraintInfo& info = infos_[id];
const auto vars = GetVariables(info);
const auto coeffs = GetCoeffs(info);
// We can only propagate more if all the enforcement literals are true.
if (info.enf_status != static_cast<int>(EnforcementStatus::IS_ENFORCED)) {
return true;
// But this should have been checked by SkipConstraint().
CHECK_EQ(info.enf_status, static_cast<int>(EnforcementStatus::IS_ENFORCED));
// We can look for disasemble before the actual push.
// This should lead to slighly better reason.
// Explore the subtree and detect cycles greedily.
// Also postpone some propagation.
if (!DisassembleSubtree(id, num_to_push)) {
return false;
}
// The lower bound of all the variables except one can be used to update the
// upper bound of the last one.
int num_pushed = 0;
const auto coeffs = GetCoeffs(info);
for (int i = 0; i < info.rev_size; ++i) {
if (max_variations[i] <= slack) continue;
for (int i = 0; i < num_to_push; ++i) {
if (!order_.VarShouldBePushedById(NegationOf(vars[i]), id)) {
++num_delayed_;
continue;
}
// TODO(user): If the new ub fall into an hole of the variable, we can
// actually relax the reason more by computing a better slack.
@@ -885,24 +968,17 @@ bool LinearPropagator::PropagateOneConstraint(int id) {
const IntegerVariable next_var = NegationOf(var);
if (actual_ub < new_ub) {
// Was pushed further due to hole. We clear it.
SetPropagatedBy(next_var, -1);
AddWatchedToQueue(next_var);
OnVariableChange(next_var, -actual_ub, -1);
} else if (actual_ub == new_ub) {
SetPropagatedBy(next_var, id);
AddWatchedToQueue(next_var);
OnVariableChange(next_var, -actual_ub, id);
// We reorder them first.
std::swap(vars[i], vars[num_pushed]);
std::swap(coeffs[i], coeffs[num_pushed]);
++num_pushed;
}
// Explore the subtree and detect cycles greedily.
// Also postpone some propagation.
if (num_pushed > 0) {
if (!DisassembleSubtree(id, num_pushed)) {
return false;
}
} else {
// The bound was not pushed because we think we are in a propagation loop.
++num_loop_aborts_;
}
}
@@ -943,7 +1019,7 @@ bool LinearPropagator::ReportConflictingCycle() {
integer_reason_.clear();
absl::int128 rhs_sum = 0;
absl::flat_hash_map<IntegerVariable, absl::int128> map_sum;
for (const auto [id, next_var] : disassemble_branch_) {
for (const auto [id, next_var, increase] : disassemble_branch_) {
const ConstraintInfo& info = infos_[id];
enforcement_propagator_->AddEnforcementReason(info.enf_id,
&literal_reason_);
@@ -1012,7 +1088,7 @@ bool LinearPropagator::ReportConflictingCycle() {
}
}
++num_simple_cycles_;
++num_short_reasons_;
VLOG(2) << "Simplified " << integer_reason_.size() << " slack "
<< implied_lb - rhs_sum;
return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
@@ -1027,7 +1103,7 @@ bool LinearPropagator::ReportConflictingCycle() {
literal_reason_.clear();
integer_reason_.clear();
IntegerVariable previous_var = kNoIntegerVariable;
for (const auto [id, next_var] : disassemble_branch_) {
for (const auto [id, next_var, increase] : disassemble_branch_) {
const ConstraintInfo& info = infos_[id];
enforcement_propagator_->AddEnforcementReason(info.enf_id,
&literal_reason_);
@@ -1049,10 +1125,26 @@ bool LinearPropagator::ReportConflictingCycle() {
<< integer_trail_->UpperBound(next_var)
<< "] : " << ConstraintDebugString(id);
}
++num_complex_cycles_;
++num_long_reasons_;
return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
}
std::pair<IntegerValue, IntegerValue> LinearPropagator::GetCycleCoefficients(
int id, IntegerVariable var, IntegerVariable next_var) {
const ConstraintInfo& info = infos_[id];
const auto coeffs = GetCoeffs(info);
const auto vars = GetVariables(info);
IntegerValue var_coeff(0);
IntegerValue next_coeff(0);
for (int i = 0; i < info.initial_size; ++i) {
if (vars[i] == var) var_coeff = coeffs[i];
if (vars[i] == NegationOf(next_var)) next_coeff = coeffs[i];
}
DCHECK_NE(var_coeff, 0);
DCHECK_NE(next_coeff, 0);
return {var_coeff, next_coeff};
}
// Note that if there is a loop in the propagated_by_ graph, it must be
// from root_id -> root_var, because each time we add an edge, we do
// disassemble.
@@ -1062,10 +1154,7 @@ bool LinearPropagator::ReportConflictingCycle() {
//
// TODO(user): Revisit the algo, no point exploring twice the same var, also
// the queue reordering heuristic might not be the best.
bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) {
disassemble_to_reorder_.ClearAndResize(in_queue_.size());
disassemble_reverse_topo_order_.clear();
bool LinearPropagator::DisassembleSubtree(int root_id, int num_tight) {
// The variable was just pushed, we explore the set of variable that will
// be pushed further due to this push. Basically, if a constraint propagated
// before and its slack will reduce due to the push, then any previously
@@ -1076,8 +1165,8 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) {
{
const ConstraintInfo& info = infos_[root_id];
const auto vars = GetVariables(info);
for (int i = 0; i < num_pushed; ++i) {
disassemble_queue_.push_back({root_id, NegationOf(vars[i])});
for (int i = 0; i < num_tight; ++i) {
disassemble_queue_.push_back({root_id, NegationOf(vars[i]), 1});
}
}
@@ -1085,17 +1174,16 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) {
// for each one. And each time we explore an id, we disassemble the tree.
absl::Span<int> id_to_count = absl::MakeSpan(id_to_propagation_count_);
while (!disassemble_queue_.empty()) {
const auto [prev_id, var] = disassemble_queue_.back();
const auto [prev_id, var, increase] = disassemble_queue_.back();
if (!disassemble_branch_.empty() &&
disassemble_branch_.back().first == prev_id &&
disassemble_branch_.back().second == var) {
disassemble_branch_.back().id == prev_id &&
disassemble_branch_.back().var == var) {
disassemble_branch_.pop_back();
disassemble_reverse_topo_order_.push_back(prev_id);
disassemble_queue_.pop_back();
continue;
}
disassemble_branch_.push_back({prev_id, var});
disassemble_branch_.push_back({prev_id, var, increase});
time_limit_->AdvanceDeterministicTime(
static_cast<double>(var_to_constraint_ids_[var].size()) * 1e-9);
@@ -1107,37 +1195,27 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) {
CHECK(!disassemble_branch_.empty());
// This is a corner case in which there is actually no cycle.
const IntegerVariable root_var = disassemble_branch_[0].second;
CHECK_EQ(disassemble_branch_[0].first, root_id);
const auto [test_id, root_var, var_increase] = disassemble_branch_[0];
CHECK_EQ(test_id, root_id);
CHECK_NE(var, root_var);
if (var == NegationOf(root_var)) continue;
// Tricky: We have a cycle here only if coeff of var >= root_coeff.
// If there is no cycle, we will just finish the branch here.
//
// TODO(user): Can we be more precise? if one coeff is big, the
// variation in slack might be big enough to push a variable twice and
// thus push a lower coeff.
const ConstraintInfo& info = infos_[id];
const auto coeffs = GetCoeffs(info);
const auto vars = GetVariables(info);
IntegerValue root_coeff(0);
IntegerValue var_coeff(0);
for (int i = 0; i < info.initial_size; ++i) {
if (vars[i] == var) var_coeff = coeffs[i];
if (vars[i] == NegationOf(root_var)) root_coeff = coeffs[i];
}
DCHECK_NE(root_coeff, 0);
DCHECK_NE(var_coeff, 0);
if (var_coeff >= root_coeff) {
// Simple case, we have a cycle var -> root_var -> ... -> var where
// all coefficient are non-increasing.
const auto [var_coeff, root_coeff] =
GetCycleCoefficients(id, var, root_var);
if (CapProdI(var_increase, var_coeff) >= root_coeff) {
++num_cycles_;
return ReportConflictingCycle();
} else {
// We don't want to continue the search from root_id.
continue;
}
// We don't want to continue the search from root_id.
// TODO(user): We could still try the simple reason, it might be a
// conflict.
++num_failed_cycles_;
continue;
}
disassemble_to_reorder_.Set(id);
if (id_to_count[id] == 0) continue; // Didn't push or was desassembled.
// The constraint pushed some variable. Identify which ones will be pushed
@@ -1165,55 +1243,28 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) {
id_to_count[id]--;
}
}
for (const auto [next_var, coeff] : disassemble_candidates_) {
if (coeff <= var_coeff) {
// We are guaranteed to push next_var only if var_coeff will move
// the slack enough.
//
// TODO(user): Keep current delta in term of the DFS so we detect
// cycle and depedendences in more cases.
disassemble_queue_.push_back({id, next_var});
for (const auto [next_var, next_var_coeff] : disassemble_candidates_) {
// If var was pushed by increase, next_var is pushed by
// (var_coeff * increase) / next_var_coeff.
//
// Note that it is okay to underevalute the increase in case of
// overflow.
const IntegerValue next_increase =
FloorRatio(CapProdI(var_coeff, increase), next_var_coeff);
if (next_increase > 0) {
disassemble_queue_.push_back({id, next_var, next_increase});
// We know this will push later, so we register hit with a sentinel
// value so that it do not block any earlier propagation. Hopefully,
// adding this "dependency" should help find a better propagation
// order.
order_.Register(id, next_var, kMinIntegerValue);
}
}
}
}
CHECK(!disassemble_to_reorder_[root_id]);
tmp_to_reorder_.clear();
std::reverse(disassemble_reverse_topo_order_.begin(),
disassemble_reverse_topo_order_.end()); // !! not unique
for (const int id : disassemble_reverse_topo_order_) {
if (!disassemble_to_reorder_[id]) continue;
disassemble_to_reorder_.Clear(id);
AddToQueueIfNeeded(id);
if (!propagation_queue_.Contains(id)) continue;
tmp_to_reorder_.push_back(id);
}
// TODO(user): Reordering can be slow since require sort and can touch many
// entries. Investigate alternatives. We could probably optimize this a bit
// more.
if (tmp_to_reorder_.empty()) return true;
const int important_size = static_cast<int>(tmp_to_reorder_.size());
for (const int id : disassemble_to_reorder_.PositionsSetAtLeastOnce()) {
if (!disassemble_to_reorder_[id]) continue;
disassemble_to_reorder_.Clear(id);
if (!propagation_queue_.Contains(id)) continue;
tmp_to_reorder_.push_back(id);
}
disassemble_to_reorder_.NotifyAllClear();
// We try to keep the same order as before for the elements not in the
// topological order.
if (important_size < tmp_to_reorder_.size()) {
propagation_queue_.SortByPos(
absl::MakeSpan(&tmp_to_reorder_[important_size],
tmp_to_reorder_.size() - important_size));
}
num_reordered_ += tmp_to_reorder_.size();
propagation_queue_.Reorder(tmp_to_reorder_);
return true;
}
@@ -1222,50 +1273,8 @@ void LinearPropagator::AddToQueueIfNeeded(int id) {
DCHECK_LT(id, infos_.size());
if (in_queue_[id]) return;
in_queue_[id] = true;
propagation_queue_.Push(id);
}
void LinearPropagator::AddWatchedToQueue(IntegerVariable var,
bool push_delayed_right_away) {
if (var >= static_cast<int>(var_to_constraint_ids_.size())) return;
time_limit_->AdvanceDeterministicTime(
static_cast<double>(var_to_constraint_ids_[var].size()) * 1e-9);
// If a constraint propagated something and is getting tighter, then it
// will likely propagate again, and we want to propagate it first.
for (const int id : var_to_constraint_ids_[var]) {
if (in_queue_[id]) continue;
if (true || id_propagated_something_[id]) {
id_propagated_something_[id] = false; // reset.
AddToQueueIfNeeded(id);
} else {
tmp_delayed_.push_back(id);
}
}
if (push_delayed_right_away) {
for (const int id : tmp_delayed_) {
AddToQueueIfNeeded(id);
}
tmp_delayed_.clear();
}
}
void LinearPropagator::SetPropagatedBy(IntegerVariable var, int id) {
int& ref_id = propagated_by_[var];
if (ref_id == id) return;
propagated_by_was_set_.Set(var);
DCHECK_GE(var, 0);
DCHECK_LT(var, propagated_by_.size());
if (ref_id != -1) {
DCHECK_GE(ref_id, 0);
DCHECK_LT(ref_id, id_to_propagation_count_.size());
id_to_propagation_count_[ref_id]--;
}
ref_id = id;
if (id != -1) id_to_propagation_count_[id]++;
in_queue_.Set(id);
propagation_queue_.push_back(id);
}
void LinearPropagator::ClearPropagatedBy() {