[CP-SAT] more work on clause management

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);

ortools/sat/clause.h

@@ -19,6 +19,7 @@
 
 #include <cstdint>
 #include <deque>
+#include <functional>
 #include <string>
 #include <utility>
 #include <vector>
@@ -785,7 +786,13 @@ class BinaryImplicationGraph : public SatPropagator {
   // Returns the next at_most_one, or a span of size 0 when finished.
   absl::Span<const Literal> 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<LiteralIndex, bool> might_have_dups_;
+  std::vector<Literal> 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

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) {

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,

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,

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<DiffnCtEvent> events;

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());

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<LiteralIndex> moved_last;
   std::vector<Literal> 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<LiteralIndex, int> 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<Literal> SatSolver::GetLastIncompatibleDecisions() {

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_; }
 

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) {