From 83a434dc4756e1508041116ce2f7bdb7e747651e Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 6 Dec 2024 11:48:47 +0100 Subject: [PATCH] [CP-SAT] improve propagation; more hint preservation; polish last sample --- ortools/sat/cp_model_presolve.cc | 22 ++- ortools/sat/cp_model_solver.cc | 22 +-- ortools/sat/diffn.cc | 150 +++++++++++++----- ortools/sat/diffn.h | 5 + ortools/sat/docs/scheduling.md | 72 +++++---- ortools/sat/presolve_context.cc | 14 +- ortools/sat/presolve_context.h | 2 + .../sequences_in_no_overlap_sample_sat.py | 65 ++++---- ortools/sat/stat_tables.cc | 2 +- 9 files changed, 237 insertions(+), 117 deletions(-) diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index f377553a18..e562ab5b83 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -177,7 +177,7 @@ bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) { if (context_->VariableIsUniqueAndRemovable(literal)) { // We can simply set it to false and ignore the constraint in this case. context_->UpdateRuleStats("enforcement: literal not used"); - CHECK(context_->SetLiteralToFalse(literal)); + CHECK(context_->SetLiteralAndHintToFalse(literal)); return RemoveConstraint(ct); } @@ -190,7 +190,7 @@ bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) { if (RefIsPositive(literal) == (obj_coeff > 0)) { // It is just more advantageous to set it to false! context_->UpdateRuleStats("enforcement: literal with unique direction"); - CHECK(context_->SetLiteralToFalse(literal)); + CHECK(context_->SetLiteralAndHintToFalse(literal)); return RemoveConstraint(ct); } } @@ -346,7 +346,7 @@ bool CpModelPresolver::PresolveBoolOr(ConstraintProto* ct) { // objective var usage by 1). if (context_->VariableIsUniqueAndRemovable(literal)) { context_->UpdateRuleStats("bool_or: singleton"); - if (!context_->SetLiteralToTrue(literal)) return true; + if (!context_->SetLiteralAndHintToTrue(literal)) return true; return RemoveConstraint(ct); } if (context_->tmp_literal_set.contains(NegatedRef(literal))) { @@ -448,8 +448,7 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) { changed = true; context_->UpdateRuleStats( "bool_and: setting unused literal in rhs to true"); - context_->UpdateLiteralSolutionHint(literal, true); - if (!context_->SetLiteralToTrue(literal)) return true; + if (!context_->SetLiteralAndHintToTrue(literal)) return true; continue; } @@ -495,8 +494,15 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) { // The other case where the constraint is redundant is treated elsewhere. if (obj_coeff < 0) { context_->UpdateRuleStats("bool_and: dual equality."); - context_->StoreBooleanEqualityRelation(enforcement, - ct->bool_and().literals(0)); + // Extending `ct` = "enforcement => implied_literal" to an equality can + // break the hint only if hint(implied_literal) = 1 and + // hint(enforcement) = 0. But in this case the `enforcement` hint can be + // increased to 1 to preserve the hint feasibility. + const int implied_literal = ct->bool_and().literals(0); + if (context_->LiteralSolutionHintIs(implied_literal, true)) { + context_->UpdateLiteralSolutionHint(enforcement, true); + } + context_->StoreBooleanEqualityRelation(enforcement, implied_literal); } } } @@ -7758,7 +7764,7 @@ bool CpModelPresolver::PresolvePureSatPart() { // Such variable needs to be fixed to some value for the SAT postsolve to // work. if (!context_->IsFixed(var)) { - CHECK(context_->IntersectDomainWith( + CHECK(context_->IntersectDomainWithAndUpdateHint( var, Domain(context_->DomainOf(var).SmallestValue()))); } context_->MarkVariableAsRemoved(var); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 7803c64a5a..66872f24e2 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1271,7 +1271,7 @@ class LnsSolver : public SubSolver { static_cast(generator_->num_fully_solved_calls()) / static_cast(num_calls); const std::string lns_info = absl::StrFormat( - "%s (d=%0.3f s=%i t=%0.2f p=%0.2f stall=%d h=%s)", source_info, + "%s (d=%0.2e 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); @@ -1550,18 +1550,22 @@ class LnsSolver : public SubSolver { } if (neighborhood.is_simple) { absl::StrAppend( - &s, " [", "relaxed:", neighborhood.num_relaxed_variables, - " in_obj:", neighborhood.num_relaxed_variables_in_objective, + &s, " [", + "relaxed:", FormatCounter(neighborhood.num_relaxed_variables), + " in_obj:", + FormatCounter(neighborhood.num_relaxed_variables_in_objective), " compo:", neighborhood.variables_that_can_be_fixed_to_local_optimum.size(), "]"); } - SOLVER_LOG(shared_->logger, s, " [d:", data.difficulty, - ", id:", task_id, ", dtime:", data.deterministic_time, "/", - data.deterministic_limit, - ", status:", ProtoEnumToString(data.status), - ", #calls:", generator_->num_calls(), - ", p:", fully_solved_proportion, "]"); + SOLVER_LOG( + shared_->logger, s, + " [d:", absl::StrFormat("%0.2e", data.difficulty), ", id:", task_id, + ", dtime:", absl::StrFormat("%0.2f", data.deterministic_time), "/", + data.deterministic_limit, + ", status:", ProtoEnumToString(data.status), + ", #calls:", generator_->num_calls(), + ", p:", fully_solved_proportion, "]"); } }; } diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 06b01cca4a..bf5bd92300 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -706,56 +706,109 @@ bool NonOverlappingRectanglesDisjunctivePropagator:: FindBoxesThatMustOverlapAHorizontalLineAndPropagate( bool fast_propagation, SchedulingConstraintHelper* x, SchedulingConstraintHelper* y) { - // Note that since we only push bounds on x, we cache the value for y just - // once. - if (!y->SynchronizeAndSetTimeDirection(true)) return false; - - // Compute relevant boxes, the one with a mandatory part of y. Because we will + // When they are many fixed box that we know do not overlap, we compute + // the bounding box of the others, and we can exclude all boxes outside this + // region. This can help, especially for some LNS neighborhood. + int num_fixed = 0; + int num_others = 0; + Rectangle other_bounding_box; + + // push_back() can be slow as it might not be inlined, so we manage directly + // our "boxes" in boxes_data[0 .. num_boxes], with a memory that is always big + // enough. + indexed_boxes_.resize(y->NumTasks()); + int num_boxes = 0; + IndexedInterval* boxes_data = indexed_boxes_.data(); + + // Compute relevant boxes, the one with a mandatory part on y. Because we will // need to sort it this way, we consider them by increasing start max. - indexed_boxes_.clear(); const auto temp = y->TaskByIncreasingNegatedStartMax(); + auto fixed_boxes = already_checked_fixed_boxes_.view(); for (int i = temp.size(); --i >= 0;) { const int box = temp[i].task_index; - // Ignore absent boxes. - if (x->IsAbsent(box) || y->IsAbsent(box)) continue; - - // Ignore boxes where the relevant presence literal is only on the y - // dimension, or if both intervals are optionals with different literals. - if (x->IsPresent(box) && !y->IsPresent(box)) continue; - if (!x->IsPresent(box) && !y->IsPresent(box) && - x->PresenceLiteral(box) != y->PresenceLiteral(box)) { - continue; + + // By definition, fixed boxes are always present. + // Doing this check optimize a bit the case where we have many fixed boxes. + if (!fixed_boxes[box]) { + // Ignore absent boxes. + if (x->IsAbsent(box) || y->IsAbsent(box)) continue; + + // Ignore boxes where the relevant presence literal is only on the y + // dimension, or if both intervals are optionals with different literals. + if (x->IsPresent(box) && !y->IsPresent(box)) continue; + if (!x->IsPresent(box) && !y->IsPresent(box) && + x->PresenceLiteral(box) != y->PresenceLiteral(box)) { + continue; + } } + // Only consider box with a mandatory part on y. const IntegerValue start_max = -temp[i].time; const IntegerValue end_min = y->EndMin(box); if (start_max < end_min) { - indexed_boxes_.push_back({box, start_max, end_min}); + boxes_data[num_boxes++] = {box, start_max, end_min}; + + // Optim: If many rectangle are fixed and known not to overlap, we might + // filter them out. + if (fixed_boxes[box]) { + ++num_fixed; + } else { + const bool is_fixed = x->StartIsFixed(box) && x->EndIsFixed(box) && + y->StartIsFixed(box) && y->EndIsFixed(box); + if (is_fixed) { + // We will "check it" below, so it will be checked next time. + fixed_boxes.Set(box); + } + + const Rectangle r = {x->StartMin(box), x->EndMax(box), start_max, + end_min}; + if (num_others == 0) { + other_bounding_box = r; + } else { + other_bounding_box.GrowToInclude(r); + } + ++num_others; + } } } - // Less than 2 boxes, no propagation. - if (indexed_boxes_.size() < 2) return true; - - // In ConstructOverlappingSets() we will always sort the output by - // x.ShiftedStartMin(t). We want to speed that up so we cache the order here. - if (!x->SynchronizeAndSetTimeDirection(x->CurrentTimeIsForward())) { - return false; + // We remove from boxes_data all the fixed and checked box outside the + // other_bounding_box. + // + // TODO(user): We could be smarter here, if we have just a few non-fixed + // boxes, likely their mandatory y-part do not span the whole horizon, so + // we could remove any fixed boxes outside these "stripes". + if (num_others == 0) return true; + if (num_fixed > 0) { + int new_size = 0; + for (int i = 0; i < num_boxes; ++i) { + const IndexedInterval& interval = boxes_data[i]; + const int box = interval.index; + const Rectangle r = {x->StartMin(box), x->EndMax(box), interval.start, + interval.end}; + if (other_bounding_box.IsDisjoint(r)) continue; + boxes_data[new_size++] = interval; + } + num_boxes = new_size; } - // Optim: Abort if all rectangle can be fixed to their mandatory y + minimium - // x position without any overlap. Technically we might still propagate the x - // end in this setting, but the current code will just abort below in - // SplitDisjointBoxes() anyway. + // Less than 2 boxes, no propagation. + const auto boxes = absl::MakeSpan(boxes_data, num_boxes); + if (boxes.size() < 2) return true; + + // Optim: Abort if all rectangle can be fixed to their mandatory y + + // minimium x position without any overlap. // // This is guaranteed to be O(N log N) whereas the algo below is O(N ^ 2). - if (indexed_boxes_.size() > 100) { + // + // TODO(user): We might still propagate the x end in this setting, but the + // current code will just abort below in SplitDisjointBoxes() anyway. + { rectangles_.clear(); - rectangles_.reserve(indexed_boxes_.size()); - for (const auto [box, y_mandatory_start, y_mandatory_end] : - indexed_boxes_) { - // Note that we invert the x/y position here in order to be already sorted - // for FindOneIntersectionIfPresent() + rectangles_.reserve(boxes.size()); + for (const auto [box, y_mandatory_start, y_mandatory_end] : boxes) { + // Note that we invert the x/y position here in order to be already + // sorted for FindOneIntersectionIfPresent() rectangles_.push_back( {/*x_min=*/y_mandatory_start, /*x_max=*/y_mandatory_end, /*y_min=*/x->StartMin(box), /*y_max=*/x->EndMin(box)}); @@ -769,6 +822,8 @@ bool NonOverlappingRectanglesDisjunctivePropagator:: } if (opt_pair == std::nullopt) { return true; + } else { + // TODO(user): Test if we have a conflict here. } } @@ -779,13 +834,12 @@ bool NonOverlappingRectanglesDisjunctivePropagator:: order_[t] = i++; } } - ConstructOverlappingSets(absl::MakeSpan(indexed_boxes_), - &events_overlapping_boxes_, order_); + ConstructOverlappingSets(boxes, &events_overlapping_boxes_, order_); // Split lists of boxes into disjoint set of boxes (w.r.t. overlap). boxes_to_propagate_.clear(); reduced_overlapping_boxes_.clear(); - int work_done = indexed_boxes_.size(); + int work_done = boxes.size(); for (int i = 0; i < events_overlapping_boxes_.size(); ++i) { work_done += events_overlapping_boxes_[i].size(); SplitDisjointBoxes(*x, events_overlapping_boxes_[i], &disjoint_boxes_); @@ -803,10 +857,11 @@ bool NonOverlappingRectanglesDisjunctivePropagator:: // And finally propagate. // - // TODO(user): Sorting of boxes seems influential on the performance. Test. + // TODO(user): Sorting of boxes seems influential on the performance. + // Test. for (const absl::Span boxes : boxes_to_propagate_) { - // The case of two boxes should be taken care of during "fast" propagation, - // so we can skip it here. + // The case of two boxes should be taken care of during "fast" + // propagation, so we can skip it here. if (!fast_propagation && boxes.size() <= 2) continue; x_.ClearOtherHelper(); @@ -857,9 +912,22 @@ bool NonOverlappingRectanglesDisjunctivePropagator:: return true; } +// Note that we optimized this function for two main use cases: +// - smallish problem where we don't have more than 100 boxes. +// - large problem with many 1000s boxes, but with only a small subset that is +// not fixed (mainly coming from LNS). bool NonOverlappingRectanglesDisjunctivePropagator::Propagate() { - global_x_.SetTimeDirection(true); - global_y_.SetTimeDirection(true); + if (!global_x_.SynchronizeAndSetTimeDirection(true)) return false; + if (!global_y_.SynchronizeAndSetTimeDirection(true)) return false; + + // If we are "diving" we maintain the set of fixed boxes for which we know + // that they are not overlapping. + const bool backtrack_since_last_call = !rev_is_in_dive_; + watcher_->SetUntilNextBacktrack(&rev_is_in_dive_); + if (backtrack_since_last_call) { + const int num_tasks = global_x_.NumTasks(); + already_checked_fixed_boxes_.ClearAndResize(num_tasks); + } // Note that the code assumes that this was registered twice in fast and slow // mode. So we will not redo some propagation in slow mode that was already diff --git a/ortools/sat/diffn.h b/ortools/sat/diffn.h index e4bce580c0..d874af62bb 100644 --- a/ortools/sat/diffn.h +++ b/ortools/sat/diffn.h @@ -127,6 +127,11 @@ class NonOverlappingRectanglesDisjunctivePropagator std::vector order_; CompactVectorVector events_overlapping_boxes_; + // List of box that are fully fixed in the current dive, and for which we + // know they are no conflict between them. + bool rev_is_in_dive_ = false; + Bitset64 already_checked_fixed_boxes_; + absl::flat_hash_set> reduced_overlapping_boxes_; std::vector> boxes_to_propagate_; std::vector> disjoint_boxes_; diff --git a/ortools/sat/docs/scheduling.md b/ortools/sat/docs/scheduling.md index 58b205b681..89d62224aa 100644 --- a/ortools/sat/docs/scheduling.md +++ b/ortools/sat/docs/scheduling.md @@ -2612,9 +2612,12 @@ transitions_in_no_overlap_sample_sat() ## Managing sequences in a no_overlap constraint In some scheduling problems, there can be constraints on sequence of tasks. For -instance, tasks of a given type may have limit on any contiguous constraints. +instance, tasks of a given type may have limit on the min or max number of +contiguous tasks of the same type. -The circuit constraint is used to maintain the current length of any sequence. +The circuit constraint is used to constraint the length of any sequence of tasks +of the same type. It uses counters attached to each task, and transition +literals to maintain these counters. ### Python code @@ -2637,7 +2640,7 @@ def sequence_constraints_with_circuit( sequence_length_constraints: Dict[str, Tuple[int, int]], sequence_cumul_constraints: Dict[str, Tuple[int, int, int]], ) -> Sequence[Tuple[cp_model.IntVar, int]]: - """This method uses a circuit constraint to rank tasks. + """This method enforces constraints on sequences of tasks of the same type. This method assumes that all starts are disjoint, meaning that all tasks have a strictly positive duration, and they appear in the same NoOverlap @@ -2650,8 +2653,10 @@ def sequence_constraints_with_circuit( The circuit constraint ensures there is at most 1 hamiltonian cycle of length > 1. If no such path exists, then no tasks are active. - We also need to enforce that any hamiltonian cycle of size > 1 must contain - the node 0. And thus, there is a self loop on node 0 iff the circuit is empty. + In this simplified model, all tasks must be performed. + + Note that we do not enforce the minimum length constraint on the last sequence + of tasks of the same type. Args: model: The CpModel to add the constraints to. @@ -2660,13 +2665,13 @@ def sequence_constraints_with_circuit( task_types: The type of all tasks. lengths: The computed length of the current sequence for each task. cumuls: The computed cumul of the current sequence for each task. - sequence_length_constraints: the array of tuple (`task_type`, - (`length_min`, `length_max`)) that specifies the minimum and maximum - length of the sequence of tasks of type `task_type`. - sequence_cumul_constraints: the array of tuple (`task_type`, - (`soft_max`, `linear_penalty`, `hard_max`)) that specifies that if the - cumul of the sequence of tasks of type `task_type` is greater than - `soft_max`, then `linear_penalty` must be added to the cost + sequence_length_constraints: the array of tuple (`task_type`, (`length_min`, + `length_max`)) that specifies the minimum and maximum length of the + sequence of tasks of type `task_type`. + sequence_cumul_constraints: the array of tuple (`task_type`, (`soft_max`, + `linear_penalty`, `hard_max`)) that specifies that if the cumul of the + sequence of tasks of type `task_type` is greater than `soft_max`, then + `linear_penalty` must be added to the cost Returns: The list of pairs (Boolean variables, penalty) to be added to the objective. @@ -2685,7 +2690,7 @@ def sequence_constraints_with_circuit( model.add(cumuls[i] == durations[i]).only_enforce_if(start_lit) # As there are no other constraints on the problem, we can add this - # redundant constraint. + # redundant constraint. This is not valid in general. model.add(starts[i] == 0).only_enforce_if(start_lit) # if node i is last. @@ -2714,32 +2719,37 @@ def sequence_constraints_with_circuit( # In a non pure problem, the following equality must be an inequality. model.add(starts[j] == starts[i] + durations[i]).only_enforce_if(lit) - # We add the constraint to incrementally maintain the length and the cumul - # variables of the sequence. + # We add the constraints to incrementally maintain the length and the + # cumul variables of the sequence. if task_types[i] == task_types[j]: # Same task type. # Increase the length of the sequence by 1. model.add(lengths[j] == lengths[i] + 1).only_enforce_if(lit) - # Make sure the length of the sequence is within the bounds. - length_max = sequence_length_constraints[task_types[j]][1] - model.add(lengths[j] <= length_max).only_enforce_if(lit) + # Make sure the length of the sequence is within the bounds of the task + # type. + type_length_max = sequence_length_constraints[task_types[j]][1] + model.add(lengths[j] <= type_length_max).only_enforce_if(lit) # Increase the cumul of the sequence by the duration of the task. model.add(cumuls[j] == cumuls[i] + durations[j]).only_enforce_if(lit) # Make sure the cumul of the sequence is within the bounds. - cumul_hard_max = sequence_cumul_constraints[task_types[j]][2] - model.add(cumuls[j] <= cumul_hard_max).only_enforce_if(lit) + type_cumul_hard_max = sequence_cumul_constraints[task_types[j]][2] + model.add(cumuls[j] <= type_cumul_hard_max).only_enforce_if(lit) - else: # Switching task type. + else: + # Switching task type. task[i] is the last task of the previous + # sequence, task[j] is the first task of the new sequence. + # # Reset the length to 1. model.add(lengths[j] == 1).only_enforce_if(lit) # Make sure the previous length is within bounds. - length_min = sequence_length_constraints[task_types[i]][0] - model.add(lengths[i] >= length_min).only_enforce_if(lit) + type_length_min = sequence_length_constraints[task_types[i]][0] + model.add(lengths[i] >= type_length_min).only_enforce_if(lit) # Reset the cumul to the duration of the task. + # Note we do not check that the duration of the task is within bounds. model.add(cumuls[j] == durations[j]).only_enforce_if(lit) # Penalize the cumul of the previous task w.r.t. the soft max @@ -2778,13 +2788,13 @@ def sequences_in_no_overlap_sample_sat(): (2, "B"), ] - # Sequence length constraints on task_types: (hard_min, hard_max) + # Sequence length constraints per task_types: (hard_min, hard_max) sequence_length_constraints = { "A": (1, 3), "B": (2, 2), } - # Sequence cumul constraints on task_types: + # Sequence accumulated durations constraints per task_types: # (soft_max, linear_penalty, hard_max) sequence_cumul_constraints = { "A": (6, 1, 10), @@ -2830,8 +2840,8 @@ def sequences_in_no_overlap_sample_sat(): # Adds NoOverlap constraint. model.add_no_overlap(intervals) - # Adds the constraints on the partial lengths and cumuls of the sequence of - # tasks. + # Adds the constraints on the lengths and cumuls of maximal sequences of + # tasks of the same type. penalty_terms = sequence_constraints_with_circuit( model, starts, @@ -2852,7 +2862,11 @@ def sequences_in_no_overlap_sample_sat(): if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE: # Prints out the makespan and the start times and ranks of all tasks. - print(f"Optimal cost: {solver.objective_value}") + if status == cp_model.OPTIMAL: + print(f"Optimal cost: {solver.objective_value}") + else: + print(f"Feasible cost: {solver.objective_value}") + to_sort = [] for t in all_tasks: to_sort.append((solver.value(starts[t]), t)) @@ -2864,7 +2878,7 @@ def sequences_in_no_overlap_sample_sat(): f" {solver.value(lengths[t])}, cumul = {solver.value(cumuls[t])} " ) else: - print(f"Solver exited with nonoptimal status: {status}") + print(f"Solver exited with the following status: {status}") sequences_in_no_overlap_sample_sat() diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index d605f385a7..85e1d86a79 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -633,6 +633,16 @@ ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralToTrue(int lit) { return SetLiteralToFalse(NegatedRef(lit)); } +ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralAndHintToFalse(int lit) { + const int var = PositiveRef(lit); + const int64_t value = RefIsPositive(lit) ? 0 : 1; + return IntersectDomainWithAndUpdateHint(var, Domain(value)); +} + +ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralAndHintToTrue(int lit) { + return SetLiteralAndHintToFalse(NegatedRef(lit)); +} + bool PresolveContext::ConstraintIsInactive(int index) const { const ConstraintProto& ct = working_model->constraints(index); if (ct.constraint_case() == @@ -1956,11 +1966,11 @@ bool PresolveContext::CanonicalizeOneObjectiveVariable(int var) { var_to_constraints_[var].contains(kObjectiveConstraint)) { UpdateRuleStats("objective: variable not used elsewhere"); if (coeff > 0) { - if (!IntersectDomainWith(var, Domain(MinOf(var)))) { + if (!IntersectDomainWithAndUpdateHint(var, Domain(MinOf(var)))) { return false; } } else { - if (!IntersectDomainWith(var, Domain(MaxOf(var)))) { + if (!IntersectDomainWithAndUpdateHint(var, Domain(MaxOf(var)))) { return false; } } diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 9c288d8e9e..4d3444d0d5 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -276,6 +276,8 @@ class PresolveContext { // Returns false if the 'lit' doesn't have the desired value in the domain. ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit); ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit); + ABSL_MUST_USE_RESULT bool SetLiteralAndHintToFalse(int lit); + ABSL_MUST_USE_RESULT bool SetLiteralAndHintToTrue(int lit); // Same as IntersectDomainWith() but take a linear expression as input. // If this expression if of size > 1, this does nothing for now, so it will diff --git a/ortools/sat/samples/sequences_in_no_overlap_sample_sat.py b/ortools/sat/samples/sequences_in_no_overlap_sample_sat.py index fa4f7bd35d..c81a09677c 100644 --- a/ortools/sat/samples/sequences_in_no_overlap_sample_sat.py +++ b/ortools/sat/samples/sequences_in_no_overlap_sample_sat.py @@ -29,7 +29,7 @@ def sequence_constraints_with_circuit( sequence_length_constraints: Dict[str, Tuple[int, int]], sequence_cumul_constraints: Dict[str, Tuple[int, int, int]], ) -> Sequence[Tuple[cp_model.IntVar, int]]: - """This method uses a circuit constraint to rank tasks. + """This method enforces constraints on sequences of tasks of the same type. This method assumes that all starts are disjoint, meaning that all tasks have a strictly positive duration, and they appear in the same NoOverlap @@ -42,8 +42,10 @@ def sequence_constraints_with_circuit( The circuit constraint ensures there is at most 1 hamiltonian cycle of length > 1. If no such path exists, then no tasks are active. - We also need to enforce that any hamiltonian cycle of size > 1 must contain - the node 0. And thus, there is a self loop on node 0 iff the circuit is empty. + In this simplified model, all tasks must be performed. + + Note that we do not enforce the minimum length constraint on the last sequence + of tasks of the same type. Args: model: The CpModel to add the constraints to. @@ -52,13 +54,13 @@ def sequence_constraints_with_circuit( task_types: The type of all tasks. lengths: The computed length of the current sequence for each task. cumuls: The computed cumul of the current sequence for each task. - sequence_length_constraints: the array of tuple (`task_type`, - (`length_min`, `length_max`)) that specifies the minimum and maximum - length of the sequence of tasks of type `task_type`. - sequence_cumul_constraints: the array of tuple (`task_type`, - (`soft_max`, `linear_penalty`, `hard_max`)) that specifies that if the - cumul of the sequence of tasks of type `task_type` is greater than - `soft_max`, then `linear_penalty` must be added to the cost + sequence_length_constraints: the array of tuple (`task_type`, (`length_min`, + `length_max`)) that specifies the minimum and maximum length of the + sequence of tasks of type `task_type`. + sequence_cumul_constraints: the array of tuple (`task_type`, (`soft_max`, + `linear_penalty`, `hard_max`)) that specifies that if the cumul of the + sequence of tasks of type `task_type` is greater than `soft_max`, then + `linear_penalty` must be added to the cost Returns: The list of pairs (Boolean variables, penalty) to be added to the objective. @@ -77,7 +79,7 @@ def sequence_constraints_with_circuit( model.add(cumuls[i] == durations[i]).only_enforce_if(start_lit) # As there are no other constraints on the problem, we can add this - # redundant constraint. + # redundant constraint. This is not valid in general. model.add(starts[i] == 0).only_enforce_if(start_lit) # if node i is last. @@ -106,32 +108,37 @@ def sequence_constraints_with_circuit( # In a non pure problem, the following equality must be an inequality. model.add(starts[j] == starts[i] + durations[i]).only_enforce_if(lit) - # We add the constraint to incrementally maintain the length and the cumul - # variables of the sequence. + # We add the constraints to incrementally maintain the length and the + # cumul variables of the sequence. if task_types[i] == task_types[j]: # Same task type. # Increase the length of the sequence by 1. model.add(lengths[j] == lengths[i] + 1).only_enforce_if(lit) - # Make sure the length of the sequence is within the bounds. - length_max = sequence_length_constraints[task_types[j]][1] - model.add(lengths[j] <= length_max).only_enforce_if(lit) + # Make sure the length of the sequence is within the bounds of the task + # type. + type_length_max = sequence_length_constraints[task_types[j]][1] + model.add(lengths[j] <= type_length_max).only_enforce_if(lit) # Increase the cumul of the sequence by the duration of the task. model.add(cumuls[j] == cumuls[i] + durations[j]).only_enforce_if(lit) # Make sure the cumul of the sequence is within the bounds. - cumul_hard_max = sequence_cumul_constraints[task_types[j]][2] - model.add(cumuls[j] <= cumul_hard_max).only_enforce_if(lit) + type_cumul_hard_max = sequence_cumul_constraints[task_types[j]][2] + model.add(cumuls[j] <= type_cumul_hard_max).only_enforce_if(lit) - else: # Switching task type. + else: + # Switching task type. task[i] is the last task of the previous + # sequence, task[j] is the first task of the new sequence. + # # Reset the length to 1. model.add(lengths[j] == 1).only_enforce_if(lit) # Make sure the previous length is within bounds. - length_min = sequence_length_constraints[task_types[i]][0] - model.add(lengths[i] >= length_min).only_enforce_if(lit) + type_length_min = sequence_length_constraints[task_types[i]][0] + model.add(lengths[i] >= type_length_min).only_enforce_if(lit) # Reset the cumul to the duration of the task. + # Note we do not check that the duration of the task is within bounds. model.add(cumuls[j] == durations[j]).only_enforce_if(lit) # Penalize the cumul of the previous task w.r.t. the soft max @@ -170,13 +177,13 @@ def sequences_in_no_overlap_sample_sat(): (2, "B"), ] - # Sequence length constraints on task_types: (hard_min, hard_max) + # Sequence length constraints per task_types: (hard_min, hard_max) sequence_length_constraints = { "A": (1, 3), "B": (2, 2), } - # Sequence cumul constraints on task_types: + # Sequence accumulated durations constraints per task_types: # (soft_max, linear_penalty, hard_max) sequence_cumul_constraints = { "A": (6, 1, 10), @@ -222,8 +229,8 @@ def sequences_in_no_overlap_sample_sat(): # Adds NoOverlap constraint. model.add_no_overlap(intervals) - # Adds the constraints on the partial lengths and cumuls of the sequence of - # tasks. + # Adds the constraints on the lengths and cumuls of maximal sequences of + # tasks of the same type. penalty_terms = sequence_constraints_with_circuit( model, starts, @@ -244,7 +251,11 @@ def sequences_in_no_overlap_sample_sat(): if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE: # Prints out the makespan and the start times and ranks of all tasks. - print(f"Optimal cost: {solver.objective_value}") + if status == cp_model.OPTIMAL: + print(f"Optimal cost: {solver.objective_value}") + else: + print(f"Feasible cost: {solver.objective_value}") + to_sort = [] for t in all_tasks: to_sort.append((solver.value(starts[t]), t)) @@ -256,7 +267,7 @@ def sequences_in_no_overlap_sample_sat(): f" {solver.value(lengths[t])}, cumul = {solver.value(cumuls[t])} " ) else: - print(f"Solver exited with nonoptimal status: {status}") + print(f"Solver exited with the following status: {status}") sequences_in_no_overlap_sample_sat() diff --git a/ortools/sat/stat_tables.cc b/ortools/sat/stat_tables.cc index 240dab37b1..66cffa8bf2 100644 --- a/ortools/sat/stat_tables.cc +++ b/ortools/sat/stat_tables.cc @@ -240,7 +240,7 @@ void SharedStatTables::AddLnsStat(absl::string_view name, lns_table_.push_back( {FormatName(name), absl::StrCat(num_improving_calls, "/", num_calls), absl::StrFormat("%2.0f%%", 100 * fully_solved_proportion), - absl::StrFormat("%0.2f", difficulty), + absl::StrFormat("%0.2e", difficulty), absl::StrFormat("%0.2f", deterministic_limit)}); }