// Copyright 2010-2025 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 ORTOOLS_SAT_DIFFN_H_ #define ORTOOLS_SAT_DIFFN_H_ #include #include #include #include "absl/container/flat_hash_set.h" #include "absl/types/span.h" #include "ortools/sat/2d_orthogonal_packing.h" #include "ortools/sat/diffn_util.h" #include "ortools/sat/disjunctive.h" #include "ortools/sat/integer.h" #include "ortools/sat/integer_base.h" #include "ortools/sat/model.h" #include "ortools/sat/no_overlap_2d_helper.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/scheduling_helpers.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" #include "ortools/util/bitset.h" #include "ortools/util/time_limit.h" namespace operations_research { namespace sat { // Propagates using a box energy reasoning. class NonOverlappingRectanglesEnergyPropagator : public PropagatorInterface { public: NonOverlappingRectanglesEnergyPropagator(NoOverlap2DConstraintHelper* helper, Model* model) : helper_(*helper), random_(model->GetOrCreate()), shared_stats_(model->GetOrCreate()), orthogonal_packing_checker_(*random_, shared_stats_) {} ~NonOverlappingRectanglesEnergyPropagator() override; bool Propagate() final; int RegisterWith(GenericLiteralWatcher* watcher); private: struct Conflict { // The Orthogonal Packing subproblem we used. std::vector items_for_opp; Rectangle rectangle_with_too_much_energy; OrthogonalPackingResult opp_result; }; std::optional FindConflict( std::vector active_box_ranges); std::vector GeneralizeExplanation(const Conflict& conflict); bool BuildAndReportEnergyTooLarge(absl::Span ranges); NoOverlap2DConstraintHelper& helper_; ModelRandomGenerator* random_; SharedStatistics* shared_stats_; OrthogonalPackingInfeasibilityDetector orthogonal_packing_checker_; int64_t num_calls_ = 0; int64_t num_conflicts_ = 0; int64_t num_conflicts_two_boxes_ = 0; int64_t num_refined_conflicts_ = 0; int64_t num_conflicts_with_slack_ = 0; NonOverlappingRectanglesEnergyPropagator( const NonOverlappingRectanglesEnergyPropagator&) = delete; NonOverlappingRectanglesEnergyPropagator& operator=( const NonOverlappingRectanglesEnergyPropagator&) = delete; }; // Enforces that the boxes with corners in (x, y), (x + dx, y), (x, y + dy) // and (x + dx, y + dy) do not overlap. void AddNonOverlappingRectangles( const std::vector& enforcement_literals, const std::vector& x, const std::vector& y, Model* model); // Non overlapping rectangles. This includes box with zero-areas. // The following is forbidden: // - a point box inside a box with a non zero area // - a line box overlapping a box with a non zero area // - one vertical line box crossing an horizontal line box. class NonOverlappingRectanglesDisjunctivePropagator : public PropagatorInterface { public: // The slow_propagators select which disjunctive algorithms to propagate. NonOverlappingRectanglesDisjunctivePropagator( NoOverlap2DConstraintHelper* helper, Model* model); ~NonOverlappingRectanglesDisjunctivePropagator() override; bool Propagate() final; void Register(int fast_priority, int slow_priority); private: bool FindBoxesThatMustOverlapAHorizontalLineAndPropagate( bool fast_propagation, absl::Span boxes); NoOverlap2DConstraintHelper* helper_; SchedulingConstraintHelper x_; GenericLiteralWatcher* watcher_; TimeLimit* time_limit_; int fast_id_; // Propagator id of the "fast" version. // Temporary data. std::vector indexed_boxes_; std::vector rectangles_; 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_; int last_helper_inprocessing_count_ = -1; absl::flat_hash_set> reduced_overlapping_boxes_; std::vector> boxes_to_propagate_; std::vector> disjoint_boxes_; std::vector non_zero_area_boxes_; DisjunctiveOverloadChecker overload_checker_; DisjunctiveDetectablePrecedences forward_detectable_precedences_; DisjunctiveDetectablePrecedences backward_detectable_precedences_; DisjunctiveNotLast forward_not_last_; DisjunctiveNotLast backward_not_last_; DisjunctiveEdgeFinding forward_edge_finding_; DisjunctiveEdgeFinding backward_edge_finding_; DisjunctiveWithTwoItems disjunctive_with_two_items_; NonOverlappingRectanglesDisjunctivePropagator( const NonOverlappingRectanglesDisjunctivePropagator&) = delete; NonOverlappingRectanglesDisjunctivePropagator& operator=( const NonOverlappingRectanglesDisjunctivePropagator&) = delete; }; // Propagator that compares the boxes pairwise. class RectanglePairwisePropagator : public PropagatorInterface { public: RectanglePairwisePropagator(NoOverlap2DConstraintHelper* helper, Model* model) : helper_(helper), shared_stats_(model->GetOrCreate()), params_(model->GetOrCreate()) {} ~RectanglePairwisePropagator() override; bool Propagate() final; int RegisterWith(GenericLiteralWatcher* watcher); private: RectanglePairwisePropagator(const RectanglePairwisePropagator&) = delete; RectanglePairwisePropagator& operator=(const RectanglePairwisePropagator&) = delete; // Return false if a conflict is found. bool FindRestrictionsAndPropagateConflict( absl::Span items1, absl::Span items2, std::vector* restrictions); bool PropagateTwoBoxes(const PairwiseRestriction& restriction); NoOverlap2DConstraintHelper* helper_; SharedStatistics* shared_stats_; const SatParameters* params_; int64_t num_calls_ = 0; int64_t num_pairwise_conflicts_ = 0; int64_t num_pairwise_propagations_ = 0; std::vector fixed_non_zero_area_boxes_; std::vector non_fixed_non_zero_area_boxes_; std::vector horizontal_zero_area_boxes_; std::vector vertical_zero_area_boxes_; std::vector point_zero_area_boxes_; }; } // namespace sat } // namespace operations_research #endif // ORTOOLS_SAT_DIFFN_H_