[CP-SAT] work on probing search; presolve

Author: lperron

ortools/sat/BUILD.bazel

@@ -394,6 +394,7 @@ cc_library(
         ":symmetry_util",
         ":synchronization",
         ":util",
+        "//ortools/util:running_stat",
         "//ortools/util:time_limit",
         "@abseil-cpp//absl/container:flat_hash_set",
         "@abseil-cpp//absl/log",
@@ -976,6 +977,7 @@ cc_library(
         "@abseil-cpp//absl/algorithm:container",
         "@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/random:bit_gen_ref",
         "@abseil-cpp//absl/random:distributions",
@@ -1753,6 +1755,7 @@ cc_test(
     size = "small",
     timeout = "moderate",
     srcs = ["cp_model_expand_test.cc"],
+    tags = ["noci"],
     deps = [
         ":cp_model_cc_proto",
         ":cp_model_checker",

ortools/sat/continuous_prober.cc

@@ -72,7 +72,8 @@ ContinuousProber::ContinuousProber(const CpModelProto& model_proto,
       shared_bounds_manager_(model->Mutable<SharedBoundsManager>()),
       shared_stats_(model->Mutable<SharedStatistics>()),
       random_(*model->GetOrCreate<ModelRandomGenerator>()),
-      base_dtime_(parameters_.shaving_deterministic_time_in_probing_search()) {
+      base_dtime_(parameters_.shaving_deterministic_time_in_probing_search()),
+      shaving_success_rate_(/*average_window_size=*/100) {
   auto* mapping = model_->GetOrCreate<CpModelMapping>();
   absl::flat_hash_set<BooleanVariable> visited;
 
@@ -140,11 +141,6 @@ SatSolver::Status ContinuousProber::Probe() {
 
   while (!time_limit_->LimitReached()) {
     const double kMaxProbingTimePerMethod = 0.1;
-    // Store current statistics to detect shaving without any improvement.
-    int64_t starting_shaving_literals =
-        counters_.shaving.num_new_literals_fixed;
-    int64_t starting_shaving_bounds = counters_.shaving.num_new_bounds;
-
     std::optional<SatSolver::Status> status = ProbeIntegerVariables(
         time_limit_->GetElapsedDeterministicTime() + kMaxProbingTimePerMethod);
     if (status.has_value()) return status.value();
@@ -181,22 +177,6 @@ SatSolver::Status ContinuousProber::Probe() {
 
       // Alternate between shaving and non-shaving phases.
       if (use_shaving_) {
-        if (counters_.shaving.num_new_literals_fixed >
-                starting_shaving_literals ||
-            counters_.shaving.num_new_bounds > starting_shaving_bounds) {
-          // We improved something. We reduce the multiplier by a factor of 2.
-          // TODO(user): We could not go below 1.0 and increase the base
-          // dtime.
-          limit_multiplier_ = std::max(1.0, limit_multiplier_ / 2);
-
-          // Update reference counters.
-          starting_shaving_literals = counters_.shaving.num_new_literals_fixed;
-          starting_shaving_bounds = counters_.shaving.num_new_bounds;
-        } else if (limit_multiplier_ < 16.0) {
-          limit_multiplier_ *= 1.5;  // Cap the maximum limit to 16 * dtime.
-        }
-
-        // Alternating shaving and non-shaving iterations.
         use_shaving_ = false;
       } else {
         use_shaving_ = base_dtime_ > 0.0;
@@ -533,6 +513,25 @@ bool ContinuousProber::IsOrbitRepresentative(int var) const {
   return var_to_representative_[var] == var;
 }
 
+void ContinuousProber::AdaptShavingMultiplier(bool success) {
+  if (success) {
+    shaving_success_rate_.Add(1.0);
+  } else {
+    shaving_success_rate_.Add(0.0);
+  }
+  // TODO(user): Try to wait until the window is full before adapting the
+  // multiplier.
+  if (--update_frequency_ <= 0) {
+    update_frequency_ = kShavingUpdateFrequency;
+    const double rate = shaving_success_rate_.WindowAverage();
+    if (rate > 0.5 && limit_multiplier_ > 0.5) {
+      limit_multiplier_ = std::max(0.5, limit_multiplier_ * 0.95);
+    } else if (rate < 0.05 && limit_multiplier_ < 10.0) {
+      limit_multiplier_ = std::min(20.0, limit_multiplier_ * 1.1);
+    }
+  }
+}
+
 SatSolver::Status ContinuousProber::ShaveLiteral(
     Literal literal, bool literal_is_an_integer_bound) {
   if (trail_->Assignment().LiteralIsAssigned(literal)) {
@@ -548,6 +547,8 @@ SatSolver::Status ContinuousProber::ShaveLiteral(
                                 base_dtime_ * limit_multiplier_));
   const SatSolver::Status status =
       ResetAndSolveIntegerProblem({literal}, model_);
+  AdaptShavingMultiplier(status == SatSolver::ASSUMPTIONS_UNSAT ||
+                         status == SatSolver::FEASIBLE);
   time_limit_->ChangeDeterministicLimit(original_dtime_limit);
   if (ReportStatus(status)) return status;
 

ortools/sat/continuous_prober.h

@@ -44,6 +44,7 @@
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/sat_solver.h"
 #include "ortools/sat/synchronization.h"
+#include "ortools/util/running_stat.h"
 #include "ortools/util/time_limit.h"
 
 namespace operations_research {
@@ -70,6 +71,7 @@ class ContinuousProber {
   static const int kTestLimitPeriod = 20;
   static const int kLogPeriod = 5000;
   static const int kSyncPeriod = 50;
+  static const int kShavingUpdateFrequency = 20;
 
   struct MethodStats {
     explicit MethodStats(absl::string_view name = "") : name(name) {}
@@ -101,6 +103,7 @@ class ContinuousProber {
   bool ReportStatus(SatSolver::Status status);
   void LogStatistics();
   SatSolver::Status PeriodicSyncAndCheck();
+  void AdaptShavingMultiplier(bool success);
 
   MethodStats GetStats(Prober* prober) const;
   static void AddStats(MethodStats& total_stats, const MethodStats& start_stats,
@@ -162,6 +165,8 @@ class ContinuousProber {
   bool use_shaving_ = false;
   std::vector<std::vector<Literal>> tmp_dnf_;
   std::vector<Literal> tmp_literals_;
+  RunningAverage shaving_success_rate_;
+  int update_frequency_ = kShavingUpdateFrequency;
 };
 
 }  // namespace sat

ortools/sat/cp_model_postsolve.cc

@@ -16,6 +16,7 @@
 #include <algorithm>
 #include <cstdint>
 #include <limits>
+#include <string>
 #include <vector>
 
 #include "absl/log/check.h"
@@ -98,7 +99,6 @@ void PostsolveExactlyOne(const ConstraintProto& ct,
 // There must be one.
 void SetEnforcementLiteralToFalse(const ConstraintProto& ct,
                                   std::vector<Domain>* domains) {
-  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;
@@ -111,9 +111,13 @@ void SetEnforcementLiteralToFalse(const ConstraintProto& ct,
     break;
   }
   if (!has_free_enforcement_literal) {
+    std::string domain_info = "\n";
+    for (const int var : UsedVariables(ct)) {
+      absl::StrAppend(&domain_info, var, ":", (*domains)[var].ToString(), "\n");
+    }
     LOG(FATAL)
-        << "Unsatisfied linear constraint with no free enforcement literal: "
-        << ProtobufShortDebugString(ct);
+        << "Unsatisfied linear constraint with no free enforcement literal:\n"
+        << ProtobufShortDebugString(ct) << domain_info;
   }
 }