[CP-SAT] vivification after import; remove unused affine in presolve;…

… remove obsolete ThreadPool usage

ortools/sat/clause.cc

@@ -483,6 +483,7 @@ void ClauseManager::DeleteRemovedClauses() {
   const int old_size = clauses_.size();
   for (int i = 0; i < old_size; ++i) {
     if (i == to_minimize_index_) to_minimize_index_ = new_size;
+    if (i == to_first_minimize_index_) to_first_minimize_index_ = new_size;
     if (i == to_probe_index_) to_probe_index_ = new_size;
     if (clauses_[i]->IsRemoved()) {
       delete clauses_[i];
@@ -493,9 +494,45 @@ void ClauseManager::DeleteRemovedClauses() {
   clauses_.resize(new_size);
 
   if (to_minimize_index_ > new_size) to_minimize_index_ = new_size;
+  if (to_first_minimize_index_ > new_size) to_first_minimize_index_ = new_size;
   if (to_probe_index_ > new_size) to_probe_index_ = new_size;
 }
 
+SatClause* ClauseManager::NextNewClauseToMinimize() {
+  for (; to_first_minimize_index_ < clauses_.size();
+       ++to_first_minimize_index_) {
+    if (clauses_[to_first_minimize_index_]->IsRemoved()) continue;
+    if (!IsRemovable(clauses_[to_first_minimize_index_])) {
+      // If the round-robin is in-sync with the new clauses, we may as well
+      // count this minimization as part of the round-robin and advance both
+      // indexes.
+      if (to_minimize_index_ == to_first_minimize_index_) {
+        ++to_minimize_index_;
+      }
+      return clauses_[to_first_minimize_index_++];
+    }
+  }
+  return nullptr;
+}
+
+SatClause* ClauseManager::NextClauseToMinimize() {
+  for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
+    if (clauses_[to_minimize_index_]->IsRemoved()) continue;
+    if (!IsRemovable(clauses_[to_minimize_index_])) {
+      return clauses_[to_minimize_index_++];
+    }
+  }
+  return nullptr;
+}
+
+SatClause* ClauseManager::NextClauseToProbe() {
+  for (; to_probe_index_ < clauses_.size(); ++to_probe_index_) {
+    if (clauses_[to_probe_index_]->IsRemoved()) continue;
+    return clauses_[to_probe_index_++];
+  }
+  return nullptr;
+}
+
 // ----- BinaryImplicationGraph -----
 
 void BinaryImplicationGraph::Resize(int num_variables) {

ortools/sat/clause.h

@@ -245,30 +245,29 @@ class ClauseManager : public SatPropagator {
     drat_proof_handler_ = drat_proof_handler;
   }
 
-  // Round-robbing selection of the next clause to minimize/probe.
-  // Note that for minimization we only look at clause kept forever.
-  //
-  // TODO(user): If more indices are needed, switch to a generic API.
-  SatClause* NextClauseToMinimize() {
-    for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
-      if (clauses_[to_minimize_index_]->IsRemoved()) continue;
-      if (!IsRemovable(clauses_[to_minimize_index_])) {
-        return clauses_[to_minimize_index_++];
-      }
-    }
-    return nullptr;
-  }
-  SatClause* NextClauseToProbe() {
-    for (; to_probe_index_ < clauses_.size(); ++to_probe_index_) {
-      if (clauses_[to_probe_index_]->IsRemoved()) continue;
-      return clauses_[to_probe_index_++];
-    }
-    return nullptr;
-  }
+  // Methods implementing pseudo-iterators over the clause database that are
+  // stable across cleanups. They all return nullptr if there are no more
+  // clauses.
+
+  // Returns the next clause to minimize that has never been minimized before.
+  // Note that we only minimize clauses kept forever.
+  SatClause* NextNewClauseToMinimize();
+  // Returns the next clause to minimize, this iterator will be reset to the
+  // start so the clauses will be returned in round-robin order.
+  // Note that we only minimize clauses kept forever.
+  SatClause* NextClauseToMinimize();
+  // Returns the next clause to probe in round-robin order.
+  SatClause* NextClauseToProbe();
 
   // Restart the scans.
   void ResetToProbeIndex() { to_probe_index_ = 0; }
   void ResetToMinimizeIndex() { to_minimize_index_ = 0; }
+  // Ensures that NextNewClauseToMinimize() returns only learned clauses.
+  // This is a noop after the first call.
+  void EnsureNewClauseIndexInitialized() {
+    if (to_first_minimize_index_ > 0) return;
+    to_first_minimize_index_ = clauses_.size();
+  }
 
   // During an inprocessing phase, it is easier to detach all clause first,
   // then simplify and then reattach them. Note however that during these
@@ -380,7 +379,9 @@ class ClauseManager : public SatPropagator {
   // Note that the unit clauses and binary clause are not kept here.
   std::vector<SatClause*> clauses_;
 
+  // TODO(user): If more indices are needed, switch to a generic API.
   int to_minimize_index_ = 0;
+  int to_first_minimize_index_ = 0;
   int to_probe_index_ = 0;
 
   // Only contains removable clause.

ortools/sat/cp_model_presolve.cc

@@ -2806,8 +2806,7 @@ bool CpModelPresolver::PresolveLinearOfSizeTwo(ConstraintProto* ct) {
       }
 
       context_->UpdateNewConstraintsVariableUsage();
-      ct->Clear();
-      return true;
+      return RemoveConstraint(ct);
     }
 
     // Code below require equality.
@@ -11623,18 +11622,7 @@ bool CpModelPresolver::PresolveAffineRelationIfAny(int var) {
   // If var is no longer used, remove. Note that we can always do that since we
   // propagated the domain above and so we can find a feasible value for a for
   // any value of the representative.
-  if (context_->VariableIsUnique(var)) {
-    // Add relation with current representative to the mapping model.
-    ConstraintProto* ct = context_->NewMappingConstraint(__FILE__, __LINE__);
-    auto* arg = ct->mutable_linear();
-    arg->add_vars(var);
-    arg->add_coeffs(1);
-    arg->add_vars(r.representative);
-    arg->add_coeffs(-r.coeff);
-    arg->add_domain(r.offset);
-    arg->add_domain(r.offset);
-    context_->RemoveVariableFromAffineRelation(var);
-  }
+  context_->RemoveNonRepresentativeAffineVariableIfUnused(var);
   return true;
 }
 
@@ -11649,6 +11637,7 @@ bool CpModelPresolver::ProcessChangedVariables(std::vector<bool>* in_queue,
       context_->modified_domains.PositionsSetAtLeastOnce();
   for (int i = 0; i < vector_that_can_grow_during_iter.size(); ++i) {
     const int v = vector_that_can_grow_during_iter[i];
+    context_->modified_domains.Clear(v);
     if (context_->VariableIsNotUsedAnymore(v)) continue;
     if (context_->ModelIsUnsat()) return false;
     if (!PresolveAffineRelationIfAny(v)) return false;
@@ -11779,6 +11768,11 @@ void CpModelPresolver::PresolveToFixPoint() {
       const int v = vector_that_can_grow_during_iter[i];
       if (context_->VariableIsNotUsedAnymore(v)) continue;
 
+      // Remove the variable from the set to allow it to be pushed again.
+      // This is necessary since a few affine logic needs to add the same
+      // variable back to a second pass of processing.
+      context_->var_with_reduced_small_degree.Clear(v);
+
       // Make sure all affine relations are propagated.
       // This also remove the relation if the degree is now one.
       if (context_->ModelIsUnsat()) return;
@@ -11819,6 +11813,9 @@ void CpModelPresolver::PresolveToFixPoint() {
 
     if (ProcessChangedVariables(&in_queue, &queue)) continue;
 
+    // TODO(user): Uncomment this line once the tests pass.
+    // DCHECK(!context_->HasUnusedAffineVariable());
+
     // Deal with integer variable only appearing in an encoding.
     for (int v = 0; v < context_->working_model->variables().size(); ++v) {
       ProcessVariableOnlyUsedInEncoding(v);

ortools/sat/cp_model_search.cc

@@ -24,7 +24,6 @@
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
-#include "absl/flags/flag.h"
 #include "absl/log/check.h"
 #include "absl/random/distributions.h"
 #include "absl/strings/str_cat.h"

ortools/sat/cp_model_search.h

@@ -20,7 +20,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
-#include "ortools/base/types.h"
+#include "absl/strings/string_view.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_mapping.h"
 #include "ortools/sat/integer.h"

ortools/sat/cp_model_solver_helpers.cc

@@ -856,14 +856,17 @@ int RegisterClausesLevelZeroImport(int id,
   CpModelMapping* const mapping = model->GetOrCreate<CpModelMapping>();
   auto* sat_solver = model->GetOrCreate<SatSolver>();
   auto* implications = model->GetOrCreate<BinaryImplicationGraph>();
-  bool share_glue_clauses =
+  const bool share_glue_clauses =
       model->GetOrCreate<SatParameters>()->share_glue_clauses();
+  const bool minimize_shared_clauses =
+      model->GetOrCreate<SatParameters>()->minimize_shared_clauses();
   auto* clause_stream = share_glue_clauses
                             ? shared_clauses_manager->GetClauseStream(id)
                             : nullptr;
   const auto& import_level_zero_clauses = [shared_clauses_manager, id, mapping,
                                            sat_solver, implications,
-                                           clause_stream]() {
+                                           clause_stream,
+                                           minimize_shared_clauses]() {
     std::vector<std::pair<int, int>> new_binary_clauses;
     shared_clauses_manager->GetUnseenBinaryClauses(id, &new_binary_clauses);
     implications->EnableSharing(false);
@@ -877,7 +880,9 @@ int RegisterClausesLevelZeroImport(int id,
     implications->EnableSharing(true);
     if (clause_stream == nullptr) return true;
 
+    int new_clauses = 0;
     std::array<Literal, UniqueClauseStream::kMaxClauseSize> local_clause;
+    sat_solver->EnsureNewClauseIndexInitialized();
     for (const absl::Span<const int> shared_clause :
          shared_clauses_manager->GetUnseenClauses(id)) {
       // Check this clause was not already learned by this worker.
@@ -893,8 +898,18 @@ int RegisterClausesLevelZeroImport(int id,
               absl::MakeSpan(local_clause).subspan(0, shared_clause.size()))) {
         return false;
       }
+      ++new_clauses;
     }
     clause_stream->RemoveWorstClauses();
+    if (minimize_shared_clauses && new_clauses > 0) {
+      // The new clauses may be subsumed, so try to minimize them to reduce
+      // overhead of sharing.
+      // We only share up to 1024 literals worth of new clauses per second, so
+      // at most 1024 decisions to vivify all new clauses, so this should be
+      // relatively cheap.
+      return sat_solver->MinimizeByPropagation(
+          /*dtime=*/0.5, /*minimize_new_clauses_only=*/true);
+    }
     return true;
   };
   model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(

ortools/sat/presolve_context.cc

@@ -742,6 +742,19 @@ void PresolveContext::UpdateNewConstraintsVariableUsage() {
   }
 }
 
+bool PresolveContext::HasUnusedAffineVariable() const {
+  for (int var = 0; var < working_model->variables_size(); ++var) {
+    if (VariableIsNotUsedAnymore(var)) continue;
+    const auto& constraints = VarToConstraints(var);
+    if (constraints.size() == 1 &&
+        constraints.contains(kAffineRelationConstraint) &&
+        GetAffineRelation(var).representative != var) {
+      return true;
+    }
+  }
+  return false;
+}
+
 // TODO(user): Also test var_to_constraints_ !!
 bool PresolveContext::ConstraintVariableUsageIsConsistent() {
   if (is_unsat_) return true;  // We do not care in this case.
@@ -893,6 +906,28 @@ void PresolveContext::RemoveAllVariablesFromAffineRelationConstraint() {
   }
 }
 
+void PresolveContext::RemoveNonRepresentativeAffineVariableIfUnused(int var) {
+  if (!VariableIsUnique(var)) {
+    return;
+  }
+  const AffineRelation::Relation r = GetAffineRelation(var);
+  if (var == r.representative) {
+    return;
+  }
+  DCHECK(VarToConstraints(var).contains(kAffineRelationConstraint));
+  DCHECK(!VariableIsNotUsedAnymore(r.representative));
+  // Add relation with current representative to the mapping model.
+  ConstraintProto* ct = NewMappingConstraint(__FILE__, __LINE__);
+  auto* arg = ct->mutable_linear();
+  arg->add_vars(var);
+  arg->add_coeffs(1);
+  arg->add_vars(r.representative);
+  arg->add_coeffs(-r.coeff);
+  arg->add_domain(r.offset);
+  arg->add_domain(r.offset);
+  RemoveVariableFromAffineRelation(var);
+}
+
 // We only call that for a non representative variable that is only used in
 // the kAffineRelationConstraint. Such variable can be ignored and should never
 // be seen again in the presolve.

ortools/sat/presolve_context.h

@@ -298,6 +298,11 @@ class PresolveContext {
   // This is meant to be used in DEBUG mode only.
   bool ConstraintVariableUsageIsConsistent();
 
+  // Loop over all variable and return true if one of them is only used in
+  // affine relation and is not a representative. This is in O(num_vars) and
+  // only meant to be used in DCHECKs.
+  bool HasUnusedAffineVariable() const;
+
   // A "canonical domain" always have a MinOf() equal to zero.
   // If needed we introduce a new variable with such canonical domain and
   // add the relation X = Y + offset.
@@ -502,6 +507,11 @@ class PresolveContext {
     return objective_domain_is_constraining_;
   }
 
+  // If var is an unused variable in an affine relation and is not a
+  // representative, we can remove it from the model. Note that this requires
+  // the variable usage graph to be up to date.
+  void RemoveNonRepresentativeAffineVariableIfUnused(int var);
+
   // Advanced usage. This should be called when a variable can be removed from
   // the problem, so we don't count it as part of an affine relation anymore.
   void RemoveVariableFromAffineRelation(int var);

ortools/sat/sat_parameters.proto

@@ -685,6 +685,10 @@ message SatParameters {
   // Implicitly disabled if share_binary_clauses is false.
   optional bool share_glue_clauses = 285 [default = false];
 
+  // Minimize and detect subsumption of shared clauses immediately after they
+  // are imported.
+  optional bool minimize_shared_clauses = 300 [default = true];
+
   // ==========================================================================
   // Debugging parameters
   // ==========================================================================

ortools/sat/sat_solver.cc

@@ -1501,7 +1501,8 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit,
   }
 }
 
-bool SatSolver::MinimizeByPropagation(double dtime) {
+bool SatSolver::MinimizeByPropagation(double dtime,
+                                      bool minimize_new_clauses_only) {
   CHECK(time_limit_ != nullptr);
   AdvanceDeterministicTime(time_limit_);
   const double threshold = time_limit_->GetElapsedDeterministicTime() + dtime;
@@ -1513,16 +1514,20 @@ bool SatSolver::MinimizeByPropagation(double dtime) {
   int num_resets = 0;
   while (!time_limit_->LimitReached() &&
          time_limit_->GetElapsedDeterministicTime() < threshold) {
-    SatClause* to_minimize = clauses_propagator_->NextClauseToMinimize();
+    SatClause* to_minimize = clauses_propagator_->NextNewClauseToMinimize();
+    if (!minimize_new_clauses_only && to_minimize == nullptr) {
+      to_minimize = clauses_propagator_->NextClauseToMinimize();
+    }
+
     if (to_minimize != nullptr) {
       TryToMinimizeClause(to_minimize);
       if (model_is_unsat_) return false;
+    } else if (minimize_new_clauses_only) {
+      break;
     } else {
-      if (to_minimize == nullptr) {
-        ++num_resets;
-        VLOG(1) << "Minimized all clauses, restarting from first one.";
-        clauses_propagator_->ResetToMinimizeIndex();
-      }
+      ++num_resets;
+      VLOG(1) << "Minimized all clauses, restarting from first one.";
+      clauses_propagator_->ResetToMinimizeIndex();
       if (num_resets > 1) break;
     }
 

ortools/sat/sat_solver.h

@@ -472,7 +472,8 @@ class SatSolver {
   // Mainly visible for testing.
   ABSL_MUST_USE_RESULT bool Propagate();
 
-  bool MinimizeByPropagation(double dtime);
+  bool MinimizeByPropagation(double dtime,
+                             bool minimize_new_clauses_only = false);
 
   // Advance the given time limit with all the deterministic time that was
   // elapsed since last call.
@@ -503,6 +504,10 @@ class SatSolver {
   // exposed to allow processing a conflict detected outside normal propagation.
   void ProcessCurrentConflict();
 
+  void EnsureNewClauseIndexInitialized() {
+    clauses_propagator_->EnsureNewClauseIndexInitialized();
+  }
+
  private:
   // All Solve() functions end up calling this one.
   Status SolveInternal(TimeLimit* time_limit, int64_t max_number_of_conflicts);

ortools/sat/subsolver.cc

@@ -136,7 +136,7 @@ void DeterministicLoop(std::vector<std::unique_ptr<SubSolver>>& subsolvers,
   std::vector<int> indices;
   std::vector<double> timing;
   to_run.reserve(batch_size);
-  ThreadPool pool("DeterministicLoop", num_threads);
+  ThreadPool pool(num_threads);
   pool.StartWorkers();
   for (int batch_index = 0;; ++batch_index) {
     VLOG(2) << "Starting deterministic batch of size " << batch_size;
@@ -207,7 +207,7 @@ void NonDeterministicLoop(std::vector<std::unique_ptr<SubSolver>>& subsolvers,
     return num_in_flight < num_threads;
   };
 
-  ThreadPool pool("NonDeterministicLoop", num_threads);
+  ThreadPool pool(num_threads);
   pool.StartWorkers();
 
   // The lambda below are using little space, but there is no reason