|
| 1 | +// Copyright 2010-2025 Google LLC |
| 2 | +// Licensed under the Apache License, Version 2.0 (the "License"); |
| 3 | +// you may not use this file except in compliance with the License. |
| 4 | +// You may obtain a copy of the License at |
| 5 | +// |
| 6 | +// http://www.apache.org/licenses/LICENSE-2.0 |
| 7 | +// |
| 8 | +// Unless required by applicable law or agreed to in writing, software |
| 9 | +// distributed under the License is distributed on an "AS IS" BASIS, |
| 10 | +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 11 | +// See the License for the specific language governing permissions and |
| 12 | +// limitations under the License. |
| 13 | + |
| 14 | +#include "ortools/sat/2d_distances_propagator.h" |
| 15 | + |
| 16 | +#include <cstdint> |
| 17 | +#include <string> |
| 18 | +#include <utility> |
| 19 | +#include <vector> |
| 20 | + |
| 21 | +#include "absl/container/flat_hash_map.h" |
| 22 | +#include "absl/log/check.h" |
| 23 | +#include "absl/log/log.h" |
| 24 | +#include "absl/types/span.h" |
| 25 | +#include "ortools/base/stl_util.h" |
| 26 | +#include "ortools/sat/cp_model.pb.h" |
| 27 | +#include "ortools/sat/integer.h" |
| 28 | +#include "ortools/sat/integer_base.h" |
| 29 | +#include "ortools/sat/linear_propagation.h" |
| 30 | +#include "ortools/sat/model.h" |
| 31 | +#include "ortools/sat/no_overlap_2d_helper.h" |
| 32 | +#include "ortools/sat/precedences.h" |
| 33 | +#include "ortools/sat/sat_base.h" |
| 34 | +#include "ortools/sat/scheduling_helpers.h" |
| 35 | +#include "ortools/sat/synchronization.h" |
| 36 | + |
| 37 | +namespace operations_research { |
| 38 | +namespace sat { |
| 39 | + |
| 40 | +Precedences2DPropagator::Precedences2DPropagator( |
| 41 | + NoOverlap2DConstraintHelper* helper, Model* model) |
| 42 | + : helper_(*helper), |
| 43 | + binary_relations_maps_(model->GetOrCreate<BinaryRelationsMaps>()), |
| 44 | + shared_stats_(model->GetOrCreate<SharedStatistics>()) { |
| 45 | + model->GetOrCreate<LinearPropagator>()->SetPushAffineUbForBinaryRelation(); |
| 46 | +} |
| 47 | + |
| 48 | +void Precedences2DPropagator::CollectPairsOfBoxesWithNonTrivialDistance() { |
| 49 | + helper_.SynchronizeAndSetDirection(); |
| 50 | + non_trivial_pairs_.clear(); |
| 51 | + |
| 52 | + struct VarUsage { |
| 53 | + // boxes[0=x, 1=y][0=start, 1=end] |
| 54 | + std::vector<int> boxes[2][2]; |
| 55 | + }; |
| 56 | + absl::flat_hash_map<IntegerVariable, VarUsage> var_to_box_and_coeffs; |
| 57 | + |
| 58 | + for (int dim = 0; dim < 2; ++dim) { |
| 59 | + const SchedulingConstraintHelper& dim_helper = |
| 60 | + dim == 0 ? helper_.x_helper() : helper_.y_helper(); |
| 61 | + for (int i = 0; i < helper_.NumBoxes(); ++i) { |
| 62 | + const absl::Span<const AffineExpression> interval_points = |
| 63 | + i == 0 ? dim_helper.Starts() : dim_helper.Ends(); |
| 64 | + for (int j = 0; j < 2; ++j) { |
| 65 | + if (interval_points[i].var != kNoIntegerVariable) { |
| 66 | + var_to_box_and_coeffs[PositiveVariable(interval_points[i].var)] |
| 67 | + .boxes[dim][j] |
| 68 | + .push_back(i); |
| 69 | + } |
| 70 | + } |
| 71 | + } |
| 72 | + } |
| 73 | + |
| 74 | + VLOG(2) << "CollectPairsOfBoxesWithNonTrivialDistance called, num_exprs: " |
| 75 | + << binary_relations_maps_->GetAllExpressionsWithAffineBounds().size(); |
| 76 | + for (const LinearExpression2& expr : |
| 77 | + binary_relations_maps_->GetAllExpressionsWithAffineBounds()) { |
| 78 | + auto it1 = var_to_box_and_coeffs.find(PositiveVariable(expr.vars[0])); |
| 79 | + auto it2 = var_to_box_and_coeffs.find(PositiveVariable(expr.vars[1])); |
| 80 | + if (it1 == var_to_box_and_coeffs.end() || |
| 81 | + it2 == var_to_box_and_coeffs.end()) { |
| 82 | + continue; |
| 83 | + } |
| 84 | + |
| 85 | + const VarUsage& usage1 = it1->second; |
| 86 | + const VarUsage& usage2 = it2->second; |
| 87 | + for (int dim = 0; dim < 2; ++dim) { |
| 88 | + const SchedulingConstraintHelper& dim_helper = |
| 89 | + dim == 0 ? helper_.x_helper() : helper_.y_helper(); |
| 90 | + for (const int box1 : usage1.boxes[dim][0 /* start */]) { |
| 91 | + for (const int box2 : usage2.boxes[dim][1 /* end */]) { |
| 92 | + const AffineExpression& start = dim_helper.Starts()[box1]; |
| 93 | + const AffineExpression& end = dim_helper.Ends()[box2]; |
| 94 | + LinearExpression2 expr2; |
| 95 | + expr2.vars[0] = start.var; |
| 96 | + expr2.vars[1] = NegationOf(end.var); |
| 97 | + expr2.coeffs[0] = start.coeff; |
| 98 | + expr2.coeffs[1] = end.coeff; |
| 99 | + expr2.SimpleCanonicalization(); |
| 100 | + expr2.DivideByGcd(); |
| 101 | + if (expr == expr2) { |
| 102 | + if (box1 < box2) { |
| 103 | + non_trivial_pairs_.push_back({box1, box2}); |
| 104 | + } else { |
| 105 | + non_trivial_pairs_.push_back({box2, box1}); |
| 106 | + } |
| 107 | + } |
| 108 | + } |
| 109 | + } |
| 110 | + } |
| 111 | + } |
| 112 | + |
| 113 | + gtl::STLSortAndRemoveDuplicates(&non_trivial_pairs_); |
| 114 | +} |
| 115 | + |
| 116 | +bool Precedences2DPropagator::Propagate() { |
| 117 | + if (!helper_.SynchronizeAndSetDirection()) return false; |
| 118 | + if (last_helper_inprocessing_count_ != helper_.InProcessingCount() || |
| 119 | + helper_.x_helper().CurrentDecisionLevel() == 0 || |
| 120 | + last_num_expressions_ != |
| 121 | + binary_relations_maps_->NumExpressionsWithAffineBounds()) { |
| 122 | + last_helper_inprocessing_count_ = helper_.InProcessingCount(); |
| 123 | + last_num_expressions_ = |
| 124 | + binary_relations_maps_->NumExpressionsWithAffineBounds(); |
| 125 | + CollectPairsOfBoxesWithNonTrivialDistance(); |
| 126 | + } |
| 127 | + |
| 128 | + num_calls_++; |
| 129 | + |
| 130 | + SchedulingConstraintHelper* helpers[2] = {&helper_.x_helper(), |
| 131 | + &helper_.y_helper()}; |
| 132 | + |
| 133 | + for (const auto& [box1, box2] : non_trivial_pairs_) { |
| 134 | + DCHECK(box1 < helper_.NumBoxes()); |
| 135 | + DCHECK(box2 < helper_.NumBoxes()); |
| 136 | + if (!helper_.IsPresent(box1) && !helper_.IsPresent(box2)) { |
| 137 | + continue; |
| 138 | + } |
| 139 | + |
| 140 | + bool is_unfeasible = true; |
| 141 | + for (int dim = 0; dim < 2; dim++) { |
| 142 | + const SchedulingConstraintHelper* helper = helpers[dim]; |
| 143 | + for (int j = 0; j < 2; j++) { |
| 144 | + int b1 = box1; |
| 145 | + int b2 = box2; |
| 146 | + if (j == 1) { |
| 147 | + std::swap(b1, b2); |
| 148 | + } |
| 149 | + LinearExpression2 expr; |
| 150 | + expr.vars[0] = helper->Starts()[b1].var; |
| 151 | + expr.vars[1] = NegationOf(helper->Ends()[b2].var); |
| 152 | + expr.coeffs[0] = helper->Starts()[b1].coeff; |
| 153 | + expr.coeffs[1] = helper->Ends()[b2].coeff; |
| 154 | + const IntegerValue ub_of_start_minus_end_value = |
| 155 | + binary_relations_maps_->UpperBound(expr) + |
| 156 | + helper->Starts()[b1].constant - helper->Ends()[b2].constant; |
| 157 | + if (ub_of_start_minus_end_value >= 0) { |
| 158 | + is_unfeasible = false; |
| 159 | + break; |
| 160 | + } |
| 161 | + if (!is_unfeasible) break; |
| 162 | + } |
| 163 | + } |
| 164 | + if (!is_unfeasible) continue; |
| 165 | + |
| 166 | + // We have a mandatory overlap on both x and y! Explain and propagate. |
| 167 | + |
| 168 | + helper_.ClearReason(); |
| 169 | + num_conflicts_++; |
| 170 | + std::vector<IntegerLiteral> reason; |
| 171 | + std::vector<Literal> lit_reason; |
| 172 | + |
| 173 | + for (int dim = 0; dim < 2; dim++) { |
| 174 | + SchedulingConstraintHelper* helper = helpers[dim]; |
| 175 | + for (int j = 0; j < 2; j++) { |
| 176 | + int b1 = box1; |
| 177 | + int b2 = box2; |
| 178 | + if (j == 1) { |
| 179 | + std::swap(b1, b2); |
| 180 | + } |
| 181 | + LinearExpression2 expr; |
| 182 | + expr.vars[0] = helper->Starts()[b1].var; |
| 183 | + expr.vars[1] = NegationOf(helper->Ends()[b2].var); |
| 184 | + expr.coeffs[0] = helper->Starts()[b1].coeff; |
| 185 | + expr.coeffs[1] = helper->Ends()[b2].coeff; |
| 186 | + binary_relations_maps_->AddReasonForUpperBoundLowerThan( |
| 187 | + expr, |
| 188 | + -(helper->Starts()[b1].constant - helper->Ends()[b2].constant), |
| 189 | + &lit_reason, &reason); |
| 190 | + } |
| 191 | + } |
| 192 | + helper_.AddPresenceReason(box1); |
| 193 | + helper_.AddPresenceReason(box2); |
| 194 | + helper_.x_helper().MutableIntegerReason()->insert( |
| 195 | + helper_.x_helper().MutableIntegerReason()->end(), reason.begin(), |
| 196 | + reason.end()); |
| 197 | + helper_.x_helper().MutableLiteralReason()->insert( |
| 198 | + helper_.x_helper().MutableLiteralReason()->end(), lit_reason.begin(), |
| 199 | + lit_reason.end()); |
| 200 | + return helper_.ReportConflict(); |
| 201 | + } |
| 202 | + return true; |
| 203 | +} |
| 204 | + |
| 205 | +int Precedences2DPropagator::RegisterWith(GenericLiteralWatcher* watcher) { |
| 206 | + const int id = watcher->Register(this); |
| 207 | + helper_.WatchAllBoxes(id); |
| 208 | + // TODO(user): add an API to BinaryRelationsMaps to watch linear2 |
| 209 | + return id; |
| 210 | +} |
| 211 | + |
| 212 | +Precedences2DPropagator::~Precedences2DPropagator() { |
| 213 | + if (!VLOG_IS_ON(1)) return; |
| 214 | + std::vector<std::pair<std::string, int64_t>> stats; |
| 215 | + stats.push_back({"Precedences2DPropagator/called", num_calls_}); |
| 216 | + stats.push_back({"Precedences2DPropagator/conflicts", num_conflicts_}); |
| 217 | + stats.push_back({"Precedences2DPropagator/pairs", non_trivial_pairs_.size()}); |
| 218 | + |
| 219 | + shared_stats_->AddStats(stats); |
| 220 | +} |
| 221 | + |
| 222 | +} // namespace sat |
| 223 | +} // namespace operations_research |
0 commit comments