diff --git a/ortools/sat/2d_orthogonal_packing.cc b/ortools/sat/2d_orthogonal_packing.cc index 4f50402ea3..41358069e2 100644 --- a/ortools/sat/2d_orthogonal_packing.cc +++ b/ortools/sat/2d_orthogonal_packing.cc @@ -18,6 +18,7 @@ #include #include #include +#include #include #include @@ -49,6 +50,8 @@ OrthogonalPackingInfeasibilityDetector:: num_trivial_conflicts_}); stats.push_back({"OrthogonalPackingInfeasibilityDetector/conflicts_two_items", num_conflicts_two_items_}); + stats.push_back({"OrthogonalPackingInfeasibilityDetector/no_energy_conflict", + num_scheduling_possible_}); shared_stats_->AddStats(stats); } @@ -220,6 +223,94 @@ std::vector GetDffConflict( return result; } +// Tries a simple heuristic to find a solution for the Resource-Constrained +// Project Scheduling Problem (RCPSP). The RCPSP can be mapped to a +// 2d bin packing where one dimension (say, x) is chosen to represent the time, +// and every item is cut into items with size_x = 1 that must remain consecutive +// in the x-axis but do not need to be aligned on the y axis. This is often +// called the cumulative relaxation of the 2d bin packing problem. +// +// Bin-packing solution RCPSP solution +// --------------- --------------- +// | ********** | | ***** | +// | ********** | | ***** | +// | ##### | | **#####*** | +// | ##### | | **#####*** | +// --------------- --------------- +// +// One interesting property is if we find an energy conflict using a +// superadditive function it means the problem is infeasible both interpreted as +// a 2d bin packing and as a RCPSP problem. In practice, that means that if we +// find a RCPSP solution for a 2d bin packing problem, there is no point on +// using Maximal DFFs to search for energy conflicts. +// +// Returns true if it found a feasible solution to the RCPSP problem. +bool FindHeuristicSchedulingSolution( + absl::Span sizes, + absl::Span demands, + absl::Span heuristic_order, IntegerValue global_end_max, + IntegerValue capacity_max, + std::vector>& profile, + std::vector>& new_profile) { + // The profile (and new profile) is a set of (time, capa_left) pairs, ordered + // by increasing time and capa_left. + profile.clear(); + profile.emplace_back(kMinIntegerValue, capacity_max); + profile.emplace_back(kMaxIntegerValue, capacity_max); + IntegerValue start_of_previous_task = kMinIntegerValue; + for (int i = 0; i < heuristic_order.size(); i++) { + const IntegerValue event_size = sizes[heuristic_order[i]]; + const IntegerValue event_demand = demands[heuristic_order[i]]; + const IntegerValue event_start_min = 0; + const IntegerValue event_start_max = global_end_max - event_size; + const IntegerValue start_min = + std::max(event_start_min, start_of_previous_task); + + // Iterate on the profile to find the step that contains start_min. + // Then push until we find a step with enough capacity. + int current = 0; + while (profile[current + 1].first <= start_min || + profile[current].second < event_demand) { + ++current; + } + + const IntegerValue actual_start = + std::max(start_min, profile[current].first); + start_of_previous_task = actual_start; + + // Compatible with the event.start_max ? + if (actual_start > event_start_max) return false; + + const IntegerValue actual_end = actual_start + event_size; + + // No need to update the profile on the last loop. + if (i == heuristic_order.size() - 1) break; + + // Update the profile. + new_profile.clear(); + new_profile.push_back( + {actual_start, profile[current].second - event_demand}); + ++current; + + while (profile[current].first < actual_end) { + new_profile.push_back( + {profile[current].first, profile[current].second - event_demand}); + ++current; + } + + if (profile[current].first > actual_end) { + new_profile.push_back( + {actual_end, new_profile.back().second + event_demand}); + } + while (current < profile.size()) { + new_profile.push_back(profile[current]); + ++current; + } + profile.swap(new_profile); + } + return true; +} + } // namespace void OrthogonalPackingInfeasibilityDetector::GetAllCandidatesForKForDff2( @@ -433,10 +524,17 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl( std::sort(index_by_decreasing_x_size_.begin(), index_by_decreasing_x_size_.end(), - [&sizes_x](int a, int b) { return sizes_x[a] > sizes_x[b]; }); + [&sizes_x, &sizes_y](int a, int b) { + // Break ties with y-size + return std::tie(sizes_x[a], sizes_y[a]) > + std::tie(sizes_x[b], sizes_y[b]); + }); std::sort(index_by_decreasing_y_size_.begin(), index_by_decreasing_y_size_.end(), - [&sizes_y](int a, int b) { return sizes_y[a] > sizes_y[b]; }); + [&sizes_y, &sizes_x](int a, int b) { + return std::tie(sizes_y[a], sizes_x[a]) > + std::tie(sizes_y[b], sizes_x[b]); + }); // First look for pairwise incompatible pairs. if (options.use_pairwise) { @@ -530,6 +628,22 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl( } if (options.use_dff_f2) { + // Checking for conflicts using f_2 is expensive, so first try a quick + // algorithm to check if there is no conflict to be found. See the comments + // on top of FindHeuristicSchedulingSolution(). + if (FindHeuristicSchedulingSolution( + sizes_x, sizes_y, index_by_decreasing_x_size_, + bounding_box_size.first, bounding_box_size.second, + scheduling_profile_, new_scheduling_profile_) || + FindHeuristicSchedulingSolution( + sizes_y, sizes_x, index_by_decreasing_y_size_, + bounding_box_size.second, bounding_box_size.first, + scheduling_profile_, new_scheduling_profile_)) { + num_scheduling_possible_++; + CHECK(result.result_ != OrthogonalPackingResult::Status::INFEASIBLE); + return result; + } + // We only check for conflicts applying this DFF on heights and widths, but // not on both, which would be too expensive if done naively. auto conflict = CheckFeasibilityWithDualFunction2( diff --git a/ortools/sat/2d_orthogonal_packing.h b/ortools/sat/2d_orthogonal_packing.h index 84274e5d7b..83eb73d75d 100644 --- a/ortools/sat/2d_orthogonal_packing.h +++ b/ortools/sat/2d_orthogonal_packing.h @@ -130,8 +130,11 @@ class OrthogonalPackingInfeasibilityDetector { absl::Span index_by_decreasing_x_size, IntegerValue x_bb_size, IntegerValue y_bb_size, int max_number_of_parameters_to_check); + // Buffers cleared and reused at each call of TestFeasibility() std::vector index_by_decreasing_x_size_; std::vector index_by_decreasing_y_size_; + std::vector> scheduling_profile_; + std::vector> new_scheduling_profile_; int64_t num_calls_ = 0; int64_t num_conflicts_ = 0; @@ -139,6 +142,7 @@ class OrthogonalPackingInfeasibilityDetector { int64_t num_trivial_conflicts_ = 0; int64_t num_conflicts_dff2_ = 0; int64_t num_conflicts_dff0_ = 0; + int64_t num_scheduling_possible_ = 0; absl::BitGenRef random_; SharedStatistics* shared_stats_; diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index d2b5b54eda..02d53e4f2d 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -36,7 +36,7 @@ namespace sat { BoolVar::BoolVar(int index, CpModelBuilder* builder) : builder_(builder), index_(index) {} -BoolVar BoolVar::WithName(const std::string& name) { +BoolVar BoolVar::WithName(absl::string_view name) { DCHECK(builder_ != nullptr); if (builder_ == nullptr) return *this; builder_->MutableProto() diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index 46ccdf5e18..29c6cb1d39 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -82,7 +82,7 @@ class BoolVar { /// Sets the name of the variable. /// Note that this will always set the "positive" version of this Boolean. - BoolVar WithName(const std::string& name); + BoolVar WithName(absl::string_view name); /// Returns the name of the variable. std::string Name() const; diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 0a752ddd1d..70be341895 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -422,20 +422,13 @@ NonOverlappingRectanglesEnergyPropagator::FindConflict( // our rectangle is the bounding box, and we need to fit inside it a set of // items corresponding to the minimum intersection of the original items // with this bounding box. - const bool use_expensive_heuristics = - (sizes_x.size() < 10) || - // Propagating a large conflict is expensive, so it's worth running an - // expensive heuristic to make it smaller. - best_conflict.opp_result.GetResult() == - OrthogonalPackingResult::Status::INFEASIBLE || - !rectangles_with_too_much_energy.conflicts.empty(); const auto opp_result = orthogonal_packing_checker_.TestFeasibility( sizes_x, sizes_y, {r.SizeX(), r.SizeY()}, - OrthogonalPackingOptions{.use_pairwise = true, + OrthogonalPackingOptions{ + .use_pairwise = true, .use_dff_f0 = true, .use_dff_f2 = true, - .dff2_max_number_of_parameters_to_check = - use_expensive_heuristics ? 25 : 3}); + .dff2_max_number_of_parameters_to_check = 100}); if (opp_result.GetResult() == OrthogonalPackingResult::Status::INFEASIBLE && (best_conflict.opp_result.GetResult() != OrthogonalPackingResult::Status::INFEASIBLE || diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index c661ae2ef4..3919064561 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -406,7 +406,7 @@ bool Prober::ProbeDnf(absl::string_view name, num_new_literals_fixed_ > previous_num_literals_fixed) { VLOG(1) << "ProbeDnf(" << name << ", num_fixed_literals=" << num_new_literals_fixed_ - previous_num_literals_fixed - << ", num_pushed_integer_bounds=" + << ", num_fixed_integer_bounds=" << num_new_integer_bounds_ - previous_num_integer_bounds << ", num_valid_conjunctions=" << num_valid_conjunctions << "/" << dnf.size() << ")"; @@ -498,7 +498,7 @@ bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model, bool FailedLiteralProbingRound(ProbingOptions options, Model* model) { WallTimer wall_timer; wall_timer.Start(); - options.log_info |= VLOG_IS_ON(2); + options.log_info |= VLOG_IS_ON(1); // Reset the solver in case it was already used. auto* sat_solver = model->GetOrCreate(); diff --git a/ortools/sat/samples/multiple_knapsack_sat.py b/ortools/sat/samples/multiple_knapsack_sat.py index e77f557f18..e50744750f 100644 --- a/ortools/sat/samples/multiple_knapsack_sat.py +++ b/ortools/sat/samples/multiple_knapsack_sat.py @@ -86,7 +86,7 @@ def main() -> None: for i in all_items: if solver.value(x[i, b]) > 0: print( - f"Item:{i} weight:{data['weights'][i]} value:{data['values'][i]}" + f'Item:{i} weight:{data["weights"][i]} value:{data["values"][i]}' ) bin_weight += data["weights"][i] bin_value += data["values"][i]