[CP-SAT] remove problematic DCHECK; tweak glue-clause-sharing

google · Aug 5, 2024 · 39b07a9 · 39b07a9
1 parent 3e1ca33
commit 39b07a9
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 10 deletions.
diff --git a/ortools/sat/cp_model_solver_helpers.cc b/ortools/sat/cp_model_solver_helpers.cc
@@ -905,6 +905,7 @@ int RegisterClausesLevelZeroImport(int id,
         return false;
       }
     }
+    clause_stream->RemoveWorstClauses();
     return true;
   };
   model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(

diff --git a/ortools/sat/feasibility_jump.cc b/ortools/sat/feasibility_jump.cc
@@ -902,7 +902,8 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() {
       // Check that the score for undoing the move is -score with both the
       // default weights (which may be `state_->weights` or
       // `state_->compound_weights`), and with `weights` explicitly.
-      if (!state_->options.use_decay) {
+      // TODO(user): Re-enable DCHECK.
+      if (/* DISABLES CODE */ false && !state_->options.use_decay) {
         DCHECK_EQ(-score, ComputeScore(state_->weights, var,
                                        prev_value - new_value, false));
         DCHECK_EQ(-score, ComputeScore(ScanWeights(), var,

diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
@@ -16,7 +16,6 @@
 #include <algorithm>
 #include <cstddef>
 #include <cstdint>
-#include <functional>
 #include <limits>
 #include <memory>
 #include <string>

diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc
@@ -1281,7 +1281,8 @@ void SharedClausesManager::Synchronize() {
         num_buffered_literals <
         UniqueClauseStream::kMaxLiteralsPerBatch / num_workers;
     const bool overfull =
-        num_buffered_literals > UniqueClauseStream::kMaxLiteralsPerBatch;
+        num_buffered_literals >
+        2 * UniqueClauseStream::kMaxLiteralsPerBatch / num_workers;
     const int new_lbd = std::clamp(lbd_threshold + underfull - overfull, 2,
                                    UniqueClauseStream::kMaxClauseSize);
     if (new_lbd != lbd_threshold) {
@@ -1329,9 +1330,6 @@ void SharedClausesManager::Synchronize() {
     VLOG(2) << "Batch #" << batches_.size() << " w/ " << batches_.back().size()
             << " clauses max size = "
             << batches_.back()[batches_.back().size() - 1].size();
-    for (auto& stream : id_to_clause_stream_) {
-      stream.RemoveWorstClauses();
-    }
   }
   // Delete batches that have been consumed by all workers.
   // Keep a few batches around for startup (min finished batch doesn't count

diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h
@@ -593,8 +593,10 @@ class UniqueClauseStream {
   // Export 4KiB of clauses per batch.
   static constexpr int kMaxLiteralsPerBatch = 4096 / sizeof(int);
   // Bound the total literals we buffer, approximately enforced so shorter
-  // clauses can replace longer ones.
-  static constexpr int kMaxBufferedLiterals = 4 * kMaxLiteralsPerBatch;
+  // clauses can replace longer ones. This can be larger than
+  // kMaxLiteralsPerBatch (hence the separate constant), but experiments suggest
+  // that this doesn't help.
+  static constexpr int kMaxBufferedLiterals = kMaxLiteralsPerBatch;
 
   UniqueClauseStream();
   // Move only - this is an expensive class to copy.
@@ -637,8 +639,8 @@ class UniqueClauseStream {
 
   // Delete longest clauses while keeping at least kMaxBufferedLiterals.
   // This guarantees that CanAccept will return the same result as before, and
-  // at least the next 4 batches will contain the same clauses, but we will emit
-  // fewer old, long clauses many batches in the future.
+  // at least the next batch will contain the same clauses, but we will emit
+  // fewer old, long clauses in the future.
   void RemoveWorstClauses();
 
   int lbd_threshold() const ABSL_LOCKS_EXCLUDED(mutex_) {