From 6b518a65e5e7826b671d856dc47d1e6b28db22cb Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 18 Nov 2025 17:12:04 +0100 Subject: [PATCH] [CP-SAT] fix bugs in lrat, inner clause handling, variable expansion --- ortools/sat/clause.cc | 11 ++ ortools/sat/cp_model_solver_helpers.cc | 4 + ortools/sat/presolve_context.cc | 57 ++++++- ortools/sat/presolve_context_test.cc | 2 +- ortools/sat/probing.cc | 80 +++++---- ortools/sat/probing.h | 3 - ortools/sat/sat_inprocessing.cc | 220 ++++++++++++++----------- ortools/sat/sat_solver.cc | 2 + ortools/sat/synchronization.cc | 23 ++- ortools/sat/synchronization.h | 11 +- ortools/sat/variable_expand.cc | 44 +++-- 11 files changed, 286 insertions(+), 171 deletions(-) diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index feaa3d19cc..f396b1089c 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -292,6 +292,9 @@ SatClause* ClauseManager::ReasonClause(int trail_index) const { SatClause* ClauseManager::ReasonClauseOrNull(BooleanVariable var) const { if (!trail_->Assignment().VariableIsAssigned(var)) return nullptr; if (trail_->AssignmentType(var) != propagator_id_) return nullptr; + + DCHECK_EQ(trail_->Reason(var), + reasons_[trail_->Info(var).trail_index]->PropagationReason()); return reasons_[trail_->Info(var).trail_index]; } @@ -546,6 +549,14 @@ bool ClauseManager::InprocessingRewriteClause( AttachOnFalse(new_clause[0], new_clause[1], clause); AttachOnFalse(new_clause[1], new_clause[0], clause); } + + // We need to change the reason now that the clause size changed because + // we cache the span into the reason data directly. + if (is_reason) { + trail_->ChangeReason(trail_->Info(new_clause[0].Variable()).trail_index, + propagator_id_); + } + return true; } diff --git a/ortools/sat/cp_model_solver_helpers.cc b/ortools/sat/cp_model_solver_helpers.cc index f8861bd359..e8a7644707 100644 --- a/ortools/sat/cp_model_solver_helpers.cc +++ b/ortools/sat/cp_model_solver_helpers.cc @@ -1168,6 +1168,10 @@ int RegisterClausesLevelZeroImport(int id, } } clause_manager->SetAddClauseCallback(std::move(callback)); + if (new_clauses > 0) { + shared_clauses_manager->NotifyNumImported(id, new_clauses); + } + if (new_clauses > 0 && !sat_solver->FinishPropagation()) return false; if (minimize_shared_clauses && new_clauses > 0) { // The new clauses may be subsumed, so try to minimize them to reduce diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 6e71b696f4..344c892d1c 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -2111,6 +2111,12 @@ bool PresolveContext::CanonicalizeObjective(bool simplify_domain) { .IntersectionWith(Domain(std::numeric_limits::min(), objective_domain_.Max())) .IsIncludedIn(objective_domain_); + if (objective_domain_is_constraining_) { + VLOG(3) << "objective domain is constraining: size: " + << objective_map_.size() + << ", implied: " << implied_domain.ToString() + << " objective: " << objective_domain_.ToString(); + } return true; } @@ -2247,14 +2253,53 @@ bool PresolveContext::SubstituteVariableInObjective( RemoveVariableFromObjective(var_in_equality); - // Because we can assume that the constraint we used was constraining - // (otherwise it would have been removed), the objective domain should be now - // constraining. - objective_domain_is_constraining_ = true; + // If the objective is small enough, recompute the value of + // objective_domain_is_constrainting_, otherwise, we just assume it to be + // true. This uses the updated objective_map_. + if (objective_map_.size() < 256) { + Domain implied_domain(0); - if (objective_domain_.IsEmpty()) { - return NotifyThatModelIsUnsat(); + // We need to sort the entries to be deterministic. + tmp_entries_.clear(); + for (const auto& entry : objective_map_) { + tmp_entries_.push_back(entry); + } + std::sort(tmp_entries_.begin(), tmp_entries_.end()); + for (const auto& entry : tmp_entries_) { + const int var = entry.first; + const int64_t coeff = entry.second; + implied_domain = + implied_domain.AdditionWith(DomainOf(var).MultiplicationBy(coeff)) + .RelaxIfTooComplex(); + } + + // This is the new domain. + // Note that the domain never include the offset. + objective_domain_ = objective_domain_.IntersectionWith(implied_domain) + .SimplifyUsingImpliedDomain(implied_domain); + + if (objective_domain_.IsEmpty()) { + return NotifyThatModelIsUnsat("empty objective domain"); + } + + // Detect if the objective domain do not limit the "optimal" objective + // value. If this is true, then we can apply any reduction that reduce the + // objective value without any issues. + objective_domain_is_constraining_ = + !implied_domain + .IntersectionWith(Domain(std::numeric_limits::min(), + objective_domain_.Max())) + .IsIncludedIn(objective_domain_); + if (objective_domain_is_constraining_) { + VLOG(3) << "objective domain is constraining: size: " + << objective_map_.size() + << ", implied: " << implied_domain.ToString() + << " objective: " << objective_domain_.ToString(); + } + } else { + objective_domain_is_constraining_ = true; } + return true; } diff --git a/ortools/sat/presolve_context_test.cc b/ortools/sat/presolve_context_test.cc index dfa5312830..05321e7306 100644 --- a/ortools/sat/presolve_context_test.cc +++ b/ortools/sat/presolve_context_test.cc @@ -506,7 +506,7 @@ TEST(PresolveContextTest, ObjectiveSubstitutionWithLargeCoeff) { objective { vars: [ 1, 2 ] coeffs: [ 2, 2 ] - domain: [ 12, 1012 ] # [0, 1000] initially, + 2*6 offset. + domain: [ 12, 36 ] # [0, 1000] initially, + 2*6 offset. offset: -9 integer_before_offset: -12 scaling_factor: 1 diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index 0adac2ebf9..f8602d4003 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -654,7 +654,6 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) { } binary_clause_extracted_.assign(trail_.Index(), false); - subsumed_clauses_.clear(); while (!time_limit_->LimitReached() && time_limit_->GetElapsedDeterministicTime() <= limit) { @@ -738,15 +737,7 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) { if (!sat_solver_->ResetToLevelZero()) return false; if (!ProcessLiteralsToFix()) return false; - if (!subsumed_clauses_.empty()) { - for (SatClause* clause : subsumed_clauses_) { - if (clause->size() == 0) continue; - ++num_subsumed_; - clause_manager_->LazyDelete(clause, - DeletionSourceForStat::SUBSUMPTION_PROBING); - } - clause_manager_->CleanUpWatchers(); - } + clause_manager_->CleanUpWatchers(); // Display stats. const int num_fixed = sat_solver_->LiteralTrail().Index(); @@ -994,7 +985,31 @@ void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision, // of all literals in the reason for this propagation. And use this // as a reason for later hyber binary resolution. Like we do when // this clause subsumes the reason. - AddImplication(last_decision, l); + ++num_new_binary_; + DCHECK(assignment_.LiteralIsTrue(l)); + CHECK_NE(l.Variable(), last_decision.Variable()); + + // We should never probe a redundant literal. + // + // TODO(user): We should be able to enforce that l is non-redundant either if + // we made sure the clause database is cleaned up before FailedLiteralProbing + // is called. This should maybe simplify the ChangeReason() handling. + DCHECK(!implication_graph_->IsRedundant(last_decision)); + + ClauseId clause_id = kNoClauseId; + if (lrat_proof_handler_ != nullptr) { + clause_id = clause_id_generator_->GetNextId(); + tmp_clause_ids_.clear(); + sat_solver_->AppendClausesFixing({l}, &tmp_clause_ids_, last_decision); + lrat_proof_handler_->AddInferredClause( + clause_id, {last_decision.Negated(), l}, tmp_clause_ids_); + } + + // Each time we extract a binary clause, we change the reason in the trail. + // This is important as it will allow us to remove clauses that are now + // subsumed by this binary, even if it was a reason. + CHECK(implication_graph_->AddBinaryClauseAndChangeReason( + clause_id, l, last_decision.Negated())); } // If we can extract a binary clause that subsume the reason clause, we do add @@ -1006,6 +1021,7 @@ void FailedLiteralProbing::MaybeSubsumeWithBinaryClause( const Literal last_decision, const Literal l) { const int trail_index = trail_.Info(l.Variable()).trail_index; if (trail_.AssignmentType(l.Variable()) != clause_propagator_id_) return; + SatClause* clause = clause_manager_->ReasonClause(trail_index); bool subsumed = false; for (const Literal lit : trail_.Reason(l.Variable())) { @@ -1027,7 +1043,12 @@ void FailedLiteralProbing::MaybeSubsumeWithBinaryClause( if (lit == last_decision.Negated()) ++test; } CHECK_EQ(test, 2); - subsumed_clauses_.push_back(clause_manager_->ReasonClause(trail_index)); + + // Because of MaybeExtractImplication(), this shouldn't be a reason anymore. + CHECK(!clause_manager_->ClauseIsUsedAsReason(clause)); + ++num_subsumed_; + clause_manager_->LazyDelete(clause, + DeletionSourceForStat::SUBSUMPTION_PROBING); } // Inspect the watcher list for last_decision, If we have a blocking @@ -1043,34 +1064,21 @@ void FailedLiteralProbing::SubsumeWithBinaryClauseUsingBlockingLiteral( const Literal last_decision) { for (const auto& w : clause_manager_->WatcherListOnFalse(last_decision.Negated())) { - if (assignment_.LiteralIsTrue(w.blocking_literal)) { - if (w.clause->IsRemoved()) continue; + if (!assignment_.LiteralIsTrue(w.blocking_literal)) continue; + if (w.clause->IsRemoved()) continue; - // This should be enough for proof correctness. - if (clause_manager_->ClauseIsUsedAsReason(w.clause)) { - MaybeExtractImplication(last_decision, w.blocking_literal); - } - subsumed_clauses_.push_back(w.clause); + // This should be enough for proof correctness. + if (clause_manager_->ClauseIsUsedAsReason(w.clause)) { + MaybeExtractImplication(last_decision, w.blocking_literal); + + // It should have been replaced by a binary clause now. + CHECK(!clause_manager_->ClauseIsUsedAsReason(w.clause)); } - } -} -void FailedLiteralProbing::AddImplication(const Literal last_decision, - const Literal l) { - ++num_new_binary_; - DCHECK(assignment_.LiteralIsTrue(l)); - CHECK_NE(l.Variable(), last_decision.Variable()); - - ClauseId clause_id = kNoClauseId; - if (lrat_proof_handler_ != nullptr) { - clause_id = clause_id_generator_->GetNextId(); - tmp_clause_ids_.clear(); - sat_solver_->AppendClausesFixing({l}, &tmp_clause_ids_, last_decision); - lrat_proof_handler_->AddInferredClause( - clause_id, {last_decision.Negated(), l}, tmp_clause_ids_); + ++num_subsumed_; + clause_manager_->LazyDelete(w.clause, + DeletionSourceForStat::SUBSUMPTION_PROBING); } - CHECK(implication_graph_->AddBinaryClause(clause_id, last_decision.Negated(), - l)); } // Adds 'not(literal)' to `to_fix_`, assuming that 'literal' directly implies diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h index 787005160a..4c9c40d4c0 100644 --- a/ortools/sat/probing.h +++ b/ortools/sat/probing.h @@ -325,8 +325,6 @@ class FailedLiteralProbing { // which is quite cheap to test here. void SubsumeWithBinaryClauseUsingBlockingLiteral(Literal last_decision); - void AddImplication(Literal last_decision, Literal l); - // Adds 'not(literal)' to `to_fix_`, assuming that 'literal' directly implies // the current decision, which itself implies all the previous decisions, with // some of them propagating 'not(literal)'. @@ -366,7 +364,6 @@ class FailedLiteralProbing { // For each literal 'l' in the trail, whether a binary clause "d => l" has // been extracted, with 'd' the decision at the same level as 'l'. std::vector binary_clause_extracted_; - std::vector subsumed_clauses_; // Temporary vector used for LRAT proofs. std::vector tmp_clause_ids_; diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc index c332021ff4..b88af37e33 100644 --- a/ortools/sat/sat_inprocessing.cc +++ b/ortools/sat/sat_inprocessing.cc @@ -54,6 +54,16 @@ namespace operations_research { namespace sat { +namespace { + +bool SomeLiteralAreAssigned(const VariablesAssignment& assignment, + absl::Span literals) { + return absl::c_any_of( + literals, [&](Literal l) { return assignment.LiteralIsAssigned(l); }); +} + +} // namespace + void PostsolveClauses::AddClauseWithSpecialLiteral( Literal literal, absl::Span clause) { bool found = false; @@ -305,12 +315,14 @@ bool Inprocessing::InprocessingRound() { total_dtime_ += time_limit_->GetElapsedDeterministicTime() - start_dtime; if (log_info) { SOLVER_LOG( - logger_, "Inprocessing.", " fixed:", trail_->Index(), - " equiv:", implication_graph_->num_redundant_literals() / 2, - " bools:", sat_solver_->NumVariables(), - " implications:", implication_graph_->ComputeNumImplicationsForLog(), - " watched:", clause_manager_->num_watched_clauses(), - " minimization:", mini_num_clause, "|", mini_num_removed, + logger_, "Inprocessing.", " fixed:", FormatCounter(trail_->Index()), + " equiv:", + FormatCounter(implication_graph_->num_redundant_literals() / 2), + " bools:", FormatCounter(sat_solver_->NumVariables()), " implications:", + FormatCounter(implication_graph_->ComputeNumImplicationsForLog()), + " watched:", FormatCounter(clause_manager_->num_watched_clauses()), + " minimization:", FormatCounter(mini_num_clause), "|", + FormatCounter(mini_num_removed), " dtime:", time_limit_->GetElapsedDeterministicTime() - start_dtime, " wtime:", wall_timer.Get(), " np_wtime:", (wall_timer.Get() - probing_time)); @@ -378,22 +390,6 @@ bool Inprocessing::RemoveFixedAndEquivalentVariables(bool log_info) { CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); if (!LevelZeroPropagate()) return false; - // Test if some work is needed. - // - // TODO(user): If only new fixed variables are there, we can use a faster - // function. We should also merge the code with the deletion code in - // sat_solver_.cc, but that require some refactoring of the dependence between - // files. - const int64_t new_num_redundant_literals = - implication_graph_->num_redundant_literals(); - const int64_t new_num_fixed_variables = trail_->Index(); - if (last_num_redundant_literals_ == new_num_redundant_literals && - last_num_fixed_variables_ == new_num_fixed_variables) { - return true; - } - last_num_fixed_variables_ = new_num_fixed_variables; - last_num_redundant_literals_ = new_num_redundant_literals; - // Start the round. WallTimer wall_timer; wall_timer.Start(); @@ -401,80 +397,116 @@ bool Inprocessing::RemoveFixedAndEquivalentVariables(bool log_info) { int64_t num_removed_literals = 0; int64_t num_inspected_literals = 0; - // We need this temporary vector for the LRAT proof settings, otherwise - // we could just have done an in-place transformation. - std::vector new_clause; - - // Used to mark clause literals. - const int num_literals(sat_solver_->NumVariables() * 2); - util_intops::StrongVector marked(num_literals, false); - - clause_manager_->DeleteRemovedClauses(); - clause_manager_->DetachAllClauses(); - for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) { - bool removed = false; - bool need_rewrite = false; - - // We first do a loop to see if there is anything to do. - for (const Literal l : clause->AsSpan()) { - if (assignment_.LiteralIsTrue(l)) { - DCHECK(lrat_proof_handler_ == nullptr || - trail_->GetUnitClauseId(l.Variable()) != kNoClauseId); - clause_manager_->LazyDelete(clause, - DeletionSourceForStat::FIXED_AT_TRUE); - num_removed_literals += clause->size(); - removed = true; - break; - } - if (assignment_.LiteralIsFalse(l) || implication_graph_->IsRedundant(l)) { - need_rewrite = true; - break; - } + // We use a huge "limit" in case we have some bad interactions and we need to + // loop often to reach the fixed point. + while (num_inspected_literals < 1e10) { + // Test if some work is needed. + // + // TODO(user): If only new fixed variables are there, we can use a faster + // function. We should also merge the code with the deletion code in + // sat_solver_.cc, but that require some refactoring of the dependence + // between files. + const int64_t new_num_redundant_literals = + implication_graph_->num_redundant_literals(); + const int64_t new_num_fixed_variables = trail_->Index(); + if (last_num_redundant_literals_ == new_num_redundant_literals && + last_num_fixed_variables_ == new_num_fixed_variables) { + return true; } + last_num_fixed_variables_ = new_num_fixed_variables; + last_num_redundant_literals_ = new_num_redundant_literals; - num_inspected_literals += clause->size(); - if (removed || !need_rewrite) continue; - num_inspected_literals += clause->size(); + // We need this temporary vector for the LRAT proof settings, otherwise + // we could just have done an in-place transformation. + std::vector new_clause; + + // Used to mark clause literals. + const int num_literals(sat_solver_->NumVariables() * 2); + util_intops::StrongVector marked(num_literals, false); + + clause_manager_->DeleteRemovedClauses(); + clause_manager_->DetachAllClauses(); + for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) { + bool removed = false; + bool need_rewrite = false; + + // We first do a loop to see if there is anything to do. + for (const Literal l : clause->AsSpan()) { + if (assignment_.LiteralIsTrue(l)) { + DCHECK(lrat_proof_handler_ == nullptr || + trail_->GetUnitClauseId(l.Variable()) != kNoClauseId); + clause_manager_->LazyDelete(clause, + DeletionSourceForStat::FIXED_AT_TRUE); + num_removed_literals += clause->size(); + removed = true; + break; + } + if (assignment_.LiteralIsFalse(l) || + implication_graph_->IsRedundant(l)) { + need_rewrite = true; + break; + } + } + + num_inspected_literals += clause->size(); + if (removed || !need_rewrite) continue; + num_inspected_literals += clause->size(); + + // Rewrite the clause. + new_clause.clear(); + clause_ids_.clear(); + for (const Literal l : clause->AsSpan()) { + const Literal r = implication_graph_->RepresentativeOf(l); + if (lrat_proof_handler_ != nullptr) { + if (!marked[r] && assignment_.LiteralIsFalse(r)) { + clause_ids_.push_back(trail_->GetUnitClauseId(r.Variable())); + } + if (r != l) { + clause_ids_.push_back( + implication_graph_->GetClauseId(l.Negated(), r)); + } + } + if (marked[r] || assignment_.LiteralIsFalse(r)) { + continue; + } + if (marked[r.NegatedIndex()] || assignment_.LiteralIsTrue(r)) { + clause_manager_->LazyDelete( + clause, DeletionSourceForStat::CONTAINS_L_AND_NOT_L); + num_removed_literals += clause->size(); + removed = true; + break; + } + marked[r] = true; + new_clause.push_back(r); + } + + // Restore marked. + for (const Literal l : new_clause) marked[l] = false; + if (removed) continue; - // Rewrite the clause. - new_clause.clear(); - clause_ids_.clear(); - for (const Literal l : clause->AsSpan()) { - const Literal r = implication_graph_->RepresentativeOf(l); if (lrat_proof_handler_ != nullptr) { - if (!marked[r] && assignment_.LiteralIsFalse(r)) { - clause_ids_.push_back(trail_->GetUnitClauseId(r.Variable())); - } - if (r != l) { - clause_ids_.push_back( - implication_graph_->GetClauseId(l.Negated(), r)); - } + clause_ids_.push_back(clause_manager_->GetClauseId(clause)); } - if (marked[r] || assignment_.LiteralIsFalse(r)) { - continue; + num_removed_literals += clause->size() - new_clause.size(); + if (!clause_manager_->InprocessingRewriteClause(clause, new_clause, + clause_ids_)) { + return false; } - if (marked[r.NegatedIndex()] || assignment_.LiteralIsTrue(r)) { - clause_manager_->LazyDelete( - clause, DeletionSourceForStat::CONTAINS_L_AND_NOT_L); - num_removed_literals += clause->size(); - removed = true; - break; - } - marked[r] = true; - new_clause.push_back(r); } - // Restore marked. - for (const Literal l : new_clause) marked[l] = false; - if (removed) continue; + // If clause became binary, make sure to clean up the relevant implication + // lists. This should be fast in all cases since it is incremental. + // + // Tricky: This might fix more variables in some corner case, so we need to + // loop to reach the "fixed point" and maintain the invariant that no clause + // contain fixed variable. + if (!implication_graph_->RemoveDuplicatesAndFixedVariables()) return false; + } - if (lrat_proof_handler_ != nullptr) { - clause_ids_.push_back(clause_manager_->GetClauseId(clause)); - } - num_removed_literals += clause->size() - new_clause.size(); - if (!clause_manager_->InprocessingRewriteClause(clause, new_clause, - clause_ids_)) { - return false; + // Invariant. There should be no clause with fixed variables left. + if (DEBUG_MODE) { + for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) { + CHECK(!SomeLiteralAreAssigned(trail_->Assignment(), clause->AsSpan())); } } @@ -485,9 +517,7 @@ bool Inprocessing::RemoveFixedAndEquivalentVariables(bool log_info) { << num_removed_literals << " dtime: " << dtime << " wtime: " << wall_timer.Get(); - // If clause became binary, make sure to clean up the relevant implication - // lists. This should be fast in all cases since it is incremental. - return implication_graph_->RemoveDuplicatesAndFixedVariables(); + return true; } // TODO(user): Use better work limits, see SAT09.CRAFTED.ramseycube.Q3inK12 @@ -540,6 +570,7 @@ bool Inprocessing::SubsumeAndStrenghtenRound(bool log_info) { std::vector> candidates_for_removal; for (int clause_index = 0; clause_index < clauses.size(); ++clause_index) { SatClause* clause = clauses[clause_index]; + DCHECK(!SomeLiteralAreAssigned(trail_->Assignment(), clause->AsSpan())); // TODO(user): Better abort limit. We could also limit the watcher sizes and // never look at really long clauses. Note that for an easier @@ -549,14 +580,6 @@ bool Inprocessing::SubsumeAndStrenghtenRound(bool log_info) { break; } - // TODO(user): Work out why this has suddenly started producing - // clauses that are satisfied at the root. - if (clause->IsSatisfied(trail_->Assignment())) { - num_removed_literals += clause->size(); - clause_manager_->LazyDelete(clause, DeletionSourceForStat::FIXED_AT_TRUE); - continue; - } - // Check for subsumption, note that this currently ignore all clauses in the // binary implication graphs. Stamping is doing some of that (and some also // happen during probing), but we could consider only direct implications @@ -652,6 +675,7 @@ bool Inprocessing::SubsumeAndStrenghtenRound(bool log_info) { new_clause.push_back(l); } CHECK_EQ(new_clause.size() + 1, clause->size()); + CHECK_GE(new_clause.size(), 2); // No-unit here. num_removed_literals += clause->size() - new_clause.size(); if (lrat_proof_handler_ != nullptr) { diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 5c417787a0..7eef18ef06 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -1446,6 +1446,8 @@ bool SatSolver::TryToMinimizeClause(SatClause* clause) { CHECK(clause != nullptr); ++counters_.minimization_num_clauses; + // TODO(user): Make sure clause do not contain any redundant literal before + // we try to minimize it. std::vector candidate; candidate.reserve(clause->size()); diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 4d3bb5680b..f6cef39a76 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -27,6 +27,7 @@ #include #include #include +#include #include #include @@ -1336,6 +1337,7 @@ int SharedClausesManager::RegisterNewId(absl::string_view worker_name, id_to_last_processed_binary_clause_.resize(id + 1, 0); id_to_last_returned_batch_.resize(id + 1, -1); id_to_last_finished_batch_.resize(id + 1, -1); + id_to_num_imported_.resize(id + 1, 0); id_to_num_exported_.resize(id + 1, 0); id_to_worker_name_.resize(id + 1); id_to_worker_name_[id] = worker_name; @@ -1410,18 +1412,27 @@ void SharedClausesManager::GetUnseenBinaryClauses( id_to_last_processed_binary_clause_[id] = last_visible_binary_clause_; } +void SharedClausesManager::NotifyNumImported(int id, int64_t num_imported) { + absl::MutexLock mutex_lock(mutex_); + id_to_num_imported_[id] += num_imported; +} + void SharedClausesManager::LogStatistics(SolverLogger* logger) { absl::MutexLock mutex_lock(mutex_); - absl::btree_map name_to_table_line; + std::vector> name_to_table_line; for (int id = 0; id < id_to_num_exported_.size(); ++id) { - if (id_to_num_exported_[id] == 0) continue; - name_to_table_line[id_to_worker_name_[id]] = id_to_num_exported_[id]; + if (id_to_num_exported_[id] == 0 && id_to_num_imported_[id] == 0) continue; + name_to_table_line.push_back({id_to_worker_name_[id], + id_to_num_exported_[id], + id_to_num_imported_[id]}); } if (!name_to_table_line.empty()) { + absl::c_sort(name_to_table_line); std::vector> table; - table.push_back({"Clauses shared", "Num"}); - for (const auto& [name, count] : name_to_table_line) { - table.push_back({FormatName(name), FormatCounter(count)}); + table.push_back({"Clauses shared", "#Exported", "#Imported"}); + for (const auto& [name, exported, imported] : name_to_table_line) { + table.push_back( + {FormatName(name), FormatCounter(exported), FormatCounter(imported)}); } SOLVER_LOG(logger, FormatTable(table)); } diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h index f87c59d074..ca75d9c917 100644 --- a/ortools/sat/synchronization.h +++ b/ortools/sat/synchronization.h @@ -872,13 +872,17 @@ class SharedClausesManager { // Ids are used to identify which worker is exporting/importing clauses. int RegisterNewId(absl::string_view worker_name, bool may_terminate_early); - // Search statistics. - void LogStatistics(SolverLogger* logger); - // Unlocks waiting binary clauses for workers if always_synchronize is false. // Periodically starts a new sharing round, making glue clauses visible. void Synchronize(); + // For statistics, notify how many clauses where imported in that worker id + // database. + void NotifyNumImported(int id, int64_t num_imported); + + // Search statistics. + void LogStatistics(SolverLogger* logger); + private: // Returns true if `reader_id` should read batches produced by `writer_id`. bool ShouldReadBatch(int reader_id, int writer_id) @@ -915,6 +919,7 @@ class SharedClausesManager { // Stats: std::vector id_to_num_exported_ ABSL_GUARDED_BY(mutex_); + std::vector id_to_num_imported_ ABSL_GUARDED_BY(mutex_); std::vector id_to_num_updated_ ABSL_GUARDED_BY(mutex_); std::vector id_to_worker_name_ ABSL_GUARDED_BY(mutex_); }; diff --git a/ortools/sat/variable_expand.cc b/ortools/sat/variable_expand.cc index bfc13d7e08..93be2ac81c 100644 --- a/ortools/sat/variable_expand.cc +++ b/ortools/sat/variable_expand.cc @@ -477,10 +477,15 @@ void TryToReplaceVariableByItsEncoding(int var, int& new_exo_to_presolve_index, // We force the full encoding if the variable is mostly encoded and some // linear1 involves domains that do not correspond to value or order // encodings. - if (!lin_domain.empty() && !values.is_fully_encoded()) { - if (context->IsMostlyFullyEncoded(var) || var_domain.Size() <= 32) { - values.ForceFullEncoding(); - } + const bool full_encoding_is_not_too_expensive = + context->IsMostlyFullyEncoded(var) || var_domain.Size() <= 32; + const bool full_encoding_is_needed = + (!lin_domain.empty() || + (var_in_objective && context->ObjectiveDomainIsConstraining())); + if (!values.is_fully_encoded() && full_encoding_is_not_too_expensive && + full_encoding_is_needed) { + VLOG(3) << "Forcing full encoding of var: " << var; + values.ForceFullEncoding(); } if (values.empty()) { @@ -511,14 +516,23 @@ void TryToReplaceVariableByItsEncoding(int var, int& new_exo_to_presolve_index, << var_has_positive_objective_coefficient << ", #implied_literals_in_complex_domains: " << num_implied_literals_in_complex_domains; - if (!lin_domain.empty() && (!values.is_fully_encoded() || - num_implied_literals_in_complex_domains > 2500)) { + if (full_encoding_is_needed && + (!values.is_fully_encoded() || + num_implied_literals_in_complex_domains > 2500)) { VLOG(2) << "Abort - fully_encode_var: " << values.is_fully_encoded() << ", num_implied_literals_in_complex_domains: " - << num_implied_literals_in_complex_domains; - context->UpdateRuleStats( - "TODO variables: only used in large value encoding and order " - "encoding."); + << num_implied_literals_in_complex_domains + << ", full_encoding_is_not_too_expensive: " + << full_encoding_is_not_too_expensive + << ", full_encoding_is_needed: " << full_encoding_is_needed; + if (var_in_objective) { + context->UpdateRuleStats( + "TODO variables: only used in constrained objective and in encoding"); + } else { + context->UpdateRuleStats( + "TODO variables: only used in large value encoding and order " + "encoding."); + } return; } @@ -616,14 +630,8 @@ void TryToReplaceVariableByItsEncoding(int var, int& new_exo_to_presolve_index, : var_domain.Max(); // Tricky: We cannot just choose an arbitrary value if the objective has // a restrictive domain! - if (!values.is_fully_encoded() && - context->ObjectiveDomainIsConstraining()) { - VLOG(2) << "Abort - objective is constraining"; - context->UpdateRuleStats( - "TODO variables: only used in constrained objective and in " - "encoding"); - return; - } + DCHECK(values.is_fully_encoded() || + !context->ObjectiveDomainIsConstraining()); // Checks for overflow before trying to substitute the variable in the // objective.