From 47306a72cafd95a33d270fcc8440c45e63ba11a3 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 13 Dec 2023 16:14:35 +0100 Subject: [PATCH] [CP-SAT] more work on clause management --- ortools/sat/clause.cc | 18 +++++++++++ ortools/sat/clause.h | 11 +++++++ ortools/sat/cp_model_checker.cc | 3 +- ortools/sat/cp_model_lns.h | 2 +- ortools/sat/cp_model_solver.cc | 2 +- ortools/sat/diffn_cuts.cc | 2 +- ortools/sat/sat_inprocessing.cc | 2 ++ ortools/sat/sat_solver.cc | 54 +++++++++++++++++++++++++++++---- ortools/sat/sat_solver.h | 1 + ortools/sat/stat_tables.cc | 5 +-- 10 files changed, 88 insertions(+), 12 deletions(-) diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 657e21ed38..e26fe09e2c 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -495,6 +495,7 @@ void LiteralWatchers::DeleteRemovedClauses() { void BinaryImplicationGraph::Resize(int num_variables) { SCOPED_TIME_STAT(&stats_); implications_.resize(num_variables << 1); + might_have_dups_.resize(num_variables << 1); is_redundant_.resize(implications_.size()); is_removed_.resize(implications_.size(), false); estimated_sizes_.resize(implications_.size(), 0); @@ -502,6 +503,20 @@ void BinaryImplicationGraph::Resize(int num_variables) { reasons_.resize(num_variables); } +void BinaryImplicationGraph::NotifyPossibleDuplicate(Literal a) { + if (might_have_dups_[a.Index()]) return; + might_have_dups_[a.Index()] = true; + to_clean_.push_back(a); +} + +void BinaryImplicationGraph::RemoveDuplicates() { + for (const Literal l : to_clean_) { + might_have_dups_[l.Index()] = false; + gtl::STLSortAndRemoveDuplicates(&implications_[l.Index()]); + } + to_clean_.clear(); +} + // TODO(user): Not all of the solver knows about representative literal, do // use them here to maintains invariant? Explore this when we start cleaning our // clauses using equivalence during search. We can easily do it for every @@ -532,6 +547,8 @@ bool BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) { estimated_sizes_[b.NegatedIndex()]++; implications_[a.NegatedIndex()].push_back(b); implications_[b.NegatedIndex()].push_back(a); + NotifyPossibleDuplicate(a); + NotifyPossibleDuplicate(b); is_dag_ = false; num_implications_ += 2; @@ -704,6 +721,7 @@ bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(int base_index) { for (const Literal b : at_most_one) { if (a == b) continue; implications_[a].push_back(b.Negated()); + NotifyPossibleDuplicate(a); } } num_implications_ += at_most_one.size() * (at_most_one.size() - 1); diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index 54f6b5a2a6..2ef8fb6cf7 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -19,6 +19,7 @@ #include #include +#include #include #include #include @@ -785,7 +786,13 @@ class BinaryImplicationGraph : public SatPropagator { // Returns the next at_most_one, or a span of size 0 when finished. absl::Span NextAtMostOne(); + // Clean up implications list that might have duplicates. + void RemoveDuplicates(); + private: + // Mark implications_[a] for cleanup in RemoveDuplicates(). + void NotifyPossibleDuplicate(Literal a); + // Simple wrapper to not forget to output newly fixed variable to the DRAT // proof if needed. This will propagate right away the implications. bool FixLiteral(Literal true_literal); @@ -846,6 +853,10 @@ class BinaryImplicationGraph : public SatPropagator { implications_; int64_t num_implications_ = 0; + // Used by RemoveDuplicates() and NotifyPossibleDuplicate(). + absl::StrongVector might_have_dups_; + std::vector to_clean_; + // Internal representation of at_most_one constraints. Each entry point to the // start of a constraint in the buffer. Constraints are terminated by // kNoLiteral. When LiteralIndex is true, then all entry in the at most one diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 5d538fd996..f50d544ef9 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -28,6 +28,7 @@ #include "absl/log/check.h" #include "absl/meta/type_traits.h" #include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/logging.h" #include "ortools/port/proto_utils.h" @@ -532,7 +533,7 @@ std::string ValidateRoutesConstraint(const CpModelProto& model, } std::string ValidateDomainIsPositive(const CpModelProto& model, int ref, - const std::string& ref_name) { + absl::string_view ref_name) { if (ref < 0) { const IntegerVariableProto& var_proto = model.variables(NegatedRef(ref)); if (var_proto.domain(var_proto.domain_size() - 1) > 0) { diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h index dfbe9bcbe1..ca157406d8 100644 --- a/ortools/sat/cp_model_lns.h +++ b/ortools/sat/cp_model_lns.h @@ -722,7 +722,7 @@ class RandomPrecedencesPackingNeighborhoodGenerator class SlicePackingNeighborhoodGenerator : public NeighborhoodGenerator { public: explicit SlicePackingNeighborhoodGenerator( - NeighborhoodGeneratorHelper const* helper, const std::string& name) + NeighborhoodGeneratorHelper const* helper, absl::string_view name) : NeighborhoodGenerator(name, helper) {} Neighborhood Generate(const CpSolverResponse& initial_solution, diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 920914f62e..ba46b08f6d 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -2278,7 +2278,7 @@ struct SharedClasses { // Encapsulate a full CP-SAT solve without presolve in the SubSolver API. class FullProblemSolver : public SubSolver { public: - FullProblemSolver(const std::string& name, + FullProblemSolver(absl::string_view name, const SatParameters& local_parameters, bool split_in_chunks, SharedClasses* shared, bool stop_at_first_solution = false) : SubSolver(stop_at_first_solution ? absl::StrCat("fs_", name) : name, diff --git a/ortools/sat/diffn_cuts.cc b/ortools/sat/diffn_cuts.cc index fbf6bba488..876e43fcfb 100644 --- a/ortools/sat/diffn_cuts.cc +++ b/ortools/sat/diffn_cuts.cc @@ -605,7 +605,7 @@ CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator( if (rectangles.size() <= 1) continue; auto generate_cuts = [product_decomposer, manager, model, &rectangles]( - const std::string& cut_name, + absl::string_view cut_name, SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper) { std::vector events; diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc index 8777302320..13a100ee84 100644 --- a/ortools/sat/sat_inprocessing.cc +++ b/ortools/sat/sat_inprocessing.cc @@ -83,6 +83,7 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) { // This one is fast since only newly fixed variables are considered. implication_graph_->RemoveFixedVariables(); + implication_graph_->RemoveDuplicates(); // This also prepare the stamping below so that we do that on a DAG and do // not consider potential new implications added by @@ -196,6 +197,7 @@ bool Inprocessing::InprocessingRound() { // updates. decision_policy_->MaybeEnablePhaseSaving(/*save_phase=*/false); + implication_graph_->RemoveDuplicates(); RETURN_IF_FALSE(DetectEquivalencesAndStamp(true, log_round_info)); RETURN_IF_FALSE(RemoveFixedAndEquivalentVariables(log_round_info)); RETURN_IF_FALSE(LevelZeroPropagate()); diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index f1866da5d2..e33d1fed50 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -1176,13 +1176,51 @@ bool SatSolver::SubsumptionIsInteresting(BooleanVariable variable) { // of here. I think the name for that (or similar) technique is called vivify. // Ideally this should be scheduled after other faster in-processing technique. void SatSolver::TryToMinimizeClause(SatClause* clause) { - CHECK_EQ(CurrentDecisionLevel(), 0); CHECK(clause != nullptr); ++counters_.minimization_num_clauses; absl::btree_set moved_last; std::vector candidate(clause->begin(), clause->end()); + // Note that CP-SAT presolve detect the clauses that share n-1 literals and + // transform them into (n-1 enforcement) => (1 literal per clause). We + // currently do not support that internally, but these clauses will still + // likely be loaded one after the other, so there is an high chance that if we + // call TryToMinimizeClause() on consecutive clauses, there will be a long + // prefix in common ! + // + // TODO(user): Exploit this more by choosing a good minimization order? + int longest_valid_prefix = 0; + if (CurrentDecisionLevel() > 0) { + // Quick linear scan to see if first literal is there. + const Literal first_decision = decisions_[0].literal; + for (int i = 0; i < candidate.size(); ++i) { + if (candidate[i].Negated() == first_decision) { + std::swap(candidate[0], candidate[i]); + longest_valid_prefix = 1; + break; + } + } + // Lets compute the full maximum prefix if we have already one match. + if (longest_valid_prefix == 1 && CurrentDecisionLevel() > 1) { + // Lets do the full algo. + absl::flat_hash_map indexing; + for (int i = 0; i < candidate.size(); ++i) { + indexing[candidate[i].NegatedIndex()] = i; + } + for (; longest_valid_prefix < CurrentDecisionLevel(); + ++longest_valid_prefix) { + const auto it = + indexing.find(decisions_[longest_valid_prefix].literal.Index()); + if (it == indexing.end()) break; + std::swap(candidate[longest_valid_prefix], candidate[it->second]); + indexing[candidate[it->second].NegatedIndex()] = it->second; + } + counters_.minimization_num_reused += longest_valid_prefix; + } + } + Backtrack(longest_valid_prefix); + while (!model_is_unsat_) { // We want each literal in candidate to appear last once in our propagation // order. We want to do that while maximizing the reutilization of the @@ -1251,8 +1289,11 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) { } // Returns if we don't have any minimization. - Backtrack(0); + // + // Note that we don't backtrack right away so maybe if the next clause as + // similar literal, we can reuse the trail prefix! if (candidate.size() == clause->size()) return; + Backtrack(0); if (candidate.size() == 1) { if (drat_proof_handler_ != nullptr) { @@ -1424,13 +1465,14 @@ bool SatSolver::MinimizeByPropagation(double dtime) { AdvanceDeterministicTime(time_limit_); } - block_clause_deletion_ = false; - clauses_propagator_->DeleteRemovedClauses(); - // Note(user): In some corner cases, the function above might find a // feasible assignment. I think it is okay to ignore this special case // that should only happen on trivial problems and just reset the solver. - return ResetToLevelZero(); + const bool result = ResetToLevelZero(); + + block_clause_deletion_ = false; + clauses_propagator_->DeleteRemovedClauses(); + return result; } std::vector SatSolver::GetLastIncompatibleDecisions() { diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index 13dcf1427c..4fae9690e0 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -429,6 +429,7 @@ class SatSolver { int64_t minimization_num_true = 0; int64_t minimization_num_subsumed = 0; int64_t minimization_num_removed_literals = 0; + int64_t minimization_num_reused = 0; }; Counters counters() const { return counters_; } diff --git a/ortools/sat/stat_tables.cc b/ortools/sat/stat_tables.cc index 8876c5eed0..2e99bf0175 100644 --- a/ortools/sat/stat_tables.cc +++ b/ortools/sat/stat_tables.cc @@ -50,7 +50,7 @@ SharedStatTables::SharedStatTables() { clauses_table_.push_back({"SAT stats", "ClassicMinim", "LitRemoved", "LitLearned", "LitForgotten", "Subsumed", "MClauses", "MDecisions", "MLitTrue", "MSubsumed", - "MLitRemoved"}); + "MLitRemoved", "MReused"}); lp_table_.push_back({"Lp stats", "Component", "Iterations", "AddedCuts", "OPTIMAL", "DUAL_F.", "DUAL_U."}); @@ -103,7 +103,8 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) { FormatCounter(counters.minimization_num_decisions), FormatCounter(counters.minimization_num_true), FormatCounter(counters.minimization_num_subsumed), - FormatCounter(counters.minimization_num_removed_literals)}); + FormatCounter(counters.minimization_num_removed_literals), + FormatCounter(counters.minimization_num_reused)}); } void SharedStatTables::AddLpStat(absl::string_view name, Model* model) {