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

better treatment of 'infinite' propagation loops

Browse Source
This commit is contained in:
Laurent Perron
2020-10-07 18:57:18 +02:00
parent a56891cf75
commit fee3fbe3ab
5 changed files with 59 additions and 35 deletions
Download Patch File Download Diff File Expand all files Collapse all files

22
ortools/sat/cp_model_search.cc
View File

@@ -191,28 +191,6 @@ std::function<LiteralIndex()> ConstructSearchStrategy(
decisions.push_back(var);
}
}
// In some corner cases (where there are propagation loops) the objective,
// or any "intermediate" variables we create when loading the model (for
// instance when we decompose large linear constraint) might not have been
// propagated correctly, so is is important to try to fix them.
//
// TODO(user): Try to find another solution, because this causes the solver
// to create a few extra Booleans for no good reason. Mainly because of the
// objective variable that in many cases is not fully propagated when the
// rest of the problem is fixed.
absl::flat_hash_set<IntegerVariable> decisions_set(decisions.begin(),
decisions.end());
const IntegerVariable num_variables =
model->GetOrCreate<IntegerTrail>()->NumIntegerVariables();
for (IntegerVariable positive_var(0); positive_var < num_variables;
positive_var += 2) {
if (!decisions_set.contains(positive_var) ||
!decisions_set.contains(NegationOf(positive_var))) {
decisions.push_back(positive_var);
}
}
default_search_strategy =
FirstUnassignedVarAtItsMinHeuristic(decisions, model);
}

43
ortools/sat/integer.cc
View File

@@ -550,6 +550,10 @@ void IntegerTrail::Untrail(const Trail& trail, int literal_trail_index) {
propagation_trail_index_ =
std::min(propagation_trail_index_, literal_trail_index);
if (level < first_level_without_full_propagation_) {
first_level_without_full_propagation_ = -1;
}
// Note that if a conflict was detected before Propagate() of this class was
// even called, it is possible that there is nothing to backtrack.
if (level >= integer_search_levels_.size()) return;
@@ -814,9 +818,6 @@ void IntegerTrail::AppendRelaxedLinearReason(
}
}
// TODO(user): When this is called during a reason computation, we can use
// the term already part of the reason we are constructed to optimize this
// further.
void IntegerTrail::RelaxLinearReason(IntegerValue slack,
absl::Span<const IntegerValue> coeffs,
std::vector<int>* trail_indices) const {
@@ -843,8 +844,17 @@ void IntegerTrail::RelaxLinearReason(IntegerValue slack,
continue;
}
// Note that both terms of the product are positive.
// This is a bit hacky, but when it is used from MergeReasonIntoInternal(),
// we never relax a reason that will not be expanded because it is already
// part of the current conflict.
const TrailEntry& entry = integer_trail_[index];
if (entry.var != kNoIntegerVariable &&
index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
(*trail_indices)[new_size++] = index;
continue;
}
// Note that both terms of the product are positive.
const TrailEntry& previous_entry = integer_trail_[entry.prev_trail_index];
const int64 diff =
CapProd(coeff.value(), (entry.bound - previous_entry.bound).value());
@@ -880,6 +890,12 @@ void IntegerTrail::RelaxLinearReason(IntegerValue slack,
continue;
}
const TrailEntry& entry = integer_trail_[index];
if (entry.var != kNoIntegerVariable &&
index <= tmp_var_to_trail_index_in_queue_[entry.var]) {
trail_indices->push_back(index);
continue;
}
const TrailEntry& previous_entry = integer_trail_[entry.prev_trail_index];
const int64 diff = CapProd(heap_entry.coeff.value(),
(entry.bound - previous_entry.bound).value());
@@ -1100,7 +1116,9 @@ bool IntegerTrail::InPropagationLoop() const {
parameters_.search_branching() != SatParameters::FIXED_SEARCH);
}
IntegerVariable IntegerTrail::MostPropagatedVarWithLargeDomain() const {
// We try to select a variable with a large domain that was propagated a lot
// already.
IntegerVariable IntegerTrail::NextVariableToBranchOnInPropagationLoop() const {
CHECK(InPropagationLoop());
++num_decisions_to_break_loop_;
std::vector<IntegerVariable> vars;
@@ -1129,6 +1147,18 @@ IntegerVariable IntegerTrail::MostPropagatedVarWithLargeDomain() const {
return best_var;
}
bool IntegerTrail::CurrentBranchHadAnIncompletePropagation() {
return first_level_without_full_propagation_ != -1;
}
IntegerVariable IntegerTrail::FirstUnassignedVariable() const {
for (IntegerVariable var(0); var < vars_.size(); var += 2) {
if (IsCurrentlyIgnored(var)) continue;
if (!IsFixed(var)) return var;
}
return kNoIntegerVariable;
}
bool IntegerTrail::EnqueueInternal(
IntegerLiteral i_lit, LazyReasonFunction lazy_reason,
absl::Span<const Literal> literal_reason,
@@ -1238,6 +1268,9 @@ bool IntegerTrail::EnqueueInternal(
const IntegerValue lb = LowerBound(i_lit.var);
const IntegerValue ub = UpperBound(i_lit.var);
if (i_lit.bound - lb < (ub - lb) / 2) {
if (first_level_without_full_propagation_ == -1) {
first_level_without_full_propagation_ = trail_->CurrentDecisionLevel();
}
return true;
}
}

17
ortools/sat/integer.h
View File

@@ -825,7 +825,13 @@ class IntegerTrail : public SatPropagator {
// Basic heuristic to detect when we are in a propagation loop, and suggest
// a good variable to branch on (taking the middle value) to get out of it.
bool InPropagationLoop() const;
IntegerVariable MostPropagatedVarWithLargeDomain() const;
IntegerVariable NextVariableToBranchOnInPropagationLoop() const;
// If we had an incomplete propagation, it is important to fix all the
// variables and not relly on the propagation to do so. This is related to the
// InPropagationLoop() code above.
bool CurrentBranchHadAnIncompletePropagation();
IntegerVariable FirstUnassignedVariable() const;
private:
// Used for DHECKs to validate the reason given to the public functions above.
@@ -989,6 +995,10 @@ class IntegerTrail : public SatPropagator {
// TrailEntry in integer_trail_.
std::vector<int> boolean_trail_index_to_integer_one_;
// We need to know if we skipped some propagation in the current branch.
// This is reverted as we backtrack over it.
int first_level_without_full_propagation_ = -1;
int64 num_enqueues_ = 0;
int64 num_untrails_ = 0;
int64 num_level_zero_enqueues_ = 0;
@@ -1006,11 +1016,6 @@ class IntegerTrail : public SatPropagator {
};
// Base class for CP like propagators.
//
// TODO(user): Think about an incremental Propagate() interface.
//
// TODO(user): Add shortcuts for the most used functions? like
// Min(IntegerVariable) and Max(IntegerVariable)?
class PropagatorInterface {
public:
PropagatorInterface() {}

10
ortools/sat/integer_search.cc
View File

@@ -729,7 +729,7 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
while (true) {
if (integer_trail->InPropagationLoop()) {
const IntegerVariable var =
integer_trail->MostPropagatedVarWithLargeDomain();
integer_trail->NextVariableToBranchOnInPropagationLoop();
if (var != kNoIntegerVariable) {
decision = GreaterOrEqualToMiddleValue(var, model);
}
@@ -737,6 +737,14 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
if (decision == kNoLiteralIndex) {
decision = heuristics.decision_policies[heuristics.policy_index]();
}
if (decision == kNoLiteralIndex &&
integer_trail->CurrentBranchHadAnIncompletePropagation()) {
const IntegerVariable var = integer_trail->FirstUnassignedVariable();
if (var != kNoIntegerVariable) {
decision = AtMinValue(var, integer_trail,
model->GetOrCreate<IntegerEncoder>());
}
}
if (decision == kNoLiteralIndex) break;
if (sat_solver->Assignment().LiteralIsAssigned(Literal(decision))) {

2
ortools/sat/synchronization.cc
View File

@@ -585,7 +585,7 @@ void SharedBoundsManager::ReportPotentialNewBounds(
}
changed_variables_since_last_synchronize_.Set(var);
if (VLOG_IS_ON(2)) {
if (VLOG_IS_ON(3)) {
const IntegerVariableProto& var_proto = model_proto.variables(var);
const std::string& var_name =
var_proto.name().empty() ? absl::StrCat("anonymous_var(", var, ")")