diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 273a0f8965..a5e1bcca24 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -869,7 +869,8 @@ struct VectorHash { } // namespace void BinaryImplicationGraph::TransformIntoMaxCliques( - std::vector>* at_most_ones) { + std::vector>* 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)" + : ""); } } diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index 86d78c474d..6c57bb7d08 100644 --- a/ortools/sat/clause.h +++ b/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>* at_most_ones); + void TransformIntoMaxCliques(std::vector>* 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_; } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 059990064a..1acf17f9ed 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/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()->MergeWithGlobalTimeLimit(global_time_limit); + *(model.GetOrCreate()) = options.parameters; + model.GetOrCreate()->MergeWithGlobalTimeLimit(options.time_limit); auto* encoder = model.GetOrCreate(); encoder->DisableImplicationBetweenLiteral(); auto* mapping = model.GetOrCreate(); @@ -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> var_constraint_pair_already_called; // The queue of "active" constraints, initialized to all of them. + TimeLimit* time_limit = options.time_limit; std::vector in_queue(context->working_model->constraints_size(), true); std::deque 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 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 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... diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 27f0a1ba87..93bc995fcd 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -257,7 +257,7 @@ NonOverlappingRectanglesDisjunctivePropagator:: y_(y->NumTasks(), model), strict_(strict), watcher_(model->GetOrCreate()), - overload_checker_(true, &x_), + overload_checker_(&x_), forward_detectable_precedences_(true, &x_), backward_detectable_precedences_(false, &x_), forward_not_last_(true, &x_), diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index 367e5b1580..9a7c091cc2 100644 --- a/ortools/sat/disjunctive.cc +++ b/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 Disjunctive( return; } + auto* watcher = model->GetOrCreate(); + const auto& sat_parameters = *model->GetOrCreate(); + if (vars.size() > 2 && sat_parameters.use_combined_no_overlap()) { + model->GetOrCreate>()->AddNoOverlap(vars); + model->GetOrCreate>()->AddNoOverlap(vars); + return; + } + SchedulingConstraintHelper* helper = new SchedulingConstraintHelper(vars, model); model->TakeOwnership(helper); - GenericLiteralWatcher* watcher = - model->GetOrCreate(); + + // Experiments to use the timetable only to propagate the disjunctive. + if (/*DISABLES_CODE*/ (false)) { + const IntegerVariable capacity = model->Add(ConstantIntegerVariable(1)); + std::vector demands(vars.size(), capacity); + TimeTablingPerTask* timetable = new TimeTablingPerTask( + demands, capacity, model->GetOrCreate(), helper); + timetable->RegisterWith(watcher); + model->TakeOwnership(timetable); + return; + } if (vars.size() == 2) { DisjunctiveWithTwoItems* propagator = new DisjunctiveWithTwoItems(helper); @@ -63,7 +81,7 @@ std::function 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 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() - ->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(), @@ -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 +CombinedDisjunctive::CombinedDisjunctive(Model* model) + : helper_(model->GetOrCreate()) { + helper_->SetTimeDirection(time_direction); + task_to_disjunctives_.resize(helper_->NumTasks()); + + auto* watcher = model->GetOrCreate(); + const int id = watcher->Register(this); + helper_->WatchAllTasks(id, watcher, /*watch_start_max=*/true, + /*watch_end_max=*/false); + watcher->NotifyThatPropagatorMayNotReachFixedPointInOnePass(id); +} + +template +void CombinedDisjunctive::AddNoOverlap( + const std::vector& 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 CombinedDisjunctive::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& 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& 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& 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); diff --git a/ortools/sat/disjunctive.h b/ortools/sat/disjunctive.h index 36ab91ee10..7cbe60965e 100644 --- a/ortools/sat/disjunctive.h +++ b/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& SortedTasks() const { return sorted_tasks_; } private: std::vector 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 window_; @@ -163,11 +167,45 @@ class DisjunctiveDetectablePrecedences : public PropagatorInterface { std::vector window_; std::vector task_by_increasing_start_max_; + std::vector processed_; + std::vector 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()->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 +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& var); + + bool Propagate() final; + + private: + AllIntervalsHelper* helper_; + std::vector> task_to_disjunctives_; + std::vector task_is_added_; + std::vector task_sets_; + std::vector end_mins_; +}; + class DisjunctiveNotLast : public PropagatorInterface { public: DisjunctiveNotLast(bool time_direction, SchedulingConstraintHelper* helper) diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h index b707068b30..0c7bdc9704 100644 --- a/ortools/sat/intervals.h +++ b/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 AllIntervals() const { + std::vector 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()); diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 4ef09f4b8d..e50e0dabbd 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/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. diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index a90f491114..c37e414b02 100644 --- a/ortools/sat/sat_parameters.proto +++ b/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. diff --git a/ortools/util/random_engine.h b/ortools/util/random_engine.h index fa7ba2c49d..edd9e72b6b 100644 --- a/ortools/util/random_engine.h +++ b/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