[CP-SAT] tune the code; improve lrat; work on encodings

Author: lperron

ortools/sat/BUILD.bazel

@@ -177,13 +177,14 @@ cc_library(
         ":presolve_context",
         ":sat_base",
         ":sat_parameters_cc_proto",
-        "//ortools/base:logging",
         "//ortools/base:protobuf_util",
         "//ortools/util:sorted_interval_list",
+        "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
+        "@abseil-cpp//absl/memory",
         "@abseil-cpp//absl/strings",
         "@abseil-cpp//absl/types:span",
         "@protobuf",
@@ -394,6 +395,7 @@ cc_library(
     hdrs = ["presolve_encoding.h"],
     deps = [
         ":cp_model_utils",
+        ":integer_base",
         ":presolve_context",
         "//ortools/base:stl_util",
         "//ortools/util:bitset",
@@ -404,6 +406,7 @@ cc_library(
         "@abseil-cpp//absl/container:inlined_vector",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
+        "@abseil-cpp//absl/strings",
         "@protobuf",
     ],
 )
@@ -1225,6 +1228,7 @@ cc_library(
         "//ortools/util:sorted_interval_list",
         "//ortools/util:time_limit",
         "@abseil-cpp//absl/base:core_headers",
+        "@abseil-cpp//absl/base:log_severity",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
@@ -1375,7 +1379,6 @@ cc_library(
         ":util",
         ":var_domination",
         ":variable_expand",
-        "//ortools/base",
         "//ortools/base:mathutil",
         "//ortools/base:protobuf_util",
         "//ortools/base:stl_util",
@@ -1396,7 +1399,6 @@ cc_library(
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
-        "@abseil-cpp//absl/container:inlined_vector",
         "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/hash",
         "@abseil-cpp//absl/log",
@@ -1685,7 +1687,6 @@ cc_library(
         "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_set",
-        "@abseil-cpp//absl/container:inlined_vector",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/log:vlog_is_on",
@@ -2455,6 +2456,7 @@ cc_test(
         "//ortools/base:logging",
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
+        "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/types:span",
         "@google_benchmark//:benchmark",
@@ -2599,6 +2601,7 @@ cc_library(
         "//ortools/util:bitset",
         "//ortools/util:sort",
         "//ortools/util:strong_integers",
+        "//ortools/util:time_limit",
         "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
@@ -2917,6 +2920,7 @@ cc_library(
         ":sat_solver",
         ":scheduling_cuts",
         ":scheduling_helpers",
+        ":synchronization",
         ":util",
         "//ortools/base:logging",
         "//ortools/base:mathutil",
@@ -2925,10 +2929,12 @@ cc_library(
         "//ortools/util:logging",
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
+        "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/base:core_headers",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
+        "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/types:span",
         "@protobuf",
@@ -4369,10 +4375,10 @@ cc_library(
         ":model",
         ":sat_base",
         ":synchronization",
-        ":util",
         "//ortools/base:strong_vector",
         "//ortools/util:bitset",
         "@abseil-cpp//absl/algorithm:container",
+        "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/log",
@@ -4399,18 +4405,13 @@ cc_library(
     srcs = ["lrat_proof_handler.cc"],
     hdrs = ["lrat_proof_handler.h"],
     deps = [
-        ":drat_checker",
-        ":drat_writer",
         ":lrat_cc_proto",
         ":lrat_checker",
         ":model",
         ":recordio",
         ":sat_base",
         ":synchronization",
-        ":util",
-        "//ortools/base:file",
         "//ortools/base:intops",
-        "//ortools/base:timer",
         "@abseil-cpp//absl/container:flat_hash_map",
         "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/flags:flag",
@@ -4442,6 +4443,8 @@ cc_test(
         ":model",
         ":sat_base",
         "//ortools/base:gmock_main",
+        "@abseil-cpp//absl/memory",
+        "@abseil-cpp//absl/strings",
         "@abseil-cpp//absl/types:span",
     ],
 )

ortools/sat/all_different.cc

@@ -33,6 +33,7 @@
 #include "ortools/sat/sat_solver.h"
 #include "ortools/util/sort.h"
 #include "ortools/util/strong_integers.h"
+#include "ortools/util/time_limit.h"
 
 namespace operations_research {
 namespace sat {
@@ -405,7 +406,7 @@ bool AllDifferentConstraint::Propagate() {
           }
         }
 
-        return trail_->EnqueueWithStoredReason(kNoClauseId, x_lit.Negated());
+        return trail_->EnqueueWithStoredReason(x_lit.Negated(), kNullClausePtr);
       }
     }
   }
@@ -417,6 +418,7 @@ AllDifferentBoundsPropagator::AllDifferentBoundsPropagator(
     absl::Span<const Literal> enforcement_literals,
     absl::Span<const AffineExpression> expressions, Model* model)
     : integer_trail_(*model->GetOrCreate<IntegerTrail>()),
+      time_limit_(model->GetOrCreate<TimeLimit>()),
       enforcement_helper_(*model->GetOrCreate<EnforcementHelper>()) {
   CHECK(!expressions.empty());
 
@@ -489,8 +491,15 @@ bool AllDifferentBoundsPropagator::PropagateLowerBounds() {
     entry.lb = integer_trail_.LowerBound(entry.expr);
     entry.ub = integer_trail_.UpperBound(entry.expr);
   }
-  IncrementalSort(bounds_.begin(), bounds_.end(),
-                  [](CachedBounds a, CachedBounds b) { return a.lb < b.lb; });
+
+  // TODO(user): The running time can be dominated by this sort. For the
+  // "permutation" case where we have as many bounds has possible lb, maybe a
+  // radix sort is more efficient.
+  time_limit_->AdvanceDeterministicTime(static_cast<double>(bounds_.size()) *
+                                        1e-8);
+  IncrementalSort(
+      bounds_.begin(), bounds_.end(),
+      [](const CachedBounds& a, const CachedBounds& b) { return a.lb < b.lb; });
 
   // We will split the affine epressions in vars sorted by lb in contiguous
   // subset with index of the form [start, start + num_in_window).

ortools/sat/all_different.h

@@ -31,6 +31,7 @@
 #include "ortools/sat/util.h"
 #include "ortools/util/bitset.h"
 #include "ortools/util/strong_integers.h"
+#include "ortools/util/time_limit.h"
 
 namespace operations_research {
 namespace sat {
@@ -215,6 +216,8 @@ class AllDifferentBoundsPropagator : public PropagatorInterface {
   IntegerValue GetValue(int index) const { return base_ + IntegerValue(index); }
 
   const IntegerTrail& integer_trail_;
+  TimeLimit* time_limit_;
+
   EnforcementHelper& enforcement_helper_;
   EnforcementId enforcement_id_;
 

ortools/sat/circuit.cc

@@ -308,7 +308,8 @@ bool CircuitPropagator::Propagate() {
         std::vector<Literal>* reason = trail_.GetEmptyVectorToStoreReason();
         FillReasonForPath(start_node, reason);
         enforcement_helper_.AddEnforcementReason(enforcement_id_, reason);
-        if (!trail_.EnqueueWithStoredReason(kNoClauseId, literal.Negated())) {
+        if (!trail_.EnqueueWithStoredReason(literal.Negated(),
+                                            kNullClausePtr)) {
           return false;
         }
       }
@@ -358,7 +359,7 @@ bool CircuitPropagator::Propagate() {
           reason->push_back(Literal(extra_reason));
         }
         const bool ok =
-            trail_.EnqueueWithStoredReason(kNoClauseId, literal.Negated());
+            trail_.EnqueueWithStoredReason(literal.Negated(), kNullClausePtr);
         if (!ok) return false;
         continue;
       }
@@ -399,7 +400,8 @@ bool CircuitPropagator::Propagate() {
           std::vector<Literal>* reason = trail_.GetEmptyVectorToStoreReason();
           FillReasonForPath(start_node, reason);
           enforcement_helper_.AddEnforcementReason(enforcement_id_, reason);
-          const bool ok = trail_.EnqueueWithStoredReason(kNoClauseId, literal);
+          const bool ok =
+              trail_.EnqueueWithStoredReason(literal, kNullClausePtr);
           if (!ok) return false;
         } else {
           trail_.EnqueueWithSameReasonAs(literal, variable_with_same_reason);
@@ -671,7 +673,7 @@ bool CircuitCoveringPropagator::Propagate() {
       auto* reason = trail_->GetEmptyVectorToStoreReason();
       FillFixedPathInReason(start, end, reason);
       const bool ok = trail_->EnqueueWithStoredReason(
-          kNoClauseId, graph_[end][start].Negated());
+          graph_[end][start].Negated(), kNullClausePtr);
       if (!ok) return false;
     }
   }