add time limit to max_clique algorithm in CP-SAT presolve; fix rare crash in CP-SAT/GLOP connection; experimental CP-SAT scheduling code to speed-up the case of multiple no_overlap with lots of shared intervals; replace algorithm behind the util default random engine

ortools/sat/clause.cc

@@ -869,7 +869,8 @@ struct VectorHash {
 }  // namespace
 
 void BinaryImplicationGraph::TransformIntoMaxCliques(
-    std::vector<std::vector<Literal>>* at_most_ones) {
+    std::vector<std::vector<Literal>>* at_most_ones,
+    int64 max_num_explored_nodes) {
   // The code below assumes a DAG.
   if (!is_dag_) DetectEquivalences();
   work_done_in_mark_descendants_ = 0;
@@ -916,7 +917,7 @@ void BinaryImplicationGraph::TransformIntoMaxCliques(
     }
 
     // We only expand the clique as long as we didn't spend too much time.
-    if (work_done_in_mark_descendants_ < 1e8) {
+    if (work_done_in_mark_descendants_ < max_num_explored_nodes) {
       clique = ExpandAtMostOne(clique);
     }
     std::sort(clique.begin(), clique.end());
@@ -937,7 +938,9 @@ void BinaryImplicationGraph::TransformIntoMaxCliques(
   if (num_extended > 0 || num_removed > 0 || num_added > 0) {
     VLOG(1) << "Clique Extended: " << num_extended
             << " Removed: " << num_removed << " Added: " << num_added
-            << (work_done_in_mark_descendants_ > 1e8 ? " (Aborted)" : "");
+            << (work_done_in_mark_descendants_ > max_num_explored_nodes
+                    ? " (Aborted)"
+                    : "");
   }
 }
 

ortools/sat/clause.h

@@ -487,7 +487,8 @@ class BinaryImplicationGraph : public SatPropagator {
   // This function will transform each of the given constraint into a maximal
   // one in the underlying implication graph. Constraints that are redundant
   // after other have been expanded (i.e. included into) will be cleared.
-  void TransformIntoMaxCliques(std::vector<std::vector<Literal>>* at_most_ones);
+  void TransformIntoMaxCliques(std::vector<std::vector<Literal>>* at_most_ones,
+                               int64 max_num_explored_nodes = 1e8);
 
   // Number of literal propagated by this class (including conflicts).
   int64 num_propagations() const { return num_propagations_; }

ortools/sat/cp_model_presolve.cc

@@ -712,6 +712,7 @@ bool PresolveAtMostOne(ConstraintProto* ct, PresolveContext* context) {
 bool PresolveIntMax(ConstraintProto* ct, PresolveContext* context) {
   if (context->ModelIsUnsat()) return false;
   if (ct->int_max().vars().empty()) {
+    context->UpdateRuleStats("int_max: no variables!");
     return MarkConstraintAsFalse(ct, context);
   }
   const int target_ref = ct->int_max().target();
@@ -866,6 +867,7 @@ bool PresolveIntMax(ConstraintProto* ct, PresolveContext* context) {
   }
 
   if (new_size == 0) {
+    context->UpdateRuleStats("int_max: no variables!");
     return MarkConstraintAsFalse(ct, context);
   }
   if (new_size == 1) {
@@ -2925,7 +2927,7 @@ void ExtractClauses(const ClauseContainer& container, CpModelProto* proto) {
   }
 }
 
-void Probe(TimeLimit* global_time_limit, PresolveContext* context) {
+void Probe(PresolveOptions options, PresolveContext* context) {
   if (context->ModelIsUnsat()) return;
 
   // Update the domain in the current CpModelProto.
@@ -2943,7 +2945,8 @@ void Probe(TimeLimit* global_time_limit, PresolveContext* context) {
   // TODO(user): Maybe do not load slow to propagate constraints? for instance
   // we do not use any linear relaxation here.
   Model model;
-  model.GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(global_time_limit);
+  *(model.GetOrCreate<SatParameters>()) = options.parameters;
+  model.GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(options.time_limit);
   auto* encoder = model.GetOrCreate<IntegerEncoder>();
   encoder->DisableImplicationBetweenLiteral();
   auto* mapping = model.GetOrCreate<CpModelMapping>();
@@ -3496,7 +3499,7 @@ void MergeNoOverlapConstraints(PresolveContext* context) {
     graph->AddAtMostOne(clique);
   }
   CHECK(graph->DetectEquivalences());
-  graph->TransformIntoMaxCliques(&cliques);
+  graph->TransformIntoMaxCliques(&cliques, /*max_num_explored_nodes=*/1e10);
 
   // Replace each no-overlap with an extended version, or remove if empty.
   int new_num_no_overlaps = 0;
@@ -3978,7 +3981,8 @@ void TryToSimplifyDomains(PresolveContext* context) {
   context->UpdateNewConstraintsVariableUsage();
 }
 
-void PresolveToFixPoint(PresolveContext* context, TimeLimit* time_limit) {
+void PresolveToFixPoint(const PresolveOptions& options,
+                        PresolveContext* context) {
   if (context->ModelIsUnsat()) return;
 
   // This is used for constraint having unique variables in them (i.e. not
@@ -3987,6 +3991,7 @@ void PresolveToFixPoint(PresolveContext* context, TimeLimit* time_limit) {
   absl::flat_hash_set<std::pair<int, int>> var_constraint_pair_already_called;
 
   // The queue of "active" constraints, initialized to all of them.
+  TimeLimit* time_limit = options.time_limit;
   std::vector<bool> in_queue(context->working_model->constraints_size(), true);
   std::deque<int> queue(context->working_model->constraints_size());
   std::iota(queue.begin(), queue.end(), 0);
@@ -4000,6 +4005,11 @@ void PresolveToFixPoint(PresolveContext* context, TimeLimit* time_limit) {
 
       const int old_num_constraint = context->working_model->constraints_size();
       const bool changed = PresolveOneConstraint(c, context);
+      if (context->ModelIsUnsat() && options.log_info) {
+        LOG(INFO) << "Unsat after presolving constraint #" << c
+                  << " (warning, dump might be inconsistent): "
+                  << context->working_model->constraints(c).ShortDebugString();
+      }
 
       // Add to the queue any newly created constraints.
       const int new_num_constraints =
@@ -4166,6 +4176,23 @@ void RemoveUnusedEquivalentVariables(PresolveContext* context) {
   context->UpdateNewConstraintsVariableUsage();
 }
 
+void LogInfoFromContext(const PresolveContext& context) {
+  LOG(INFO) << "- " << context.affine_relations.NumRelations()
+            << " affine relations were detected.";
+  LOG(INFO) << "- " << context.var_equiv_relations.NumRelations()
+            << " variable equivalence relations were detected.";
+  std::map<std::string, int> sorted_rules(context.stats_by_rule_name.begin(),
+                                          context.stats_by_rule_name.end());
+  for (const auto& entry : sorted_rules) {
+    if (entry.second == 1) {
+      LOG(INFO) << "- rule '" << entry.first << "' was applied 1 time.";
+    } else {
+      LOG(INFO) << "- rule '" << entry.first << "' was applied " << entry.second
+                << " times.";
+    }
+  }
+}
+
 }  // namespace.
 
 // =============================================================================
@@ -4223,14 +4250,14 @@ bool PresolveCpModel(const PresolveOptions& options,
   }
 
   // Main propagation loop.
-  PresolveToFixPoint(&context, options.time_limit);
+  PresolveToFixPoint(options, &context);
 
   // Runs the probing.
   // TODO(user): do that and the pure-SAT part below more than once.
   if (options.parameters.cp_model_probing_level() > 0) {
     if (options.time_limit == nullptr || !options.time_limit->LimitReached()) {
-      Probe(options.time_limit, &context);
-      PresolveToFixPoint(&context, options.time_limit);
+      Probe(options, &context);
+      PresolveToFixPoint(options, &context);
     }
   }
 
@@ -4276,10 +4303,12 @@ bool PresolveCpModel(const PresolveOptions& options,
 
     // Call the main presolve to remove the fixed variables and do more
     // deductions.
-    PresolveToFixPoint(&context, options.time_limit);
+    PresolveToFixPoint(options, &context);
   }
 
   if (context.ModelIsUnsat()) {
+    if (options.log_info) LogInfoFromContext(context);
+
     // Set presolved_model to the simplest UNSAT problem (empty clause).
     presolved_model->Clear();
     presolved_model->add_constraints()->mutable_bool_or();
@@ -4402,22 +4431,7 @@ bool PresolveCpModel(const PresolveOptions& options,
   ApplyVariableMapping(mapping, presolved_model);
 
   // Stats and checks.
-  if (options.log_info) {
-    LOG(INFO) << "- " << context.affine_relations.NumRelations()
-              << " affine relations were detected.";
-    LOG(INFO) << "- " << context.var_equiv_relations.NumRelations()
-              << " variable equivalence relations were detected.";
-    std::map<std::string, int> sorted_rules(context.stats_by_rule_name.begin(),
-                                            context.stats_by_rule_name.end());
-    for (const auto& entry : sorted_rules) {
-      if (entry.second == 1) {
-        LOG(INFO) << "- rule '" << entry.first << "' was applied 1 time.";
-      } else {
-        LOG(INFO) << "- rule '" << entry.first << "' was applied "
-                  << entry.second << " times.";
-      }
-    }
-  }
+  if (options.log_info) LogInfoFromContext(context);
 
   // One possible error that is difficult to avoid here: because of our
   // objective expansion, we might detect a possible overflow...

ortools/sat/diffn.cc

@@ -257,7 +257,7 @@ NonOverlappingRectanglesDisjunctivePropagator::
       y_(y->NumTasks(), model),
       strict_(strict),
       watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
-      overload_checker_(true, &x_),
+      overload_checker_(&x_),
       forward_detectable_precedences_(true, &x_),
       backward_detectable_precedences_(false, &x_),
       forward_not_last_(true, &x_),

ortools/sat/disjunctive.cc

@@ -20,6 +20,7 @@
 #include "ortools/sat/all_different.h"
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/sat/sat_solver.h"
+#include "ortools/sat/timetable.h"
 #include "ortools/util/sort.h"
 
 namespace operations_research {
@@ -47,11 +48,28 @@ std::function<void(Model*)> Disjunctive(
       return;
     }
 
+    auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
+    const auto& sat_parameters = *model->GetOrCreate<SatParameters>();
+    if (vars.size() > 2 && sat_parameters.use_combined_no_overlap()) {
+      model->GetOrCreate<CombinedDisjunctive<true>>()->AddNoOverlap(vars);
+      model->GetOrCreate<CombinedDisjunctive<false>>()->AddNoOverlap(vars);
+      return;
+    }
+
     SchedulingConstraintHelper* helper =
         new SchedulingConstraintHelper(vars, model);
     model->TakeOwnership(helper);
-    GenericLiteralWatcher* watcher =
-        model->GetOrCreate<GenericLiteralWatcher>();
+
+    // Experiments to use the timetable only to propagate the disjunctive.
+    if (/*DISABLES_CODE*/ (false)) {
+      const IntegerVariable capacity = model->Add(ConstantIntegerVariable(1));
+      std::vector<IntegerVariable> demands(vars.size(), capacity);
+      TimeTablingPerTask* timetable = new TimeTablingPerTask(
+          demands, capacity, model->GetOrCreate<IntegerTrail>(), helper);
+      timetable->RegisterWith(watcher);
+      model->TakeOwnership(timetable);
+      return;
+    }
 
     if (vars.size() == 2) {
       DisjunctiveWithTwoItems* propagator = new DisjunctiveWithTwoItems(helper);
@@ -63,7 +81,7 @@ std::function<void(Model*)> Disjunctive(
       {
         // Only one direction is needed by this one.
         DisjunctiveOverloadChecker* overload_checker =
-            new DisjunctiveOverloadChecker(true, helper);
+            new DisjunctiveOverloadChecker(helper);
         const int id = overload_checker->RegisterWith(watcher);
         watcher->SetPropagatorPriority(id, 1);
         model->TakeOwnership(overload_checker);
@@ -94,8 +112,8 @@ std::function<void(Model*)> Disjunctive(
     // Note that we keep this one even when there is just two intervals. This is
     // because it might push a variable that is after both of the intervals
     // using the fact that they are in disjunction.
-    if (model->GetOrCreate<SatParameters>()
-            ->use_precedences_in_disjunctive_constraint()) {
+    if (sat_parameters.use_precedences_in_disjunctive_constraint() &&
+        !sat_parameters.use_combined_no_overlap()) {
       for (const bool time_direction : {true, false}) {
         DisjunctivePrecedences* precedences = new DisjunctivePrecedences(
             time_direction, helper, model->GetOrCreate<IntegerTrail>(),
@@ -174,6 +192,22 @@ void TaskSet::RemoveEntryWithIndex(int index) {
   optimized_restart_ = 0;
 }
 
+IntegerValue TaskSet::ComputeEndMin() const {
+  DCHECK(std::is_sorted(sorted_tasks_.begin(), sorted_tasks_.end()));
+  const int size = sorted_tasks_.size();
+  IntegerValue end_min = kMinIntegerValue;
+  for (int i = optimized_restart_; i < size; ++i) {
+    const Entry& e = sorted_tasks_[i];
+    if (e.start_min >= end_min) {
+      optimized_restart_ = i;
+      end_min = e.start_min + e.duration_min;
+    } else {
+      end_min += e.duration_min;
+    }
+  }
+  return end_min;
+}
+
 IntegerValue TaskSet::ComputeEndMin(int task_to_ignore,
                                     int* critical_index) const {
   // The order in which we process tasks with the same start-min doesn't matter.
@@ -181,6 +215,14 @@ IntegerValue TaskSet::ComputeEndMin(int task_to_ignore,
   bool ignored = false;
   const int size = sorted_tasks_.size();
   IntegerValue end_min = kMinIntegerValue;
+
+  // If the ignored task is last and was the start of the critical block, then
+  // we need to reset optimized_restart_.
+  if (optimized_restart_ + 1 == size &&
+      sorted_tasks_[optimized_restart_].task == task_to_ignore) {
+    optimized_restart_ = 0;
+  }
+
   for (int i = optimized_restart_; i < size; ++i) {
     const Entry& e = sorted_tasks_[i];
     if (e.task == task_to_ignore) {
@@ -223,31 +265,35 @@ bool DisjunctiveWithTwoItems::Propagate() {
     return true;
   }
 
-  if (helper_->IsPresent(task_before) &&
-      helper_->StartMin(task_after) < helper_->EndMin(task_before)) {
-    // Reason for precedences if both present.
-    helper_->ClearReason();
-    helper_->AddReasonForBeingBefore(task_before, task_after);
+  if (helper_->IsPresent(task_before)) {
+    const IntegerValue end_min_before = helper_->EndMin(task_before);
+    if (helper_->StartMin(task_after) < end_min_before) {
+      // Reason for precedences if both present.
+      helper_->ClearReason();
+      helper_->AddReasonForBeingBefore(task_before, task_after);
 
-    // Reason for the bound push.
-    helper_->AddPresenceReason(task_before);
-    helper_->AddEndMinReason(task_before, helper_->EndMin(task_before));
-    if (!helper_->IncreaseStartMin(task_after, helper_->EndMin(task_before))) {
-      return false;
+      // Reason for the bound push.
+      helper_->AddPresenceReason(task_before);
+      helper_->AddEndMinReason(task_before, end_min_before);
+      if (!helper_->IncreaseStartMin(task_after, end_min_before)) {
+        return false;
+      }
     }
   }
 
-  if (helper_->IsPresent(task_after) &&
-      helper_->EndMax(task_before) > helper_->StartMax(task_after)) {
-    // Reason for precedences if both present.
-    helper_->ClearReason();
-    helper_->AddReasonForBeingBefore(task_before, task_after);
+  if (helper_->IsPresent(task_after)) {
+    const IntegerValue start_max_after = helper_->StartMax(task_after);
+    if (helper_->EndMax(task_before) > start_max_after) {
+      // Reason for precedences if both present.
+      helper_->ClearReason();
+      helper_->AddReasonForBeingBefore(task_before, task_after);
 
-    // Reason for the bound push.
-    helper_->AddPresenceReason(task_after);
-    helper_->AddStartMaxReason(task_after, helper_->StartMax(task_after));
-    if (!helper_->DecreaseEndMax(task_before, helper_->StartMax(task_after))) {
-      return false;
+      // Reason for the bound push.
+      helper_->AddPresenceReason(task_after);
+      helper_->AddStartMaxReason(task_after, start_max_after);
+      if (!helper_->DecreaseEndMax(task_before, start_max_after)) {
+        return false;
+      }
     }
   }
 
@@ -261,8 +307,151 @@ int DisjunctiveWithTwoItems::RegisterWith(GenericLiteralWatcher* watcher) {
   return id;
 }
 
+template <bool time_direction>
+CombinedDisjunctive<time_direction>::CombinedDisjunctive(Model* model)
+    : helper_(model->GetOrCreate<AllIntervalsHelper>()) {
+  helper_->SetTimeDirection(time_direction);
+  task_to_disjunctives_.resize(helper_->NumTasks());
+
+  auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
+  const int id = watcher->Register(this);
+  helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/true,
+                         /*watch_end_max=*/false);
+  watcher->NotifyThatPropagatorMayNotReachFixedPointInOnePass(id);
+}
+
+template <bool time_direction>
+void CombinedDisjunctive<time_direction>::AddNoOverlap(
+    const std::vector<IntervalVariable>& vars) {
+  const int index = task_sets_.size();
+  task_sets_.emplace_back(vars.size());
+  end_mins_.push_back(kMinIntegerValue);
+  for (const IntervalVariable var : vars) {
+    task_to_disjunctives_[var.value()].push_back(index);
+  }
+}
+
+template <bool time_direction>
+bool CombinedDisjunctive<time_direction>::Propagate() {
+  helper_->SetTimeDirection(time_direction);
+  const auto& task_by_increasing_end_min = helper_->TaskByIncreasingEndMin();
+  const auto& task_by_decreasing_start_max =
+      helper_->TaskByDecreasingStartMax();
+
+  for (auto& task_set : task_sets_) task_set.Clear();
+  end_mins_.assign(end_mins_.size(), kMinIntegerValue);
+  IntegerValue max_of_end_min = kMinIntegerValue;
+
+  const int num_tasks = helper_->NumTasks();
+  task_is_added_.assign(num_tasks, false);
+  int queue_index = num_tasks - 1;
+  for (const auto task_time : task_by_increasing_end_min) {
+    const int t = task_time.task_index;
+    const IntegerValue end_min = task_time.time;
+    if (helper_->IsAbsent(t)) continue;
+
+    // Update all task sets.
+    while (queue_index >= 0) {
+      const auto to_insert = task_by_decreasing_start_max[queue_index];
+      const int task_index = to_insert.task_index;
+      const IntegerValue start_max = to_insert.time;
+      if (end_min <= start_max) break;
+      if (helper_->IsPresent(task_index)) {
+        task_is_added_[task_index] = true;
+        const IntegerValue shifted_smin = helper_->ShiftedStartMin(task_index);
+        const IntegerValue duration_min = helper_->DurationMin(task_index);
+        for (const int d_index : task_to_disjunctives_[task_index]) {
+          // TODO(user): AddEntry() and ComputeEndMin() could be combined.
+          task_sets_[d_index].AddEntry(
+              {task_index, shifted_smin, duration_min});
+          end_mins_[d_index] = task_sets_[d_index].ComputeEndMin();
+          max_of_end_min = std::max(max_of_end_min, end_mins_[d_index]);
+        }
+      }
+      --queue_index;
+    }
+
+    // Find out amongst the disjunctives in which t appear, the one with the
+    // largest end_min, ignoring t itself. This will be the new start min for t.
+    IntegerValue new_start_min = helper_->StartMin(t);
+    if (new_start_min >= max_of_end_min) continue;
+    int best_critical_index = 0;
+    int best_d_index = -1;
+    if (task_is_added_[t]) {
+      for (const int d_index : task_to_disjunctives_[t]) {
+        if (new_start_min >= end_mins_[d_index]) continue;
+        int critical_index = 0;
+        const IntegerValue end_min_of_critical_tasks =
+            task_sets_[d_index].ComputeEndMin(/*task_to_ignore=*/t,
+                                              &critical_index);
+        DCHECK_LE(end_min_of_critical_tasks, max_of_end_min);
+        if (end_min_of_critical_tasks > new_start_min) {
+          new_start_min = end_min_of_critical_tasks;
+          best_d_index = d_index;
+          best_critical_index = critical_index;
+        }
+      }
+    } else {
+      // If the task t was not added, then there is no task to ignore and
+      // end_mins_[d_index] is up to date.
+      for (const int d_index : task_to_disjunctives_[t]) {
+        if (end_mins_[d_index] > new_start_min) {
+          new_start_min = end_mins_[d_index];
+          best_d_index = d_index;
+        }
+      }
+      if (best_d_index != -1) {
+        const IntegerValue end_min_of_critical_tasks =
+            task_sets_[best_d_index].ComputeEndMin(/*task_to_ignore=*/t,
+                                                   &best_critical_index);
+        CHECK_EQ(end_min_of_critical_tasks, new_start_min);
+      }
+    }
+
+    // Do we push something?
+    if (best_d_index == -1) continue;
+
+    // Same reason as DisjunctiveDetectablePrecedences.
+    // TODO(user): Maybe factor out the code? It does require a function with a
+    // lot of arguments though.
+    helper_->ClearReason();
+    const std::vector<TaskSet::Entry>& sorted_tasks =
+        task_sets_[best_d_index].SortedTasks();
+    const IntegerValue window_start =
+        sorted_tasks[best_critical_index].start_min;
+    for (int i = best_critical_index; i < sorted_tasks.size(); ++i) {
+      const int ct = sorted_tasks[i].task;
+      if (ct == t) continue;
+      helper_->AddPresenceReason(ct);
+      helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
+                                    window_start);
+      helper_->AddStartMaxReason(ct, end_min - 1);
+    }
+    helper_->AddEndMinReason(t, end_min);
+    if (!helper_->IncreaseStartMin(t, new_start_min)) {
+      return false;
+    }
+
+    // We need to reorder t inside task_set_. Note that if t is in the set,
+    // it means that the task is present and that IncreaseStartMin() did push
+    // its start (by opposition to an optional interval where the push might
+    // not happen if its start is not optional).
+    if (task_is_added_[t]) {
+      const IntegerValue shifted_smin = helper_->ShiftedStartMin(t);
+      const IntegerValue duration_min = helper_->DurationMin(t);
+      for (const int d_index : task_to_disjunctives_[t]) {
+        task_sets_[d_index].NotifyEntryIsNowLastIfPresent(
+            {t, shifted_smin, duration_min});
+        end_mins_[d_index] = task_sets_[d_index].ComputeEndMin();
+        max_of_end_min = std::max(max_of_end_min, end_mins_[d_index]);
+      }
+    }
+  }
+  return true;
+}
+
 bool DisjunctiveOverloadChecker::Propagate() {
-  helper_->SetTimeDirection(time_direction_);
+  helper_->SetTimeDirection(/*is_forward=*/true);
 
   // Split problem into independent part.
   //
@@ -432,7 +621,7 @@ bool DisjunctiveOverloadChecker::PropagateSubwindow(
 int DisjunctiveOverloadChecker::RegisterWith(GenericLiteralWatcher* watcher) {
   // This propagator reach the fix point in one pass.
   const int id = watcher->Register(this);
-  helper_->SetTimeDirection(time_direction_);
+  helper_->SetTimeDirection(/*is_forward=*/true);
   helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/false,
                          /*watch_end_max=*/true);
   return id;
@@ -441,6 +630,9 @@ int DisjunctiveOverloadChecker::RegisterWith(GenericLiteralWatcher* watcher) {
 bool DisjunctiveDetectablePrecedences::Propagate() {
   helper_->SetTimeDirection(time_direction_);
 
+  to_propagate_.clear();
+  processed_.assign(helper_->NumTasks(), false);
+
   // Split problem into independent part.
   //
   // The "independent" window can be processed separately because for each of
@@ -509,72 +701,130 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
   IncrementalSort(task_by_increasing_end_min.begin(),
                   task_by_increasing_end_min.end());
 
+  // Invariant: need_update is false implies that task_set_end_min is equal to
+  // task_set_.ComputeEndMin().
+  //
+  // TODO(user): Maybe it is just faster to merge ComputeEndMin() with
+  // AddEntry().
   task_set_.Clear();
+  bool need_update = false;
+  IntegerValue task_set_end_min = kMinIntegerValue;
+
   int queue_index = 0;
+  int blocking_task = -1;
   const int queue_size = task_by_increasing_start_max_.size();
   for (const auto task_time : task_by_increasing_end_min) {
-    const int t = task_time.task_index;
-    const IntegerValue end_min = task_time.time;
-    DCHECK(!helper_->IsAbsent(t));
+    const int current_task = task_time.task_index;
+    DCHECK(!helper_->IsAbsent(current_task));
 
-    while (queue_index < queue_size) {
+    for (; queue_index < queue_size; ++queue_index) {
       const auto to_insert = task_by_increasing_start_max_[queue_index];
       const IntegerValue start_max = to_insert.time;
-      if (end_min <= start_max) break;
+      const IntegerValue current_end_min = task_time.time;
+      if (current_end_min <= start_max) break;
 
-      const int task_index = to_insert.task_index;
-      DCHECK(helper_->IsPresent(task_index));
-      task_set_.AddEntry({task_index, helper_->ShiftedStartMin(task_index),
-                          helper_->DurationMin(task_index)});
-      ++queue_index;
+      const int t = to_insert.task_index;
+      DCHECK(helper_->IsPresent(t));
+
+      // If t has not been processed yet, it has a mandatory part, and rather
+      // than adding it right away to task_set, we will delay all propagation
+      // until current_task is equal to this "blocking task".
+      //
+      // This idea is introduced in "Linear-Time Filtering Algorithms for the
+      // Disjunctive Constraints" Hamed Fahimi, Claude-Guy Quimper.
+      //
+      // Experiments seems to indicate that it is slighlty faster rather than
+      // having to ignore one of the task already inserted into task_set_ when
+      // we have tasks with mandatory parts. It also open-up more option for the
+      // data structure used in task_set_.
+      if (!processed_[t]) {
+        if (blocking_task != -1) {
+          // We have two blocking tasks, which means they are in conflict.
+          helper_->ClearReason();
+          helper_->AddPresenceReason(blocking_task);
+          helper_->AddPresenceReason(t);
+          helper_->AddReasonForBeingBefore(blocking_task, t);
+          helper_->AddReasonForBeingBefore(t, blocking_task);
+          return helper_->ReportConflict();
+        }
+        DCHECK_LT(start_max, helper_->EndMin(t));
+        DCHECK(to_propagate_.empty());
+        blocking_task = t;
+        to_propagate_.push_back(t);
+      } else {
+        need_update = true;
+        task_set_.AddEntry(
+            {t, helper_->ShiftedStartMin(t), helper_->DurationMin(t)});
+      }
     }
 
-    // task_set_ contains all the tasks that must be executed before t. They are
-    // in "detectable precedence" because their start_max is smaller than the
-    // end-min of t like so:
-    //          [(the task t)
-    //                     (a task in task_set_)]
-    // From there, we deduce that the start-min of t is greater or equal to the
-    // end-min of the critical tasks.
-    //
-    // Note that this works as well when IsPresent(t) is false.
-    int critical_index = 0;
-    const IntegerValue end_min_of_critical_tasks =
-        task_set_.ComputeEndMin(/*task_to_ignore=*/t, &critical_index);
-    if (end_min_of_critical_tasks > helper_->StartMin(t)) {
-      const std::vector<TaskSet::Entry>& sorted_tasks = task_set_.SortedTasks();
-      helper_->ClearReason();
-
-      // We need:
-      // - StartMax(ct) < EndMin(t) for the detectable precedence.
-      // - StartMin(ct) >= window_start for end_min_of_critical_tasks.
-      const IntegerValue window_start = sorted_tasks[critical_index].start_min;
-      for (int i = critical_index; i < sorted_tasks.size(); ++i) {
-        const int ct = sorted_tasks[i].task;
-        if (ct == t) continue;
-        DCHECK(helper_->IsPresent(ct));
-        helper_->AddPresenceReason(ct);
-        helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
-                                      window_start);
-        helper_->AddStartMaxReason(ct, end_min - 1);
-      }
-
-      // Add the reason for t (we only need the end-min).
-      helper_->AddEndMinReason(t, end_min);
-
-      // This augment the start-min of t and subsequently it can augment the
-      // next end_min_of_critical_tasks, but our deduction is still valid.
-      if (!helper_->IncreaseStartMin(t, end_min_of_critical_tasks)) {
-        return false;
-      }
-
-      // We need to reorder t inside task_set_. Note that if t is in the set,
-      // it means that the task is present and that IncreaseStartMin() did push
-      // its start (by opposition to an optional interval where the push might
-      // not happen if its start is not optional).
-      task_set_.NotifyEntryIsNowLastIfPresent(
-          {t, helper_->ShiftedStartMin(t), helper_->DurationMin(t)});
+    // If we have a blocking task, we delay the propagation until current_task
+    // is the blocking task.
+    if (blocking_task != current_task) {
+      to_propagate_.push_back(current_task);
+      if (blocking_task != -1) continue;
     }
+    for (const int t : to_propagate_) {
+      DCHECK(!processed_[t]);
+      processed_[t] = true;
+      if (need_update) {
+        need_update = false;
+        task_set_end_min = task_set_.ComputeEndMin();
+      }
+
+      // task_set_ contains all the tasks that must be executed before t. They
+      // are in "detectable precedence" because their start_max is smaller than
+      // the end-min of t like so:
+      //          [(the task t)
+      //                     (a task in task_set_)]
+      // From there, we deduce that the start-min of t is greater or equal to
+      // the end-min of the critical tasks.
+      //
+      // Note that this works as well when IsPresent(t) is false.
+      if (task_set_end_min > helper_->StartMin(t)) {
+        const int critical_index = task_set_.GetCriticalIndex();
+        const std::vector<TaskSet::Entry>& sorted_tasks =
+            task_set_.SortedTasks();
+        helper_->ClearReason();
+
+        // We need:
+        // - StartMax(ct) < EndMin(t) for the detectable precedence.
+        // - StartMin(ct) >= window_start for the value of task_set_end_min.
+        const IntegerValue end_min = helper_->EndMin(t);
+        const IntegerValue window_start =
+            sorted_tasks[critical_index].start_min;
+        for (int i = critical_index; i < sorted_tasks.size(); ++i) {
+          const int ct = sorted_tasks[i].task;
+          DCHECK_NE(ct, t);
+          helper_->AddPresenceReason(ct);
+          helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
+                                        window_start);
+          helper_->AddStartMaxReason(ct, end_min - 1);
+        }
+
+        // Add the reason for t (we only need the end-min).
+        helper_->AddEndMinReason(t, end_min);
+
+        // This augment the start-min of t. Note that t is not in task set
+        // yet, so we will use this updated start if we ever add it there.
+        if (!helper_->IncreaseStartMin(t, task_set_end_min)) {
+          return false;
+        }
+      }
+
+      if (t == blocking_task) {
+        // Insert the blocking_task. Note that because we just pushed it,
+        // it will be last in task_set_ and also the only reason used to push
+        // any of the subsequent tasks. In particular, the reason will be valid
+        // even though task_set might contains tasks with a start_max greater or
+        // equal to the end_min of the task we push.
+        need_update = true;
+        blocking_task = -1;
+        task_set_.AddEntry(
+            {t, helper_->ShiftedStartMin(t), helper_->DurationMin(t)});
+      }
+    }
+    to_propagate_.clear();
   }
   return true;
 }
@@ -645,7 +895,6 @@ bool DisjunctivePrecedences::Propagate() {
       const IntegerValue window_start = sorted_tasks[critical_index].start_min;
       for (int i = critical_index; i < sorted_tasks.size(); ++i) {
         const int ct = sorted_tasks[i].task;
-        DCHECK(helper_->IsPresent(ct));
         helper_->AddPresenceReason(ct);
         helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
                                       window_start);

ortools/sat/disjunctive.h

@@ -105,12 +105,18 @@ class TaskSet {
   // task_to_ignore to the id of this task. This returns 0 if the set is empty
   // in which case critical_index will be left unchanged.
   IntegerValue ComputeEndMin(int task_to_ignore, int* critical_index) const;
+  IntegerValue ComputeEndMin() const;
+
+  // Warning, this is only valid if ComputeEndMin() was just called. It is the
+  // same index as if one called ComputeEndMin(-1, &critical_index), but saves
+  // another unneeded loop.
+  int GetCriticalIndex() const { return optimized_restart_; }
+
   const std::vector<Entry>& SortedTasks() const { return sorted_tasks_; }
 
  private:
   std::vector<Entry> sorted_tasks_;
   mutable int optimized_restart_ = 0;
-  DISALLOW_COPY_AND_ASSIGN(TaskSet);
 };
 
 // ============================================================================
@@ -125,9 +131,8 @@ class TaskSet {
 
 class DisjunctiveOverloadChecker : public PropagatorInterface {
  public:
-  DisjunctiveOverloadChecker(bool time_direction,
-                             SchedulingConstraintHelper* helper)
-      : time_direction_(time_direction), helper_(helper), theta_tree_() {
+  explicit DisjunctiveOverloadChecker(SchedulingConstraintHelper* helper)
+      : helper_(helper) {
     // Resize this once and for all.
     task_to_event_.resize(helper_->NumTasks());
   }
@@ -137,7 +142,6 @@ class DisjunctiveOverloadChecker : public PropagatorInterface {
  private:
   bool PropagateSubwindow(IntegerValue global_window_end);
 
-  const bool time_direction_;
   SchedulingConstraintHelper* helper_;
 
   std::vector<TaskTime> window_;
@@ -163,11 +167,45 @@ class DisjunctiveDetectablePrecedences : public PropagatorInterface {
   std::vector<TaskTime> window_;
   std::vector<TaskTime> task_by_increasing_start_max_;
 
+  std::vector<bool> processed_;
+  std::vector<int> to_propagate_;
+
   const bool time_direction_;
   SchedulingConstraintHelper* helper_;
   TaskSet task_set_;
 };
 
+// Singleton model class wich is just a SchedulingConstraintHelper will all
+// the intervals.
+class AllIntervalsHelper : public SchedulingConstraintHelper {
+ public:
+  explicit AllIntervalsHelper(Model* model)
+      : SchedulingConstraintHelper(
+            model->GetOrCreate<IntervalsRepository>()->AllIntervals(), model) {}
+};
+
+// This propagates the same things as DisjunctiveDetectablePrecedences, except
+// that it only sort the full set of intervals once and then work on a combined
+// set of disjunctives.
+template <bool time_direction>
+class CombinedDisjunctive : public PropagatorInterface {
+ public:
+  explicit CombinedDisjunctive(Model* model);
+
+  // After creation, this must be called for all the disjunctive constraints
+  // in the model.
+  void AddNoOverlap(const std::vector<IntervalVariable>& var);
+
+  bool Propagate() final;
+
+ private:
+  AllIntervalsHelper* helper_;
+  std::vector<std::vector<int>> task_to_disjunctives_;
+  std::vector<bool> task_is_added_;
+  std::vector<TaskSet> task_sets_;
+  std::vector<IntegerValue> end_mins_;
+};
+
 class DisjunctiveNotLast : public PropagatorInterface {
  public:
   DisjunctiveNotLast(bool time_direction, SchedulingConstraintHelper* helper)

ortools/sat/intervals.h

@@ -92,6 +92,15 @@ class IntervalsRepository {
     return integer_trail_->UpperBound(size_var);
   }
 
+  // Utility function that returns a vector will all intervals.
+  std::vector<IntervalVariable> AllIntervals() const {
+    std::vector<IntervalVariable> result;
+    for (IntervalVariable i(0); i < NumIntervals(); ++i) {
+      result.push_back(i);
+    }
+    return result;
+  }
+
  private:
   // External classes needed.
   IntegerTrail* integer_trail_;
@@ -396,6 +405,7 @@ inline void SchedulingConstraintHelper::ClearReason() {
 }
 
 inline void SchedulingConstraintHelper::AddPresenceReason(int t) {
+  DCHECK(IsPresent(t));
   AddOtherReason(t);
   if (reason_for_presence_[t] != kNoLiteralIndex) {
     literal_reason_.push_back(Literal(reason_for_presence_[t]).Negated());

ortools/sat/linear_programming_constraint.cc

@@ -637,22 +637,24 @@ void LinearProgrammingConstraint::UpdateSimplexIterationLimit(
   if (sat_parameters_.linearization_level() < 2) return;
   const int64 num_degenerate_columns = CalculateDegeneracy();
   const int64 num_cols = simplex_.GetProblemNumCols().value();
+  if (num_cols <= 0) {
+    return;
+  }
+  CHECK_GT(num_cols, 0);
   const bool is_degenerate = num_degenerate_columns >= 0.3 * num_cols;
-  const int64 decrease_factor = 10 * num_degenerate_columns / num_cols;
+  const int64 decrease_factor = (10 * num_degenerate_columns) / num_cols;
   if (simplex_.GetProblemStatus() == glop::ProblemStatus::DUAL_FEASIBLE) {
     // We reached here probably because we predicted wrong. We use this as a
     // signal to increase the iterations or punish less for degeneracy compare
     // to the other part.
-    // TODO(user): Derive a formula to update the limit using degeneracy to
-    // simplify the code.
     if (is_degenerate) {
-      next_simplex_iter_ /= decrease_factor;
+      next_simplex_iter_ /= std::max(1LL, decrease_factor);
     } else {
       next_simplex_iter_ *= 2;
     }
   } else if (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL) {
     if (is_degenerate) {
-      next_simplex_iter_ /= 2 * decrease_factor;
+      next_simplex_iter_ /= std::max(1LL, 2 * decrease_factor);
     } else {
       // This is the most common case. We use the size of the problem to
       // determine the limit and ignore the previous limit.

ortools/sat/sat_parameters.proto

@@ -21,7 +21,7 @@ option java_multiple_files = true;
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 133
+// NEXT TAG: 134
 message SatParameters {
   // ==========================================================================
   // Branching and polarity
@@ -712,6 +712,11 @@ message SatParameters {
   // numerical imprecision issues.
   optional bool use_exact_lp_reason = 109 [default = true];
 
+  // This can be beneficial if there is a lot of no-overlap constraints but a
+  // relatively low number of different intervals in the problem. Like 1000
+  // intervals, but 1M intervals in the no-overlap constraints covering them.
+  optional bool use_combined_no_overlap = 133 [default = false];
+
   // ==========================================================================
   // MIP -> CP-SAT (i.e. IP with integer coeff) conversion parameters that are
   // used by our automatic "scaling" algorithm.

ortools/util/random_engine.h

@@ -20,7 +20,7 @@
 
 namespace operations_research {
 
-using random_engine_t = std::default_random_engine;
+using random_engine_t = std::mt19937;
 
 }  // namespace operations_research