diff --git a/ortools/linear_solver/solve.cc b/ortools/linear_solver/solve.cc index 3092d0d8bf..811da1a193 100644 --- a/ortools/linear_solver/solve.cc +++ b/ortools/linear_solver/solve.cc @@ -68,7 +68,6 @@ #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/options.h" -#include "ortools/base/timer.h" #include "ortools/linear_solver/linear_solver.h" #include "ortools/linear_solver/linear_solver.pb.h" #include "ortools/lp_data/lp_parser.h" diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 07639d6238..8bfbb193a5 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -712,13 +712,12 @@ void PropagateEncodingFromEquivalenceRelations(const CpModelProto& model_proto, // It is important to do that first, since otherwise mapping a == literal // might creates the underlying >= and <= literals. for (int i = 0; i < 2; ++i) { - for (const auto value_literal : + for (const auto [value1, literal1] : encoder->PartialGreaterThanEncoding(var1)) { - const IntegerValue value1 = value_literal.first; const IntegerValue bound2 = FloorRatio(rhs - value1 * coeff1, coeff2); ++num_associations; encoder->AssociateToIntegerLiteral( - value_literal.second, IntegerLiteral::LowerOrEqual(var2, bound2)); + literal1, IntegerLiteral::LowerOrEqual(var2, bound2)); } std::swap(var1, var2); std::swap(coeff1, coeff2); diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 0b3775daac..ee733b42c0 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -128,23 +128,14 @@ BooleanOrIntegerLiteral CpModelView::MedianValue(int var) const { result.boolean_literal_index = mapping_.Literal(var).NegatedIndex(); } else if (mapping_.IsInteger(var)) { const IntegerVariable variable = mapping_.Integer(var); - CHECK_NE(variable, kNoIntegerVariable); - CHECK(integer_encoder_.VariableIsFullyEncoded(variable)); - std::vector encoding = - integer_encoder_.RawDomainEncoding(variable); - std::sort(encoding.begin(), encoding.end(), - ValueLiteralPair::CompareByValue()); - std::vector unassigned_sorted_literals; - for (const auto& p : encoding) { - if (!boolean_assignment_.LiteralIsAssigned(p.literal)) { - unassigned_sorted_literals.push_back(p.literal); - } - } + const std::vector encoding = + integer_encoder_.FullDomainEncoding(variable); + // 5 values -> returns the second. // 4 values -> returns the second too. // Array is 0 based. - const int target = (unassigned_sorted_literals.size() + 1) / 2 - 1; - result.boolean_literal_index = unassigned_sorted_literals[target].Index(); + const int target = (encoding.size() + 1) / 2 - 1; + result.boolean_literal_index = encoding[target].literal.Index(); } return result; } diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index fbe4b5b7ef..5df9ef8655 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -2748,6 +2748,9 @@ class LnsSolver : public SubSolver { "presolve"); } local_response = local_response_manager->GetResponse(); + // If the solution is found during presolve. solution_info has not been + // set in the local_response. We set it manually. + local_response.set_solution_info(absl::StrCat(lns_info, " [presolve]")); local_response.set_status(presolve_status); } const std::string solution_info = local_response.solution_info(); diff --git a/ortools/sat/feasibility_pump.cc b/ortools/sat/feasibility_pump.cc index 8b60828d64..9e336c36bc 100644 --- a/ortools/sat/feasibility_pump.cc +++ b/ortools/sat/feasibility_pump.cc @@ -600,7 +600,8 @@ bool FeasibilityPump::PropagationRounding() { if (time_limit_->LimitReached()) return false; // Get the bounds of the variable. const IntegerVariable var = integer_variables_[var_index]; - const Domain& domain = (*domains_)[var]; + CHECK(VariableIsPositive(var)); + const Domain& domain = (*domains_)[GetPositiveOnlyIndex(var)]; const IntegerValue lb = integer_trail_->LowerBound(var); const IntegerValue ub = integer_trail_->UpperBound(var); diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc index 7094b1233e..f5d61bc077 100644 --- a/ortools/sat/implied_bounds.cc +++ b/ortools/sat/implied_bounds.cc @@ -53,32 +53,20 @@ ImpliedBounds::~ImpliedBounds() { shared_stats_->AddStats(stats); } -void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { - if (!parameters_.use_implied_bounds()) return; +bool ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { + if (!parameters_.use_implied_bounds()) return true; const IntegerVariable var = integer_literal.var; - // Update our local level-zero bound. - if (var >= level_zero_lower_bounds_.size()) { - level_zero_lower_bounds_.resize(var.value() + 1, kMinIntegerValue); - new_level_zero_bounds_.Resize(var + 1); - } - level_zero_lower_bounds_[var] = std::max( - level_zero_lower_bounds_[var], integer_trail_->LevelZeroLowerBound(var)); - // Ignore any Add() with a bound worse than the level zero one. // TODO(user): Check that this never happen? it shouldn't. - if (integer_literal.bound <= level_zero_lower_bounds_[var]) { - return; - } + const IntegerValue root_lb = integer_trail_->LevelZeroLowerBound(var); + if (integer_literal.bound <= root_lb) return true; // We skip any IntegerLiteral referring to a variable with only two // consecutive possible values. This is because, once shifted this will // already be a variable in [0, 1] so we shouldn't gain much by substituing // it. - if (integer_trail_->LevelZeroLowerBound(var) + 1 >= - integer_trail_->LevelZeroUpperBound(var)) { - return; - } + if (root_lb + 1 >= integer_trail_->LevelZeroUpperBound(var)) return true; // Add or update the current bound. const auto key = std::make_pair(literal.Index(), var); @@ -88,7 +76,7 @@ void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { insert_result.first->second = integer_literal.bound; } else { // No new info. - return; + return true; } } @@ -112,23 +100,20 @@ void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { // crosses integer_literal.bound. const auto it = bounds_.find(std::make_pair(literal.NegatedIndex(), var)); if (it != bounds_.end()) { - if (it->second <= level_zero_lower_bounds_[var]) { + if (it->second <= root_lb) { // The other bounds is worse than the new level-zero bound which can // happen because of lazy update, so here we just remove it. bounds_.erase(it); } else { const IntegerValue deduction = std::min(integer_literal.bound, it->second); - DCHECK_GT(deduction, level_zero_lower_bounds_[var]); - DCHECK_GT(deduction, integer_trail_->LevelZeroLowerBound(var)); + DCHECK_GT(deduction, root_lb); - // TODO(user): support Enqueueing level zero fact at a positive level. - // That is, do not loose the info on backtrack. This should be doable. It - // is also why we return a bool in case of conflict when pushing - // deduction. ++num_deductions_; - level_zero_lower_bounds_[var] = deduction; - new_level_zero_bounds_.Set(var); + if (!integer_trail_->RootLevelEnqueue( + IntegerLiteral::GreaterOrEqual(var, deduction))) { + return false; + } VLOG(2) << "Deduction old: " << IntegerLiteral::GreaterOrEqual( @@ -144,7 +129,7 @@ void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { bounds_.erase(std::make_pair(literal.Index(), var)); // No need to update var_to_bounds_ in this case. - return; + return true; } } } @@ -157,7 +142,12 @@ void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { // constraint using this bound is protected by the variable optional literal. // Alternativelly we could disable optional variable when we are at // linearization level 2. - if (integer_trail_->IsOptional(var)) return; + if (integer_trail_->IsOptional(var)) return true; + + // The information below is currently only used for cuts. + // So no need to store it if we aren't going to use it. + if (parameters_.linearization_level() == 0) return true; + if (parameters_.cut_level() == 0) return true; // If we have a new implied bound and the literal has a view, add it to // var_to_bounds_. Note that we might add more than one entry with the same @@ -183,6 +173,7 @@ void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { {integer_encoder_->GetLiteralView(literal.Negated()), integer_literal.bound, false}); } + return true; } const std::vector& ImpliedBounds::GetImpliedBounds( @@ -195,11 +186,9 @@ const std::vector& ImpliedBounds::GetImpliedBounds( // is tighter. int new_size = 0; std::vector& ref = var_to_bounds_[var]; - const IntegerValue level_zero_lb = std::max( - level_zero_lower_bounds_[var], integer_trail_->LevelZeroLowerBound(var)); - level_zero_lower_bounds_[var] = level_zero_lb; + const IntegerValue root_lb = integer_trail_->LevelZeroLowerBound(var); for (const ImpliedBoundEntry& entry : ref) { - if (entry.lower_bound <= level_zero_lb) continue; + if (entry.lower_bound <= root_lb) continue; ref[new_size++] = entry; } ref.resize(new_size); @@ -217,15 +206,16 @@ void ImpliedBounds::AddLiteralImpliesVarEqValue(Literal literal, literal_to_var_to_value_[literal.Index()][var] = value; } -void ImpliedBounds::ProcessIntegerTrail(Literal first_decision) { - if (!parameters_.use_implied_bounds()) return; +bool ImpliedBounds::ProcessIntegerTrail(Literal first_decision) { + if (!parameters_.use_implied_bounds()) return true; CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 1); tmp_integer_literals_.clear(); integer_trail_->AppendNewBounds(&tmp_integer_literals_); for (const IntegerLiteral lit : tmp_integer_literals_) { - Add(first_decision, lit); + if (!Add(first_decision, lit)) return false; } + return true; } void ImpliedBounds::AddElementEncoding( @@ -249,20 +239,6 @@ const std::vector& ImpliedBounds::GetElementEncodedVariables() return element_encoded_variables_; } -bool ImpliedBounds::EnqueueNewDeductions() { - CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); - for (const IntegerVariable var : - new_level_zero_bounds_.PositionsSetAtLeastOnce()) { - if (!integer_trail_->Enqueue( - IntegerLiteral::GreaterOrEqual(var, level_zero_lower_bounds_[var]), - {}, {})) { - return false; - } - } - new_level_zero_bounds_.SparseClearAll(); - return sat_solver_->FinishPropagation(); -} - std::string EncodingStr(const std::vector& enc) { std::string result; for (const ValueLiteralPair& term : enc) { diff --git a/ortools/sat/implied_bounds.h b/ortools/sat/implied_bounds.h index 4dc2d08baf..6c6ff9e63a 100644 --- a/ortools/sat/implied_bounds.h +++ b/ortools/sat/implied_bounds.h @@ -97,7 +97,7 @@ class ImpliedBounds { // Not that it checks right aways if there is another bound on the same // variable involving literal.Negated(), in which case we can improve the // level zero lower bound of the variable. - void Add(Literal literal, IntegerLiteral integer_literal); + bool Add(Literal literal, IntegerLiteral integer_literal); // Adds literal => var == value. void AddLiteralImpliesVarEqValue(Literal literal, IntegerVariable var, @@ -108,7 +108,7 @@ class ImpliedBounds { // // Preconditions: The decision level must be one (CHECKed). And the decision // must be equal to first decision (we currently do not CHECK that). - void ProcessIntegerTrail(Literal first_decision); + bool ProcessIntegerTrail(Literal first_decision); // Returns all the implied bounds stored for the given variable. // Note that only literal with an IntegerView are considered here. @@ -148,14 +148,6 @@ class ImpliedBounds { // is infeasible. bool EnqueueNewDeductions(); - // When a literal does not have an integer view, we do not add any - // ImpliedBoundEntry. This allows to create missing entries for a literal for - // which a view was just created. - // - // TODO(user): Implement and call when we create new views in the linear - // relaxation. - void NotifyNewIntegerView(Literal literal) {} - private: const SatParameters& parameters_; SatSolver* sat_solver_; @@ -175,16 +167,16 @@ class ImpliedBounds { absl::flat_hash_map, IntegerValue> bounds_; - // Note(user): The plan is to use these during cut generation, so only the + // Note(user): This is currently only used during cut generation, so only the // Literal with an IntegerView that can be used in the LP relaxation need to // be kept here. // - // TODO(user): Use inlined vectors. + // TODO(user): Use inlined vectors. Even better, we actually only process + // all variables at once, so no need to organize it by IntegerVariable even + // if that might be more friendly cache-wise. std::vector empty_implied_bounds_; absl::StrongVector> var_to_bounds_; - - // Track the list of variables with some implied bounds. SparseBitset has_implied_bounds_; // Stores implied values per variable. @@ -200,11 +192,6 @@ class ImpliedBounds { empty_element_encoding_; std::vector element_encoded_variables_; - // TODO(user): Ideally, this should go away if we manage to push level-zero - // fact at a positive level directly. - absl::StrongVector level_zero_lower_bounds_; - SparseBitset new_level_zero_bounds_; - // Stats. int64_t num_deductions_ = 0; int64_t num_enqueued_in_var_to_bounds_ = 0; diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index d522d1b8fd..b7e0b15de3 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -66,8 +66,10 @@ void IntegerEncoder::FullyEncodeVariable(IntegerVariable var) { if (VariableIsFullyEncoded(var)) return; CHECK_EQ(0, sat_solver_->CurrentDecisionLevel()); - CHECK(!(*domains_)[var].IsEmpty()); // UNSAT. We don't deal with that here. - CHECK_LT((*domains_)[var].Size(), 100000) + var = PositiveVariable(var); + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + CHECK(!domains_[index].IsEmpty()); // UNSAT. We don't deal with that here. + CHECK_LT(domains_[index].Size(), 100000) << "Domain too large for full encoding."; // TODO(user): Maybe we can optimize the literal creation order and their @@ -79,7 +81,7 @@ void IntegerEncoder::FullyEncodeVariable(IntegerVariable var) { // garbage. Note that it is okay to call the function on values no longer // reachable, as this will just do nothing. tmp_values_.clear(); - for (const int64_t v : (*domains_)[var].Values()) { + for (const int64_t v : domains_[index].Values()) { tmp_values_.push_back(IntegerValue(v)); } for (const IntegerValue v : tmp_values_) { @@ -98,13 +100,13 @@ bool IntegerEncoder::VariableIsFullyEncoded(IntegerVariable var) const { // Once fully encoded, the status never changes. if (is_fully_encoded_[index]) return true; - if (!VariableIsPositive(var)) var = PositiveVariable(var); + var = PositiveVariable(var); // TODO(user): Cache result as long as equality_by_var_[index] is unchanged? // It might not be needed since if the variable is not fully encoded, then // PartialDomainEncoding() will filter unreachable values, and so the size // check will be false until further value have been encoded. - const int64_t initial_domain_size = (*domains_)[var].Size(); + const int64_t initial_domain_size = domains_[index].Size(); if (equality_by_var_[index].size() < initial_domain_size) return false; // This cleans equality_by_var_[index] as a side effect and in particular, @@ -116,7 +118,7 @@ bool IntegerEncoder::VariableIsFullyEncoded(IntegerVariable var) const { // not properly synced because the propagation is not finished. const auto& ref = equality_by_var_[index]; int i = 0; - for (const int64_t v : (*domains_)[var].Values()) { + for (const int64_t v : domains_[index].Values()) { if (i < ref.size() && v == ref[i].value) { i++; } @@ -135,7 +137,6 @@ std::vector IntegerEncoder::FullDomainEncoding( std::vector IntegerEncoder::PartialDomainEncoding( IntegerVariable var) const { - CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); if (index >= equality_by_var_.size()) return {}; @@ -163,15 +164,6 @@ std::vector IntegerEncoder::PartialDomainEncoding( return result; } -std::vector IntegerEncoder::RawDomainEncoding( - IntegerVariable var) const { - CHECK(VariableIsPositive(var)); - const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); - if (index >= equality_by_var_.size()) return {}; - - return equality_by_var_[index]; -} - // Note that by not inserting the literal in "order" we can in the worst case // use twice as much implication (2 by literals) instead of only one between // consecutive literals. @@ -202,57 +194,77 @@ void IntegerEncoder::AddImplications( void IntegerEncoder::AddAllImplicationsBetweenAssociatedLiterals() { CHECK_EQ(0, sat_solver_->CurrentDecisionLevel()); add_implications_ = true; - for (const absl::btree_map& encoding : - encoding_by_var_) { + + // This is tricky: AddBinaryClause() might trigger propagation that causes the + // encoding to be filtered. So we make a copy... + const int num_vars = encoding_by_var_.size(); + for (PositiveOnlyIndex index(0); index < num_vars; ++index) { LiteralIndex previous = kNoLiteralIndex; - for (const auto value_literal : encoding) { - const Literal lit = value_literal.second; + const IntegerVariable var(2 * index.value()); + for (const auto [unused, literal] : PartialGreaterThanEncoding(var)) { if (previous != kNoLiteralIndex) { - // lit => previous. - sat_solver_->AddBinaryClause(lit.Negated(), Literal(previous)); + // literal => previous. + sat_solver_->AddBinaryClause(literal.Negated(), Literal(previous)); } - previous = lit.Index(); + previous = literal.Index(); } } } std::pair IntegerEncoder::Canonicalize( IntegerLiteral i_lit) const { + const bool positive = VariableIsPositive(i_lit.var); + if (!positive) i_lit = i_lit.Negated(); + const IntegerVariable var(i_lit.var); + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); IntegerValue after(i_lit.bound); IntegerValue before(i_lit.bound - 1); - DCHECK_GE(before, (*domains_)[var].Min()); - DCHECK_LE(after, (*domains_)[var].Max()); + DCHECK_GE(before, domains_[index].Min()); + DCHECK_LE(after, domains_[index].Max()); int64_t previous = std::numeric_limits::min(); - for (const ClosedInterval& interval : (*domains_)[var]) { + for (const ClosedInterval& interval : domains_[index]) { if (before > previous && before < interval.start) before = previous; if (after > previous && after < interval.start) after = interval.start; if (after <= interval.end) break; previous = interval.end; } - return {IntegerLiteral::GreaterOrEqual(var, after), - IntegerLiteral::LowerOrEqual(var, before)}; + if (positive) { + return {IntegerLiteral::GreaterOrEqual(var, after), + IntegerLiteral::LowerOrEqual(var, before)}; + } else { + return {IntegerLiteral::LowerOrEqual(var, before), + IntegerLiteral::GreaterOrEqual(var, after)}; + } } Literal IntegerEncoder::GetOrCreateAssociatedLiteral(IntegerLiteral i_lit) { - if (i_lit.bound <= (*domains_)[i_lit.var].Min()) { - return GetTrueLiteral(); - } - if (i_lit.bound > (*domains_)[i_lit.var].Max()) { - return GetFalseLiteral(); + // Remove trivial literal. + { + const PositiveOnlyIndex index = GetPositiveOnlyIndex(i_lit.var); + if (VariableIsPositive(i_lit.var)) { + if (i_lit.bound <= domains_[index].Min()) return GetTrueLiteral(); + if (i_lit.bound > domains_[index].Max()) return GetFalseLiteral(); + } else { + const IntegerValue bound = -i_lit.bound; + if (bound >= domains_[index].Max()) return GetTrueLiteral(); + if (bound < domains_[index].Min()) return GetFalseLiteral(); + } } - const auto canonicalization = Canonicalize(i_lit); - const IntegerLiteral new_lit = canonicalization.first; - - const LiteralIndex index = GetAssociatedLiteral(new_lit); - if (index != kNoLiteralIndex) return Literal(index); - const LiteralIndex n_index = GetAssociatedLiteral(canonicalization.second); - if (n_index != kNoLiteralIndex) return Literal(n_index).Negated(); + // Canonicalize and see if we have an equivalent literal already. + const auto canonical_lit = Canonicalize(i_lit); + if (VariableIsPositive(i_lit.var)) { + const LiteralIndex index = GetAssociatedLiteral(canonical_lit.first); + if (index != kNoLiteralIndex) return Literal(index); + } else { + const LiteralIndex index = GetAssociatedLiteral(canonical_lit.second); + if (index != kNoLiteralIndex) return Literal(index).Negated(); + } ++num_created_variables_; const Literal literal(sat_solver_->NewBooleanVariable(), true); - AssociateToIntegerLiteral(literal, new_lit); + AssociateToIntegerLiteral(literal, canonical_lit.first); // TODO(user): on some problem this happens. We should probably make sure that // we don't create extra fixed Boolean variable for no reason. @@ -292,9 +304,12 @@ Literal IntegerEncoder::GetOrCreateLiteralAssociatedToEquality( // Check for trivial true/false literal to avoid creating variable for no // reasons. - const Domain& domain = (*domains_)[var]; - if (!domain.Contains(value.value())) return GetFalseLiteral(); - if (value == domain.Min() && value == domain.Max()) { + const Domain& domain = domains_[GetPositiveOnlyIndex(var)]; + if (!domain.Contains(VariableIsPositive(var) ? value.value() + : -value.value())) { + return GetFalseLiteral(); + } + if (domain.IsFixed()) { AssociateToIntegerEqualValue(GetTrueLiteral(), var, value); return GetTrueLiteral(); } @@ -316,27 +331,73 @@ Literal IntegerEncoder::GetOrCreateLiteralAssociatedToEquality( void IntegerEncoder::AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit) { - const auto& domain = (*domains_)[i_lit.var]; + // Always transform to positive variable. + if (!VariableIsPositive(i_lit.var)) { + i_lit = i_lit.Negated(); + literal = literal.Negated(); + } + + const PositiveOnlyIndex index = GetPositiveOnlyIndex(i_lit.var); + const Domain& domain = domains_[index]; const IntegerValue min(domain.Min()); const IntegerValue max(domain.Max()); if (i_lit.bound <= min) { sat_solver_->AddUnitClause(literal); - } else if (i_lit.bound > max) { + return; + } + if (i_lit.bound > max) { sat_solver_->AddUnitClause(literal.Negated()); - } else { - const auto pair = Canonicalize(i_lit); - HalfAssociateGivenLiteral(pair.first, literal); - HalfAssociateGivenLiteral(pair.second, literal.Negated()); + return; + } - // Detect the case >= max or <= min and properly register them. Note that - // both cases will happen at the same time if there is just two possible - // value in the domain. - if (pair.first.bound == max) { - AssociateToIntegerEqualValue(literal, i_lit.var, max); + if (index >= encoding_by_var_.size()) { + encoding_by_var_.resize(index.value() + 1); + } + auto& var_encoding = encoding_by_var_[index]; + + // We just insert the part corresponding to the literal with positive + // variable. + const auto canonical_pair = Canonicalize(i_lit); + const auto [it, inserted] = + var_encoding.insert({canonical_pair.first.bound, literal}); + if (!inserted) { + const Literal associated(it->second); + if (associated != literal) { + DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); + sat_solver_->AddClauseDuringSearch({literal, associated.Negated()}); + sat_solver_->AddClauseDuringSearch({literal.Negated(), associated}); } - if (-pair.second.bound == min) { - AssociateToIntegerEqualValue(literal.Negated(), i_lit.var, min); + return; + } + AddImplications(var_encoding, it, literal); + + // Corner case if adding implication cause this to be fixed. + if (sat_solver_->CurrentDecisionLevel() == 0) { + if (sat_solver_->Assignment().LiteralIsTrue(literal)) { + delayed_to_fix_->integer_literal_to_fix.push_back(canonical_pair.first); } + if (sat_solver_->Assignment().LiteralIsFalse(literal)) { + delayed_to_fix_->integer_literal_to_fix.push_back(canonical_pair.second); + } + } + + // Resize reverse encoding. + const int new_size = + 1 + std::max(literal.Index().value(), literal.NegatedIndex().value()); + if (new_size > reverse_encoding_.size()) { + reverse_encoding_.resize(new_size); + } + reverse_encoding_[literal.Index()].push_back(canonical_pair.first); + reverse_encoding_[literal.NegatedIndex()].push_back(canonical_pair.second); + + // Detect the case >= max or <= min and properly register them. Note that + // both cases will happen at the same time if there is just two possible + // value in the domain. + if (canonical_pair.first.bound == max) { + AssociateToIntegerEqualValue(literal, i_lit.var, max); + } + if (-canonical_pair.second.bound == min) { + AssociateToIntegerEqualValue(literal.Negated(), i_lit.var, min); } } @@ -352,7 +413,8 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, // Detect literal view. Note that the same literal can be associated to more // than one variable, and thus already have a view. We don't change it in // this case. - const Domain& domain = (*domains_)[var]; + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + const Domain& domain = domains_[index]; if (value == 1 && domain.Min() >= 0 && domain.Max() <= 1) { if (literal.Index() >= literal_view_.size()) { literal_view_.resize(literal.Index().value() + 1, kNoIntegerVariable); @@ -378,7 +440,6 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, // If this key is already associated, make the two literals equal. const Literal representative = insert_result.first->second; if (representative != literal) { - DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); sat_solver_->AddClauseDuringSearch({literal, representative.Negated()}); sat_solver_->AddClauseDuringSearch({literal.Negated(), representative}); } @@ -394,7 +455,6 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, // Update equality_by_var. Note that due to the // equality_to_associated_literal_ hash table, there should never be any // duplicate values for a given variable. - const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); if (index >= equality_by_var_.size()) { equality_by_var_.resize(index.value() + 1); is_fully_encoded_.resize(index.value() + 1); @@ -402,7 +462,7 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, equality_by_var_[index].push_back({value, literal}); // Fix literal for constant domain. - if (value == domain.Min() && value == domain.Max()) { + if (domain.IsFixed()) { sat_solver_->AddUnitClause(literal); return; } @@ -440,72 +500,48 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, reverse_equality_encoding_[literal.Index()].push_back({var, value}); } -// TODO(user): The hard constraints we add between associated literals seems to -// work for optional variables, but I am not 100% sure why!! I think it works -// because these literals can only appear in a conflict if the presence literal -// of the optional variables is true. -void IntegerEncoder::HalfAssociateGivenLiteral(IntegerLiteral i_lit, - Literal literal) { - // Resize reverse encoding. - const int new_size = 1 + literal.Index().value(); - if (new_size > reverse_encoding_.size()) { - reverse_encoding_.resize(new_size); - } - - // Associate the new literal to i_lit. - if (i_lit.var >= encoding_by_var_.size()) { - encoding_by_var_.resize(i_lit.var.value() + 1); - } - auto& var_encoding = encoding_by_var_[i_lit.var]; - auto insert_result = var_encoding.insert({i_lit.bound, literal}); - if (insert_result.second) { // New item. - AddImplications(var_encoding, insert_result.first, literal); - if (sat_solver_->Assignment().LiteralIsTrue(literal)) { - if (sat_solver_->CurrentDecisionLevel() == 0) { - newly_fixed_integer_literals_.push_back(i_lit); - } - } - - // TODO(user): do that for the other branch too? - reverse_encoding_[literal.Index()].push_back(i_lit); - } else { - const Literal associated(insert_result.first->second); - if (associated != literal) { - DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); - sat_solver_->AddClauseDuringSearch({literal, associated.Negated()}); - sat_solver_->AddClauseDuringSearch({literal.Negated(), associated}); - } +// TODO(user): Canonicalization might be slow. +LiteralIndex IntegerEncoder::GetAssociatedLiteral(IntegerLiteral i_lit) const { + IntegerValue bound; + const auto canonical_pair = Canonicalize(i_lit); + const LiteralIndex result = + SearchForLiteralAtOrBefore(canonical_pair.first, &bound); + // const LiteralIndex result = SearchForLiteralAtOrBefore(i_lit, &bound); + if (result != kNoLiteralIndex && bound >= i_lit.bound) { + return result; } + return kNoLiteralIndex; } -bool IntegerEncoder::LiteralIsAssociated(IntegerLiteral i) const { - if (i.var >= encoding_by_var_.size()) return false; - const absl::btree_map& encoding = - encoding_by_var_[i.var]; - return encoding.find(i.bound) != encoding.end(); -} - -LiteralIndex IntegerEncoder::GetAssociatedLiteral(IntegerLiteral i) const { - if (i.var >= encoding_by_var_.size()) return kNoLiteralIndex; - const absl::btree_map& encoding = - encoding_by_var_[i.var]; - const auto result = encoding.find(i.bound); - if (result == encoding.end()) return kNoLiteralIndex; - return result->second.Index(); -} - +// Note that we assume the input literal is canonicalized and do not fall into +// a hole. Otherwise, this work but will likely return a literal before and +// not one equivalent to it (which can be after!). LiteralIndex IntegerEncoder::SearchForLiteralAtOrBefore( - IntegerLiteral i, IntegerValue* bound) const { - // We take the element before the upper_bound() which is either the encoding - // of i if it already exists, or the encoding just before it. - if (i.var >= encoding_by_var_.size()) return kNoLiteralIndex; - const absl::btree_map& encoding = - encoding_by_var_[i.var]; - auto after_it = encoding.upper_bound(i.bound); - if (after_it == encoding.begin()) return kNoLiteralIndex; - --after_it; - *bound = after_it->first; - return after_it->second.Index(); + IntegerLiteral i_lit, IntegerValue* bound) const { + const PositiveOnlyIndex index = GetPositiveOnlyIndex(i_lit.var); + if (index >= encoding_by_var_.size()) return kNoLiteralIndex; + const auto& encoding = encoding_by_var_[index]; + if (VariableIsPositive(i_lit.var)) { + // We need the entry at or before. + // We take the element before the upper_bound() which is either the encoding + // of i if it already exists, or the encoding just before it. + auto after_it = encoding.upper_bound(i_lit.bound); + if (after_it == encoding.begin()) return kNoLiteralIndex; + --after_it; + *bound = after_it->first; + return after_it->second.Index(); + } else { + // We ask for who is implied by -var >= -bound, so we look for + // the var >= value with value > bound and take its negation. + auto after_it = encoding.upper_bound(-i_lit.bound); + if (after_it == encoding.end()) return kNoLiteralIndex; + + // Compute tight bound if there are holes, we have X <= candidate. + const Domain& domain = domains_[index]; + if (after_it->first <= domain.Min()) return kNoLiteralIndex; + *bound = -domain.ValueAtOrBefore(after_it->first.value() - 1); + return after_it->second.NegatedIndex(); + } } ABSL_MUST_USE_RESULT bool IntegerEncoder::LiteralOrNegationHasView( @@ -528,6 +564,102 @@ ABSL_MUST_USE_RESULT bool IntegerEncoder::LiteralOrNegationHasView( return false; } +std::vector IntegerEncoder::PartialGreaterThanEncoding( + IntegerVariable var) const { + std::vector result; + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + if (index >= encoding_by_var_.size()) return result; + if (VariableIsPositive(var)) { + for (const auto [value, literal] : encoding_by_var_[index]) { + result.push_back({value, literal}); + } + return result; + } + + // Tricky: we need to account for holes. + const Domain& domain = domains_[index]; + if (domain.IsEmpty()) return result; + int i = 0; + int64_t previous; + const int num_intervals = domain.NumIntervals(); + for (const auto [value, literal] : encoding_by_var_[index]) { + while (value > domain[i].end) { + previous = domain[i].end; + ++i; + if (i == num_intervals) break; + } + if (i == num_intervals) break; + if (value <= domain[i].start) { + if (i == 0) continue; + result.push_back({-previous, literal.Negated()}); + } else { + result.push_back({-value + 1, literal.Negated()}); + } + } + std::reverse(result.begin(), result.end()); + return result; +} + +bool IntegerEncoder::UpdateEncodingOnInitialDomainChange(IntegerVariable var, + Domain domain) { + DCHECK(VariableIsPositive(var)); + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + if (index >= encoding_by_var_.size()) return true; + + // Fix >= literal that can be fixed. + // We filter and canonicalize the encoding. + int i = 0; + int num_fixed = 0; + tmp_encoding_.clear(); + for (const auto [value, literal] : encoding_by_var_[index]) { + while (i < domain.NumIntervals() && value > domain[i].end) ++i; + if (i == domain.NumIntervals()) { + // We are past the end, so always false. + if (trail_->Assignment().LiteralIsTrue(literal)) return false; + if (trail_->Assignment().LiteralIsFalse(literal)) continue; + ++num_fixed; + trail_->EnqueueWithUnitReason(literal.Negated()); + continue; + } + if (i == 0 && value <= domain[0].start) { + // We are at or before the beginning, so always true. + if (trail_->Assignment().LiteralIsTrue(literal)) continue; + if (trail_->Assignment().LiteralIsFalse(literal)) return false; + ++num_fixed; + trail_->EnqueueWithUnitReason(literal); + continue; + } + + // Note that we canonicalize the literal if it fall into a hole. + tmp_encoding_.push_back( + {std::max(value, domain[i].start), literal}); + } + encoding_by_var_[index].clear(); + for (const auto [value, literal] : tmp_encoding_) { + encoding_by_var_[index].insert({value, literal}); + } + + // Same for equality encoding. + // This will be lazily cleaned on the next PartialDomainEncoding() call. + i = 0; + for (const ValueLiteralPair pair : PartialDomainEncoding(var)) { + while (i < domain.NumIntervals() && pair.value > domain[i].end) ++i; + if (i == domain.NumIntervals() || pair.value < domain[i].start) { + if (trail_->Assignment().LiteralIsTrue(pair.literal)) return false; + if (trail_->Assignment().LiteralIsFalse(pair.literal)) continue; + ++num_fixed; + trail_->EnqueueWithUnitReason(pair.literal.Negated()); + } + } + + if (num_fixed > 0) { + VLOG(1) << "Domain intersection fixed " << num_fixed + << " encoding literals"; + } + + return true; +} + IntegerTrail::~IntegerTrail() { if (parameters_.log_search_progress() && num_decisions_to_break_loop_ > 0) { VLOG(1) << "Num decisions to break propagation loop: " @@ -555,26 +687,33 @@ bool IntegerTrail::Propagate(Trail* trail) { // // 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. + // a big chunk of work. if (level == 0) { - for (const IntegerLiteral i_lit : encoder_->NewlyFixedIntegerLiterals()) { + for (const IntegerLiteral i_lit : delayed_to_fix_->integer_literal_to_fix) { if (IsCurrentlyIgnored(i_lit.var)) continue; - if (!Enqueue(i_lit, {}, {})) return false; - } - encoder_->ClearNewlyFixedIntegerLiterals(); - for (const IntegerLiteral i_lit : integer_literal_to_fix_) { - if (IsCurrentlyIgnored(i_lit.var)) continue; - if (!Enqueue(i_lit, {}, {})) return false; + // Note that we do not call Enqueue here but directly the update domain + // function so that we do not abort even if the level zero bounds were + // up to date. + const IntegerValue lb = + std::max(LevelZeroLowerBound(i_lit.var), i_lit.bound); + const IntegerValue ub = LevelZeroUpperBound(i_lit.var); + if (!UpdateInitialDomain(i_lit.var, Domain(lb.value(), ub.value()))) { + sat_solver_->NotifyThatModelIsUnsat(); + return false; + } } - integer_literal_to_fix_.clear(); + delayed_to_fix_->integer_literal_to_fix.clear(); - for (const Literal lit : literal_to_fix_) { - if (trail_->Assignment().LiteralIsFalse(lit)) return false; + for (const Literal lit : delayed_to_fix_->literal_to_fix) { + if (trail_->Assignment().LiteralIsFalse(lit)) { + sat_solver_->NotifyThatModelIsUnsat(); + return false; + } if (trail_->Assignment().LiteralIsTrue(lit)) continue; trail_->EnqueueWithUnitReason(lit); } - literal_to_fix_.clear(); + delayed_to_fix_->literal_to_fix.clear(); } // Process all the "associated" literals and Enqueue() the corresponding @@ -644,12 +783,14 @@ void IntegerTrail::Untrail(const Trail& trail, int literal_trail_index) { } void IntegerTrail::ReserveSpaceForNumVariables(int num_vars) { + // We only store the domain for the positive variable. + domains_->reserve(num_vars); + // Because we always create both a variable and its negation. const int size = 2 * num_vars; vars_.reserve(size); is_ignored_literals_.reserve(size); integer_trail_.reserve(size); - domains_->reserve(size); var_trail_index_cache_.reserve(size); tmp_var_to_trail_index_in_queue_.reserve(size); } @@ -677,7 +818,6 @@ IntegerVariable IntegerTrail::AddIntegerVariable(IntegerValue lower_bound, is_ignored_literals_.push_back(kNoLiteralIndex); vars_.push_back({-upper_bound, static_cast(integer_trail_.size())}); integer_trail_.push_back({-upper_bound, NegationOf(i)}); - domains_->push_back(Domain(-upper_bound.value(), -lower_bound.value())); var_trail_index_cache_.resize(vars_.size(), integer_trail_.size()); tmp_var_to_trail_index_in_queue_.resize(vars_.size(), 0); @@ -697,49 +837,40 @@ IntegerVariable IntegerTrail::AddIntegerVariable(const Domain& domain) { } const Domain& IntegerTrail::InitialVariableDomain(IntegerVariable var) const { - return (*domains_)[var]; + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + if (VariableIsPositive(var)) return (*domains_)[index]; + temp_domain_ = (*domains_)[index].Negation(); + return temp_domain_; } +// Note that we don't support optional variable here. Or at least if you set +// the domain of an optional variable to zero, the problem will be declared +// unsat. bool IntegerTrail::UpdateInitialDomain(IntegerVariable var, Domain domain) { CHECK_EQ(trail_->CurrentDecisionLevel(), 0); + if (!VariableIsPositive(var)) { + var = NegationOf(var); + domain = domain.Negation(); + } - const Domain& old_domain = InitialVariableDomain(var); + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + const Domain& old_domain = (*domains_)[index]; domain = domain.IntersectionWith(old_domain); if (old_domain == domain) return true; if (domain.IsEmpty()) return false; - (*domains_)[var] = domain; - (*domains_)[NegationOf(var)] = domain.Negation(); + (*domains_)[index] = domain; - // TODO(user): That works, but it might be better to simply update the - // bounds here directly. This is because these function might call again - // UpdateInitialDomain(), and we will abort after realizing that the domain - // didn't change this time. - CHECK(Enqueue(IntegerLiteral::GreaterOrEqual(var, IntegerValue(domain.Min())), - {}, {})); - CHECK(Enqueue(IntegerLiteral::LowerOrEqual(var, IntegerValue(domain.Max())), - {}, {})); + // Update directly the level zero bounds. + CHECK_GE(domain.Min(), LowerBound(var)); + CHECK_LE(domain.Max(), UpperBound(var)); + vars_[var].current_bound = domain.Min(); + integer_trail_[var.value()].bound = domain.Min(); + vars_[NegationOf(var)].current_bound = -domain.Max(); + integer_trail_[NegationOf(var).value()].bound = -domain.Max(); - // Set to false excluded literals. - int i = 0; - int num_fixed = 0; - for (const ValueLiteralPair pair : encoder_->PartialDomainEncoding(var)) { - while (i < domain.NumIntervals() && pair.value > domain[i].end) ++i; - if (i == domain.NumIntervals() || pair.value < domain[i].start) { - ++num_fixed; - if (trail_->Assignment().LiteralIsTrue(pair.literal)) return false; - if (!trail_->Assignment().LiteralIsFalse(pair.literal)) { - trail_->EnqueueWithUnitReason(pair.literal.Negated()); - } - } - } - if (num_fixed > 0) { - VLOG(1) << "Domain intersection fixed " << num_fixed - << " equality literal corresponding to values outside the new " - "domain."; - } - - return true; + // Update the encoding. + return encoder_->UpdateEncodingOnInitialDomainChange(var, domain); } IntegerVariable IntegerTrail::GetOrCreateConstantIntegerVariable( @@ -1037,6 +1168,28 @@ std::string IntegerTrail::DebugString() { return result; } +bool IntegerTrail::RootLevelEnqueue(IntegerLiteral i_lit) { + if (i_lit.bound <= LevelZeroLowerBound(i_lit.var)) return true; + if (i_lit.bound > LevelZeroUpperBound(i_lit.var)) { + sat_solver_->NotifyThatModelIsUnsat(); + return false; + } + if (trail_->CurrentDecisionLevel() == 0) { + if (!Enqueue(i_lit, {}, {})) { + sat_solver_->NotifyThatModelIsUnsat(); + return false; + } + return true; + } + + // We update right away the level zero bounds, but delay the actual enqueue + // until we are back at level zero. This allow to properly push any associated + // literal. + integer_trail_[i_lit.var.value()].bound = i_lit.bound; + delayed_to_fix_->integer_literal_to_fix.push_back(i_lit); + return true; +} + bool IntegerTrail::SafeEnqueue( IntegerLiteral i_lit, absl::Span integer_reason) { // Note that ReportConflict() deal correctly with constant literals. @@ -1196,7 +1349,7 @@ void IntegerTrail::EnqueueLiteralInternal( // If we are fixing something at a positive level, remember it. if (!integer_search_levels_.empty() && integer_reason.empty() && literal_reason.empty() && lazy_reason == nullptr) { - literal_to_fix_.push_back(literal); + delayed_to_fix_->literal_to_fix.push_back(literal); } const int trail_index = trail_->Index(); @@ -1294,22 +1447,13 @@ IntegerVariable IntegerTrail::FirstUnassignedVariable() const { } void IntegerTrail::CanonicalizeLiteralIfNeeded(IntegerLiteral* i_lit) { - const auto& domain = (*domains_)[i_lit->var]; + const PositiveOnlyIndex index = GetPositiveOnlyIndex(i_lit->var); + const Domain& domain = (*domains_)[index]; if (domain.NumIntervals() <= 1) return; - - // TODO(user): we could cache a starting index since in most situation we - // ask for tighter and tigher canonicalization. Alternatively, we could - // use binary search. - int index = 0; - const int size = domain.NumIntervals(); - while (index < size && i_lit->bound > domain[index].end) { - ++index; - } - if (index == size) { - // We will be out of bound and deal with that below. - DCHECK_GT(i_lit->bound, UpperBound(i_lit->var)); + if (VariableIsPositive(i_lit->var)) { + i_lit->bound = domain.ValueAtOrAfter(i_lit->bound.value()); } else { - i_lit->bound = std::max(i_lit->bound, IntegerValue(domain[index].start)); + i_lit->bound = -domain.ValueAtOrBefore(-i_lit->bound.value()); } } @@ -1421,12 +1565,6 @@ bool IntegerTrail::EnqueueInternal( bitset->Set(i_lit.var); } - if (!integer_search_levels_.empty() && integer_reason.empty() && - literal_reason.empty() && lazy_reason == nullptr && - trail_index_with_same_reason >= integer_trail_.size()) { - integer_literal_to_fix_.push_back(i_lit); - } - // Enqueue the strongest associated Boolean literal implied by this one. // Because we linked all such literal with implications, all the one before // will be propagated by the SAT solver. @@ -1456,7 +1594,8 @@ bool IntegerTrail::EnqueueInternal( // it first, and then we use it as a reason for i_lit. We do that so that // MergeReasonIntoInternal() will not unecessarily expand further the reason // for i_lit. - if (IntegerLiteral::GreaterOrEqual(i_lit.var, bound) == i_lit) { + if (bound >= i_lit.bound) { + DCHECK_EQ(bound, i_lit.bound); if (!trail_->Assignment().LiteralIsTrue(to_enqueue)) { EnqueueLiteralInternal(to_enqueue, lazy_reason, literal_reason, integer_reason); @@ -1497,6 +1636,14 @@ bool IntegerTrail::EnqueueInternal( } DCHECK_GT(trail_->CurrentDecisionLevel(), 0); + // If we are not at level zero but there is not reason, we have a root level + // deduction. Remember it so that we don't forget on the next restart. + if (!integer_search_levels_.empty() && integer_reason.empty() && + literal_reason.empty() && lazy_reason == nullptr && + trail_index_with_same_reason >= integer_trail_.size()) { + if (!RootLevelEnqueue(i_lit)) return false; + } + int reason_index = literals_reason_starts_.size(); if (lazy_reason != nullptr) { if (integer_trail_.size() >= lazy_reasons_.size()) { diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 4a34c02e6e..4a8f74404a 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -320,8 +320,9 @@ struct AffineExpression { IntegerValue constant = IntegerValue(0); }; -// A model singleton that holds the INITIAL integer variable domains. -struct IntegerDomains : public absl::StrongVector {}; +// A model singleton that holds the root level integer variable domains. +// we just store a single domain for both var and its negation. +struct IntegerDomains : public absl::StrongVector {}; // A model singleton used for debugging. If this is set in the model, then we // can check that various derived constraint do not exclude this solution (if it @@ -374,6 +375,16 @@ struct LiteralValueValue { } }; +// Sometimes we propagate fact with no reason at a positive level, those +// will automatically be fixed on the next restart. +// +// TODO(user): If we change the logic to not restart right away, we probably +// need to remove duplicates bounds for the same variable. +struct DelayedRootLevelDeduction { + std::vector literal_to_fix; + std::vector integer_literal_to_fix; +}; + // Each integer variable x will be associated with a set of literals encoding // (x >= v) for some values of v. This class maintains the relationship between // the integer variables and such literals which can be created by a call to @@ -396,7 +407,9 @@ class IntegerEncoder { public: explicit IntegerEncoder(Model* model) : sat_solver_(model->GetOrCreate()), - domains_(model->GetOrCreate()), + trail_(model->GetOrCreate()), + delayed_to_fix_(model->GetOrCreate()), + domains_(*model->GetOrCreate()), num_created_variables_(0) {} ~IntegerEncoder() { @@ -426,24 +439,17 @@ class IntegerEncoder { // called. bool VariableIsFullyEncoded(IntegerVariable var) const; - // Computes the full encoding of a variable on which FullyEncodeVariable() has - // been called. The returned elements are always sorted by increasing - // IntegerValue and we filter values associated to false literals. + // Returns the list of literal <=> var == value currently associated to the + // given variable. The result is sorted by value. We filter literal at false, + // and if a literal is true, then you will get a singleton. To be sure to get + // the full set of encoded value, then you should call this at level zero. // - // Performance note: This function is not particularly fast, however it should - // only be required during domain creation. + // The FullDomainEncoding() just check VariableIsFullyEncoded() and returns + // the same result. std::vector FullDomainEncoding(IntegerVariable var) const; - - // Same as FullDomainEncoding() but only returns the list of value that are - // currently associated to a literal. In particular this has no guarantee to - // span the full domain of the given variable (but it might). std::vector PartialDomainEncoding( IntegerVariable var) const; - // Raw encoding. May be incomplete and is not sorted. Contains all literals, - // true or false. - std::vector RawDomainEncoding(IntegerVariable var) const; - // Returns the "canonical" (i_lit, negation of i_lit) pair. This mainly // deal with domain with initial hole like [1,2][5,6] so that if one ask // for x <= 3, this get canonicalized in the pair (x <= 2, x >= 5). @@ -478,12 +484,11 @@ class IntegerEncoder { void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value); - // Returns true iff the given integer literal is associated. The second - // version returns the associated literal or kNoLiteralIndex. Note that none - // of these function call Canonicalize() first for speed, so it is possible - // that this returns false even though GetOrCreateAssociatedLiteral() would - // not create a new literal. - bool LiteralIsAssociated(IntegerLiteral i_lit) const; + // Returns kNoLiteralIndex if there is no associated or the associated literal + // otherwise. + // + // Tricky: for domain with hole, like [0,1][5,6], we assume some equivalence + // classes, like >=2, >=3, >=4 are all the same as >= 5. LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const; LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const; @@ -529,15 +534,6 @@ class IntegerEncoder { return temp_associated_vars_; } - // 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 @@ -561,7 +557,7 @@ class IntegerEncoder { // Ex: if 'i' is (x >= 4) and we already created a literal associated to // (x >= 2) but not to (x >= 3), we will return the literal associated with // (x >= 2). - LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i, + LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i_lit, IntegerValue* bound) const; // Gets the literal always set to true, make it if it does not exist. @@ -580,20 +576,14 @@ class IntegerEncoder { // Returns the set of Literal associated to IntegerLiteral of the form var >= // value. We make a copy, because this can be easily invalidated when calling // any function of this class. So it is less efficient but safer. - absl::btree_map PartialGreaterThanEncoding( - IntegerVariable var) const { - if (var >= encoding_by_var_.size()) { - return absl::btree_map(); - } - return encoding_by_var_[var]; - } + std::vector PartialGreaterThanEncoding( + IntegerVariable var) const; + + // Makes sure all element in the >= encoding are non-trivial and canonical. + // The input variable must be positive. + bool UpdateEncodingOnInitialDomainChange(IntegerVariable var, Domain domain); private: - // Only add the equivalence between i_lit and literal, if there is already an - // associated literal with i_lit, this make literal and this associated - // literal equivalent. - void HalfAssociateGivenLiteral(IntegerLiteral i_lit, Literal literal); - // Adds the implications: // Literal(before) <= associated_lit <= Literal(after). // Arguments: @@ -607,7 +597,9 @@ class IntegerEncoder { Literal associated_lit); SatSolver* sat_solver_; - IntegerDomains* domains_; + Trail* trail_; + DelayedRootLevelDeduction* delayed_to_fix_; + const IntegerDomains& domains_; bool add_implications_ = true; int64_t num_created_variables_ = 0; @@ -616,9 +608,18 @@ class IntegerEncoder { // by bound (so we can properly add implications between the literals // corresponding to the same variable). // + // Note that we only keep this for positive variable. + // The one for the negation can be infered by it. + // + // Like x >= 1 x >= 4 x >= 5 + // Correspond to x <= 0 x <= 3 x <= 4 + // That is -x >= 0 -x >= -2 -x >= -4 + // + // With potentially stronger <= bound if we fall into domain holes. + // // TODO(user): Remove the entry no longer needed because of level zero // propagations. - absl::StrongVector> + absl::StrongVector> encoding_by_var_; // Store for a given LiteralIndex the list of its associated IntegerLiterals. @@ -632,8 +633,6 @@ class IntegerEncoder { // Used by GetAllAssociatedVariables(). mutable std::vector temp_associated_vars_; - std::vector newly_fixed_integer_literals_; - // Store for a given LiteralIndex its IntegerVariable view or kNoLiteralIndex // if there is none. absl::StrongVector literal_view_; @@ -660,6 +659,7 @@ class IntegerEncoder { // Temporary memory used by FullyEncodeVariable(). std::vector tmp_values_; + std::vector tmp_encoding_; DISALLOW_COPY_AND_ASSIGN(IntegerEncoder); }; @@ -671,9 +671,11 @@ class IntegerTrail : public SatPropagator { public: explicit IntegerTrail(Model* model) : SatPropagator("IntegerTrail"), + delayed_to_fix_(model->GetOrCreate()), domains_(model->GetOrCreate()), encoder_(model->GetOrCreate()), trail_(model->GetOrCreate()), + sat_solver_(model->GetOrCreate()), parameters_(*model->GetOrCreate()) { model->GetOrCreate()->AddPropagator(this); } @@ -934,6 +936,15 @@ class IntegerTrail : public SatPropagator { ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, LazyReasonFunction lazy_reason); + // Sometimes we infer some root level bounds but we are not at the root level. + // In this case, we will update the level-zero bounds right away, but will + // delay the current push until the next restart. + // + // Note that if you want to also push the literal at the current level, then + // just calling Enqueue() is enough. Since there is no reason, the literal + // will still be recorded properly. + ABSL_MUST_USE_RESULT bool RootLevelEnqueue(IntegerLiteral i_lit); + // Enqueues the given literal on the trail. // See the comment of Enqueue() for the reason format. void EnqueueLiteral(Literal literal, absl::Span literal_reason, @@ -1028,7 +1039,8 @@ class IntegerTrail : public SatPropagator { // Return true if we can fix new fact at level zero. bool HasPendingRootLevelDeduction() const { - return !literal_to_fix_.empty() || !integer_literal_to_fix_.empty(); + return !delayed_to_fix_->literal_to_fix.empty() || + !delayed_to_fix_->integer_literal_to_fix.empty(); } private: @@ -1170,14 +1182,6 @@ class IntegerTrail : public SatPropagator { tmp_var_to_trail_index_in_queue_; mutable SparseBitset added_variables_; - // Sometimes we propagate fact with no reason at a positive level, those - // will automatically be fixed on the next restart. - // - // TODO(user): If we change the logic to not restart right away, we probably - // need to not store duplicates bounds for the same variable. - std::vector literal_to_fix_; - std::vector integer_literal_to_fix_; - // Temporary heap used by RelaxLinearReason(); struct RelaxHeapEntry { int index; @@ -1212,9 +1216,12 @@ class IntegerTrail : public SatPropagator { std::vector*> watchers_; std::vector reversible_classes_; + mutable Domain temp_domain_; + DelayedRootLevelDeduction* delayed_to_fix_; IntegerDomains* domains_; IntegerEncoder* encoder_; Trail* trail_; + SatSolver* sat_solver_; const SatParameters& parameters_; // Temporary "hash" to keep track of all the conditional enqueue that were diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index a701c924c0..7873546ff8 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -869,11 +869,6 @@ bool IntegerSearchHelper::BeforeTakingDecision() { } if (sat_solver_->CurrentDecisionLevel() == 0) { - if (!implied_bounds_->EnqueueNewDeductions()) { - sat_solver_->NotifyThatModelIsUnsat(); - return false; - } - auto* level_zero_callbacks = model_->GetOrCreate(); for (const auto& cb : level_zero_callbacks->callbacks) { if (!cb()) { @@ -964,7 +959,7 @@ bool IntegerSearchHelper::TakeDecision(Literal decision) { // Update the implied bounds each time we enqueue a literal at level zero. // This is "almost free", so we might as well do it. if (old_level == 0 && sat_solver_->CurrentDecisionLevel() == 1) { - implied_bounds_->ProcessIntegerTrail(decision); + if (!implied_bounds_->ProcessIntegerTrail(decision)) return false; product_detector_->ProcessTrailAtLevelOne(); } diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index 98fea6ad00..52f0b8fb22 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -93,15 +93,18 @@ std::pair GetMinAndMaxNotEncoded( IntegerVariable var, const absl::flat_hash_set& encoded_values, const Model& model) { + CHECK(VariableIsPositive(var)); + const PositiveOnlyIndex index = GetPositiveOnlyIndex(var); + const auto* domains = model.Get(); - if (domains == nullptr || var >= domains->size()) { + if (domains == nullptr || index >= domains->size()) { return {kMaxIntegerValue, kMinIntegerValue}; } // The domain can be large, but the list of values shouldn't, so this // runs in O(encoded_values.size()); IntegerValue min = kMaxIntegerValue; - for (const int64_t v : (*domains)[var].Values()) { + for (const int64_t v : (*domains)[index].Values()) { if (!encoded_values.contains(IntegerValue(v))) { min = IntegerValue(v); break; @@ -109,7 +112,8 @@ std::pair GetMinAndMaxNotEncoded( } IntegerValue max = kMinIntegerValue; - for (const int64_t v : (*domains)[NegationOf(var)].Values()) { + const Domain negated_domain = (*domains)[index].Negation(); + for (const int64_t v : negated_domain.Values()) { if (!encoded_values.contains(IntegerValue(-v))) { max = IntegerValue(-v); break; @@ -284,8 +288,7 @@ void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const auto* encoder = model.Get(); if (integer_trail == nullptr || encoder == nullptr) return; - const absl::btree_map& greater_than_encoding = - encoder->PartialGreaterThanEncoding(var); + const auto& greater_than_encoding = encoder->PartialGreaterThanEncoding(var); if (greater_than_encoding.empty()) return; // Start by the var >= side. @@ -297,19 +300,19 @@ void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, lb_constraint.AddTerm(var, IntegerValue(1)); LiteralIndex prev_literal_index = kNoLiteralIndex; for (const auto entry : greater_than_encoding) { - if (entry.first <= prev_used_bound) continue; + if (entry.value <= prev_used_bound) continue; - const LiteralIndex literal_index = entry.second.Index(); - const IntegerValue diff = prev_used_bound - entry.first; + const LiteralIndex literal_index = entry.literal.Index(); + const IntegerValue diff = prev_used_bound - entry.value; // Skip the entry if the literal doesn't have a view. - if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue; + if (!lb_constraint.AddLiteralTerm(entry.literal, diff)) continue; if (prev_literal_index != kNoLiteralIndex) { // Add var <= prev_var, which is the same as var + not(prev_var) <= 1 relaxation->at_most_ones.push_back( {Literal(literal_index), Literal(prev_literal_index).Negated()}); } - prev_used_bound = entry.first; + prev_used_bound = entry.value; prev_literal_index = literal_index; } relaxation->linear_constraints.push_back(lb_constraint.Build()); @@ -324,12 +327,12 @@ void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, lb_constraint.AddTerm(var, IntegerValue(-1)); for (const auto entry : encoder->PartialGreaterThanEncoding(NegationOf(var))) { - if (entry.first <= prev_used_bound) continue; - const IntegerValue diff = prev_used_bound - entry.first; + if (entry.value <= prev_used_bound) continue; + const IntegerValue diff = prev_used_bound - entry.value; // Skip the entry if the literal doesn't have a view. - if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue; - prev_used_bound = entry.first; + if (!lb_constraint.AddLiteralTerm(entry.literal, diff)) continue; + prev_used_bound = entry.value; } relaxation->linear_constraints.push_back(lb_constraint.Build()); } diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index 661a9f2116..6acb66cda9 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -83,7 +83,7 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) { if (callback_ != nullptr) callback_(decision); } - implied_bounds_->ProcessIntegerTrail(decision); + if (!implied_bounds_->ProcessIntegerTrail(decision)) return false; product_detector_->ProcessTrailAtLevelOne(); integer_trail_->AppendNewBounds(&new_integer_bounds_); for (int i = saved_index + 1; i < trail_.Index(); ++i) { diff --git a/ortools/sat/samples/boolean_product_sample_sat.py b/ortools/sat/samples/boolean_product_sample_sat.py index 3763dc4e8b..d0ce55463b 100755 --- a/ortools/sat/samples/boolean_product_sample_sat.py +++ b/ortools/sat/samples/boolean_product_sample_sat.py @@ -26,10 +26,10 @@ def BooleanProductSampleSat(): y = model.NewBoolVar('y') p = model.NewBoolVar('p') - # x and y implies p, rewrite as not(x and y) or p + # x and y implies p, rewrite as not(x and y) or p. model.AddBoolOr(x.Not(), y.Not(), p) - # p implies x and y, expanded into two implication + # p implies x and y, expanded into two implications. model.AddImplication(p, x) model.AddImplication(p, y) diff --git a/ortools/sat/sat_decision.cc b/ortools/sat/sat_decision.cc index b84fe3c329..f7cb2a9b91 100644 --- a/ortools/sat/sat_decision.cc +++ b/ortools/sat/sat_decision.cc @@ -44,7 +44,7 @@ void SatDecisionPolicy::IncreaseNumVariables(int num_variables) { activities_.resize(num_variables, parameters_.initial_variables_activity()); tie_breakers_.resize(num_variables, 0.0); - num_bumps_.resize(num_variables, 0); + num_bumps_.clear(); pq_need_update_for_var_at_trail_index_.IncreaseSize(num_variables); weighted_sign_.resize(num_variables, 0.0); @@ -144,7 +144,7 @@ void SatDecisionPolicy::ResetDecisionHeuristic() { variable_activity_increment_ = 1.0; activities_.assign(num_variables, parameters_.initial_variables_activity()); tie_breakers_.assign(num_variables, 0.0); - num_bumps_.assign(num_variables, 0); + num_bumps_.clear(); var_ordering_.Clear(); polarity_phase_ = 0; @@ -303,6 +303,9 @@ void SatDecisionPolicy::UpdateWeightedSign( void SatDecisionPolicy::BumpVariableActivities( const std::vector& literals) { if (parameters_.use_erwa_heuristic()) { + if (num_bumps_.size() != activities_.size()) { + num_bumps_.resize(activities_.size(), 0); + } for (const Literal literal : literals) { // Note that we don't really need to bump level 0 variables since they // will never be backtracked over. However it is faster to simply bump @@ -419,6 +422,10 @@ void SatDecisionPolicy::Untrail(int target_trail_index) { DCHECK_LT(target_trail_index, trail_.Index()); if (parameters_.use_erwa_heuristic()) { + if (num_bumps_.size() != activities_.size()) { + num_bumps_.resize(activities_.size(), 0); + } + // The ERWA parameter between the new estimation of the learning rate and // the old one. TODO(user): Expose parameters for these values. const double alpha = std::max(0.06, 0.4 - 1e-6 * num_conflicts_); diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 6e3c8dc430..d3ecf95e42 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -666,6 +666,7 @@ bool SatSolver::ReapplyAssumptionsIfNeeded() { bool SatSolver::PropagateAndStopAfterOneConflictResolution() { SCOPED_TIME_STAT(&stats_); if (Propagate()) return true; + if (model_is_unsat_) return false; ++counters_.num_failures; const int conflict_trail_index = trail_->Index(); diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index a8e018b32f..b7ec7e17d0 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -946,14 +946,8 @@ inline std::function AtMostOneConstraint( inline std::function ClauseConstraint( absl::Span literals) { return [=](Model* model) { - std::vector cst; - cst.reserve(literals.size()); - for (const Literal l : literals) { - cst.emplace_back(l, Coefficient(1)); - } - model->GetOrCreate()->AddLinearConstraint( - /*use_lower_bound=*/true, Coefficient(1), - /*use_upper_bound=*/false, Coefficient(1), &cst); + model->GetOrCreate()->AddProblemClause(literals, + /*is_safe=*/false); }; } diff --git a/ortools/util/sorted_interval_list.cc b/ortools/util/sorted_interval_list.cc index 54265ef2b8..2fad5dd85c 100644 --- a/ortools/util/sorted_interval_list.cc +++ b/ortools/util/sorted_interval_list.cc @@ -235,6 +235,30 @@ int64_t Domain::SmallestValue() const { return result; } +int64_t Domain::ValueAtOrBefore(int64_t input) const { + // Because we only compare by start and there is no duplicate starts, this + // should be the next interval after the one that has a chance to contains + // value. + auto it = std::upper_bound(intervals_.begin(), intervals_.end(), + ClosedInterval(input, input)); + if (it == intervals_.begin()) return input; + --it; + return input <= it->end ? input : it->end; +} + +int64_t Domain::ValueAtOrAfter(int64_t input) const { + // Because we only compare by start and there is no duplicate starts, this + // should be the next interval after the one that has a chance to contains + // value. + auto it = std::upper_bound(intervals_.begin(), intervals_.end(), + ClosedInterval(input, input)); + if (it == intervals_.end()) return input; + const int64_t candidate = it->start; + if (it == intervals_.begin()) return candidate; + --it; + return input <= it->end ? input : candidate; +} + int64_t Domain::FixedValue() const { DCHECK(IsFixed()); return intervals_.front().start; diff --git a/ortools/util/sorted_interval_list.h b/ortools/util/sorted_interval_list.h index 88b3803c23..59913f1a5b 100644 --- a/ortools/util/sorted_interval_list.h +++ b/ortools/util/sorted_interval_list.h @@ -244,6 +244,13 @@ class Domain { */ int64_t SmallestValue() const; + /** + * Returns the closest value in the domain that is <= (resp. >=) to the input. + * Do not change the input if there is no such value. + */ + int64_t ValueAtOrBefore(int64_t input) const; + int64_t ValueAtOrAfter(int64_t input) const; + /** * Returns true iff the domain is reduced to a single value. * The domain must not be empty.