[CP-SAT] fix rare crash

Author: lperron

ortools/sat/clause.cc

@@ -244,21 +244,25 @@ bool ClauseManager::Propagate(Trail* trail) {
           }
         }
 
-        reasons_[trail->Index()] = it->clause;
-        if (propagation_level == 0 && lrat_proof_handler_ != nullptr) {
-          const ClauseId clause_id = GetClauseId(it->clause);
-          const int size = it->clause->size();
-          std::vector<ClauseId>& unit_ids = clause_ids_scratchpad_;
-          unit_ids.clear();
-          for (int i = 1; i < size; ++i) {
-            unit_ids.push_back(trail_->GetUnitClauseId(literals[i].Variable()));
+        if (propagation_level == 0) {
+          if (lrat_proof_handler_ != nullptr) {
+            std::vector<ClauseId>& unit_ids = clause_ids_scratchpad_;
+            unit_ids.clear();
+            const int size = it->clause->size();
+            for (int i = 1; i < size; ++i) {
+              unit_ids.push_back(
+                  trail_->GetUnitClauseId(literals[i].Variable()));
+            }
+            unit_ids.push_back(GetClauseId(it->clause));
+            const ClauseId new_clause_id = clause_id_generator_->GetNextId();
+            lrat_proof_handler_->AddInferredClause(
+                new_clause_id, {other_watched_literal}, unit_ids);
+            helper.EnqueueWithUnitReason(other_watched_literal, new_clause_id);
+          } else {
+            trail_->EnqueueWithUnitReason(other_watched_literal);
           }
-          unit_ids.push_back(clause_id);
-          const ClauseId new_clause_id = clause_id_generator_->GetNextId();
-          lrat_proof_handler_->AddInferredClause(
-              new_clause_id, {other_watched_literal}, unit_ids);
-          helper.EnqueueWithUnitReason(other_watched_literal, new_clause_id);
         } else {
+          reasons_[trail->Index()] = it->clause;
           helper.EnqueueAtLevel(other_watched_literal, propagation_level);
         }
         *new_it++ = *it;
@@ -296,6 +300,7 @@ SatClause* ClauseManager::ReasonClauseOrNull(BooleanVariable var) const {
   if (!trail_->Assignment().VariableIsAssigned(var)) return nullptr;
   if (trail_->AssignmentType(var) != propagator_id_) return nullptr;
   SatClause* result = reasons_[trail_->Info(var).trail_index];
+  DCHECK(result != nullptr) << trail_->Info(var).DebugString();
 
   // Tricky: In some corner case, that clause was subsumed, so we don't want
   // to check it nor use it.
@@ -306,6 +311,7 @@ SatClause* ClauseManager::ReasonClauseOrNull(BooleanVariable var) const {
 
 bool ClauseManager::ClauseIsUsedAsReason(SatClause* clause) const {
   DCHECK(clause != nullptr);
+  if (clause->empty()) return false;
   return clause == ReasonClauseOrNull(clause->PropagatedLiteral().Variable());
 }
 
@@ -642,13 +648,24 @@ void ClauseManager::CleanUpWatchers() {
 void ClauseManager::DeleteRemovedClauses() {
   if (!is_clean_) CleanUpWatchers();
 
+  if (DEBUG_MODE) {
+    // This help debug issues, as it is easier to check for nullptr rather than
+    // detect a pointer that has been deleted.
+    for (int i = 0; i < reasons_.size(); ++i) {
+      if (reasons_[i] != nullptr && reasons_[i]->empty()) {
+        reasons_[i] = nullptr;
+      }
+    }
+  }
+
   int new_size = 0;
   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()) {
+      DCHECK(!clauses_info_.contains(clauses_[i]));
       delete clauses_[i];
     } else {
       clauses_[new_size++] = clauses_[i];

ortools/sat/clause.h

@@ -313,6 +313,7 @@ class ClauseManager : public SatPropagator {
   // 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();
 

ortools/sat/linear_constraint.cc

@@ -296,17 +296,6 @@ void DivideByGCD(LinearConstraint* constraint) {
   }
 }
 
-void MakeAllCoefficientsPositive(LinearConstraint* constraint) {
-  const int size = constraint->num_terms;
-  for (int i = 0; i < size; ++i) {
-    const IntegerValue coeff = constraint->coeffs[i];
-    if (coeff < 0) {
-      constraint->coeffs[i] = -coeff;
-      constraint->vars[i] = NegationOf(constraint->vars[i]);
-    }
-  }
-}
-
 void MakeAllVariablesPositive(LinearConstraint* constraint) {
   const int size = constraint->num_terms;
   for (int i = 0; i < size; ++i) {

ortools/sat/linear_constraint.h

@@ -350,9 +350,6 @@ double ScalarProduct(const LinearConstraint& constraint1,
 // also tighten the constraint bounds assuming all the variables are integer.
 void DivideByGCD(LinearConstraint* constraint);
 
-// Makes all coefficients positive by transforming a variable to its negation.
-void MakeAllCoefficientsPositive(LinearConstraint* constraint);
-
 // Makes all variables "positive" by transforming a variable to its negation.
 void MakeAllVariablesPositive(LinearConstraint* constraint);
 

ortools/sat/linear_constraint_test.cc

@@ -181,14 +181,6 @@ TEST(LinearConstraintCopyTest, BasicBehavior) {
   EXPECT_EQ(ct, other);
 }
 
-TEST(MakeAllCoefficientsPositiveTest, BasicBehavior) {
-  // Note that this relies on the fact that the negation of an IntegerVariable
-  // var is is the one with IntegerVariable(var.value() ^ 1);
-  LinearConstraint ct = CreateUbConstraintForTest({-2, 0, -7, 0}, 10);
-  MakeAllCoefficientsPositive(&ct);
-  EXPECT_EQ(ct, CreateUbConstraintForTest({0, 2, 0, 7}, 10));
-}
-
 TEST(LinearConstraintBuilderTest, DuplicateCoefficient) {
   Model model;
   model.GetOrCreate<IntegerEncoder>();

ortools/sat/linear_programming_constraint.cc

@@ -218,8 +218,8 @@ LinearConstraint ScatteredIntegerVector::ConvertToLinearConstraint(
   result.ub = upper_bound;
 
   if (extra_term != std::nullopt) {
-    result.vars[new_size] += extra_term->first;
-    result.coeffs[new_size] += extra_term->second;
+    result.vars[new_size] = extra_term->first;
+    result.coeffs[new_size] = extra_term->second;
     ++new_size;
   }
 

ortools/sat/sat_inprocessing.cc

@@ -1487,10 +1487,9 @@ bool BoundedVariableElimination::DoOneRound(bool log_info) {
   DCHECK(
       std::all_of(marked_.begin(), marked_.end(), [](bool b) { return !b; }));
 
-  // TODO(user): add a local dtime limit for the corner case where this take too
-  // much time. We can adapt the limit depending on how much we want to spend on
+  // TODO(user): adapt the dtime limit depending on how much we want to spend on
   // inprocessing.
-  while (!time_limit_->LimitReached() && !queue_.IsEmpty()) {
+  while (!time_limit_->LimitReached() && !queue_.IsEmpty() && dtime_ < 10.0) {
     const BooleanVariable top = queue_.Top().var;
     queue_.Pop();
 
@@ -1538,7 +1537,6 @@ bool BoundedVariableElimination::DoOneRound(bool log_info) {
   literal_to_clauses_.clear();
   literal_to_num_clauses_.clear();
 
-  dtime_ += 1e-8 * num_inspected_literals_;
   time_limit_->AdvanceDeterministicTime(dtime_);
   log_info |= VLOG_IS_ON(2);
   LOG_IF(INFO, log_info) << "BVE."
@@ -1885,10 +1883,12 @@ bool BoundedVariableElimination::CrossProduct(BooleanVariable var) {
   for (const ClauseIndex i : literal_to_clauses_[lit]) {
     const auto c = clauses_[i]->AsSpan();
     if (!c.empty()) score += clause_weight + c.size();
+    dtime_ += 1e-8 * c.size();
   }
   for (const ClauseIndex i : literal_to_clauses_[not_lit]) {
     const auto c = clauses_[i]->AsSpan();
     if (!c.empty()) score += clause_weight + c.size();
+    dtime_ += 1.0e-8 * c.size();
   }
 
   // Compute the new score after BVE.

ortools/sat/sat_solver.cc

@@ -3030,6 +3030,7 @@ void SatSolver::CleanClauseDatabaseIfNeeded() {
   std::vector<Entry> entries;
   auto& clauses_info = *(clauses_propagator_->mutable_clauses_info());
   for (auto& entry : clauses_info) {
+    DCHECK(!entry.first->empty());  // Should have been deleted !
     entry.second.num_cleanup_rounds_since_last_bumped++;
     if (clauses_propagator_->ClauseIsUsedAsReason(entry.first)) continue;