diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 92e12d242e..eac2f70128 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -100,7 +100,7 @@ void IntegerEncoder::FullyEncodeVariable(IntegerVariable var) { AssociateToIntegerEqualValue(literals[i], var, values[i]); } - // Mark var and of Negation(var) as fully encoded. + // Mark var and Negation(var) as fully encoded. const int required_size = std::max(var, NegationOf(var)).value() + 1; if (required_size > is_fully_encoded_.size()) { is_fully_encoded_.resize(required_size, false); @@ -262,7 +262,6 @@ Literal IntegerEncoder::GetOrCreateLiteralAssociatedToEquality( void IntegerEncoder::AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit) { - CHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal)); const auto& domain = (*domains_)[i_lit.var]; const IntegerValue min(domain.front().start); const IntegerValue max(domain.back().end); @@ -334,10 +333,6 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, return; } - // If the literal was already assigned before beeing associated, we may - // not propagate properly the update to the variable domain. - CHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal)); - // Special case for the first and last value. if (value == domain.front().start) { // Note that this will recursively call AssociateToIntegerEqualValue() but @@ -371,8 +366,6 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, // of the optional variables is true. void IntegerEncoder::HalfAssociateGivenLiteral(IntegerLiteral i_lit, Literal literal) { - CHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal)); - // Resize reverse encoding. const int new_size = 1 + literal.Index().value(); if (new_size > reverse_encoding_.size()) reverse_encoding_.resize(new_size); @@ -380,6 +373,10 @@ void IntegerEncoder::HalfAssociateGivenLiteral(IntegerLiteral i_lit, // Associate the new literal to i_lit. if (!LiteralIsAssociated(i_lit)) { AddImplications(i_lit, literal); + if (sat_solver_->Assignment().LiteralIsTrue(literal)) { + CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); + newly_fixed_integer_literals_.push_back(i_lit); + } reverse_encoding_[literal.Index()].push_back(i_lit); } else { const Literal associated(GetAssociatedLiteral(i_lit)); @@ -433,6 +430,22 @@ bool IntegerTrail::Propagate(Trail* trail) { // into one that use one of the domain value. var_to_current_lb_interval_index_.SetLevel(level); + // This is required because when loading a model it is possible that we add + // (literal <-> integer literal) associations for literals that have already + // been propagated here. This often happens when the presolve is off + // and many variables are fixed. + // + // TODO(user): refactor the interaction IntegerTrail <-> IntegerEncoder so + // that we can just push right away such literal. Unfortunately, this is is + // a big chunck of work. + if (level == 0) { + for (const IntegerLiteral i_lit : encoder_->NewlyFixedIntegerLiterals()) { + if (IsCurrentlyIgnored(i_lit.var)) continue; + if (!Enqueue(i_lit, {}, {})) return false; + } + encoder_->ClearNewlyFixedIntegerLiterals(); + } + // Process all the "associated" literals and Enqueue() the corresponding // bounds. while (propagation_trail_index_ < trail->Index()) { @@ -545,11 +558,14 @@ std::vector IntegerTrail::InitialVariableDomain( bool IntegerTrail::UpdateInitialDomain(IntegerVariable var, std::vector domain) { + CHECK_EQ(trail_->CurrentDecisionLevel(), 0); + // TODO(user): A bit inefficient as this recreate a vector for no reason. const std::vector old_domain = InitialVariableDomain(var); - if (old_domain == domain) return true; - domain = IntersectionOfSortedDisjointIntervals(domain, old_domain); + domain = IntersectionOfSortedDisjointIntervals( + domain, {{LowerBound(var).value(), UpperBound(var).value()}}); + if (old_domain == domain) return true; if (domain.empty()) return false; // TODO(user): we currently keep the domain in domains_ but also in diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 2cbd18eb1b..2c98cbf168 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -310,6 +310,15 @@ class IntegerEncoder { return reverse_encoding_[lit.Index()]; } + // This is part of a "hack" to deal with new association involving a fixed + // literal. Note that these are only allowed at the decision level zero. + const std::vector NewlyFixedIntegerLiterals() const { + return newly_fixed_integer_literals_; + } + void ClearNewlyFixedIntegerLiterals() { + newly_fixed_integer_literals_.clear(); + } + // If it exists, returns a [0,1] integer variable which is equal to 1 iff the // given literal is true. Returns kNoIntegerVariable if such variable does not // exist. Note that one can create one by creating a new IntegerVariable and @@ -377,6 +386,7 @@ class IntegerEncoder { // Store for a given LiteralIndex the list of its associated IntegerLiterals. const InlinedIntegerLiteralVector empty_integer_literal_vector_; ITIVector reverse_encoding_; + std::vector newly_fixed_integer_literals_; // Store for a given LiteralIndex its IntegerVariable view or kNoLiteralIndex // if there is none. @@ -735,7 +745,7 @@ class IntegerTrail : public SatPropagator { // TrailEntry in integer_trail_. std::vector boolean_trail_index_to_integer_one_; - int64 num_enqueues_; + int64 num_enqueues_ = 0; std::vector*> watchers_; std::vector reversible_classes_; diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 6f31c8f256..41cb6b1b62 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -106,7 +106,7 @@ std::function FollowHint( } else { const IntegerVariable integer_var = vars[i].int_var; const IntegerValue lb = integer_trail->LowerBound(integer_var); - const IntegerValue ub = integer_trail->LowerBound(integer_var); + const IntegerValue ub = integer_trail->UpperBound(integer_var); if (lb == ub) continue; // We try first (<= value), but if this do not reduce the domain we @@ -222,6 +222,7 @@ std::function ExploitIntegerLpSolution( if (value > lb && value <= ub) { const Literal ge = encoder->GetOrCreateAssociatedLiteral( IntegerLiteral::GreaterOrEqual(positive_var, value)); + auto domain = (*model->GetOrCreate())[positive_var]; CHECK(!trail->Assignment().VariableIsAssigned(ge.Variable())); last_decision_followed_lp = true; return ge.Index();