Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
implied_bounds.cc
Go to the documentation of this file.
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
15
16#include <stddef.h>
17#include <stdint.h>
18
19#include <algorithm>
20#include <array>
21#include <bitset>
22#include <string>
23#include <utility>
24#include <vector>
25
26#include "absl/container/btree_map.h"
27#include "absl/container/flat_hash_map.h"
28#include "absl/container/flat_hash_set.h"
29#include "absl/log/check.h"
30#include "absl/log/log.h"
31#include "absl/log/vlog_is_on.h"
32#include "absl/meta/type_traits.h"
33#include "absl/types/span.h"
37#include "ortools/sat/clause.h"
38#include "ortools/sat/integer.h"
41#include "ortools/sat/model.h"
46#include "ortools/util/bitset.h"
49
50namespace operations_research {
51namespace sat {
52
53// Just display some global statistics on destruction.
55 if (!VLOG_IS_ON(1)) return;
56 if (shared_stats_ == nullptr) return;
57 std::vector<std::pair<std::string, int64_t>> stats;
58 stats.push_back({"implied_bound/num_deductions", num_deductions_});
59 stats.push_back({"implied_bound/num_stored", bounds_.size()});
60 stats.push_back(
61 {"implied_bound/num_stored_with_view", num_enqueued_in_var_to_bounds_});
62 shared_stats_->AddStats(stats);
63}
64
65bool ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) {
66 if (!parameters_.use_implied_bounds()) return true;
67 const IntegerVariable var = integer_literal.var;
68
69 // Ignore any Add() with a bound worse than the level zero one.
70 // TODO(user): Check that this never happen? it shouldn't.
71 const IntegerValue root_lb = integer_trail_->LevelZeroLowerBound(var);
72 if (integer_literal.bound <= root_lb) return true;
73
74 // We skip any IntegerLiteral referring to a variable with only two
75 // consecutive possible values. This is because, once shifted this will
76 // already be a variable in [0, 1] so we shouldn't gain much by substituing
77 // it.
78 if (root_lb + 1 >= integer_trail_->LevelZeroUpperBound(var)) return true;
79
80 // Add or update the current bound.
81 const auto key = std::make_pair(literal.Index(), var);
82 auto insert_result = bounds_.insert({key, integer_literal.bound});
83 if (!insert_result.second) {
84 if (insert_result.first->second < integer_literal.bound) {
85 insert_result.first->second = integer_literal.bound;
86 } else {
87 // No new info.
88 return true;
89 }
90 }
91
92 // Checks if the variable is now fixed.
93 if (integer_trail_->LevelZeroUpperBound(var) == integer_literal.bound) {
94 AddLiteralImpliesVarEqValue(literal, var, integer_literal.bound);
95 } else {
96 const auto it =
97 bounds_.find(std::make_pair(literal.Index(), NegationOf(var)));
98 if (it != bounds_.end() && it->second == -integer_literal.bound) {
99 AddLiteralImpliesVarEqValue(literal, var, integer_literal.bound);
100 }
101 }
102
103 // Check if we have any deduction. Since at least one of (literal,
104 // literal.Negated()) must be true, we can take the min bound as valid at
105 // level zero.
106 //
107 // TODO(user): Like in probing, we can also create hole in the domain if there
108 // is some implied bounds for (literal.NegatedIndex, NegagtionOf(var)) that
109 // crosses integer_literal.bound.
110 const auto it = bounds_.find(std::make_pair(literal.NegatedIndex(), var));
111 if (it != bounds_.end()) {
112 if (it->second <= root_lb) {
113 // The other bounds is worse than the new level-zero bound which can
114 // happen because of lazy update, so here we just remove it.
115 bounds_.erase(it);
116 } else {
117 const IntegerValue deduction =
118 std::min(integer_literal.bound, it->second);
119 DCHECK_GT(deduction, root_lb);
120
121 ++num_deductions_;
122 if (!integer_trail_->RootLevelEnqueue(
123 IntegerLiteral::GreaterOrEqual(var, deduction))) {
124 return false;
125 }
126
127 VLOG(2) << "Deduction old: "
129 var, integer_trail_->LevelZeroLowerBound(var))
130 << " new: " << IntegerLiteral::GreaterOrEqual(var, deduction);
131
132 // The entries that are equal to the min no longer need to be stored once
133 // the level zero bound is enqueued.
134 if (it->second == deduction) {
135 bounds_.erase(it);
136 }
137 if (integer_literal.bound == deduction) {
138 bounds_.erase(std::make_pair(literal.Index(), var));
139
140 // No need to update var_to_bounds_ in this case.
141 return true;
142 }
143 }
144 }
145
146 // The information below is currently only used for cuts.
147 // So no need to store it if we aren't going to use it.
148 if (parameters_.linearization_level() == 0) return true;
149 if (parameters_.cut_level() == 0) return true;
150
151 // If we have a new implied bound and the literal has a view, add it to
152 // var_to_bounds_. Note that we might add more than one entry with the same
153 // literal_view, and we will later need to lazily clean the vector up.
154 if (integer_encoder_->GetLiteralView(literal) != kNoIntegerVariable) {
155 if (var_to_bounds_.size() <= var) {
156 var_to_bounds_.resize(var.value() + 1);
157 has_implied_bounds_.Resize(var + 1);
158 }
159 ++num_enqueued_in_var_to_bounds_;
160 has_implied_bounds_.Set(var);
161 var_to_bounds_[var].emplace_back(integer_encoder_->GetLiteralView(literal),
162 integer_literal.bound);
163 } else if (integer_encoder_->GetLiteralView(literal.Negated()) !=
165 if (var_to_bounds_.size() <= var) {
166 var_to_bounds_.resize(var.value() + 1);
167 has_implied_bounds_.Resize(var + 1);
168 }
169 ++num_enqueued_in_var_to_bounds_;
170 has_implied_bounds_.Set(var);
171 var_to_bounds_[var].emplace_back(
172 NegationOf(integer_encoder_->GetLiteralView(literal.Negated())),
173 integer_literal.bound);
174 }
175 return true;
176}
177
178const std::vector<ImpliedBoundEntry>& ImpliedBounds::GetImpliedBounds(
179 IntegerVariable var) {
180 if (var >= var_to_bounds_.size()) return empty_implied_bounds_;
181
182 // Lazily remove obsolete entries from the vector.
183 //
184 // TODO(user): Check no duplicate and remove old entry if the enforcement
185 // is tighter.
186 int new_size = 0;
187 std::vector<ImpliedBoundEntry>& ref = var_to_bounds_[var];
188 const IntegerValue root_lb = integer_trail_->LevelZeroLowerBound(var);
189 for (const ImpliedBoundEntry& entry : ref) {
190 if (entry.lower_bound <= root_lb) continue;
191 ref[new_size++] = entry;
192 }
193 ref.resize(new_size);
194
195 return ref;
196}
197
199 IntegerVariable var,
200 IntegerValue value) {
201 if (!VariableIsPositive(var)) {
202 var = NegationOf(var);
203 value = -value;
204 }
205 literal_to_var_to_value_[literal.Index()][var] = value;
206}
207
209 if (!parameters_.use_implied_bounds()) return true;
210
211 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 1);
212 tmp_integer_literals_.clear();
213 integer_trail_->AppendNewBounds(&tmp_integer_literals_);
214 for (const IntegerLiteral lit : tmp_integer_literals_) {
215 if (!Add(first_decision, lit)) return false;
216 }
217 return true;
218}
219
220void ElementEncodings::Add(IntegerVariable var,
221 const std::vector<ValueLiteralPair>& encoding,
222 int exactly_one_index) {
223 if (!var_to_index_to_element_encodings_.contains(var)) {
224 element_encoded_variables_.push_back(var);
225 }
226 var_to_index_to_element_encodings_[var][exactly_one_index] = encoding;
227}
228
229const absl::btree_map<int, std::vector<ValueLiteralPair>>&
230ElementEncodings::Get(IntegerVariable var) {
231 const auto& it = var_to_index_to_element_encodings_.find(var);
232 if (it == var_to_index_to_element_encodings_.end()) {
233 return empty_element_encoding_;
234 } else {
235 return it->second;
236 }
237}
238
239const std::vector<IntegerVariable>&
241 return element_encoded_variables_;
242}
243
244// If a variable has a size of 2, it is most likely reduced to an affine
245// expression pointing to a variable with domain [0,1] or [-1,0].
246// If the original variable has been removed from the model, then there are no
247// implied values from any exactly_one constraint to its domain.
248// If we are lucky, one of the literal of the exactly_one constraints, and its
249// negation are used to encode the Boolean variable of the affine.
250//
251// This may fail if exactly_one(l0, l1, l2, l3); l0 and l1 imply x = 0,
252// l2 and l3 imply x = 1. In that case, one must look at the binary
253// implications to find the missing link.
254//
255// TODO(user): Consider removing this once we are more complete in our implied
256// bounds repository. Because if we can reconcile an encoding, then any of the
257// literal in the at most one should imply a value on the boolean view use in
258// the size2 affine.
259std::vector<LiteralValueValue> TryToReconcileEncodings(
260 const AffineExpression& size2_affine, const AffineExpression& affine,
261 absl::Span<const ValueLiteralPair> affine_var_encoding,
262 bool put_affine_left_in_result, IntegerEncoder* integer_encoder) {
263 IntegerVariable binary = size2_affine.var;
264 std::vector<LiteralValueValue> terms;
265 if (!integer_encoder->VariableIsFullyEncoded(binary)) return terms;
266 const std::vector<ValueLiteralPair>& size2_enc =
267 integer_encoder->FullDomainEncoding(binary);
268
269 // TODO(user): I am not sure how this can happen since size2_affine is
270 // supposed to be non-fixed. Maybe we miss some propag. Investigate.
271 if (size2_enc.size() != 2) return terms;
272
273 Literal lit0 = size2_enc[0].literal;
274 IntegerValue value0 = size2_affine.ValueAt(size2_enc[0].value);
275 Literal lit1 = size2_enc[1].literal;
276 IntegerValue value1 = size2_affine.ValueAt(size2_enc[1].value);
277
278 for (const auto& [unused, candidate_literal] : affine_var_encoding) {
279 if (candidate_literal == lit1) {
280 std::swap(lit0, lit1);
281 std::swap(value0, value1);
282 }
283 if (candidate_literal != lit0) continue;
284
285 // Build the decomposition.
286 for (const auto& [value, literal] : affine_var_encoding) {
287 const IntegerValue size_2_value = literal == lit0 ? value0 : value1;
288 const IntegerValue affine_value = affine.ValueAt(value);
289 if (put_affine_left_in_result) {
290 terms.push_back({literal, affine_value, size_2_value});
291 } else {
292 terms.push_back({literal, size_2_value, affine_value});
293 }
294 }
295 break;
296 }
297
298 return terms;
299}
300
301// Specialized case of encoding reconciliation when both variables have a domain
302// of size of 2.
303std::vector<LiteralValueValue> TryToReconcileSize2Encodings(
304 const AffineExpression& left, const AffineExpression& right,
305 IntegerEncoder* integer_encoder) {
306 std::vector<LiteralValueValue> terms;
307 if (!integer_encoder->VariableIsFullyEncoded(left.var) ||
308 !integer_encoder->VariableIsFullyEncoded(right.var)) {
309 return terms;
310 }
311 const std::vector<ValueLiteralPair> left_enc =
312 integer_encoder->FullDomainEncoding(left.var);
313 const std::vector<ValueLiteralPair> right_enc =
314 integer_encoder->FullDomainEncoding(right.var);
315 if (left_enc.size() != 2 || right_enc.size() != 2) {
316 VLOG(2) << "encodings are not fully propagated";
317 return terms;
318 }
319
320 const Literal left_lit0 = left_enc[0].literal;
321 const IntegerValue left_value0 = left.ValueAt(left_enc[0].value);
322 const Literal left_lit1 = left_enc[1].literal;
323 const IntegerValue left_value1 = left.ValueAt(left_enc[1].value);
324
325 const Literal right_lit0 = right_enc[0].literal;
326 const IntegerValue right_value0 = right.ValueAt(right_enc[0].value);
327 const Literal right_lit1 = right_enc[1].literal;
328 const IntegerValue right_value1 = right.ValueAt(right_enc[1].value);
329
330 if (left_lit0 == right_lit0 || left_lit0 == right_lit1.Negated()) {
331 terms.push_back({left_lit0, left_value0, right_value0});
332 terms.push_back({left_lit0.Negated(), left_value1, right_value1});
333 } else if (left_lit0 == right_lit1 || left_lit0 == right_lit0.Negated()) {
334 terms.push_back({left_lit0, left_value0, right_value1});
335 terms.push_back({left_lit0.Negated(), left_value1, right_value0});
336 } else if (left_lit1 == right_lit1 || left_lit1 == right_lit0.Negated()) {
337 terms.push_back({left_lit1.Negated(), left_value0, right_value0});
338 terms.push_back({left_lit1, left_value1, right_value1});
339 } else if (left_lit1 == right_lit0 || left_lit1 == right_lit1.Negated()) {
340 terms.push_back({left_lit1.Negated(), left_value0, right_value1});
341 terms.push_back({left_lit1, left_value1, right_value0});
342 } else {
343 VLOG(3) << "Complex size 2 encoding case, need to scan exactly_ones";
344 }
345
346 return terms;
347}
348
349std::vector<LiteralValueValue> ProductDecomposer::TryToDecompose(
350 const AffineExpression& left, const AffineExpression& right) {
351 if (integer_trail_->IsFixed(left) || integer_trail_->IsFixed(right)) {
352 return {};
353 }
354
355 // Fill in the encodings for the left variable.
356 const absl::btree_map<int, std::vector<ValueLiteralPair>>& left_encodings =
357 element_encodings_->Get(left.var);
358
359 // Fill in the encodings for the right variable.
360 const absl::btree_map<int, std::vector<ValueLiteralPair>>& right_encodings =
361 element_encodings_->Get(right.var);
362
363 std::vector<int> compatible_keys;
364 for (const auto& [index, encoding] : left_encodings) {
365 if (right_encodings.contains(index)) {
366 compatible_keys.push_back(index);
367 }
368 }
369
370 if (compatible_keys.empty()) {
371 if (integer_trail_->InitialVariableDomain(left.var).Size() == 2) {
372 for (const auto& [index, right_encoding] : right_encodings) {
373 const std::vector<LiteralValueValue> result = TryToReconcileEncodings(
374 left, right, right_encoding,
375 /*put_affine_left_in_result=*/false, integer_encoder_);
376 if (!result.empty()) {
377 return result;
378 }
379 }
380 }
381 if (integer_trail_->InitialVariableDomain(right.var).Size() == 2) {
382 for (const auto& [index, left_encoding] : left_encodings) {
383 const std::vector<LiteralValueValue> result = TryToReconcileEncodings(
384 right, left, left_encoding,
385 /*put_affine_left_in_result=*/true, integer_encoder_);
386 if (!result.empty()) {
387 return result;
388 }
389 }
390 }
391 if (integer_trail_->InitialVariableDomain(left.var).Size() == 2 &&
392 integer_trail_->InitialVariableDomain(right.var).Size() == 2) {
393 const std::vector<LiteralValueValue> result =
394 TryToReconcileSize2Encodings(left, right, integer_encoder_);
395 if (!result.empty()) {
396 return result;
397 }
398 }
399 return {};
400 }
401
402 if (compatible_keys.size() > 1) {
403 VLOG(3) << "More than one exactly_one involved in the encoding of the two "
404 "variables";
405 }
406
407 // Select the compatible encoding with the minimum index.
408 const int min_index =
409 *std::min_element(compatible_keys.begin(), compatible_keys.end());
410 // By construction, encodings follow the order of literals in the exactly_one
411 // constraint.
412 const std::vector<ValueLiteralPair>& left_encoding =
413 left_encodings.at(min_index);
414 const std::vector<ValueLiteralPair>& right_encoding =
415 right_encodings.at(min_index);
416 DCHECK_EQ(left_encoding.size(), right_encoding.size());
417
418 // Build decomposition of the product.
419 std::vector<LiteralValueValue> terms;
420 for (int i = 0; i < left_encoding.size(); ++i) {
421 const Literal literal = left_encoding[i].literal;
422 DCHECK_EQ(literal, right_encoding[i].literal);
423 terms.push_back({literal, left.ValueAt(left_encoding[i].value),
424 right.ValueAt(right_encoding[i].value)});
425 }
426
427 return terms;
428}
429
430// TODO(user): Experiment with x * x where constants = 0, x is
431// fully encoded, and the domain is small.
433 const AffineExpression& right,
434 LinearConstraintBuilder* builder) {
435 DCHECK(builder != nullptr);
436 builder->Clear();
437
438 if (integer_trail_->IsFixed(left)) {
439 if (integer_trail_->IsFixed(right)) {
440 builder->AddConstant(integer_trail_->FixedValue(left) *
441 integer_trail_->FixedValue(right));
442 return true;
443 }
444 builder->AddTerm(right, integer_trail_->FixedValue(left));
445 return true;
446 }
447
448 if (integer_trail_->IsFixed(right)) {
449 builder->AddTerm(left, integer_trail_->FixedValue(right));
450 return true;
451 }
452
453 // Linearization is possible if both left and right have the same Boolean
454 // variable.
455 if (PositiveVariable(left.var) == PositiveVariable(right.var) &&
456 integer_trail_->LowerBound(PositiveVariable(left.var)) == 0 &&
457 integer_trail_->UpperBound(PositiveVariable(left.var)) == 1) {
458 const IntegerValue left_coeff =
459 VariableIsPositive(left.var) ? left.coeff : -left.coeff;
460 const IntegerValue right_coeff =
461 VariableIsPositive(right.var) ? right.coeff : -right.coeff;
462 builder->AddTerm(PositiveVariable(left.var),
463 left_coeff * right_coeff + left.constant * right_coeff +
464 left_coeff * right.constant);
465 builder->AddConstant(left.constant * right.constant);
466 return true;
467 }
468
469 const std::vector<LiteralValueValue> decomposition =
470 TryToDecompose(left, right);
471 if (decomposition.empty()) return false;
472
473 IntegerValue min_coefficient = kMaxIntegerValue;
474 for (const LiteralValueValue& term : decomposition) {
475 min_coefficient =
476 std::min(min_coefficient, term.left_value * term.right_value);
477 }
478 for (const LiteralValueValue& term : decomposition) {
479 const IntegerValue coefficient =
480 term.left_value * term.right_value - min_coefficient;
481 if (coefficient == 0) continue;
482 if (!builder->AddLiteralTerm(term.literal, coefficient)) {
483 return false;
484 }
485 }
486 builder->AddConstant(min_coefficient);
487 return true;
488}
489
491 : enabled_(
492 model->GetOrCreate<SatParameters>()->detect_linearized_product() &&
493 model->GetOrCreate<SatParameters>()->linearization_level() > 1),
494 rlt_enabled_(model->GetOrCreate<SatParameters>()->add_rlt_cuts() &&
495 model->GetOrCreate<SatParameters>()->linearization_level() >
496 1),
497 sat_solver_(model->GetOrCreate<SatSolver>()),
498 trail_(model->GetOrCreate<Trail>()),
499 integer_trail_(model->GetOrCreate<IntegerTrail>()),
500 integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
501 shared_stats_(model->GetOrCreate<SharedStatistics>()) {}
502
504 if (!VLOG_IS_ON(1)) return;
505 if (shared_stats_ == nullptr) return;
506 std::vector<std::pair<std::string, int64_t>> stats;
507 stats.push_back(
508 {"product_detector/num_processed_binary", num_processed_binary_});
509 stats.push_back(
510 {"product_detector/num_processed_exactly_one", num_processed_exo_});
511 stats.push_back(
512 {"product_detector/num_processed_ternary", num_processed_ternary_});
513 stats.push_back({"product_detector/num_trail_updates", num_trail_updates_});
514 stats.push_back({"product_detector/num_products", num_products_});
515 stats.push_back({"product_detector/num_conditional_equalities",
516 num_conditional_equalities_});
517 stats.push_back(
518 {"product_detector/num_conditional_zeros", num_conditional_zeros_});
519 stats.push_back({"product_detector/num_int_products", num_int_products_});
520 shared_stats_->AddStats(stats);
521}
522
524 absl::Span<const Literal> ternary_clause) {
525 if (ternary_clause.size() != 3) return;
526 ++num_processed_ternary_;
527
528 if (rlt_enabled_) ProcessTernaryClauseForRLT(ternary_clause);
529 if (!enabled_) return;
530
531 candidates_[GetKey(ternary_clause[0].Index(), ternary_clause[1].Index())]
532 .push_back(ternary_clause[2].Index());
533 candidates_[GetKey(ternary_clause[0].Index(), ternary_clause[2].Index())]
534 .push_back(ternary_clause[1].Index());
535 candidates_[GetKey(ternary_clause[1].Index(), ternary_clause[2].Index())]
536 .push_back(ternary_clause[0].Index());
537
538 // We mark the literal of the ternary clause as seen.
539 // Only a => b with a seen need to be looked at.
540 for (const Literal l : ternary_clause) {
541 if (l.Index() >= seen_.size()) seen_.resize(l.Index() + 1);
542 seen_[l.Index()] = true;
543 }
544}
545
546// If all have view, add to flat representation.
547void ProductDetector::ProcessTernaryClauseForRLT(
548 absl::Span<const Literal> ternary_clause) {
549 const int old_size = ternary_clauses_with_view_.size();
550 for (const Literal l : ternary_clause) {
551 const IntegerVariable var =
552 integer_encoder_->GetLiteralView(Literal(l.Variable(), true));
553 if (var == kNoIntegerVariable || !VariableIsPositive(var)) {
554 ternary_clauses_with_view_.resize(old_size);
555 return;
556 }
557 ternary_clauses_with_view_.push_back(l.IsPositive() ? var
558 : NegationOf(var));
559 }
560}
561
563 absl::Span<const Literal> ternary_exo) {
564 if (ternary_exo.size() != 3) return;
565 ++num_processed_exo_;
566
567 if (rlt_enabled_) ProcessTernaryClauseForRLT(ternary_exo);
568 if (!enabled_) return;
569
570 ProcessNewProduct(ternary_exo[0].Index(), ternary_exo[1].NegatedIndex(),
571 ternary_exo[2].NegatedIndex());
572 ProcessNewProduct(ternary_exo[1].Index(), ternary_exo[0].NegatedIndex(),
573 ternary_exo[2].NegatedIndex());
574 ProcessNewProduct(ternary_exo[2].Index(), ternary_exo[0].NegatedIndex(),
575 ternary_exo[1].NegatedIndex());
576}
577
578// TODO(user): As product are discovered, we could remove entries from our
579// hash maps!
581 absl::Span<const Literal> binary_clause) {
582 if (!enabled_) return;
583 if (binary_clause.size() != 2) return;
584 ++num_processed_binary_;
585 const std::array<LiteralIndex, 2> key =
586 GetKey(binary_clause[0].NegatedIndex(), binary_clause[1].NegatedIndex());
587 std::array<LiteralIndex, 3> ternary;
588 for (const LiteralIndex l : candidates_[key]) {
589 ternary[0] = key[0];
590 ternary[1] = key[1];
591 ternary[2] = l;
592 std::sort(ternary.begin(), ternary.end());
593 const int l_index = ternary[0] == l ? 0 : ternary[1] == l ? 1 : 2;
594 std::bitset<3>& bs = detector_[ternary];
595 if (bs[l_index]) continue;
596 bs[l_index] = true;
597 if (bs[0] && bs[1] && l_index != 2) {
598 ProcessNewProduct(ternary[2], Literal(ternary[0]).NegatedIndex(),
599 Literal(ternary[1]).NegatedIndex());
600 }
601 if (bs[0] && bs[2] && l_index != 1) {
602 ProcessNewProduct(ternary[1], Literal(ternary[0]).NegatedIndex(),
603 Literal(ternary[2]).NegatedIndex());
604 }
605 if (bs[1] && bs[2] && l_index != 0) {
606 ProcessNewProduct(ternary[0], Literal(ternary[1]).NegatedIndex(),
607 Literal(ternary[2]).NegatedIndex());
608 }
609 }
610}
611
613 if (!enabled_) return;
614 for (LiteralIndex a(0); a < seen_.size(); ++a) {
615 if (!seen_[a]) continue;
616 if (trail_->Assignment().LiteralIsAssigned(Literal(a))) continue;
617 const Literal not_a = Literal(a).Negated();
618 for (const Literal b : graph->DirectImplications(Literal(a))) {
619 ProcessBinaryClause({not_a, b}); // a => b;
620 }
621 }
622}
623
625 if (!enabled_) return;
626 if (trail_->CurrentDecisionLevel() != 1) return;
627 ++num_trail_updates_;
628
629 const SatSolver::Decision decision = sat_solver_->Decisions()[0];
630 if (decision.literal.Index() >= seen_.size() ||
631 !seen_[decision.literal.Index()]) {
632 return;
633 }
634 const Literal not_a = decision.literal.Negated();
635 const int current_index = trail_->Index();
636 for (int i = decision.trail_index + 1; i < current_index; ++i) {
637 const Literal b = (*trail_)[i];
638 ProcessBinaryClause({not_a, b});
639 }
640}
641
643 const auto it = products_.find(GetKey(a.Index(), b.Index()));
644 if (it == products_.end()) return kNoLiteralIndex;
645 return it->second;
646}
647
648std::array<LiteralIndex, 2> ProductDetector::GetKey(LiteralIndex a,
649 LiteralIndex b) const {
650 std::array<LiteralIndex, 2> key{a, b};
651 if (key[0] > key[1]) std::swap(key[0], key[1]);
652 return key;
653}
654
655void ProductDetector::ProcessNewProduct(LiteralIndex p, LiteralIndex a,
656 LiteralIndex b) {
657 // If many literal correspond to the same product, we just keep one.
658 ++num_products_;
659 products_[GetKey(a, b)] = p;
660
661 // This is used by ProductIsLinearizable().
662 has_product_.insert(
663 GetKey(Literal(a).IsPositive() ? a : Literal(a).NegatedIndex(),
664 Literal(b).IsPositive() ? b : Literal(b).NegatedIndex()));
665}
666
668 IntegerVariable b) const {
669 if (a == b) return true;
670 if (a == NegationOf(b)) return true;
671
672 // Otherwise, we need both a and b to be expressible as linear expression
673 // involving Booleans whose product is also expressible.
674 if (integer_trail_->InitialVariableDomain(a).Size() != 2) return false;
675 if (integer_trail_->InitialVariableDomain(b).Size() != 2) return false;
676
677 const LiteralIndex la =
678 integer_encoder_->GetAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
679 a, integer_trail_->LevelZeroUpperBound(a)));
680 if (la == kNoLiteralIndex) return false;
681
682 const LiteralIndex lb =
683 integer_encoder_->GetAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
684 b, integer_trail_->LevelZeroUpperBound(b)));
685 if (lb == kNoLiteralIndex) return false;
686
687 // Any product involving la/not(la) * lb/not(lb) can be used.
688 return has_product_.contains(
689 GetKey(Literal(la).IsPositive() ? la : Literal(la).NegatedIndex(),
690 Literal(lb).IsPositive() ? lb : Literal(lb).NegatedIndex()));
691}
692
694 IntegerVariable b) const {
695 const auto it = int_products_.find({a.Index(), PositiveVariable(b)});
696 if (it == int_products_.end()) return kNoIntegerVariable;
697 return VariableIsPositive(b) ? it->second : NegationOf(it->second);
698}
699
700void ProductDetector::ProcessNewProduct(IntegerVariable p, Literal l,
701 IntegerVariable x) {
702 if (!VariableIsPositive(x)) {
703 x = NegationOf(x);
704 p = NegationOf(p);
705 }
706
707 // We only store one product if there are many.
708 ++num_int_products_;
709 int_products_[{l.Index(), x}] = p;
710}
711
713 IntegerVariable y) {
714 ++num_conditional_equalities_;
715 if (x == y) return;
716
717 // We process both possibilities (product = x or product = y).
718 for (int i = 0; i < 2; ++i) {
719 if (!VariableIsPositive(x)) {
720 x = NegationOf(x);
721 y = NegationOf(y);
722 }
723 bool seen = false;
724
725 // TODO(user): Linear scan can be bad if b => X = many other variables.
726 // Hopefully this will not be common.
727 std::vector<IntegerVariable>& others =
728 conditional_equalities_[{l.Index(), x}];
729 for (const IntegerVariable o : others) {
730 if (o == y) {
731 seen = true;
732 break;
733 }
734 }
735
736 if (!seen) {
737 others.push_back(y);
738 if (conditional_zeros_.contains({l.NegatedIndex(), x})) {
739 ProcessNewProduct(/*p=*/x, l, y);
740 }
741 }
742 std::swap(x, y);
743 }
744}
745
747 ++num_conditional_zeros_;
748 p = PositiveVariable(p);
749 auto [_, inserted] = conditional_zeros_.insert({l.Index(), p});
750 if (inserted) {
751 const auto it = conditional_equalities_.find({l.NegatedIndex(), p});
752 if (it != conditional_equalities_.end()) {
753 for (const IntegerVariable x : it->second) {
754 ProcessNewProduct(p, l.Negated(), x);
755 }
756 }
757 }
758}
759
760namespace {
761
762std::pair<IntegerVariable, IntegerVariable> Canonicalize(IntegerVariable a,
763 IntegerVariable b) {
764 if (a < b) return {a, b};
765 return {b, a};
766}
767
768double GetLiteralLpValue(
769 IntegerVariable var,
770 const util_intops::StrongVector<IntegerVariable, double>& lp_values) {
771 return VariableIsPositive(var) ? lp_values[var]
772 : 1.0 - lp_values[PositiveVariable(var)];
773}
774
775} // namespace
776
777void ProductDetector::UpdateRLTMaps(
778 const util_intops::StrongVector<IntegerVariable, double>& lp_values,
779 IntegerVariable var1, double lp1, IntegerVariable var2, double lp2,
780 IntegerVariable bound_var, double bound_lp) {
781 // we have var1 * var2 <= bound_var, and this is only useful if it is better
782 // than the trivial bound <= var1 or <= var2.
783 if (bound_lp > lp1 && bound_lp > lp2) return;
784
785 const auto [it, inserted] =
786 bool_rlt_ubs_.insert({Canonicalize(var1, var2), bound_var});
787
788 // Replace if better.
789 if (!inserted && bound_lp < GetLiteralLpValue(it->second, lp_values)) {
790 it->second = bound_var;
791 }
792
793 // This will increase a RLT cut violation and is a good candidate.
794 if (lp1 * lp2 > bound_lp + 1e-4) {
795 bool_rlt_candidates_[var1].push_back(var2);
796 bool_rlt_candidates_[var2].push_back(var1);
797 }
798}
799
800// TODO(user): limit work if too many ternary.
802 absl::Span<const IntegerVariable> lp_vars,
804 // TODO(user): Maybe we shouldn't reconstruct this every time, but it is hard
805 // in case of multiple lps to make sure we don't use variables not in the lp
806 // otherwise.
807 bool_rlt_ubs_.clear();
808
809 // If we transform a linear constraint to sum positive_coeff * bool <= rhs.
810 // We will list all interesting multiplicative candidate for each variable.
811 bool_rlt_candidates_.clear();
812 const int size = ternary_clauses_with_view_.size();
813 if (size == 0) return;
814
815 is_in_lp_vars_.resize(integer_trail_->NumIntegerVariables().value());
816 for (const IntegerVariable var : lp_vars) is_in_lp_vars_.Set(var);
817
818 for (int i = 0; i < size; i += 3) {
819 const IntegerVariable var1 = ternary_clauses_with_view_[i];
820 const IntegerVariable var2 = ternary_clauses_with_view_[i + 1];
821 const IntegerVariable var3 = ternary_clauses_with_view_[i + 2];
822
823 if (!is_in_lp_vars_[PositiveVariable(var1)]) continue;
824 if (!is_in_lp_vars_[PositiveVariable(var2)]) continue;
825 if (!is_in_lp_vars_[PositiveVariable(var3)]) continue;
826
827 // If we have l1 + l2 + l3 >= 1, then for all (i, j) pair we have
828 // !li * !lj <= lk. We are looking for violation like this.
829 const double lp1 = GetLiteralLpValue(var1, lp_values);
830 const double lp2 = GetLiteralLpValue(var2, lp_values);
831 const double lp3 = GetLiteralLpValue(var3, lp_values);
832
833 UpdateRLTMaps(lp_values, NegationOf(var1), 1.0 - lp1, NegationOf(var2),
834 1.0 - lp2, var3, lp3);
835 UpdateRLTMaps(lp_values, NegationOf(var1), 1.0 - lp1, NegationOf(var3),
836 1.0 - lp3, var2, lp2);
837 UpdateRLTMaps(lp_values, NegationOf(var2), 1.0 - lp2, NegationOf(var3),
838 1.0 - lp3, var1, lp1);
839 }
840
841 // Clear.
842 // TODO(user): Just switch to memclear() when dense.
843 for (const IntegerVariable var : lp_vars) is_in_lp_vars_.ClearBucket(var);
844}
845
846} // namespace sat
847} // namespace operations_research
const std::vector< Literal > & DirectImplications(Literal literal)
Definition clause.cc:2466
void Add(IntegerVariable var, const std::vector< ValueLiteralPair > &encoding, int exactly_one_index)
const absl::btree_map< int, std::vector< ValueLiteralPair > > & Get(IntegerVariable var)
Returns an empty map if there is no such encoding.
const std::vector< IntegerVariable > & GetElementEncodedVariables() const
Get an unsorted set of variables appearing in element encodings.
bool ProcessIntegerTrail(Literal first_decision)
~ImpliedBounds()
Just display some global statistics on destruction.
void AddLiteralImpliesVarEqValue(Literal literal, IntegerVariable var, IntegerValue value)
Adds literal => var == value.
bool Add(Literal literal, IntegerLiteral integer_literal)
const std::vector< ImpliedBoundEntry > & GetImpliedBounds(IntegerVariable var)
const std::vector< ValueLiteralPair > & FullDomainEncoding(IntegerVariable var) const
Definition integer.cc:146
IntegerVariable GetLiteralView(Literal lit) const
Definition integer.h:249
bool VariableIsFullyEncoded(IntegerVariable var) const
Definition integer.cc:111
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff=IntegerValue(1))
void AddTerm(IntegerVariable var, IntegerValue coeff)
void AddConstant(IntegerValue value)
Adds the corresponding term to the current linear expression.
void Clear()
Clears all added terms and constants. Keeps the original bounds.
LiteralIndex NegatedIndex() const
Definition sat_base.h:92
LiteralIndex Index() const
Definition sat_base.h:91
bool TryToLinearize(const AffineExpression &left, const AffineExpression &right, LinearConstraintBuilder *builder)
std::vector< LiteralValueValue > TryToDecompose(const AffineExpression &left, const AffineExpression &right)
void InitializeBooleanRLTCuts(absl::Span< const IntegerVariable > lp_vars, const util_intops::StrongVector< IntegerVariable, double > &lp_values)
void ProcessTernaryClause(absl::Span< const Literal > ternary_clause)
void ProcessTernaryExactlyOne(absl::Span< const Literal > ternary_exo)
void ProcessImplicationGraph(BinaryImplicationGraph *graph)
Utility function to process a bunch of implication all at once.
LiteralIndex GetProduct(Literal a, Literal b) const
Query function mainly used for testing.
bool ProductIsLinearizable(IntegerVariable a, IntegerVariable b) const
void ProcessConditionalEquality(Literal l, IntegerVariable x, IntegerVariable y)
void ProcessConditionalZero(Literal l, IntegerVariable p)
void ProcessBinaryClause(absl::Span< const Literal > binary_clause)
Simple class to add statistics by name and print them at the end.
iterator insert(const_iterator pos, const value_type &x)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::vector< LiteralValueValue > TryToReconcileSize2Encodings(const AffineExpression &left, const AffineExpression &right, IntegerEncoder *integer_encoder)
const LiteralIndex kNoLiteralIndex(-1)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
std::vector< LiteralValueValue > TryToReconcileEncodings(const AffineExpression &size2_affine, const AffineExpression &affine, absl::Span< const ValueLiteralPair > affine_var_encoding, bool put_affine_left_in_result, IntegerEncoder *integer_encoder)
bool VariableIsPositive(IntegerVariable i)
In SWIG mode, we don't want anything besides these top-level includes.
IntegerValue ValueAt(IntegerValue var_value) const
Returns the value of this affine expression given its variable value.
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)