[CP-SAT] fix fuzzer bugs; add presolve/merging of boolean constraints to help reduction/linear relation

ortools/sat/BUILD.bazel

@@ -336,6 +336,8 @@ cc_library(
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
         "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/random",
+        "@com_google_absl//absl/random:bit_gen_ref",
     ],
 )
 

ortools/sat/cp_model_presolve.cc

@@ -6146,13 +6146,12 @@ void CpModelPresolver::PresolvePureSatPart() {
     }
 
     if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
-      // We currently preserve these "complex" bool_and since their linear
-      // relaxation can be stronger than the part.
-      //
-      // TODO(user): Find a way to presolve that here but recover them later
-      // from their clause representation?
-      if (ct.enforcement_literal().size() > 1 &&
-          ct.bool_and().literals().size() > 1) {
+      // We currently do not expand "complex" bool_and that would result
+      // in too many literals.
+      const int left_size = ct.enforcement_literal().size();
+      const int right_size = ct.bool_and().literals().size();
+      if (left_size > 1 && right_size > 1 &&
+          (left_size + 1) * right_size > 1000) {
         continue;
       }
 
@@ -9503,6 +9502,106 @@ void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(
   }
 }
 
+// TODO(user): Use better heuristic where we look at at most one.
+void CpModelPresolver::MergeClauses() {
+  if (context_->ModelIsUnsat()) return;
+  ClauseWithOneMissingHasher hasher(*context_->random());
+
+  WallTimer wall_timer;
+  wall_timer.Start();
+  int64_t work_done = 0;
+  const int64_t work_limit = 1e8;
+
+  std::vector<int> to_clean;
+
+  int64_t num_collisions = 0;
+  int64_t num_merges = 0;
+  int64_t num_saved_literals = 0;
+
+  absl::flat_hash_map<uint64_t, std::pair<int, int>> detector_map;
+  const int num_constraints = context_->working_model->constraints_size();
+  for (int c = 0; c < num_constraints; ++c) {
+    ConstraintProto* ct = context_->working_model->mutable_constraints(c);
+    if (ct->constraint_case() != ConstraintProto::kBoolOr) continue;
+
+    // Both of these test shouldn't happen, but we have them to be safe.
+    if (!ct->enforcement_literal().empty()) continue;
+    if (ct->bool_or().literals().size() <= 2) continue;
+
+    std::sort(ct->mutable_bool_or()->mutable_literals()->begin(),
+              ct->mutable_bool_or()->mutable_literals()->end());
+    hasher.RegisterClause(c, ct->bool_or().literals());
+
+    bool merged = false;
+    work_done += ct->bool_or().literals().size();
+    if (work_done > work_limit) break;
+    for (const int ref : ct->bool_or().literals()) {
+      const uint64_t hash = hasher.HashWithout(c, ref);
+      const auto it = detector_map.find(hash);
+      if (it != detector_map.end()) {
+        ++num_collisions;
+        const int base_c = it->second.first;
+        auto* and_ct = context_->working_model->mutable_constraints(base_c);
+        if (ClauseIsEnforcementImpliesLiteral(
+                ct->bool_or().literals(), and_ct->enforcement_literal(), ref)) {
+          ++num_merges;
+          num_saved_literals += ct->bool_or().literals().size() - 1;
+          merged = true;
+          and_ct->mutable_bool_and()->add_literals(ref);
+          ct->Clear();
+          context_->UpdateConstraintVariableUsage(c);
+          break;
+        }
+      }
+    }
+
+    if (!merged) {
+      // Stupid heuristic: take first literal.
+      const int ref = ct->bool_or().literals(0);
+      const uint64_t hash = hasher.HashWithout(c, ref);
+      const auto [_, inserted] = detector_map.insert({hash, {c, ref}});
+      if (inserted) {
+        to_clean.push_back(c);
+        context_->tmp_literals.clear();
+        for (const int lit : ct->bool_or().literals()) {
+          if (lit == ref) continue;
+          context_->tmp_literals.push_back(NegatedRef(lit));
+        }
+        ct->Clear();
+        ct->mutable_enforcement_literal()->Assign(
+            context_->tmp_literals.begin(), context_->tmp_literals.end());
+        ct->mutable_bool_and()->add_literals(ref);
+      }
+    }
+  }
+
+  // Retransform to bool_or bool_and with a single rhs.
+  for (const int c : to_clean) {
+    ConstraintProto* ct = context_->working_model->mutable_constraints(c);
+    if (ct->bool_and().literals().size() > 1) {
+      context_->UpdateConstraintVariableUsage(c);
+      continue;
+    }
+
+    // We have a single bool_and, lets transform it back to single bool_or.
+    context_->tmp_literals.clear();
+    context_->tmp_literals.push_back(ct->bool_and().literals(0));
+    for (const int ref : ct->enforcement_literal()) {
+      context_->tmp_literals.push_back(NegatedRef(ref));
+    }
+    ct->Clear();
+    ct->mutable_bool_or()->mutable_literals()->Assign(
+        context_->tmp_literals.begin(), context_->tmp_literals.end());
+  }
+
+  if (num_merges > 0) {
+    SOLVER_LOG(logger_, "[MergeClauses]", " #num_collisions=", num_collisions,
+               " #num_merges=", num_merges,
+               " #num_saved_literals=", num_saved_literals, " work=", work_done,
+               "/", work_limit, " time=", wall_timer.Get(), "s");
+  }
+}
+
 // =============================================================================
 // Public API.
 // =============================================================================
@@ -9710,6 +9809,13 @@ CpSolverStatus CpModelPresolver::Presolve() {
     ProcessSetPPC();
     if (context_->ModelIsUnsat()) return InfeasibleStatus();
 
+    // We do that after the duplicate, SAT and SetPPC constraints.
+    if (!context_->time_limit()->LimitReached()) {
+      // Merge clauses that differ in just one literal.
+      // Heuristic use at_most_one to try to tighten the initial LP Relaxation.
+      MergeClauses();
+    }
+
     // TODO(user): Decide where is the best place for this. Fow now we do it
     // after max clique to get all the bool_and converted to at most ones.
     if (context_->params().symmetry_level() > 0 && !context_->ModelIsUnsat() &&

ortools/sat/cp_model_presolve.h

@@ -253,6 +253,19 @@ class CpModelPresolver {
 
   void MergeNoOverlapConstraints();
 
+  // Heuristic to merge clauses that differ in only one literal.
+  // The idea is to regroup a bunch of clauses into a single bool_and.
+  // This serves a bunch of purpose:
+  // - Smaller model.
+  // - Stronger dual reasoning since less locks.
+  // - If the negation of the rhs of the bool_and are in at most one, we will
+  //   have a stronger LP relaxation.
+  //
+  // TODO(user): If the merge procedure is successful we might want to develop
+  // a custom propagators for such bool_and. It should in theory be more
+  // efficient than the two watcher literal scheme for clauses. Investigate!
+  void MergeClauses();
+
   // Boths function are responsible for dealing with affine relations.
   // The second one returns false on UNSAT.
   void EncodeAllAffineRelations();

ortools/sat/cuts.cc

@@ -658,7 +658,8 @@ void IntegerRoundingCutHelper::ComputeCut(
     best_cut_.max_magnitude =
         std::max(best_cut_.max_magnitude, IntTypeAbs(new_coeff));
   }
-  best_cut_.max_magnitude = std::max(best_cut_.max_magnitude, best_cut_.rhs);
+  best_cut_.max_magnitude =
+      std::max(best_cut_.max_magnitude, IntTypeAbs(best_cut_.rhs));
 
   // Create the base super-additive function f().
   const IntegerValue rhs_remainder =

ortools/sat/lp_utils.cc

@@ -270,7 +270,9 @@ void RemoveNearZeroTerms(const SatParameters& params, MPModelProto* mp_model,
       const int var = ct->var_index(i);
       const double coeff = ct->coefficient(i);
       if (std::abs(coeff) * max_bounds[var] < threshold) {
-        largest_removed = std::max(largest_removed, std::abs(coeff));
+        if (max_bounds[var] != 0) {
+          largest_removed = std::max(largest_removed, std::abs(coeff));
+        }
         continue;
       }
       ct->set_var_index(new_size, var);
@@ -282,6 +284,23 @@ void RemoveNearZeroTerms(const SatParameters& params, MPModelProto* mp_model,
     ct->mutable_coefficient()->Truncate(new_size);
   }
 
+  // We also do the same for the objective coefficient.
+  if (num_variables > 0) {
+    const double threshold =
+        params.mip_wanted_precision() / static_cast<double>(num_variables);
+    for (int var = 0; var < num_variables; ++var) {
+      const double coeff = mp_model->variable(var).objective_coefficient();
+      if (coeff == 0.0) continue;
+      if (std::abs(coeff) * max_bounds[var] < threshold) {
+        ++num_removed;
+        if (max_bounds[var] != 0) {
+          largest_removed = std::max(largest_removed, std::abs(coeff));
+        }
+        mp_model->mutable_variable(var)->clear_objective_coefficient();
+      }
+    }
+  }
+
   if (num_removed > 0) {
     // Note that when a variable is fixed to zero, the code here remove all its
     // coefficients, so the largest magnitude can be quite large.

ortools/sat/presolve_util.cc

@@ -564,5 +564,21 @@ bool ActivityBoundHelper::PresolveEnforcement(
   return true;
 }
 
+void ClauseWithOneMissingHasher::RegisterClause(int c,
+                                                absl::Span<const int> clause) {
+  uint64_t hash = 0;
+  for (const int ref : clause) {
+    const Index index = IndexFromLiteral(ref);
+    while (index >= literal_to_hash_.size()) {
+      // We use random value for a literal hash.
+      literal_to_hash_.push_back(absl::Uniform<uint64_t>(random_));
+    }
+    hash ^= literal_to_hash_[index];
+  }
+
+  if (c >= clause_to_hash_.size()) clause_to_hash_.resize(c + 1, 0);
+  clause_to_hash_[c] = hash;
+}
+
 }  // namespace sat
 }  // namespace operations_research

ortools/sat/presolve_util.h

@@ -21,6 +21,8 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/random/bit_gen_ref.h"
+#include "absl/random/random.h"
 #include "absl/strings/string_view.h"
 #include "absl/types/span.h"
 #include "ortools/base/integral_types.h"
@@ -201,6 +203,54 @@ class ActivityBoundHelper {
   absl::flat_hash_set<int> triggered_amo_;
 };
 
+// Class to help detects clauses that differ on a single literal.
+class ClauseWithOneMissingHasher {
+ public:
+  explicit ClauseWithOneMissingHasher(absl::BitGenRef random)
+      : random_(random) {}
+
+  // We use the proto encoding of literals here.
+  void RegisterClause(int c, absl::Span<const int> clause);
+
+  // Get a hash of the clause with index c and literal ref removed.
+  // This assumes that ref was part of the clause. Work in O(1).
+  uint64_t HashWithout(int c, int ref) const {
+    return clause_to_hash_[c] ^ literal_to_hash_[IndexFromLiteral(ref)];
+  }
+
+ private:
+  DEFINE_STRONG_INDEX_TYPE(Index);
+  Index IndexFromLiteral(int ref) const {
+    return Index(ref >= 0 ? 2 * ref : -2 * ref - 1);
+  }
+
+  absl::BitGenRef random_;
+  absl::StrongVector<Index, uint64_t> literal_to_hash_;
+  std::vector<uint64_t> clause_to_hash_;
+};
+
+// Specific function. Returns true if the negation of all literals in clause
+// except literal is exactly equal to the literal of enforcement.
+//
+// We assumes that enforcement and negated(clause) are sorted lexicographically
+// Or negated(enforcement) and clause. Both option works. If not, we will only
+// return false more often. When we return true, the property is enforced.
+//
+// TODO(user): For the same complexity, we do not need to specify literal and
+// can recover it.
+inline bool ClauseIsEnforcementImpliesLiteral(absl::Span<const int> clause,
+                                              absl::Span<const int> enforcement,
+                                              int literal) {
+  if (clause.size() != enforcement.size() + 1) return false;
+  int j = 0;
+  for (int i = 0; i < clause.size(); ++i) {
+    if (clause[i] == literal) continue;
+    if (clause[i] != NegatedRef(enforcement[j])) return false;
+    ++j;
+  }
+  return true;
+}
+
 }  // namespace sat
 }  // namespace operations_research