[CP-SAT] fix bugs in lrat, inner clause handling, variable expansion

Author: lperron

ortools/sat/clause.cc

@@ -292,6 +292,9 @@ SatClause* ClauseManager::ReasonClause(int trail_index) const {
 SatClause* ClauseManager::ReasonClauseOrNull(BooleanVariable var) const {
   if (!trail_->Assignment().VariableIsAssigned(var)) return nullptr;
   if (trail_->AssignmentType(var) != propagator_id_) return nullptr;
+
+  DCHECK_EQ(trail_->Reason(var),
+            reasons_[trail_->Info(var).trail_index]->PropagationReason());
   return reasons_[trail_->Info(var).trail_index];
 }
 
@@ -546,6 +549,14 @@ bool ClauseManager::InprocessingRewriteClause(
     AttachOnFalse(new_clause[0], new_clause[1], clause);
     AttachOnFalse(new_clause[1], new_clause[0], clause);
   }
+
+  // We need to change the reason now that the clause size changed because
+  // we cache the span into the reason data directly.
+  if (is_reason) {
+    trail_->ChangeReason(trail_->Info(new_clause[0].Variable()).trail_index,
+                         propagator_id_);
+  }
+
   return true;
 }
 

ortools/sat/cp_model_solver_helpers.cc

@@ -1168,6 +1168,10 @@ int RegisterClausesLevelZeroImport(int id,
       }
     }
     clause_manager->SetAddClauseCallback(std::move(callback));
+    if (new_clauses > 0) {
+      shared_clauses_manager->NotifyNumImported(id, new_clauses);
+    }
+
     if (new_clauses > 0 && !sat_solver->FinishPropagation()) return false;
     if (minimize_shared_clauses && new_clauses > 0) {
       // The new clauses may be subsumed, so try to minimize them to reduce

ortools/sat/presolve_context.cc

@@ -2111,6 +2111,12 @@ bool PresolveContext::CanonicalizeObjective(bool simplify_domain) {
            .IntersectionWith(Domain(std::numeric_limits<int64_t>::min(),
                                     objective_domain_.Max()))
            .IsIncludedIn(objective_domain_);
+  if (objective_domain_is_constraining_) {
+    VLOG(3) << "objective domain is constraining: size: "
+            << objective_map_.size()
+            << ", implied: " << implied_domain.ToString()
+            << " objective: " << objective_domain_.ToString();
+  }
   return true;
 }
 
@@ -2247,14 +2253,53 @@ bool PresolveContext::SubstituteVariableInObjective(
 
   RemoveVariableFromObjective(var_in_equality);
 
-  // Because we can assume that the constraint we used was constraining
-  // (otherwise it would have been removed), the objective domain should be now
-  // constraining.
-  objective_domain_is_constraining_ = true;
+  // If the objective is small enough,  recompute the value of
+  // objective_domain_is_constrainting_, otherwise, we just assume it to be
+  // true. This uses the updated objective_map_.
+  if (objective_map_.size() < 256) {
+    Domain implied_domain(0);
 
-  if (objective_domain_.IsEmpty()) {
-    return NotifyThatModelIsUnsat();
+    // We need to sort the entries to be deterministic.
+    tmp_entries_.clear();
+    for (const auto& entry : objective_map_) {
+      tmp_entries_.push_back(entry);
+    }
+    std::sort(tmp_entries_.begin(), tmp_entries_.end());
+    for (const auto& entry : tmp_entries_) {
+      const int var = entry.first;
+      const int64_t coeff = entry.second;
+      implied_domain =
+          implied_domain.AdditionWith(DomainOf(var).MultiplicationBy(coeff))
+              .RelaxIfTooComplex();
+    }
+
+    // This is the new domain.
+    // Note that the domain never include the offset.
+    objective_domain_ = objective_domain_.IntersectionWith(implied_domain)
+                            .SimplifyUsingImpliedDomain(implied_domain);
+
+    if (objective_domain_.IsEmpty()) {
+      return NotifyThatModelIsUnsat("empty objective domain");
+    }
+
+    // Detect if the objective domain do not limit the "optimal" objective
+    // value. If this is true, then we can apply any reduction that reduce the
+    // objective value without any issues.
+    objective_domain_is_constraining_ =
+        !implied_domain
+             .IntersectionWith(Domain(std::numeric_limits<int64_t>::min(),
+                                      objective_domain_.Max()))
+             .IsIncludedIn(objective_domain_);
+    if (objective_domain_is_constraining_) {
+      VLOG(3) << "objective domain is constraining: size: "
+              << objective_map_.size()
+              << ", implied: " << implied_domain.ToString()
+              << " objective: " << objective_domain_.ToString();
+    }
+  } else {
+    objective_domain_is_constraining_ = true;
   }
+
   return true;
 }
 

ortools/sat/presolve_context_test.cc

@@ -506,7 +506,7 @@ TEST(PresolveContextTest, ObjectiveSubstitutionWithLargeCoeff) {
     objective {
       vars: [ 1, 2 ]
       coeffs: [ 2, 2 ]
-      domain: [ 12, 1012 ]  #  [0, 1000] initially, + 2*6 offset.
+      domain: [ 12, 36 ]  #  [0, 1000] initially, + 2*6 offset.
       offset: -9
       integer_before_offset: -12
       scaling_factor: 1

ortools/sat/probing.cc

@@ -654,7 +654,6 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
   }
 
   binary_clause_extracted_.assign(trail_.Index(), false);
-  subsumed_clauses_.clear();
 
   while (!time_limit_->LimitReached() &&
          time_limit_->GetElapsedDeterministicTime() <= limit) {
@@ -738,15 +737,7 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
 
   if (!sat_solver_->ResetToLevelZero()) return false;
   if (!ProcessLiteralsToFix()) return false;
-  if (!subsumed_clauses_.empty()) {
-    for (SatClause* clause : subsumed_clauses_) {
-      if (clause->size() == 0) continue;
-      ++num_subsumed_;
-      clause_manager_->LazyDelete(clause,
-                                  DeletionSourceForStat::SUBSUMPTION_PROBING);
-    }
-    clause_manager_->CleanUpWatchers();
-  }
+  clause_manager_->CleanUpWatchers();
 
   // Display stats.
   const int num_fixed = sat_solver_->LiteralTrail().Index();
@@ -994,7 +985,31 @@ void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
   // of all literals in the reason for this propagation. And use this
   // as a reason for later hyber binary resolution. Like we do when
   // this clause subsumes the reason.
-  AddImplication(last_decision, l);
+  ++num_new_binary_;
+  DCHECK(assignment_.LiteralIsTrue(l));
+  CHECK_NE(l.Variable(), last_decision.Variable());
+
+  // We should never probe a redundant literal.
+  //
+  // TODO(user): We should be able to enforce that l is non-redundant either if
+  // we made sure the clause database is cleaned up before FailedLiteralProbing
+  // is called. This should maybe simplify the ChangeReason() handling.
+  DCHECK(!implication_graph_->IsRedundant(last_decision));
+
+  ClauseId clause_id = kNoClauseId;
+  if (lrat_proof_handler_ != nullptr) {
+    clause_id = clause_id_generator_->GetNextId();
+    tmp_clause_ids_.clear();
+    sat_solver_->AppendClausesFixing({l}, &tmp_clause_ids_, last_decision);
+    lrat_proof_handler_->AddInferredClause(
+        clause_id, {last_decision.Negated(), l}, tmp_clause_ids_);
+  }
+
+  // Each time we extract a binary clause, we change the reason in the trail.
+  // This is important as it will allow us to remove clauses that are now
+  // subsumed by this binary, even if it was a reason.
+  CHECK(implication_graph_->AddBinaryClauseAndChangeReason(
+      clause_id, l, last_decision.Negated()));
 }
 
 // If we can extract a binary clause that subsume the reason clause, we do add
@@ -1006,6 +1021,7 @@ void FailedLiteralProbing::MaybeSubsumeWithBinaryClause(
     const Literal last_decision, const Literal l) {
   const int trail_index = trail_.Info(l.Variable()).trail_index;
   if (trail_.AssignmentType(l.Variable()) != clause_propagator_id_) return;
+  SatClause* clause = clause_manager_->ReasonClause(trail_index);
 
   bool subsumed = false;
   for (const Literal lit : trail_.Reason(l.Variable())) {
@@ -1027,7 +1043,12 @@ void FailedLiteralProbing::MaybeSubsumeWithBinaryClause(
     if (lit == last_decision.Negated()) ++test;
   }
   CHECK_EQ(test, 2);
-  subsumed_clauses_.push_back(clause_manager_->ReasonClause(trail_index));
+
+  // Because of MaybeExtractImplication(), this shouldn't be a reason anymore.
+  CHECK(!clause_manager_->ClauseIsUsedAsReason(clause));
+  ++num_subsumed_;
+  clause_manager_->LazyDelete(clause,
+                              DeletionSourceForStat::SUBSUMPTION_PROBING);
 }
 
 // Inspect the watcher list for last_decision, If we have a blocking
@@ -1043,34 +1064,21 @@ void FailedLiteralProbing::SubsumeWithBinaryClauseUsingBlockingLiteral(
     const Literal last_decision) {
   for (const auto& w :
        clause_manager_->WatcherListOnFalse(last_decision.Negated())) {
-    if (assignment_.LiteralIsTrue(w.blocking_literal)) {
-      if (w.clause->IsRemoved()) continue;
+    if (!assignment_.LiteralIsTrue(w.blocking_literal)) continue;
+    if (w.clause->IsRemoved()) continue;
 
-      // This should be enough for proof correctness.
-      if (clause_manager_->ClauseIsUsedAsReason(w.clause)) {
-        MaybeExtractImplication(last_decision, w.blocking_literal);
-      }
-      subsumed_clauses_.push_back(w.clause);
-    }
-  }
-}
+    // This should be enough for proof correctness.
+    if (clause_manager_->ClauseIsUsedAsReason(w.clause)) {
+      MaybeExtractImplication(last_decision, w.blocking_literal);
 
-void FailedLiteralProbing::AddImplication(const Literal last_decision,
-                                          const Literal l) {
-  ++num_new_binary_;
-  DCHECK(assignment_.LiteralIsTrue(l));
-  CHECK_NE(l.Variable(), last_decision.Variable());
+      // It should have been replaced by a binary clause now.
+      CHECK(!clause_manager_->ClauseIsUsedAsReason(w.clause));
+    }
 
-  ClauseId clause_id = kNoClauseId;
-  if (lrat_proof_handler_ != nullptr) {
-    clause_id = clause_id_generator_->GetNextId();
-    tmp_clause_ids_.clear();
-    sat_solver_->AppendClausesFixing({l}, &tmp_clause_ids_, last_decision);
-    lrat_proof_handler_->AddInferredClause(
-        clause_id, {last_decision.Negated(), l}, tmp_clause_ids_);
+    ++num_subsumed_;
+    clause_manager_->LazyDelete(w.clause,
+                                DeletionSourceForStat::SUBSUMPTION_PROBING);
   }
-  CHECK(implication_graph_->AddBinaryClause(clause_id, last_decision.Negated(),
-                                            l));
 }
 
 // Adds 'not(literal)' to `to_fix_`, assuming that 'literal' directly implies

ortools/sat/probing.h

@@ -325,8 +325,6 @@ class FailedLiteralProbing {
   // which is quite cheap to test here.
   void SubsumeWithBinaryClauseUsingBlockingLiteral(Literal last_decision);
 
-  void AddImplication(Literal last_decision, Literal l);
-
   // Adds 'not(literal)' to `to_fix_`, assuming that 'literal' directly implies
   // the current decision, which itself implies all the previous decisions, with
   // some of them propagating 'not(literal)'.
@@ -366,7 +364,6 @@ class FailedLiteralProbing {
   // For each literal 'l' in the trail, whether a binary clause "d => l" has
   // been extracted, with 'd' the decision at the same level as 'l'.
   std::vector<bool> binary_clause_extracted_;
-  std::vector<SatClause*> subsumed_clauses_;
 
   // Temporary vector used for LRAT proofs.
   std::vector<ClauseId> tmp_clause_ids_;