From 97cf1237e06d90cd3f0936a82c3ec69623a8821d Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 22 Mar 2024 15:55:16 +0100 Subject: [PATCH] [CP-SAT] new sample;improve no_overlap_2d code --- ortools/sat/2d_orthogonal_packing.cc | 90 ++++- ortools/sat/2d_orthogonal_packing.h | 9 + ortools/sat/2d_packing_brute_force.cc | 339 ++++++++++++++++++ ortools/sat/2d_packing_brute_force.h | 40 +++ ortools/sat/BUILD.bazel | 17 +- ortools/sat/cuts.h | 2 +- ortools/sat/diffn.cc | 1 + ortools/sat/diffn_util.cc | 27 +- ortools/sat/diffn_util.h | 5 + ortools/sat/docs/channeling.md | 71 ++++ ortools/sat/samples/BUILD.bazel | 2 + .../index_first_boolvar_true_sample_sat.py | 74 ++++ 12 files changed, 672 insertions(+), 5 deletions(-) create mode 100644 ortools/sat/2d_packing_brute_force.cc create mode 100644 ortools/sat/2d_packing_brute_force.h create mode 100644 ortools/sat/samples/index_first_boolvar_true_sample_sat.py diff --git a/ortools/sat/2d_orthogonal_packing.cc b/ortools/sat/2d_orthogonal_packing.cc index 71b37f4e37..7f5f88c889 100644 --- a/ortools/sat/2d_orthogonal_packing.cc +++ b/ortools/sat/2d_orthogonal_packing.cc @@ -27,6 +27,7 @@ #include "absl/random/distributions.h" #include "absl/types/span.h" #include "ortools/base/logging.h" +#include "ortools/sat/2d_packing_brute_force.h" #include "ortools/sat/integer.h" #include "ortools/sat/util.h" #include "ortools/util/bitset.h" @@ -52,6 +53,14 @@ OrthogonalPackingInfeasibilityDetector:: num_conflicts_two_items_}); stats.push_back({"OrthogonalPackingInfeasibilityDetector/no_energy_conflict", num_scheduling_possible_}); + stats.push_back({"OrthogonalPackingInfeasibilityDetector/brute_force_calls", + num_brute_force_calls_}); + stats.push_back( + {"OrthogonalPackingInfeasibilityDetector/brute_force_conflicts", + num_brute_force_conflicts_}); + stats.push_back( + {"OrthogonalPackingInfeasibilityDetector/brute_force_relaxations", + num_brute_force_relaxation_}); shared_stats_->AddStats(stats); } @@ -550,6 +559,55 @@ OrthogonalPackingInfeasibilityDetector::CheckFeasibilityWithDualFunction2( return best_result; } +bool OrthogonalPackingInfeasibilityDetector::RelaxConflictWithBruteForce( + OrthogonalPackingResult& result, + std::pair bounding_box_size) { + const int num_items_originally = + result.items_participating_on_conflict_.size(); + std::vector sizes_x; + std::vector sizes_y; + std::vector indexes; + std::vector to_be_removed(num_items_originally, false); + + sizes_x.reserve(num_items_originally - 1); + sizes_y.reserve(num_items_originally - 1); + for (int i = 0; i < num_items_originally; i++) { + sizes_x.clear(); + sizes_y.clear(); + // Look for a conflict using all non-removed items but the i-th one. + for (int j = 0; j < num_items_originally; j++) { + if (i == j || to_be_removed[j]) { + continue; + } + sizes_x.push_back(result.items_participating_on_conflict_[j].size_x); + sizes_y.push_back(result.items_participating_on_conflict_[j].size_y); + } + const auto solution = + BruteForceOrthogonalPacking(sizes_x, sizes_y, bounding_box_size); + if (solution.empty()) { + // We still have a conflict if we remove the i-th item! + to_be_removed[i] = true; + } + } + if (!std::any_of(to_be_removed.begin(), to_be_removed.end(), + [](bool b) { return b; })) { + return false; + } + OrthogonalPackingResult original = result; + result.slack_ = 0; + result.conflict_type_ = OrthogonalPackingResult::ConflictType::BRUTE_FORCE; + result.result_ = OrthogonalPackingResult::Status::INFEASIBLE; + result.items_participating_on_conflict_.clear(); + for (int i = 0; i < num_items_originally; i++) { + if (to_be_removed[i]) { + continue; + } + result.items_participating_on_conflict_.push_back( + original.items_participating_on_conflict_[i]); + } + return true; +} + OrthogonalPackingResult OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl( absl::Span sizes_x, @@ -687,6 +745,7 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl( return result; } + bool found_scheduling_solution = false; 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 @@ -701,9 +760,11 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl( scheduling_profile_, new_scheduling_profile_)) { num_scheduling_possible_++; CHECK(result.result_ != OrthogonalPackingResult::Status::INFEASIBLE); - return result; + found_scheduling_solution = true; } + } + if (!found_scheduling_solution && options.use_dff_f2) { // 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( @@ -730,6 +791,30 @@ OrthogonalPackingInfeasibilityDetector::TestFeasibilityImpl( } } + if (result.result_ == OrthogonalPackingResult::Status::UNKNOWN && + num_items <= options.brute_force_threshold) { + num_brute_force_calls_++; + auto solution = + BruteForceOrthogonalPacking(sizes_x, sizes_y, bounding_box_size); + if (solution.empty()) { + result.conflict_type_ = ConflictType::BRUTE_FORCE; + result.result_ = OrthogonalPackingResult::Status::INFEASIBLE; + result.items_participating_on_conflict_.resize(num_items); + for (int i = 0; i < num_items; i++) { + result.items_participating_on_conflict_[i] = make_item(i); + } + } else { + result.result_ = OrthogonalPackingResult::Status::FEASIBLE; + } + } + + if (result.result_ == OrthogonalPackingResult::Status::INFEASIBLE && + result.items_participating_on_conflict_.size() <= + options.brute_force_threshold) { + num_brute_force_relaxation_ += + RelaxConflictWithBruteForce(result, bounding_box_size); + } + return result; } @@ -760,6 +845,9 @@ OrthogonalPackingResult OrthogonalPackingInfeasibilityDetector::TestFeasibility( // The total area of the items was larger than the area of the box. num_trivial_conflicts_++; break; + case ConflictType::BRUTE_FORCE: + num_brute_force_conflicts_++; + break; case ConflictType::NO_CONFLICT: LOG(FATAL) << "Should never happen"; break; diff --git a/ortools/sat/2d_orthogonal_packing.h b/ortools/sat/2d_orthogonal_packing.h index d777014767..40e296e0b0 100644 --- a/ortools/sat/2d_orthogonal_packing.h +++ b/ortools/sat/2d_orthogonal_packing.h @@ -33,6 +33,7 @@ struct OrthogonalPackingOptions { bool use_pairwise = true; bool use_dff_f0 = true; bool use_dff_f2 = true; + int brute_force_threshold = 6; int dff2_max_number_of_parameters_to_check = std::numeric_limits::max(); }; @@ -119,6 +120,7 @@ class OrthogonalPackingResult { PAIRWISE, DFF_F0, DFF_F2, + BRUTE_FORCE, }; Status result_; @@ -144,6 +146,10 @@ class OrthogonalPackingInfeasibilityDetector { const OrthogonalPackingOptions& options = OrthogonalPackingOptions()); private: + bool RelaxConflictWithBruteForce( + OrthogonalPackingResult& result, + std::pair bounding_box_size); + OrthogonalPackingResult TestFeasibilityImpl( absl::Span sizes_x, absl::Span sizes_y, @@ -190,6 +196,9 @@ class OrthogonalPackingInfeasibilityDetector { int64_t num_conflicts_dff2_ = 0; int64_t num_conflicts_dff0_ = 0; int64_t num_scheduling_possible_ = 0; + int64_t num_brute_force_calls_ = 0; + int64_t num_brute_force_conflicts_ = 0; + int64_t num_brute_force_relaxation_ = 0; absl::BitGenRef random_; SharedStatistics* shared_stats_; diff --git a/ortools/sat/2d_packing_brute_force.cc b/ortools/sat/2d_packing_brute_force.cc new file mode 100644 index 0000000000..542fc2a5e4 --- /dev/null +++ b/ortools/sat/2d_packing_brute_force.cc @@ -0,0 +1,339 @@ +// Copyright 2010-2024 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "ortools/sat/2d_packing_brute_force.h" + +#include +#include +#include +#include + +#include "absl/container/inlined_vector.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" +#include "ortools/sat/diffn_util.h" +#include "ortools/sat/integer.h" + +namespace operations_research { +namespace sat { + +namespace { + +enum class RectangleRelationship { + TOUCHING_NEITHER_LEFT_OR_BOTTOM, + TOUCHING_BOTTOM, + TOUCHING_LEFT, + OVERLAP, +}; + +// TODO(user): write faster and less hacky implementation +RectangleRelationship GetRectangleRelationship(const Rectangle& rectangle, + const Rectangle& other) { + if (!rectangle.IsDisjoint(other)) { + return RectangleRelationship::OVERLAP; + } + const Rectangle item_position_left = {.x_min = rectangle.x_min - 1, + .x_max = rectangle.x_max - 1, + .y_min = rectangle.y_min, + .y_max = rectangle.y_max}; + const Rectangle item_position_bottom = {.x_min = rectangle.x_min, + .x_max = rectangle.x_max, + .y_min = rectangle.y_min - 1, + .y_max = rectangle.y_max - 1}; + if (!item_position_left.IsDisjoint(other)) { + return RectangleRelationship::TOUCHING_LEFT; + } + if (!item_position_bottom.IsDisjoint(other)) { + return RectangleRelationship::TOUCHING_BOTTOM; + } + return RectangleRelationship::TOUCHING_NEITHER_LEFT_OR_BOTTOM; +} + +bool ShouldPlaceItemAtPosition( + int i, IntegerValue x, IntegerValue y, + absl::Span sizes_x, + absl::Span sizes_y, + std::pair bounding_box_size, + absl::InlinedVector& item_positions, + absl::InlinedVector& placed_item_indexes) { + const int num_items = sizes_x.size(); + const Rectangle item_position = { + .x_min = x, .x_max = x + sizes_x[i], .y_min = y, .y_max = y + sizes_y[i]}; + + // Check if it fits in the BB. + if (item_position.x_max > bounding_box_size.first || + item_position.y_max > bounding_box_size.second) { + return false; + } + + // Break symmetry: force 0th item to be in the bottom left quarter. + if (i == 0 && + (2 * item_position.x_min > bounding_box_size.first - sizes_x[i] || + 2 * item_position.y_min > bounding_box_size.second - sizes_y[i])) { + return false; + } + + // Check if it is conflicting with another item. + bool is_conflicting_left = x == 0; + bool is_conflicting_bottom = y == 0; + for (int j = 0; j < num_items; ++j) { + if (i != j && placed_item_indexes[j]) { + const RectangleRelationship pos = + GetRectangleRelationship(item_position, item_positions[j]); + if (pos == RectangleRelationship::OVERLAP) { + return false; + } + is_conflicting_left = + is_conflicting_left || pos == RectangleRelationship::TOUCHING_LEFT; + is_conflicting_bottom = is_conflicting_bottom || + pos == RectangleRelationship::TOUCHING_BOTTOM; + } + } + + // Finally, check if it touching something both on the bottom and to the left. + if (!is_conflicting_left || !is_conflicting_bottom) { + return false; + } + return true; +} + +// TODO(user): try the graph-based algorithm by S. Fekete, J. Shepers, and +// J. Van Der Ween, https://arxiv.org/abs/cs/0604045. +bool BruteForceOrthogonalPackingImpl( + absl::Span sizes_x, + absl::Span sizes_y, + std::pair bounding_box_size, + IntegerValue smallest_x, IntegerValue smallest_y, + absl::InlinedVector& item_positions, + absl::InlinedVector& placed_item_indexes, + const absl::InlinedVector< + absl::InlinedVector, 16>, 16>& + potential_item_positions) { + const auto add_position_if_valid = + [&item_positions, bounding_box_size, &sizes_x, &sizes_y, + &placed_item_indexes]( + absl::InlinedVector, 16>& + positions, + int i, IntegerValue x, IntegerValue y) { + if (ShouldPlaceItemAtPosition(i, x, y, sizes_x, sizes_y, + bounding_box_size, item_positions, + placed_item_indexes)) { + positions.push_back({x, y}); + } + }; + + const int num_items = sizes_x.size(); + bool has_unplaced_item = false; + for (int i = 0; i < num_items; ++i) { + if (placed_item_indexes[i]) { + continue; + } + if (potential_item_positions[i].empty()) { + return false; + } + + has_unplaced_item = true; + placed_item_indexes[i] = true; + for (std::pair potential_position : + potential_item_positions[i]) { + // Place the item on its candidate position. + item_positions[i] = {.x_min = potential_position.first, + .x_max = potential_position.first + sizes_x[i], + .y_min = potential_position.second, + .y_max = potential_position.second + sizes_y[i]}; + const Rectangle& item_position = item_positions[i]; + + // Now the hard part of the algorithm: create the new "potential + // positions" vector after placing this item. Describing the actual set of + // acceptable places to put consider for the next item in the search would + // be pretty complex. For example: + // +----------------------------+ + // | | + // |x | + // |--------+ | + // |88888888| | + // |88888888| | + // |--------+ | + // |####| | + // |####|x x | + // |####| +------+ | + // |####| |......| | + // |####| |......| | + // |####| |......| | + // |####|x x |......| | + // |####+---------+......| | + // |####|OOOOOOOOO|......| | + // |####|OOOOOOOOO|......| | + // |####|OOOOOOOOO|......|x | + // +----+---------+------+------+ + // + // To make things simpler, we just consider: + // - all previous positions if they didn't got invalid due to the new + // item; + // - new position are derived getting the right-top most corner of the + // added item and connecting it to the bottom and the left with a line. + // New potential positions are the intersection of this line with either + // the current items or the box. For example, if we add a box to the + // example above (representing the two lines by '*'): + // +----------------------------+ + // | | + // | | + // |--------+ | + // |88888888| | + // |88888888| | + // |--------+ | + // |####| | + // |####| | + // |####| +------+ | + // |x###|x |......|x | + // |************************** | + // |####| |......|@@@* | + // |####| |......|@@@* | + // |####+---------+......|@@@* | + // |####|OOOOOOOOO|......|@@@* | + // |####|OOOOOOOOO|......|@@@* | + // |####|OOOOOOOOO|......|@@@*x | + // +----+---------+------+------+ + // + // This method finds potential locations that are not useful for any item, + // but we will detect that by testing each item one by one. + absl::InlinedVector< + absl::InlinedVector, 16>, 16> + new_potential_positions(num_items); + for (int k = 0; k < num_items; ++k) { + if (k == i || !placed_item_indexes[k]) { + continue; + } + + bool add_below = + // We only add points below this one... + item_positions[k].y_max <= item_position.y_min && + // ...and where we can fit at least the smallest element. + item_position.x_max + smallest_x <= bounding_box_size.first && + item_positions[k].y_max + smallest_y <= bounding_box_size.second; + bool add_left = + item_positions[k].x_max <= item_position.x_min && + item_positions[k].x_max + smallest_x <= bounding_box_size.first && + item_position.y_max + smallest_y <= bounding_box_size.second; + for (int j = 0; j < num_items; ++j) { + if (k == j || placed_item_indexes[j]) { + continue; + } + if (add_below) { + add_position_if_valid(new_potential_positions[j], j, + item_position.x_max, item_positions[k].y_max); + } + if (add_left) { + add_position_if_valid(new_potential_positions[j], j, + item_positions[k].x_max, item_position.y_max); + } + } + } + bool is_unfeasible = false; + for (int j = 0; j < num_items; ++j) { + // No positions to attribute to the item we just placed. + if (i == j || placed_item_indexes[j]) { + continue; + } + // First copy previously valid positions that remain valid. + for (const std::pair& original_position : + potential_item_positions[j]) { + const Rectangle item_in_pos = { + .x_min = original_position.first, + .x_max = original_position.first + sizes_x[j], + .y_min = original_position.second, + .y_max = original_position.second + sizes_y[j]}; + + if (!item_in_pos.IsDisjoint(item_position)) { + // That was a valid position for item j, but now it is in conflict + // with newly added item i. + continue; + } + new_potential_positions[j].push_back(original_position); + } + add_position_if_valid(new_potential_positions[j], j, + item_positions[i].x_max, 0); + add_position_if_valid(new_potential_positions[j], j, 0, + item_positions[i].y_max); + if (new_potential_positions[j].empty()) { + // After placing the item i, there is no valid place to choose for the + // item j. We must pick another placement for i. + is_unfeasible = true; + break; + } + } + if (is_unfeasible) { + continue; + } + if (BruteForceOrthogonalPackingImpl( + sizes_x, sizes_y, bounding_box_size, smallest_x, smallest_y, + item_positions, placed_item_indexes, new_potential_positions)) { + return true; + } + } + // Placing this item at the current bottom-left positions level failed. + // Restore placed_item_indexes to its original value and try another one. + placed_item_indexes[i] = false; + } + return !has_unplaced_item; +} + +} // namespace + +std::vector BruteForceOrthogonalPacking( + absl::Span sizes_x, + absl::Span sizes_y, + std::pair bounding_box_size) { + IntegerValue smallest_x = std::numeric_limits::max(); + IntegerValue smallest_y = std::numeric_limits::max(); + int num_items = sizes_x.size(); + absl::InlinedVector item_index_sorted_by_area_desc(num_items); + absl::InlinedVector< + absl::InlinedVector, 16>, 16> + potential_item_positions(num_items); + for (int i = 0; i < num_items; ++i) { + smallest_x = std::min(smallest_x, sizes_x[i]); + smallest_y = std::min(smallest_y, sizes_y[i]); + item_index_sorted_by_area_desc[i] = i; + potential_item_positions[i].push_back({0, 0}); + } + std::sort(item_index_sorted_by_area_desc.begin(), + item_index_sorted_by_area_desc.end(), + [sizes_x, sizes_y](int a, int b) { + return sizes_x[a] * sizes_y[a] > sizes_x[b] * sizes_y[b]; + }); + absl::InlinedVector new_sizes_x(num_items); + absl::InlinedVector new_sizes_y(num_items); + for (int i = 0; i < num_items; ++i) { + new_sizes_x[i] = sizes_x[item_index_sorted_by_area_desc[i]]; + new_sizes_y[i] = sizes_y[item_index_sorted_by_area_desc[i]]; + } + absl::InlinedVector item_positions(num_items); + absl::InlinedVector placed_item_indexes(num_items); + const bool found_solution = BruteForceOrthogonalPackingImpl( + new_sizes_x, new_sizes_y, bounding_box_size, smallest_x, smallest_y, + item_positions, placed_item_indexes, potential_item_positions); + if (!found_solution) { + return {}; + } + std::vector result(num_items); + for (int i = 0; i < num_items; ++i) { + result[item_index_sorted_by_area_desc[i]] = item_positions[i]; + } + VLOG_EVERY_N_SEC(2, 3) << "Found a feasible packing by brute force. Dot:\n " + << RenderDot(bounding_box_size, result); + return result; +} + +} // namespace sat +} // namespace operations_research diff --git a/ortools/sat/2d_packing_brute_force.h b/ortools/sat/2d_packing_brute_force.h new file mode 100644 index 0000000000..a5ef0ad5f0 --- /dev/null +++ b/ortools/sat/2d_packing_brute_force.h @@ -0,0 +1,40 @@ +// Copyright 2010-2024 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef OR_TOOLS_SAT_2D_PACKING_BRUTE_FORCE_H_ +#define OR_TOOLS_SAT_2D_PACKING_BRUTE_FORCE_H_ + +#include +#include + +#include "absl/types/span.h" +#include "ortools/sat/diffn_util.h" +#include "ortools/sat/integer.h" + +namespace operations_research { +namespace sat { + +// Try to solve the Orthogonal Packing Problem by enumeration of all possible +// solutions. Returns an empty vector if the problem is infeasible, otherwise +// returns the items in the positions they appear in the solution in the same +// order as the input arguments. +// Warning: do not call this with too many item as it will run forever. +std::vector BruteForceOrthogonalPacking( + absl::Span sizes_x, + absl::Span sizes_y, + std::pair bounding_box_size); + +} // namespace sat +} // namespace operations_research + +#endif // OR_TOOLS_SAT_2D_PACKING_BRUTE_FORCE_H_ diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 2a03e3e838..4c35261e21 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -1818,7 +1818,6 @@ cc_library( "@com_google_absl//absl/container:inlined_vector", "@com_google_absl//absl/log:check", "@com_google_absl//absl/random:bit_gen_ref", - "@com_google_absl//absl/random:distributions", "@com_google_absl//absl/strings:str_format", "@com_google_absl//absl/types:span", ], @@ -1829,6 +1828,7 @@ cc_library( srcs = ["2d_orthogonal_packing.cc"], hdrs = ["2d_orthogonal_packing.h"], deps = [ + ":2d_packing_brute_force", ":integer", ":synchronization", ":util", @@ -1842,6 +1842,21 @@ cc_library( ], ) +cc_library( + name = "2d_packing_brute_force", + srcs = ["2d_packing_brute_force.cc"], + hdrs = ["2d_packing_brute_force.h"], + deps = [ + ":diffn_util", + ":integer", + "//ortools/util:bitset", + "@com_google_absl//absl/container:inlined_vector", + "@com_google_absl//absl/log", + "@com_google_absl//absl/log:check", + "@com_google_absl//absl/types:span", + ], +) + cc_library( name = "2d_orthogonal_packing_testing", testonly = 1, diff --git a/ortools/sat/cuts.h b/ortools/sat/cuts.h index d6fe1772e2..c7b6639ffd 100644 --- a/ortools/sat/cuts.h +++ b/ortools/sat/cuts.h @@ -653,7 +653,7 @@ class BoolRLTCutHelper { explicit BoolRLTCutHelper(Model* model) : product_detector_(model->GetOrCreate()), shared_stats_(model->GetOrCreate()), - lp_values_(model->GetOrCreate()){}; + lp_values_(model->GetOrCreate()) {}; ~BoolRLTCutHelper(); // Precompute data according to the current lp relaxation. diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 19b927b6f0..2ffc5028da 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -428,6 +428,7 @@ NonOverlappingRectanglesEnergyPropagator::FindConflict( .use_pairwise = true, .use_dff_f0 = true, .use_dff_f2 = true, + .brute_force_threshold = 6, .dff2_max_number_of_parameters_to_check = 100}); if (opp_result.GetResult() == OrthogonalPackingResult::Status::INFEASIBLE && (best_conflict.opp_result.GetResult() != diff --git a/ortools/sat/diffn_util.cc b/ortools/sat/diffn_util.cc index b3c7b196c3..6a44c7d7f6 100644 --- a/ortools/sat/diffn_util.cc +++ b/ortools/sat/diffn_util.cc @@ -21,8 +21,9 @@ #include #include #include -#include #include +#include +#include #include #include #include @@ -31,7 +32,6 @@ #include "absl/container/inlined_vector.h" #include "absl/log/check.h" #include "absl/random/bit_gen_ref.h" -#include "absl/random/distributions.h" #include "absl/types/span.h" #include "ortools/base/logging.h" #include "ortools/base/stl_util.h" @@ -1490,5 +1490,28 @@ FindRectanglesResult FindRectanglesWithEnergyConflictMC( return result; } +std::string RenderDot(std::pair bb_sizes, + absl::Span solution) { + const std::vector colors = {"red", "green", "blue", + "cyan", "yellow", "purple"}; + std::stringstream ss; + ss << "digraph {\n"; + ss << " graph [ bgcolor=lightgray width=" << 2 * bb_sizes.first + << " height=" << 2 * bb_sizes.second << "]\n"; + ss << " node [style=filled]\n"; + ss << " bb [fillcolor=\"grey\" pos=\"" << bb_sizes.first << "," + << bb_sizes.second << "!\" shape=box width=" << 2 * bb_sizes.first + << " height=" << 2 * bb_sizes.second << "]\n"; + for (int i = 0; i < solution.size(); ++i) { + ss << " " << i << " [fillcolor=\"" << colors[i % colors.size()] + << "\" pos=\"" << 2 * solution[i].x_min + solution[i].SizeX() << "," + << 2 * solution[i].y_min + solution[i].SizeY() + << "!\" shape=box width=" << 2 * solution[i].SizeX() + << " height=" << 2 * solution[i].SizeY() << "]\n"; + } + ss << "}\n"; + return ss.str(); +} + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/diffn_util.h b/ortools/sat/diffn_util.h index 9b6c351347..685cb0ff99 100644 --- a/ortools/sat/diffn_util.h +++ b/ortools/sat/diffn_util.h @@ -588,6 +588,11 @@ FindRectanglesResult FindRectanglesWithEnergyConflictMC( const std::vector& intervals, absl::BitGenRef random, double temperature, double candidate_energy_usage_factor); +// Render a packing solution as a Graphviz dot file. Only works in the "neato" +// or "fdp" Graphviz backends. +std::string RenderDot(std::pair bb_sizes, + absl::Span solution); + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/docs/channeling.md b/ortools/sat/docs/channeling.md index 756b08f58c..74de0de410 100644 --- a/ortools/sat/docs/channeling.md +++ b/ortools/sat/docs/channeling.md @@ -385,6 +385,77 @@ x=9 y=1 b=1 x=10 y=0 b=1 ``` +## Computing the index of the first Boolean variable set to true + +A common request is to compute the index of the first Boolean variable set to +true. It can be encoded using a min_equality constraint. The index will be set +to the number of Boolean variables if they are all false. + +### Python code + +```python +#!/usr/bin/env python3 +"""Compute the index of the first Boolean variable set to true.""" + +from ortools.sat.python import cp_model + + +class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback): + """Print intermediate solutions.""" + + def __init__(self, index: cp_model.IntVar, boolvars: list[cp_model.IntVar]): + cp_model.CpSolverSolutionCallback.__init__(self) + self.__index = index + self.__boolvars = boolvars + + def on_solution_callback(self) -> None: + line = "" + for v in self.__boolvars: + line += f"{self.value(v)}" + line += f" -> {self.value(self.__index)}" + print(line) + + +def index_first_solution_true_sample_sat(): + """Compute the index of the first Boolean variable set to true.""" + + # Model. + model = cp_model.CpModel() + + # Variables + num_bool_vars = 5 + bool_vars = [model.new_bool_var(f"{i}") for i in range(num_bool_vars)] + index = model.new_int_var(0, num_bool_vars, "index") + + # Channeling between the index and the Boolean variables. + model.add_min_equality( + index, + [ + num_bool_vars - bool_vars[i] * (num_bool_vars - i) + for i in range(num_bool_vars) + ], + ) + + # Flip bool_vars in increasing order. + model.add_decision_strategy( + bool_vars, cp_model.CHOOSE_FIRST, cp_model.SELECT_MIN_VALUE + ) + + # Create a solver and solve with a fixed search. + solver = cp_model.CpSolver() + + # Force the solver to follow the decision strategy exactly. + solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + + # Search and print out all solutions. + solution_printer = VarArraySolutionPrinter(index, bool_vars) + solver.solve(model, solution_printer) + + +index_first_solution_true_sample_sat() +``` ## A bin-packing problem diff --git a/ortools/sat/samples/BUILD.bazel b/ortools/sat/samples/BUILD.bazel index 891e34c0ba..b064e3daa6 100644 --- a/ortools/sat/samples/BUILD.bazel +++ b/ortools/sat/samples/BUILD.bazel @@ -43,6 +43,8 @@ code_sample_py(name = "cumulative_variable_profile_sample_sat") code_sample_cc_py(name = "earliness_tardiness_cost_sample_sat") +code_sample_py(name = "index_first_boolvar_true_sample_sat") + code_sample_cc_py(name = "interval_sample_sat") code_sample_cc_py(name = "minimal_jobshop_sat") diff --git a/ortools/sat/samples/index_first_boolvar_true_sample_sat.py b/ortools/sat/samples/index_first_boolvar_true_sample_sat.py new file mode 100644 index 0000000000..7d70de0528 --- /dev/null +++ b/ortools/sat/samples/index_first_boolvar_true_sample_sat.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +# Copyright 2010-2024 Google LLC +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +"""Compute the index of the first Boolean variable set to true.""" + +from ortools.sat.python import cp_model + + +class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback): + """Print intermediate solutions.""" + + def __init__(self, index: cp_model.IntVar, boolvars: list[cp_model.IntVar]): + cp_model.CpSolverSolutionCallback.__init__(self) + self.__index = index + self.__boolvars = boolvars + + def on_solution_callback(self) -> None: + line = "" + for v in self.__boolvars: + line += f"{self.value(v)}" + line += f" -> {self.value(self.__index)}" + print(line) + + +def index_first_solution_true_sample_sat(): + """Compute the index of the first Boolean variable set to true.""" + + # Model. + model = cp_model.CpModel() + + # Variables + num_bool_vars = 5 + bool_vars = [model.new_bool_var(f"{i}") for i in range(num_bool_vars)] + index = model.new_int_var(0, num_bool_vars, "index") + + # Channeling between the index and the Boolean variables. + model.add_min_equality( + index, + [ + num_bool_vars - bool_vars[i] * (num_bool_vars - i) + for i in range(num_bool_vars) + ], + ) + + # Flip bool_vars in increasing order. + model.add_decision_strategy( + bool_vars, cp_model.CHOOSE_FIRST, cp_model.SELECT_MIN_VALUE + ) + + # Create a solver and solve with a fixed search. + solver = cp_model.CpSolver() + + # Force the solver to follow the decision strategy exactly. + solver.parameters.search_branching = cp_model.FIXED_SEARCH + # Enumerate all solutions. + solver.parameters.enumerate_all_solutions = True + + # Search and print out all solutions. + solution_printer = VarArraySolutionPrinter(index, bool_vars) + solver.solve(model, solution_printer) + + +index_first_solution_true_sample_sat()