diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 001ad9b81c..e9d20cd03f 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -191,28 +191,6 @@ std::function 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 decisions_set(decisions.begin(), - decisions.end()); - const IntegerVariable num_variables = - model->GetOrCreate()->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); } diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 8982c8d169..ce4c881b62 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -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 coeffs, std::vector* 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 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 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; } } diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 417e049dcf..012e94614e 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -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 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() {} diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 3ddea120c1..a33907cf8b 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -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()); + } + } if (decision == kNoLiteralIndex) break; if (sat_solver->Assignment().LiteralIsAssigned(Literal(decision))) { diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 4adc1f5e1d..d4d3563c01 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -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, ")")