[CP-SAT] extensive work on scheduling; add new cumulative with profil…

…e example

ortools/sat/clause.cc

@@ -504,50 +504,51 @@ void BinaryImplicationGraph::Resize(int num_variables) {
 }
 
 // TODO(user): Not all of the solver knows about representative literal, do
-// use them here and in AddBinaryClauseDuringSearch() to maintains invariant?
-// Explore this when we start cleaning our clauses using equivalence during
-// search. We can easily do it for every conflict we learn instead of here.
-void BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
+// use them here to maintains invariant? Explore this when we start cleaning our
+// clauses using equivalence during search. We can easily do it for every
+// conflict we learn instead of here.
+bool BinaryImplicationGraph::AddBinaryClause(Literal a, Literal b) {
   SCOPED_TIME_STAT(&stats_);
+
+  // Tricky: If this is the first clause, the propagator will be added and
+  // assumed to be in a "propagated" state. This makes sure this is the case.
+  if (IsEmpty()) propagation_trail_index_ = trail_->Index();
+
   if (drat_proof_handler_ != nullptr) {
     // TODO(user): Like this we will duplicate all binary clause from the
     // problem. However this leads to a simpler API (since we don't need to
     // special case the loading of the original clauses) and we mainly use drat
     // proof for testing anyway.
     drat_proof_handler_->AddClause({a, b});
   }
+
   estimated_sizes_[a.NegatedIndex()]++;
   estimated_sizes_[b.NegatedIndex()]++;
   implications_[a.NegatedIndex()].push_back(b);
   implications_[b.NegatedIndex()].push_back(a);
   is_dag_ = false;
   num_implications_ += 2;
-}
-
-bool BinaryImplicationGraph::AddBinaryClauseDuringSearch(Literal a, Literal b) {
-  SCOPED_TIME_STAT(&stats_);
-
-  // Tricky: If this is the first clause, the propagator will be added and
-  // assumed to be in a "propagated" state. This makes sure this is the case.
-  if (IsEmpty()) propagation_trail_index_ = trail_->Index();
-
-  AddBinaryClause(a, b);
 
   const auto& assignment = trail_->Assignment();
-  if (assignment.LiteralIsFalse(a)) {
-    if (assignment.LiteralIsAssigned(b)) {
-      if (assignment.LiteralIsFalse(b)) return false;
-    } else {
-      reasons_[trail_->Index()] = a;
-      trail_->Enqueue(b, propagator_id_);
-    }
-  } else if (assignment.LiteralIsFalse(b)) {
-    if (!assignment.LiteralIsAssigned(a)) {
-      reasons_[trail_->Index()] = b;
-      trail_->Enqueue(a, propagator_id_);
+  if (trail_->CurrentDecisionLevel() == 0) {
+    CHECK(!assignment.LiteralIsAssigned(a));
+    CHECK(!assignment.LiteralIsAssigned(b));
+  } else {
+    if (assignment.LiteralIsFalse(a)) {
+      if (assignment.LiteralIsAssigned(b)) {
+        if (assignment.LiteralIsFalse(b)) return false;
+      } else {
+        reasons_[trail_->Index()] = a;
+        trail_->Enqueue(b, propagator_id_);
+      }
+    } else if (assignment.LiteralIsFalse(b)) {
+      if (!assignment.LiteralIsAssigned(a)) {
+        reasons_[trail_->Index()] = b;
+        trail_->Enqueue(a, propagator_id_);
+      }
     }
   }
-  is_dag_ = false;
+
   return true;
 }
 

ortools/sat/clause.h

@@ -488,18 +488,19 @@ class BinaryImplicationGraph : public SatPropagator {
 
   // Adds the binary clause (a OR b), which is the same as (not a => b).
   // Note that it is also equivalent to (not b => a).
-  void AddBinaryClause(Literal a, Literal b);
-  void AddImplication(Literal a, Literal b) {
+  //
+  // Preconditions:
+  // - If we are at root node, then none of the literal should be assigned.
+  //   This is Checked and is there to track inefficiency as we do not need a
+  //   clause in this case.
+  // - If we are at a positive decision level, we will propagate something if
+  //   we can. However, if both literal are false, we will just return false
+  //   and do nothing. In all other case, we will return true.
+  bool AddBinaryClause(Literal a, Literal b);
+  bool AddImplication(Literal a, Literal b) {
     return AddBinaryClause(a.Negated(), b);
   }
 
-  // Same as AddBinaryClause() but enqueues a possible unit propagation. Note
-  // that if the binary clause propagates, it must do so at the last level, this
-  // is DCHECKed.
-  //
-  // Return false and do nothing if both a and b are currently false.
-  bool AddBinaryClauseDuringSearch(Literal a, Literal b);
-
   // An at most one constraint of size n is a compact way to encode n * (n - 1)
   // implications. This must only be called at level zero.
   //

ortools/sat/cp_model_loader.cc

@@ -1535,16 +1535,7 @@ void LoadLinMaxConstraint(const ConstraintProto& ct, Model* m) {
 
 void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m) {
   auto* mapping = m->GetOrCreate<CpModelMapping>();
-  auto* params = m->GetOrCreate<SatParameters>();
-  const int num_intervals = ct.no_overlap().intervals_size();
-  if (num_intervals <=
-          params->max_size_to_create_precedence_literals_in_disjunctive() &&
-      params->use_strong_propagation_in_disjunctive()) {
-    AddDisjunctiveWithBooleanPrecedences(
-        mapping->Intervals(ct.no_overlap().intervals()), m);
-  } else {
-    m->Add(Disjunctive(mapping->Intervals(ct.no_overlap().intervals())));
-  }
+  AddDisjunctive(mapping->Intervals(ct.no_overlap().intervals()), m);
 }
 
 void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m) {

ortools/sat/cp_model_presolve.h

@@ -16,6 +16,7 @@
 
 #include <array>
 #include <cstdint>
+#include <deque>
 #include <utility>
 #include <vector>
 

ortools/sat/cp_model_search.cc

@@ -342,7 +342,17 @@ std::function<BooleanOrIntegerLiteral()> ConstructUserSearchStrategy(
 std::function<BooleanOrIntegerLiteral()> ConstructHeuristicSearchStrategy(
     const CpModelProto& cp_model_proto, Model* model) {
   if (ModelHasSchedulingConstraints(cp_model_proto)) {
-    return SchedulingSearchHeuristic(model);
+    if (model->GetOrCreate<SatParameters>()
+            ->use_dynamic_precedence_in_disjunctive()) {
+      // We combine the two, because the precedence only work for disjunctive,
+      // and not if we only have cumulative constraints.
+      return SequentialSearch({SchedulingPrecedenceSearchHeuristic(model),
+                               SchedulingSearchHeuristic(model)});
+    } else {
+      // Precedence based model seems better, but the other one lead to faster
+      // solution.
+      return SchedulingSearchHeuristic(model);
+    }
   }
   return PseudoCost(model);
 }
@@ -616,6 +626,7 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
     strategies["auto"] = new_params;
 
     new_params.set_search_branching(SatParameters::FIXED_SEARCH);
+    new_params.set_use_dynamic_precedence_in_disjunctive(false);
     strategies["fixed"] = new_params;
   }
 

ortools/sat/cp_model_solver.cc

@@ -126,6 +126,11 @@ ABSL_FLAG(bool, cp_model_dump_models, false,
           "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|"
           "mapping_model}.pb.txt.");
 
+ABSL_FLAG(
+    bool, cp_model_export_model, false,
+    "DEBUG ONLY. When set to true, SolveCpModel() will dump its input model "
+    "protos in text format to 'FLAGS_cp_model_dump_prefix'{name}.pb.txt.");
+
 ABSL_FLAG(bool, cp_model_dump_text_proto, true,
           "DEBUG ONLY, dump models in text proto instead of binary proto.");
 
@@ -194,7 +199,7 @@ std::string Summarize(absl::string_view input) {
 }
 
 template <class M>
-void DumpModelProto(const M& proto, const std::string& name) {
+void DumpModelProto(const M& proto, absl::string_view name) {
   std::string filename;
   if (absl::GetFlag(FLAGS_cp_model_dump_text_proto)) {
     filename = absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), name,
@@ -1736,7 +1741,7 @@ void LoadCpModel(const CpModelProto& model_proto, Model* model) {
     // Report the initial objective variable bounds.
     auto* integer_trail = model->GetOrCreate<IntegerTrail>();
     shared_response_manager->UpdateInnerObjectiveBounds(
-        absl::StrCat(model->Name(), " initial_propagation"),
+        absl::StrCat(model->Name(), " (initial_propagation)"),
         integer_trail->LowerBound(objective_var),
         integer_trail->UpperBound(objective_var));
 
@@ -1858,6 +1863,13 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, Model* model) {
     }
   };
 
+  // Make sure we are not at a postive level.
+  if (!model->GetOrCreate<SatSolver>()->ResetToLevelZero()) {
+    shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
+        model->Name());
+    return;
+  }
+
   // Reconfigure search heuristic if it was changed.
   ConfigureSearchHeuristics(model);
 
@@ -2788,8 +2800,8 @@ class ObjectiveShavingSolver : public SubSolver {
 
  private:
   std::string Info() {
-    return absl::StrCat(name(), " #vars=", local_proto_.variables().size(),
-                        " #csts=", local_proto_.constraints().size());
+    return absl::StrCat(name(), " (vars=", local_proto_.variables().size(),
+                        " csts=", local_proto_.constraints().size(), ")");
   }
 
   bool ResetModel() {
@@ -3082,7 +3094,7 @@ class LnsSolver : public SubSolver {
           static_cast<double>(generator_->num_fully_solved_calls()) /
           static_cast<double>(num_calls);
       const std::string lns_info = absl::StrFormat(
-          "%s(d=%0.2f s=%i t=%0.2f p=%0.2f stall=%d h=%s)", source_info,
+          "%s (d=%0.2f s=%i t=%0.2f p=%0.2f stall=%d h=%s)", source_info,
           data.difficulty, task_id, data.deterministic_limit,
           fully_solved_proportion, stall, search_info);
 
@@ -3991,6 +4003,13 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
     DumpModelProto(model_proto, "model");
   }
+  if (absl::GetFlag(FLAGS_cp_model_export_model)) {
+    if (model_proto.name().empty()) {
+      DumpModelProto(model_proto, "unnamed_model");
+    } else {
+      DumpModelProto(model_proto, model_proto.name());
+    }
+  }
 #endif  // __PORTABLE_PLATFORM__
 
 #if !defined(__PORTABLE_PLATFORM__)

ortools/sat/cumulative.cc

@@ -143,7 +143,7 @@ std::function<void(Model*)> Cumulative(
       //
       // TODO(user): A better place for stuff like this could be in the
       // presolver so that it is easier to disable and play with alternatives.
-      if (in_disjunction.size() > 1) model->Add(Disjunctive(in_disjunction));
+      if (in_disjunction.size() > 1) AddDisjunctive(in_disjunction, model);
       if (in_disjunction.size() == vars.size()) return;
     }
 

ortools/sat/diffn.cc

@@ -283,12 +283,8 @@ NonOverlappingRectanglesDisjunctivePropagator::
       x_(x->NumTasks(), model),
       watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
       overload_checker_(&x_),
-      forward_detectable_precedences_(
-          true, model->GetOrCreate<PrecedenceRelations>(),
-          model->GetOrCreate<PrecedencesPropagator>(), &x_),
-      backward_detectable_precedences_(
-          false, model->GetOrCreate<PrecedenceRelations>(),
-          model->GetOrCreate<PrecedencesPropagator>(), &x_),
+      forward_detectable_precedences_(true, &x_),
+      backward_detectable_precedences_(false, &x_),
       forward_not_last_(true, &x_),
       backward_not_last_(false, &x_),
       forward_edge_finding_(true, &x_),