[CP-SAT] more work on encodings, lrat

Author: lperron

ortools/sat/BUILD.bazel

@@ -1209,6 +1209,7 @@ cc_library(
         "//ortools/util:saturated_arithmetic",
         "//ortools/util:sorted_interval_list",
         "@abseil-cpp//absl/algorithm:container",
+        "@abseil-cpp//absl/base:log_severity",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/log",
@@ -1559,6 +1560,7 @@ cc_library(
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
+        "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:inlined_vector",

ortools/sat/clause.h

@@ -262,6 +262,11 @@ class ClauseManager : public SatPropagator {
   absl::flat_hash_map<SatClause*, ClauseInfo>* mutable_clauses_info() {
     return &clauses_info_;
   }
+  int LbdOrZeroIfNotRemovable(SatClause* const clause) const {
+    auto it = clauses_info_.find(clause);
+    if (it == clauses_info_.end()) return 0;
+    return it->second.lbd;
+  }
 
   // Total number of clauses inspected during calls to Propagate().
   int64_t num_inspected_clauses() const { return num_inspected_clauses_; }

ortools/sat/cp_model_postsolve.cc

@@ -97,7 +97,7 @@ void PostsolveExactlyOne(const ConstraintProto& ct,
 // There must be one.
 void SetEnforcementLiteralToFalse(const ConstraintProto& ct,
                                   std::vector<Domain>* domains) {
-  CHECK(!ct.enforcement_literal().empty());
+  CHECK(!ct.enforcement_literal().empty()) << ProtobufShortDebugString(ct);
   bool has_free_enforcement_literal = false;
   for (const int enf : ct.enforcement_literal()) {
     if ((*domains)[PositiveRef(enf)].IsFixed()) continue;

ortools/sat/cp_model_presolve.cc

@@ -4504,6 +4504,7 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
     // actual changes.
     if (is_in_objective &&
         !context_->SubstituteVariableInObjective(var, var_coeff, *ct)) {
+      if (context_->ModelIsUnsat()) return false;
       continue;
     }
 
@@ -13170,13 +13171,12 @@ void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(int var) {
     return;
   }
 
-  int new_exo_to_presolve_index = -1;
-  TryToReplaceVariableByItsEncoding(var, new_exo_to_presolve_index, context_,
-                                    solution_crush_);
-  if (new_exo_to_presolve_index != -1) {
-    if (PresolveExactlyOne(context_->working_model->mutable_constraints(
-            new_exo_to_presolve_index))) {
-      context_->UpdateConstraintVariableUsage(new_exo_to_presolve_index);
+  // Presolve newly created constraints.
+  const int old_size = context_->working_model->constraints_size();
+  TryToReplaceVariableByItsEncoding(var, context_, solution_crush_);
+  for (int c = old_size; c < context_->working_model->constraints_size(); ++c) {
+    if (PresolveOneConstraint(c)) {
+      context_->UpdateConstraintVariableUsage(c);
     }
   }
 }

ortools/sat/cp_model_presolve_test.cc

@@ -8158,6 +8158,7 @@ TEST(PresolveCpModelTest, SolveDiophantine) {
   // Should solve in < .01 second. Note that deterministic time is not
   // completely accurate.
   params.set_max_deterministic_time(.001);
+  params.set_num_workers(1);
   const CpSolverResponse response_with =
       SolveWithParameters(model_proto, params);
 

ortools/sat/integer_search.cc

@@ -1366,9 +1366,9 @@ bool IntegerSearchHelper::BeforeTakingDecision() {
   DCHECK(sat_solver_->PropagationIsDone());
 
   // If we pushed root level deductions, we go back to level zero and call
-  // Propagate() to incorporate them. Note that the propagation is not strcily
+  // Propagate() to incorporate them. Note that the propagation is not strictly
   // needed, but it is nicer to be at fixed point when we call the level zero
-  // callabacks.
+  // callbacks.
   if (integer_trail_->HasPendingRootLevelDeduction()) {
     sat_solver_->Backtrack(0);
     if (!sat_solver_->Propagate()) {
@@ -1843,7 +1843,8 @@ SatSolver::Status ContinuousProber::Probe() {
           tmp_dnf_.push_back({literal});
         }
         ++num_at_least_one_probed_;
-        if (!prober_->ProbeDnf("at_least_one", tmp_dnf_)) {
+        if (!prober_->ProbeDnf("at_least_one", tmp_dnf_,
+                               Prober::DnfType::kAtLeastOne, clause)) {
           return SatSolver::INFEASIBLE;
         }
 
@@ -1866,7 +1867,8 @@ SatSolver::Status ContinuousProber::Probe() {
         }
         tmp_dnf_.push_back(tmp_literals_);
         ++num_at_most_one_probed_;
-        if (!prober_->ProbeDnf("at_most_one", tmp_dnf_)) {
+        if (!prober_->ProbeDnf("at_most_one", tmp_dnf_,
+                               Prober::DnfType::kAtLeastOneOrZero)) {
           return SatSolver::INFEASIBLE;
         }
 
@@ -1887,12 +1889,12 @@ SatSolver::Status ContinuousProber::Probe() {
           for (; current_bv2_ < bool_vars_.size(); ++current_bv2_) {
             const BooleanVariable& bv2 = bool_vars_[current_bv2_];
             if (assignment.VariableIsAssigned(bv2)) continue;
-            if (!prober_->ProbeDnf(
-                    "pair_of_bool_vars",
-                    {{Literal(bv1, true), Literal(bv2, true)},
-                     {Literal(bv1, true), Literal(bv2, false)},
-                     {Literal(bv1, false), Literal(bv2, true)},
-                     {Literal(bv1, false), Literal(bv2, false)}})) {
+            if (!prober_->ProbeDnf("pair_of_bool_vars",
+                                   {{Literal(bv1, false), Literal(bv2, false)},
+                                    {Literal(bv1, false), Literal(bv2, true)},
+                                    {Literal(bv1, true), Literal(bv2, false)},
+                                    {Literal(bv1, true), Literal(bv2, true)}},
+                                   Prober::DnfType::kAtLeastOneCombination)) {
               return SatSolver::INFEASIBLE;
             }
             RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
@@ -1910,12 +1912,12 @@ SatSolver::Status ContinuousProber::Probe() {
           if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
             continue;
           }
-          if (!prober_->ProbeDnf(
-                  "rnd_pair_of_bool_vars",
-                  {{Literal(bv1, true), Literal(bv2, true)},
-                   {Literal(bv1, true), Literal(bv2, false)},
-                   {Literal(bv1, false), Literal(bv2, true)},
-                   {Literal(bv1, false), Literal(bv2, false)}})) {
+          if (!prober_->ProbeDnf("rnd_pair_of_bool_vars",
+                                 {{Literal(bv1, false), Literal(bv2, false)},
+                                  {Literal(bv1, false), Literal(bv2, true)},
+                                  {Literal(bv1, true), Literal(bv2, false)},
+                                  {Literal(bv1, true), Literal(bv2, true)}},
+                                 Prober::DnfType::kAtLeastOneCombination)) {
             return SatSolver::INFEASIBLE;
           }
 
@@ -1948,12 +1950,13 @@ SatSolver::Status ContinuousProber::Probe() {
         }
         tmp_dnf_.clear();
         for (int i = 0; i < 8; ++i) {
-          tmp_dnf_.push_back({Literal(bv1, (i & 1) > 0),
+          tmp_dnf_.push_back({Literal(bv1, (i & 4) > 0),
                               Literal(bv2, (i & 2) > 0),
-                              Literal(bv3, (i & 4) > 0)});
+                              Literal(bv3, (i & 1) > 0)});
         }
 
-        if (!prober_->ProbeDnf("rnd_triplet_of_bool_vars", tmp_dnf_)) {
+        if (!prober_->ProbeDnf("rnd_triplet_of_bool_vars", tmp_dnf_,
+                               Prober::DnfType::kAtLeastOneCombination)) {
           return SatSolver::INFEASIBLE;
         }
 

ortools/sat/lrat_proof_handler.cc

@@ -146,8 +146,32 @@ bool LratProofHandler::AddAssumedClause(ClauseId id,
   return true;
 }
 
+void LratProofHandler::PinClause(ClauseId id,
+                                 absl::Span<const Literal> clause) {
+  DCHECK_NE(id, kNoClauseId);
+  DCHECK_EQ(pinned_clause_id_, kNoClauseId);
+  pinned_clause_id_ = id;
+  if (drat_checker_ != nullptr || drat_writer_ != nullptr) {
+    pinned_clause_.assign(clause.begin(), clause.end());
+  }
+  delete_pinned_clause_ = false;
+}
+
+void LratProofHandler::UnpinClause(ClauseId id) {
+  DCHECK_NE(id, kNoClauseId);
+  DCHECK_EQ(pinned_clause_id_, id);
+  pinned_clause_id_ = kNoClauseId;
+  if (delete_pinned_clause_) {
+    DeleteClause(id, pinned_clause_);
+  }
+}
+
 void LratProofHandler::DeleteClause(ClauseId id,
                                     absl::Span<const Literal> clause) {
+  if (pinned_clause_id_ == id) {
+    delete_pinned_clause_ = true;
+    return;
+  }
   VLOG(1) << "DeleteClause: id=" << id
           << " literals=" << absl::StrJoin(clause, ",");
   if (drat_checker_ != nullptr) {

ortools/sat/lrat_proof_handler.h

@@ -63,6 +63,14 @@ class LratProofHandler {
   // checks are enabled and the ID is already used by another clause).
   bool AddAssumedClause(ClauseId id, absl::Span<const Literal> clause);
 
+  // Prevents the given clause from being deleted, until UnpinClause() is called
+  // with the same ID. At most one clause can be pinned at any time.
+  void PinClause(ClauseId id, absl::Span<const Literal> clause);
+
+  // Unpins the clause with the given ID, and deletes it if a call to
+  // DeleteClause() for this clause was made since it was pinned.
+  void UnpinClause(ClauseId id);
+
   // Deletes a problem or inferred clause. The clause literals are only needed
   // when checking DRAT.
   void DeleteClause(ClauseId id, absl::Span<const Literal> clause);
@@ -92,7 +100,11 @@ class LratProofHandler {
 
   bool all_problem_clauses_loaded_ = false;
   int64_t num_assumed_clauses_ = 0;
-  bool debug_crash_on_error_;
+  bool debug_crash_on_error_ = false;
+
+  ClauseId pinned_clause_id_ = kNoClauseId;
+  std::vector<Literal> pinned_clause_;
+  bool delete_pinned_clause_ = false;
 
   // Only used when checking DRAT, because the DRAT checker does not support
   // interleaving problem and inferred clauses.