[CP-SAT] limit effort in feasibility_jump; new experimental scheduling search on cumulative

Author: lperron

ortools/sat/feasibility_jump.cc

@@ -508,7 +508,8 @@ std::function<void()> FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) {
 
 double FeasibilityJumpSolver::ComputeScore(absl::Span<const double> weights,
                                            int var, int64_t delta,
-                                           bool linear_only) const {
+                                           bool linear_only) {
+  ++num_scores_computed_;
   constexpr double kEpsilon = 1.0 / std::numeric_limits<int64_t>::max();
   double score =
       evaluator_->LinearEvaluator().WeightedViolationDelta(weights, var, delta);
@@ -818,10 +819,9 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() {
   RecomputeVarsToScan(general_jumps_);
   InitializeCompoundWeights();
   auto effort = [&]() {
-    return num_general_evals_ + num_linear_evals_ + num_weight_updates_ +
-           num_general_moves_;
+    return num_scores_computed_ + num_weight_updates_ + num_general_moves_;
   };
-  const int64_t effort_limit = effort() + 20000;
+  const int64_t effort_limit = effort() + 100000;
   while (effort() < effort_limit) {
     int var;
     int64_t value;

ortools/sat/feasibility_jump.h

@@ -165,7 +165,7 @@ class FeasibilityJumpSolver : public SubSolver {
 
   // Returns the weighted violation delta plus epsilon * the objective delta.
   double ComputeScore(absl::Span<const double> weights, int var, int64_t delta,
-                      bool linear_only) const;
+                      bool linear_only);
 
   // Computes the optimal value for variable v, considering only the violation
   // of linear constraints.
@@ -303,6 +303,7 @@ class FeasibilityJumpSolver : public SubSolver {
   int64_t num_restarts_ = 0;
   int64_t num_solutions_imported_ = 0;
   int64_t num_weight_updates_ = 0;
+  int64_t num_scores_computed_ = 0;
 
   std::unique_ptr<CompoundMoveBuilder> move_;
 

ortools/sat/integer_search.cc

@@ -679,7 +679,8 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
   auto* repo = model->GetOrCreate<IntervalsRepository>();
   auto* integer_trail = model->GetOrCreate<IntegerTrail>();
   auto* trail = model->GetOrCreate<Trail>();
-  return [repo, integer_trail, trail]() {
+  auto* search_helper = model->GetOrCreate<IntegerSearchHelper>();
+  return [repo, integer_trail, trail, search_helper]() {
     SchedulingConstraintHelper* best_helper = nullptr;
     int best_before = 0;
     int best_after = 0;
@@ -715,6 +716,7 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
         // Set their demand to zero.
         while (next_end < num_tasks && by_emin[next_end].time == time) {
           const int t = by_emin[next_end].task_index;
+          if (!helper->IsPresent(t)) continue;
           if (added_demand[t] > 0) {
             current_height -= added_demand[t];
             added_demand[t] = 0;
@@ -730,6 +732,7 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
         // TODO(user): tie-break tasks not fitting in the profile smartly.
         while (next_start < num_tasks && by_smin[next_start].time == time) {
           const int t = by_smin[next_start].task_index;
+          if (!helper->IsPresent(t)) continue;
           if (added_demand[t] == -1) continue;  // Corner case.
           const IntegerValue demand_min = h.demand_helper->DemandMin(t);
           if (current_height + demand_min <= capacity_max) {
@@ -763,6 +766,9 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
       }
       open_tasks.push_back(first_skipped_task);
 
+      // TODO(user): If the two box cannot overlap because of high demand, use
+      // repo.CreateDisjunctivePrecedenceLiteral() instead.
+      //
       // TODO(user): Add heuristic ordering for creating interesting precedence
       // first.
       bool found_precedence_to_add = false;
@@ -817,10 +823,29 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
       //
       // TODO(user): We need to add the reason for demand_min and capacity_max.
       // TODO(user): unfortunately we can't report it from here.
+      std::vector<IntegerLiteral> integer_reason;
+      if (!h.capacity.IsConstant()) {
+        integer_reason.push_back(
+            integer_trail->UpperBoundAsLiteral(h.capacity));
+      }
+      const auto& demands = h.demand_helper->Demands();
+      for (const int t : open_tasks) {
+        if (helper->IsOptional(t)) {
+          CHECK(trail->Assignment().LiteralIsTrue(helper->PresenceLiteral(t)));
+          conflict.push_back(helper->PresenceLiteral(t).Negated());
+        }
+        const AffineExpression d = demands[t];
+        if (!d.IsConstant()) {
+          integer_reason.push_back(integer_trail->LowerBoundAsLiteral(d));
+        }
+      }
+      integer_trail->ReportConflict(conflict, integer_reason);
+      search_helper->NotifyThatConflictWasFoundDuringGetDecision();
       if (VLOG_IS_ON(2)) {
         LOG(INFO) << "Conflict between precedences !";
         for (const int t : open_tasks) LOG(INFO) << helper->TaskDebugString(t);
       }
+      return BooleanOrIntegerLiteral();
     }
 
     // TODO(user): add heuristic criteria, right now we stop at first
@@ -1252,9 +1277,9 @@ bool IntegerSearchHelper::BeforeTakingDecision() {
   return true;
 }
 
-LiteralIndex IntegerSearchHelper::GetDecision(
-    const std::function<BooleanOrIntegerLiteral()>& f) {
-  LiteralIndex decision = kNoLiteralIndex;
+bool IntegerSearchHelper::GetDecision(
+    const std::function<BooleanOrIntegerLiteral()>& f, LiteralIndex* decision) {
+  *decision = kNoLiteralIndex;
   while (!time_limit_->LimitReached()) {
     BooleanOrIntegerLiteral new_decision;
     if (integer_trail_->InPropagationLoop()) {
@@ -1267,6 +1292,12 @@ LiteralIndex IntegerSearchHelper::GetDecision(
     }
     if (!new_decision.HasValue()) {
       new_decision = f();
+      if (must_process_conflict_) {
+        must_process_conflict_ = false;
+        sat_solver_->ProcessCurrentConflict();
+        (void)sat_solver_->FinishPropagation();
+        return false;
+      }
     }
     if (!new_decision.HasValue() &&
         integer_trail_->CurrentBranchHadAnIncompletePropagation()) {
@@ -1283,13 +1314,13 @@ LiteralIndex IntegerSearchHelper::GetDecision(
     // until we have a conflict with these decisions, but it is currently
     // hard to do so.
     if (new_decision.boolean_literal_index != kNoLiteralIndex) {
-      decision = new_decision.boolean_literal_index;
+      *decision = new_decision.boolean_literal_index;
     } else {
-      decision =
+      *decision =
           encoder_->GetOrCreateAssociatedLiteral(new_decision.integer_literal)
               .Index();
     }
-    if (sat_solver_->Assignment().LiteralIsAssigned(Literal(decision))) {
+    if (sat_solver_->Assignment().LiteralIsAssigned(Literal(*decision))) {
       // TODO(user): It would be nicer if this can never happen. For now, it
       // does because of the Propagate() not reaching the fixed point as
       // mentioned in a TODO above. As a work-around, we display a message
@@ -1300,7 +1331,7 @@ LiteralIndex IntegerSearchHelper::GetDecision(
     }
     break;
   }
-  return decision;
+  return true;
 }
 
 bool IntegerSearchHelper::TakeDecision(Literal decision) {
@@ -1382,17 +1413,22 @@ SatSolver::Status IntegerSearchHelper::SolveIntegerProblem() {
 
     LiteralIndex decision = kNoLiteralIndex;
     while (true) {
+      if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus();
       if (heuristics.next_decision_override != nullptr) {
         // Note that to properly count the num_times, we do not want to move
         // this function, but actually call that copy.
-        decision = GetDecision(heuristics.next_decision_override);
+        if (!GetDecision(heuristics.next_decision_override, &decision)) {
+          continue;
+        }
         if (decision == kNoLiteralIndex) {
           heuristics.next_decision_override = nullptr;
         }
       }
       if (decision == kNoLiteralIndex) {
-        decision =
-            GetDecision(heuristics.decision_policies[heuristics.policy_index]);
+        if (!GetDecision(heuristics.decision_policies[heuristics.policy_index],
+                         &decision)) {
+          continue;
+        }
       }
 
       // Probing?

ortools/sat/integer_search.h

@@ -271,7 +271,16 @@ class IntegerSearchHelper {
 
   // Calls the decision heuristics and extract a non-fixed literal.
   // Note that we do not want to copy the function here.
-  LiteralIndex GetDecision(const std::function<BooleanOrIntegerLiteral()>& f);
+  //
+  // Returns false if a conflict was found while trying to take a decision.
+  bool GetDecision(const std::function<BooleanOrIntegerLiteral()>& f,
+                   LiteralIndex* decision);
+
+  // Functions passed to GetDecision() might call this to notify a conflict
+  // was detected.
+  void NotifyThatConflictWasFoundDuringGetDecision() {
+    must_process_conflict_ = true;
+  }
 
   // Tries to take the current decision, this might backjump.
   // Returns false if the model is UNSAT.
@@ -301,6 +310,8 @@ class IntegerSearchHelper {
   TimeLimit* time_limit_;
   PseudoCosts* pseudo_costs_;
   IntegerVariable objective_var_ = kNoIntegerVariable;
+
+  bool must_process_conflict_ = false;
 };
 
 // This class will loop continuously on model variables and try to probe/shave

ortools/sat/intervals.cc

@@ -127,8 +127,9 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral(
   disjunctive_precedences_.insert({{b, a}, a_before_b.Negated()});
 
   // Also insert it in precedences.
-  precedences_.insert({{a, b}, a_before_b});
-  precedences_.insert({{b, a}, a_before_b.Negated()});
+  // TODO(user): also add the reverse like start_b + 1 <= end_a if negated?
+  precedences_.insert({{end_a, start_b}, a_before_b});
+  precedences_.insert({{end_b, start_a}, a_before_b.Negated()});
 
   enforcement_literals.push_back(a_before_b);
   AddConditionalAffinePrecedence(enforcement_literals, end_a, start_b, model_);
@@ -147,12 +148,12 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral(
 
 bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
                                                   IntervalVariable b) {
-  if (precedences_.find({a, b}) != disjunctive_precedences_.end()) return false;
+  const AffineExpression x = End(a);
+  const AffineExpression y = Start(b);
+  if (precedences_.find({x, y}) != precedences_.end()) return false;
 
   // We want l => x <= y and not(l) => x > y <=> y + 1 <= x
   // Do not create l if the relation is always true or false.
-  const AffineExpression x = End(a);
-  const AffineExpression y = Start(b);
   if (integer_trail_->UpperBound(x) <= integer_trail_->LowerBound(y)) {
     return false;
   }
@@ -163,7 +164,9 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
   // Create a new literal.
   const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
   const Literal x_before_y = Literal(boolean_var, true);
-  precedences_.insert({{a, b}, x_before_y});
+
+  // TODO(user): Also add {{y_plus_one, x}, x_before_y.Negated()} ?
+  precedences_.insert({{x, y}, x_before_y});
 
   AffineExpression y_plus_one = y;
   y_plus_one.constant += 1;
@@ -174,7 +177,9 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a,
 
 LiteralIndex IntervalsRepository::GetPrecedenceLiteral(
     IntervalVariable a, IntervalVariable b) const {
-  const auto it = precedences_.find({a, b});
+  const AffineExpression x = End(a);
+  const AffineExpression y = Start(b);
+  const auto it = precedences_.find({x, y});
   if (it != precedences_.end()) return it->second.Index();
   return kNoLiteralIndex;
 }

ortools/sat/intervals.h

@@ -241,9 +241,13 @@ class IntervalsRepository {
       demand_helper_repository_;
 
   // Disjunctive and normal precedences.
+  //
+  // Note that for normal precedences, we use directly the affine expression so
+  // that if many intervals share the same start, we don't re-create Booleans
+  // for no reason.
   absl::flat_hash_map<std::pair<IntervalVariable, IntervalVariable>, Literal>
       disjunctive_precedences_;
-  absl::flat_hash_map<std::pair<IntervalVariable, IntervalVariable>, Literal>
+  absl::flat_hash_map<std::pair<AffineExpression, AffineExpression>, Literal>
       precedences_;
 
   // Disjunctive/Cumulative helpers_.

ortools/sat/lb_tree_search.cc

@@ -538,8 +538,11 @@ SatSolver::Status LbTreeSearch::Search(
     while (true) {
       // TODO(user): We sometimes branch on the objective variable, this should
       // probably be avoided.
-      const LiteralIndex decision =
-          search_helper_->GetDecision(search_heuristic_);
+      if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus();
+      LiteralIndex decision;
+      if (!search_helper_->GetDecision(search_heuristic_, &decision)) {
+        continue;
+      }
 
       // No new decision: search done.
       if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;

ortools/sat/sat_parameters.proto

@@ -745,9 +745,8 @@ message SatParameters {
 
   // Whether we try to branch on decision "interval A before interval B" rather
   // than on intervals bounds. This usually works better, but slow down a bit
-  // the time to find first solutions.
+  // the time to find the first solution.
   //
-  // Note that for cumulative, this currently seems worse.
   // These parameters are still EXPERIMENTAL, the result should be correct, but
   // it some corner cases, they can cause some failing CHECK in the solver.
   optional bool use_dynamic_precedence_in_disjunctive = 263 [default = false];

ortools/sat/sat_solver.cc

@@ -584,7 +584,8 @@ bool SatSolver::FinishPropagation() {
   int num_loop = 0;
   while (true) {
     const int old_decision_level = current_decision_level_;
-    if (!PropagateAndStopAfterOneConflictResolution()) {
+    if (!Propagate()) {
+      ProcessCurrentConflict();
       if (model_is_unsat_) return false;
       if (current_decision_level_ == old_decision_level) {
         CHECK(!assumptions_.empty());
@@ -682,10 +683,9 @@ bool SatSolver::ReapplyAssumptionsIfNeeded() {
   return (status == SatSolver::FEASIBLE);
 }
 
-bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
+void SatSolver::ProcessCurrentConflict() {
   SCOPED_TIME_STAT(&stats_);
-  if (Propagate()) return true;
-  if (model_is_unsat_) return false;
+  if (model_is_unsat_) return;
 
   ++counters_.num_failures;
   const int conflict_trail_index = trail_->Index();
@@ -703,15 +703,15 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
     // it reduces to only one literal in which case we can just fix it.
     const int highest_level =
         DecisionLevel((*trail_)[max_trail_index].Variable());
-    if (highest_level == 1) return false;
+    if (highest_level == 1) return;
   }
 
   ComputeFirstUIPConflict(max_trail_index, &learned_conflict_,
                           &reason_used_to_infer_the_conflict_,
                           &subsumed_clauses_);
 
   // An empty conflict means that the problem is UNSAT.
-  if (learned_conflict_.empty()) return SetModelUnsat();
+  if (learned_conflict_.empty()) return (void)SetModelUnsat();
   DCHECK(IsConflictValid(learned_conflict_));
   DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_));
 
@@ -789,7 +789,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
     int pb_backjump_level;
     ComputePBConflict(max_trail_index, initial_slack, &pb_conflict_,
                       &pb_backjump_level);
-    if (pb_backjump_level == -1) return SetModelUnsat();
+    if (pb_backjump_level == -1) return (void)SetModelUnsat();
 
     // Convert the conflict into the vector<LiteralWithCoeff> form.
     std::vector<LiteralWithCoeff> cst;
@@ -817,7 +817,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
                                                   trail_));
       CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_);
       counters_.num_learned_pb_literals += cst.size();
-      return false;
+      return;
     }
 
     // Continue with the normal clause flow, but use the PB conflict clause
@@ -941,7 +941,6 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() {
       learned_conflict_, is_redundant);
   restart_->OnConflict(conflict_trail_index, conflict_decision_level,
                        conflict_lbd);
-  return false;
 }
 
 SatSolver::Status SatSolver::ReapplyDecisionsUpTo(
@@ -1339,8 +1338,9 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit,
     }
 
     const int old_level = current_decision_level_;
-    if (!PropagateAndStopAfterOneConflictResolution()) {
+    if (!Propagate()) {
       // A conflict occurred, continue the loop.
+      ProcessCurrentConflict();
       if (model_is_unsat_) return StatusWithLog(INFEASIBLE);
       if (old_level == current_decision_level_) {
         CHECK(!assumptions_.empty());