[CP-SAT] improve lns for makespan objective; fix jeasibility jump che…

…ck failed; fix non deterministic search with gap limits

ortools/sat/cp_model_lns.h

@@ -28,13 +28,14 @@
 #include "absl/random/bit_gen_ref.h"
 #include "absl/strings/string_view.h"
 #include "absl/synchronization/mutex.h"
-#include "absl/time/time.h"
 #include "absl/types/span.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/integer.h"
+#include "ortools/sat/model.h"
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/subsolver.h"
 #include "ortools/sat/synchronization.h"
+#include "ortools/sat/util.h"
 #include "ortools/util/adaptative_parameter_value.h"
 
 namespace operations_research {
@@ -203,6 +204,19 @@ class NeighborhoodGeneratorHelper : public SubSolver {
     return absl::MakeSpan(type_to_constraints_[type]);
   }
 
+  // Checks if an interval is active w.r.t. the initial_solution.
+  // An interval is inactive if and only if it is either unperformed in the
+  // solution or constant in the model.
+  bool IntervalIsActive(int index,
+                        const CpSolverResponse& initial_solution) const
+      ABSL_SHARED_LOCKS_REQUIRED(domain_mutex_);
+
+  // Filters a vector of intervals against the initial_solution, and returns
+  // only the active intervals.
+  void FilterInactiveIntervals(absl::Span<const int> unfiltered_intervals,
+                               const CpSolverResponse& initial_solution,
+                               std::vector<int>* filtered_intervals) const;
+
   // Returns the list of indices of active interval constraints according
   // to the initial_solution and the parameter lns_focus_on_performed_intervals.
   // If true, this method returns the list of performed intervals in the
@@ -411,8 +425,9 @@ class NeighborhoodGenerator {
   }
 
   // Process all the recently added solve data and update this generator
-  // score and difficulty.
-  void Synchronize();
+  // score and difficulty. This returns the sum of the deterministic time of
+  // each SolveData.
+  double Synchronize();
 
   // Returns a short description of the generator.
   std::string name() const { return name_; }
@@ -455,12 +470,6 @@ class NeighborhoodGenerator {
     return deterministic_limit_;
   }
 
-  // The sum of the deterministic time spent in this generator.
-  double deterministic_time() const {
-    absl::MutexLock mutex_lock(&generator_mutex_);
-    return deterministic_time_;
-  }
-
  protected:
   const std::string name_;
   const NeighborhoodGeneratorHelper& helper_;
@@ -481,7 +490,6 @@ class NeighborhoodGenerator {
   int64_t num_improving_calls_ = 0;
   int64_t num_consecutive_non_improving_calls_ = 0;
   int64_t next_time_limit_bump_ = 50;
-  double deterministic_time_ = 0.0;
   double current_average_ = 0.0;
 };
 
@@ -605,6 +613,7 @@ class LocalBranchingLpBasedNeighborhoodGenerator
 // intervals.
 Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals(
     absl::Span<const int> intervals_to_relax,
+    absl::Span<const int> variables_to_fix,
     const CpSolverResponse& initial_solution, absl::BitGenRef random,
     const NeighborhoodGeneratorHelper& helper);
 

ortools/sat/cp_model_solver.cc

@@ -3333,10 +3333,9 @@ class LnsSolver : public SubSolver {
   }
 
   void Synchronize() override {
-    generator_->Synchronize();
-    const double diff = generator_->deterministic_time() - deterministic_time();
-    AddTaskDeterministicDuration(diff);
-    shared_->time_limit->AdvanceDeterministicTime(diff);
+    const double dtime = generator_->Synchronize();
+    AddTaskDeterministicDuration(dtime);
+    shared_->time_limit->AdvanceDeterministicTime(dtime);
   }
 
   std::vector<std::string> TableLineStats() const override {
@@ -4153,8 +4152,13 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
     }
     if (is_pure_sat) {
       for (const ConstraintProto& ct : model_proto.constraints()) {
-        if (ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolOr &&
-            ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolAnd) {
+        if (ct.constraint_case() != ConstraintProto::kBoolOr &&
+            ct.constraint_case() != ConstraintProto::kBoolAnd) {
+          is_pure_sat = false;
+          break;
+        }
+        if (ct.constraint_case() == ConstraintProto::kBoolAnd &&
+            ct.enforcement_literal().size() > 1) {
           is_pure_sat = false;
           break;
         }

ortools/sat/disjunctive.cc

@@ -17,6 +17,7 @@
 #include <functional>
 #include <vector>
 
+#include "absl/algorithm/container.h"
 #include "absl/log/check.h"
 #include "ortools/sat/all_different.h"
 #include "ortools/sat/integer.h"
@@ -508,8 +509,9 @@ bool CombinedDisjunctive<time_direction>::Propagate() {
 }
 
 bool DisjunctiveOverloadChecker::Propagate() {
-  if (!helper_->SynchronizeAndSetTimeDirection(/*is_forward=*/true))
+  if (!helper_->SynchronizeAndSetTimeDirection(/*is_forward=*/true)) {
     return false;
+  }
 
   // Split problem into independent part.
   //
@@ -522,20 +524,21 @@ bool DisjunctiveOverloadChecker::Propagate() {
   // all task in the window, [start_min, end_min] is inside the window, and the
   // end min of any set of task to the left is <= window_start, and the
   // start_min of any task to the right is >= end_min.
-  window_.clear();
   IntegerValue window_end = kMinIntegerValue;
   IntegerValue relevant_end;
+  int window_size = 0;
   int relevant_size = 0;
   for (const TaskTime task_time : helper_->TaskByIncreasingShiftedStartMin()) {
     const int task = task_time.task_index;
     if (helper_->IsAbsent(task)) continue;
 
+    // Extend window.
     const IntegerValue start_min = task_time.time;
     if (start_min < window_end) {
-      window_.push_back(task_time);
+      window_[window_size++] = task_time;
       window_end += helper_->SizeMin(task);
       if (window_end > helper_->EndMax(task)) {
-        relevant_size = window_.size();
+        relevant_size = window_size;
         relevant_end = window_end;
       }
       continue;
@@ -544,21 +547,19 @@ bool DisjunctiveOverloadChecker::Propagate() {
     // Process current window.
     // We don't need to process the end of the window (after relevant_size)
     // because these interval can be greedily assembled in a feasible solution.
-    window_.resize(relevant_size);
-    if (relevant_size > 0 && !PropagateSubwindow(relevant_end)) {
+    if (relevant_size > 0 && !PropagateSubwindow(relevant_size, relevant_end)) {
       return false;
     }
 
     // Start of the next window.
-    window_.clear();
-    window_.push_back(task_time);
+    window_size = 0;
+    window_[window_size++] = task_time;
     window_end = start_min + helper_->SizeMin(task);
     relevant_size = 0;
   }
 
   // Process last window.
-  window_.resize(relevant_size);
-  if (relevant_size > 0 && !PropagateSubwindow(relevant_end)) {
+  if (relevant_size > 0 && !PropagateSubwindow(relevant_size, relevant_end)) {
     return false;
   }
 
@@ -573,24 +574,28 @@ bool DisjunctiveOverloadChecker::Propagate() {
 // overload after every insertion, but we could use an upper bound of the
 // theta envelope to save us from checking the actual value.
 bool DisjunctiveOverloadChecker::PropagateSubwindow(
-    IntegerValue global_window_end) {
+    int relevant_size, IntegerValue global_window_end) {
   // Set up theta tree and task_by_increasing_end_max_.
-  const int window_size = window_.size();
-  theta_tree_.Reset(window_size);
+  int num_events = 0;
   task_by_increasing_end_max_.clear();
-  for (int i = 0; i < window_size; ++i) {
+  for (int i = 0; i < relevant_size; ++i) {
     // No point adding a task if its end_max is too large.
-    const int task = window_[i].task_index;
+    const TaskTime& task_time = window_[i];
+    const int task = task_time.task_index;
     const IntegerValue end_max = helper_->EndMax(task);
     if (end_max < global_window_end) {
-      task_to_event_[task] = i;
+      window_[num_events] = task_time;
+      task_to_event_[task] = num_events;
       task_by_increasing_end_max_.push_back({task, end_max});
+      ++num_events;
     }
   }
+  theta_tree_.Reset(num_events);
 
   // Introduce events by increasing end_max, check for overloads.
-  std::sort(task_by_increasing_end_max_.begin(),
-            task_by_increasing_end_max_.end());
+  // If end_max is the same, we want to add high start-min first.
+  absl::c_reverse(task_by_increasing_end_max_);
+  absl::c_stable_sort(task_by_increasing_end_max_);
   for (const auto task_time : task_by_increasing_end_max_) {
     const int current_task = task_time.task_index;
 
@@ -624,7 +629,7 @@ bool DisjunctiveOverloadChecker::PropagateSubwindow(
       const IntegerValue window_start = window_[critical_event].time;
       const IntegerValue window_end =
           theta_tree_.GetEnvelopeOf(critical_event) - 1;
-      for (int event = critical_event; event < window_size; event++) {
+      for (int event = critical_event; event < num_events; event++) {
         const IntegerValue energy_min = theta_tree_.EnergyMin(event);
         if (energy_min > 0) {
           const int task = window_[event].task_index;
@@ -657,7 +662,7 @@ bool DisjunctiveOverloadChecker::PropagateSubwindow(
         const IntegerValue window_start = window_[critical_event].time;
         const IntegerValue window_end =
             current_end + optional_size_min - available_energy - 1;
-        for (int event = critical_event; event < window_size; event++) {
+        for (int event = critical_event; event < num_events; event++) {
           const IntegerValue energy_min = theta_tree_.EnergyMin(event);
           if (energy_min > 0) {
             const int task = window_[event].task_index;

ortools/sat/disjunctive.h

@@ -135,23 +135,25 @@ class TaskSet {
 class DisjunctiveOverloadChecker : public PropagatorInterface {
  public:
   explicit DisjunctiveOverloadChecker(SchedulingConstraintHelper* helper)
-      : helper_(helper) {
-    // Resize this once and for all.
-    task_to_event_.resize(helper_->NumTasks());
-  }
+      : helper_(helper),
+        window_(new TaskTime[helper->NumTasks()]),
+        task_to_event_(new int[helper->NumTasks()]) {}
+
   bool Propagate() final;
   int RegisterWith(GenericLiteralWatcher* watcher);
 
  private:
-  bool PropagateSubwindow(IntegerValue global_window_end);
+  bool PropagateSubwindow(int relevat_size, IntegerValue global_window_end);
 
   SchedulingConstraintHelper* helper_;
 
-  std::vector<TaskTime> window_;
+  // Size assigned at construction, stay fixed afterwards.
+  std::unique_ptr<TaskTime[]> window_;
+  std::unique_ptr<int[]> task_to_event_;
+
   std::vector<TaskTime> task_by_increasing_end_max_;
 
   ThetaLambdaTree<IntegerValue> theta_tree_;
-  std::vector<int> task_to_event_;
 };
 
 class DisjunctiveDetectablePrecedences : public PropagatorInterface {

ortools/sat/docs/README.md

@@ -1,23 +1,12 @@
-| [home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Python API](https://or-tools.github.io/docs/python/ortools/sat/python/cp_model.html) |
+| [home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Python API](https://google.github.io/or-tools/python/ortools/sat/python/cp_model.html) |
 | ----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | -------------------------------- |
 
 # Using the CP-SAT solver
 
 https://developers.google.com/optimization/cp/cp_solver
 
 
-<!--ts-->
-* [Using the CP-SAT solver](#using-the-cp-sat-solver)
-   * [Documentation structure](#documentation-structure)
-   * [Searching for one (optimal) solution of a CP-SAT model](#searching-for-one-optimal-solution-of-a-cp-sat-model)
-      * [Python code samples](#python-code-samples)
-      * [C++ code samples](#c-code-samples)
-      * [Java code samples](#java-code-samples)
-      * [C# code samples](#c-code-samples-1)
 
-<!-- Created by https://github.com/ekalinin/github-markdown-toc -->
-
-<!--te-->
 
 ## Documentation structure
 

ortools/sat/docs/boolean_logic.md

@@ -6,30 +6,7 @@
 https://developers.google.com/optimization/
 
 
-<!--ts-->
-* [Boolean logic recipes for the CP-SAT solver.](#boolean-logic-recipes-for-the-cp-sat-solver)
-   * [Introduction](#introduction)
-   * [Boolean variables and literals](#boolean-variables-and-literals)
-      * [Python code](#python-code)
-      * [C++ code](#c-code)
-      * [Java code](#java-code)
-      * [C# code](#c-code-1)
-   * [Boolean constraints](#boolean-constraints)
-      * [Python code](#python-code-1)
-      * [C++ code](#c-code-2)
-      * [Java code](#java-code-1)
-      * [C# code](#c-code-3)
-   * [Reified constraints](#reified-constraints)
-      * [Python code](#python-code-2)
-      * [C++ code](#c-code-4)
-      * [Java code](#java-code-2)
-      * [C# code](#c-code-5)
-   * [Product of two Boolean Variables](#product-of-two-boolean-variables)
-      * [Python code](#python-code-3)
-
-<!-- Created by https://github.com/ekalinin/github-markdown-toc -->
-
-<!--te-->
+
 
 ## Introduction
 

ortools/sat/docs/channeling.md

@@ -5,22 +5,7 @@
 
 https://developers.google.com/optimization/
 
-<!--ts-->
-* [Channeling constraints](#channeling-constraints)
-   * [If-Then-Else expressions](#if-then-else-expressions)
-      * [Python code](#python-code)
-      * [C++ code](#c-code)
-      * [Java code](#java-code)
-      * [C# code](#c-code-1)
-   * [A bin-packing problem](#a-bin-packing-problem)
-      * [Python code](#python-code-1)
-      * [C++ code](#c-code-2)
-      * [Java code](#java-code-1)
-      * [C# code](#c-code-3)
-
-<!-- Created by https://github.com/ekalinin/github-markdown-toc -->
-
-<!--te-->
+
 
 A *channeling constraint* links variables inside a model. They're used when you
 want to express a complicated relationship between variables, such as "if this

ortools/sat/docs/integer_arithmetic.md

@@ -5,38 +5,7 @@
 
 https://developers.google.com/optimization/
 
-<!--ts-->
-* [Integer arithmetic recipes for the CP-SAT solver.](#integer-arithmetic-recipes-for-the-cp-sat-solver)
-   * [Introduction](#introduction)
-   * [Integer variables](#integer-variables)
-      * [Interval domain](#interval-domain)
-      * [Non-contiguous domain](#non-contiguous-domain)
-      * [Boolean variables](#boolean-variables)
-      * [Other methods](#other-methods)
-   * [Linear constraints](#linear-constraints)
-      * [C++ and Java linear constraints and linear expressions](#c-and-java-linear-constraints-and-linear-expressions)
-      * [Python and C# linear constraints and linear expressions](#python-and-c-linear-constraints-and-linear-expressions)
-      * [Generic linear constraint](#generic-linear-constraint)
-      * [Limitations](#limitations)
-   * [Rabbits and Pheasants examples](#rabbits-and-pheasants-examples)
-      * [Python code](#python-code)
-      * [C++ code](#c-code)
-      * [Java code](#java-code)
-      * [C# code](#c-code-1)
-   * [Earliness-Tardiness cost function.](#earliness-tardiness-cost-function)
-      * [Python code](#python-code-1)
-      * [C++ code](#c-code-2)
-      * [Java code](#java-code-1)
-      * [C# code](#c-code-3)
-   * [Step function.](#step-function)
-      * [Python code](#python-code-2)
-      * [C++ code](#c-code-4)
-      * [Java code](#java-code-2)
-      * [C# code](#c-code-5)
-
-<!-- Created by https://github.com/ekalinin/github-markdown-toc -->
-
-<!--te-->
+
 
 ## Introduction
 
@@ -764,8 +733,6 @@ step_function_sample_sat()
 ```cpp
 #include <stdlib.h>
 
-#include <memory>
-
 #include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/sat/cp_model.h"