[CP-SAT] fix vivification bug; more work on encodings

Author: lperron

ortools/sat/BUILD.bazel

@@ -335,7 +335,9 @@ cc_library(
         "//ortools/util:time_limit",
         "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/base:core_headers",
+        "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:btree",
+        "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/types:span",
     ],
@@ -393,8 +395,32 @@ cc_library(
     deps = [
         ":cp_model_utils",
         ":presolve_context",
+        "//ortools/base:stl_util",
+        "//ortools/util:bitset",
         "//ortools/util:sorted_interval_list",
+        "@abseil-cpp//absl/algorithm:container",
+        "@abseil-cpp//absl/container:flat_hash_map",
+        "@abseil-cpp//absl/container:flat_hash_set",
+        "@abseil-cpp//absl/container:inlined_vector",
         "@abseil-cpp//absl/log",
+        "@abseil-cpp//absl/log:check",
+        "@protobuf",
+    ],
+)
+
+cc_test(
+    name = "presolve_encoding_test",
+    srcs = ["presolve_encoding_test.cc"],
+    deps = [
+        ":cp_model_cc_proto",
+        ":model",
+        ":presolve_context",
+        ":presolve_encoding",
+        "//ortools/base:gmock_main",
+        "//ortools/base:parse_test_proto",
+        "//ortools/util:sorted_interval_list",
+        "@abseil-cpp//absl/container:flat_hash_map",
+        "@abseil-cpp//absl/log:check",
     ],
 )
 
@@ -975,8 +1001,10 @@ cc_library(
         "//ortools/util:sigint",
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
+        "//ortools/util:testing_utils",
         "//ortools/util:time_limit",
         "@abseil-cpp//absl/base:core_headers",
+        "@abseil-cpp//absl/base:log_severity",
         "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",

ortools/sat/clause.cc

@@ -529,7 +529,8 @@ bool ClauseManager::InprocessingRewriteClause(
   }
   const bool is_reason = ClauseIsUsedAsReason(clause);
 
-  CHECK(!is_reason || new_clause[0] == clause->PropagatedLiteral());
+  CHECK(!is_reason || new_clause[0] == clause->PropagatedLiteral())
+      << new_clause << " old " << clause->AsSpan();
 
   if (new_clause.empty()) return false;  // UNSAT.
 
@@ -682,12 +683,24 @@ SatClause* ClauseManager::NextNewClauseToMinimize() {
 }
 
 SatClause* ClauseManager::NextClauseToMinimize() {
+  const int old = to_first_minimize_index_;
   for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) {
     if (clauses_[to_minimize_index_]->IsRemoved()) continue;
     if (!IsRemovable(clauses_[to_minimize_index_])) {
       return clauses_[to_minimize_index_++];
     }
   }
+
+  // Lets reset and try once more to find one.
+  to_minimize_index_ = 0;
+  ++num_to_minimize_index_resets_;
+  for (; to_minimize_index_ < old; ++to_minimize_index_) {
+    if (clauses_[to_minimize_index_]->IsRemoved()) continue;
+    if (!IsRemovable(clauses_[to_minimize_index_])) {
+      return clauses_[to_minimize_index_++];
+    }
+  }
+
   return nullptr;
 }
 

ortools/sat/clause.h

@@ -308,6 +308,7 @@ class ClauseManager : public SatPropagator {
   // Returns the next clause to minimize that has never been minimized before.
   // Note that we only minimize clauses kept forever.
   SatClause* NextNewClauseToMinimize();
+
   // Returns the next clause to minimize, this iterator will be reset to the
   // start so the clauses will be returned in round-robin order.
   // Note that we only minimize clauses kept forever.
@@ -324,7 +325,10 @@ class ClauseManager : public SatPropagator {
 
   // Restart the scans.
   void ResetToProbeIndex() { to_probe_index_ = 0; }
-  void ResetToMinimizeIndex() { to_minimize_index_ = 0; }
+  int64_t NumToMinimizeIndexResets() const {
+    return num_to_minimize_index_resets_;
+  }
+
   // Ensures that NextNewClauseToMinimize() returns only learned clauses.
   // This is a noop after the first call.
   void EnsureNewClauseIndexInitialized() {
@@ -499,6 +503,8 @@ class ClauseManager : public SatPropagator {
 
   // TODO(user): If more indices are needed, switch to a generic API.
   int to_minimize_index_ = 0;
+
+  int num_to_minimize_index_resets_ = 0;
   int to_first_minimize_index_ = 0;
   int to_probe_index_ = 0;