Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
presolve_context.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 <algorithm>
17#include <cstdint>
18#include <cstdlib>
19#include <limits>
20#include <numeric>
21#include <optional>
22#include <string>
23#include <tuple>
24#include <utility>
25#include <vector>
26
27#include "absl/base/attributes.h"
28#include "absl/container/btree_map.h"
29#include "absl/container/flat_hash_map.h"
30#include "absl/container/flat_hash_set.h"
31#include "absl/flags/flag.h"
32#include "absl/log/check.h"
33#include "absl/log/log.h"
34#include "absl/log/vlog_is_on.h"
35#include "absl/meta/type_traits.h"
36#include "absl/numeric/int128.h"
37#include "absl/strings/str_cat.h"
38#include "absl/strings/string_view.h"
39#include "absl/types/span.h"
46#include "ortools/sat/integer.h"
48#include "ortools/sat/model.h"
51#include "ortools/sat/util.h"
53#include "ortools/util/bitset.h"
58
59ABSL_FLAG(bool, cp_model_debug_postsolve, false,
60 "DEBUG ONLY. When set to true, the mapping_model.proto will contains "
61 "file:line of the code that created that constraint. This is helpful "
62 "for debugging postsolve");
63
64namespace operations_research {
65namespace sat {
66
68 return context->GetLiteralRepresentative(ref_);
69}
70
71int SavedVariable::Get() const { return ref_; }
72
73void PresolveContext::ClearStats() { stats_by_rule_name_.clear(); }
74
76 IntegerVariableProto* const var = working_model->add_variables();
77 FillDomainInProto(domain, var);
79 return working_model->variables_size() - 1;
80}
81
83 const Domain& domain, absl::Span<const std::pair<int, int64_t>> definition,
84 bool append_constraint_to_mapping_model) {
85 if (domain.Size() == 1) {
86 UpdateRuleStats("TODO new_var_definition : use boolean equation");
87 }
88
89 const int new_var = NewIntVar(domain);
90
91 // Create new linear constraint new_var = definition.
92 // TODO(user): When we encounter overflow (rare), we still create a variable.
93 auto* new_linear =
94 append_constraint_to_mapping_model
95 ? NewMappingConstraint(__FILE__, __LINE__)->mutable_linear()
96 : working_model->add_constraints()->mutable_linear();
97 for (const auto [var, coeff] : definition) {
98 new_linear->add_vars(var);
99 new_linear->add_coeffs(coeff);
100 }
101 new_linear->add_vars(new_var);
102 new_linear->add_coeffs(-1);
103 new_linear->add_domain(0);
104 new_linear->add_domain(0);
105 if (PossibleIntegerOverflow(*working_model, new_linear->vars(),
106 new_linear->coeffs())) {
107 UpdateRuleStats("TODO new_var_definition : possible overflow.");
108 if (append_constraint_to_mapping_model) {
109 mapping_model->mutable_constraints()->RemoveLast();
110 } else {
111 working_model->mutable_constraints()->RemoveLast();
112 }
113 return -1;
114 }
115 if (!append_constraint_to_mapping_model) {
117 }
118
119 solution_crush_.SetVarToLinearExpression(new_var, definition);
120 return new_var;
121}
122
123int PresolveContext::NewBoolVar(absl::string_view source) {
124 UpdateRuleStats(absl::StrCat("new_bool: ", source));
125 return NewIntVar(Domain(0, 1));
126}
127
128int PresolveContext::NewBoolVarWithClause(absl::Span<const int> clause) {
129 const int new_var = NewBoolVar("with clause");
130 solution_crush_.SetVarToClause(new_var, clause);
131 return new_var;
132}
133
135 absl::Span<const int> conjunction) {
136 const int new_var = NewBoolVar("with conjunction");
137 solution_crush_.SetVarToConjunction(new_var, conjunction);
138 return new_var;
139}
140
142 if (!true_literal_is_defined_) {
143 true_literal_is_defined_ = true;
144 true_literal_ = NewIntVar(Domain(1));
145 solution_crush_.SetVarToConjunction(true_literal_, {});
146 }
147 return true_literal_;
148}
149
151
152// a => b.
154 if (a == b) return;
155 ConstraintProto* const ct = working_model->add_constraints();
158}
159
160// b => x in [lb, ub].
161void PresolveContext::AddImplyInDomain(int b, int x, const Domain& domain) {
162 ConstraintProto* const imply = working_model->add_constraints();
163
164 // Doing it like this seems to use slightly less memory.
165 // TODO(user): Find the best way to create such small proto.
166 imply->mutable_enforcement_literal()->Resize(1, b);
167 LinearConstraintProto* mutable_linear = imply->mutable_linear();
168 mutable_linear->mutable_vars()->Resize(1, x);
169 mutable_linear->mutable_coeffs()->Resize(1, 1);
170 FillDomainInProto(domain, mutable_linear);
171}
172
174 const Domain& domain) {
175 ConstraintProto* const imply = working_model->add_constraints();
176
177 imply->mutable_enforcement_literal()->Resize(1, b);
178 LinearConstraintProto* mutable_linear = imply->mutable_linear();
179 FillDomainInProto(domain, mutable_linear);
181}
182
184 return domains_[PositiveRef(ref)].IsEmpty();
185}
186
187bool PresolveContext::IsFixed(int ref) const {
188 DCHECK_LT(PositiveRef(ref), domains_.size());
189 DCHECK(!DomainIsEmpty(ref));
190 return domains_[PositiveRef(ref)].IsFixed();
191}
192
194 const int var = PositiveRef(ref);
195 return domains_[var].Min() >= 0 && domains_[var].Max() <= 1;
196}
197
199 DCHECK(CanBeUsedAsLiteral(lit));
200 if (RefIsPositive(lit)) {
201 return domains_[lit].Min() == 1;
202 } else {
203 return domains_[PositiveRef(lit)].Max() == 0;
204 }
205}
206
208 DCHECK(CanBeUsedAsLiteral(lit));
209 if (RefIsPositive(lit)) {
210 return domains_[lit].Max() == 0;
211 } else {
212 return domains_[PositiveRef(lit)].Min() == 1;
213 }
214}
215
216int64_t PresolveContext::MinOf(int ref) const {
217 DCHECK(!DomainIsEmpty(ref));
218 return RefIsPositive(ref) ? domains_[PositiveRef(ref)].Min()
219 : -domains_[PositiveRef(ref)].Max();
220}
221
222int64_t PresolveContext::MaxOf(int ref) const {
223 DCHECK(!DomainIsEmpty(ref));
224 return RefIsPositive(ref) ? domains_[PositiveRef(ref)].Max()
225 : -domains_[PositiveRef(ref)].Min();
226}
227
228int64_t PresolveContext::FixedValue(int ref) const {
229 DCHECK(!DomainIsEmpty(ref));
230 CHECK(IsFixed(ref));
231 return RefIsPositive(ref) ? domains_[PositiveRef(ref)].Min()
232 : -domains_[PositiveRef(ref)].Min();
233}
234
236 int64_t result = expr.offset();
237 for (int i = 0; i < expr.vars_size(); ++i) {
238 const int64_t coeff = expr.coeffs(i);
239 if (coeff > 0) {
240 result += coeff * MinOf(expr.vars(i));
241 } else {
242 result += coeff * MaxOf(expr.vars(i));
243 }
244 }
245 return result;
246}
247
249 int64_t result = expr.offset();
250 for (int i = 0; i < expr.vars_size(); ++i) {
251 const int64_t coeff = expr.coeffs(i);
252 if (coeff > 0) {
253 result += coeff * MaxOf(expr.vars(i));
254 } else {
255 result += coeff * MinOf(expr.vars(i));
256 }
257 }
258 return result;
259}
260
262 for (int i = 0; i < expr.vars_size(); ++i) {
263 if (expr.coeffs(i) != 0 && !IsFixed(expr.vars(i))) return false;
264 }
265 return true;
266}
267
269 int64_t result = expr.offset();
270 for (int i = 0; i < expr.vars_size(); ++i) {
271 if (expr.coeffs(i) == 0) continue;
272 result += expr.coeffs(i) * FixedValue(expr.vars(i));
273 }
274 return result;
275}
276
278 const LinearExpressionProto& expr) const {
279 int64_t result = expr.offset();
280 for (int i = 0; i < expr.vars_size(); ++i) {
281 if (expr.coeffs(i) == 0) continue;
282 const Domain& domain = domains_[expr.vars(i)];
283 if (!domain.IsFixed()) return std::nullopt;
284 result += expr.coeffs(i) * domain.Min();
285 }
286 return result;
287}
288
290 const LinearExpressionProto& expr) const {
291 Domain result(expr.offset());
292 for (int i = 0; i < expr.vars_size(); ++i) {
293 result = result.AdditionWith(
294 DomainOf(expr.vars(i)).MultiplicationBy(expr.coeffs(i)));
295 }
296 return result;
297}
298
300 const LinearExpressionProto& expr) const {
301 if (expr.vars().size() != 1) return false;
302 return CanBeUsedAsLiteral(expr.vars(0));
303}
304
306 const LinearExpressionProto& expr) const {
307 const int ref = expr.vars(0);
308 return RefIsPositive(ref) == (expr.coeffs(0) > 0) ? ref : NegatedRef(ref);
309}
310
312 const LinearExpressionProto& expr) const {
313 return expr.offset() == 0 && expr.vars_size() == 1 && expr.coeffs(0) == 1;
314}
315
317 int* literal) const {
318 if (expr.vars_size() != 1) return false;
319 const int ref = expr.vars(0);
320 const int var = PositiveRef(ref);
321 if (MinOf(var) < 0 || MaxOf(var) > 1) return false;
322
323 if (expr.offset() == 0 && expr.coeffs(0) == 1 && RefIsPositive(ref)) {
324 if (literal != nullptr) *literal = ref;
325 return true;
326 }
327 if (expr.offset() == 1 && expr.coeffs(0) == -1 && RefIsPositive(ref)) {
328 if (literal != nullptr) *literal = NegatedRef(ref);
329 return true;
330 }
331 if (expr.offset() == 1 && expr.coeffs(0) == 1 && !RefIsPositive(ref)) {
332 if (literal != nullptr) *literal = ref;
333 return true;
334 }
335 return false;
336}
337
338// Note that we only support converted intervals.
340 const ConstraintProto& proto = working_model->constraints(ct_ref);
341 if (!proto.enforcement_literal().empty()) return false;
342 if (!IsFixed(proto.interval().start())) return false;
343 if (!IsFixed(proto.interval().size())) return false;
344 if (!IsFixed(proto.interval().end())) return false;
345 return true;
346}
347
348std::string PresolveContext::IntervalDebugString(int ct_ref) const {
349 if (IntervalIsConstant(ct_ref)) {
350 return absl::StrCat("interval_", ct_ref, "(", StartMin(ct_ref), "..",
351 EndMax(ct_ref), ")");
352 } else if (ConstraintIsOptional(ct_ref)) {
353 const int literal =
354 working_model->constraints(ct_ref).enforcement_literal(0);
355 if (SizeMin(ct_ref) == SizeMax(ct_ref)) {
356 return absl::StrCat("interval_", ct_ref, "(lit=", literal, ", ",
357 StartMin(ct_ref), " --(", SizeMin(ct_ref), ")--> ",
358 EndMax(ct_ref), ")");
359 } else {
360 return absl::StrCat("interval_", ct_ref, "(lit=", literal, ", ",
361 StartMin(ct_ref), " --(", SizeMin(ct_ref), "..",
362 SizeMax(ct_ref), ")--> ", EndMax(ct_ref), ")");
363 }
364 } else if (SizeMin(ct_ref) == SizeMax(ct_ref)) {
365 return absl::StrCat("interval_", ct_ref, "(", StartMin(ct_ref), " --(",
366 SizeMin(ct_ref), ")--> ", EndMax(ct_ref), ")");
367 } else {
368 return absl::StrCat("interval_", ct_ref, "(", StartMin(ct_ref), " --(",
369 SizeMin(ct_ref), "..", SizeMax(ct_ref), ")--> ",
370 EndMax(ct_ref), ")");
371 }
372}
373
374int64_t PresolveContext::StartMin(int ct_ref) const {
375 const IntervalConstraintProto& interval =
376 working_model->constraints(ct_ref).interval();
377 return MinOf(interval.start());
378}
379
380int64_t PresolveContext::StartMax(int ct_ref) const {
381 const IntervalConstraintProto& interval =
382 working_model->constraints(ct_ref).interval();
383 return MaxOf(interval.start());
384}
385
386int64_t PresolveContext::EndMin(int ct_ref) const {
387 const IntervalConstraintProto& interval =
388 working_model->constraints(ct_ref).interval();
389 return MinOf(interval.end());
390}
391
392int64_t PresolveContext::EndMax(int ct_ref) const {
393 const IntervalConstraintProto& interval =
394 working_model->constraints(ct_ref).interval();
395 return MaxOf(interval.end());
396}
397
398int64_t PresolveContext::SizeMin(int ct_ref) const {
399 const IntervalConstraintProto& interval =
400 working_model->constraints(ct_ref).interval();
401 return MinOf(interval.size());
402}
403
404int64_t PresolveContext::SizeMax(int ct_ref) const {
405 const IntervalConstraintProto& interval =
406 working_model->constraints(ct_ref).interval();
407 return MaxOf(interval.size());
408}
409
410// Tricky: If this variable is equivalent to another one (but not the
411// representative) and appear in just one constraint, then this constraint must
412// be the affine defining one. And in this case the code using this function
413// should do the proper stuff.
415 if (!ConstraintVariableGraphIsUpToDate()) return false;
416 const int var = PositiveRef(ref);
417 return var_to_constraints_[var].size() == 1;
418}
419
421 return !params_.keep_all_feasible_solutions_in_presolve() &&
422 VariableIsUnique(ref);
423}
424
426 if (!ConstraintVariableGraphIsUpToDate()) return false;
427 const int var = PositiveRef(ref);
428 return var_to_constraints_[var].size() == 2 &&
429 var_to_constraints_[var].contains(kObjectiveConstraint);
430}
431
432// Tricky: Same remark as for VariableIsUniqueAndRemovable().
433//
434// Also if the objective domain is constraining, we can't have a preferred
435// direction, so we cannot easily remove such variable.
437 if (!ConstraintVariableGraphIsUpToDate()) return false;
438 const int var = PositiveRef(ref);
439 return !params_.keep_all_feasible_solutions_in_presolve() &&
440 !objective_domain_is_constraining_ && VariableWithCostIsUnique(var);
441}
442
443// Here, even if the variable is equivalent to others, if its affine defining
444// constraints where removed, then it is not needed anymore.
446 if (!ConstraintVariableGraphIsUpToDate()) return false;
447 return var_to_constraints_[PositiveRef(ref)].empty();
448}
449
451 removed_variables_.insert(PositiveRef(ref));
452}
453
454// Note(user): I added an indirection and a function for this to be able to
455// display debug information when this return false. This should actually never
456// return false in the cases where it is used.
458 // It is okay to reuse removed fixed variable.
459 if (IsFixed(ref)) return false;
460 if (!removed_variables_.contains(PositiveRef(ref))) return false;
461 if (!var_to_constraints_[PositiveRef(ref)].empty()) {
462 SOLVER_LOG(logger_, "Variable ", PositiveRef(ref),
463 " was removed, yet it appears in some constraints!");
464 SOLVER_LOG(logger_, "affine relation: ",
466 for (const int c : var_to_constraints_[PositiveRef(ref)]) {
467 SOLVER_LOG(logger_, "constraint #", c, " : ",
468 c >= 0
469 ? ProtobufShortDebugString(working_model->constraints(c))
470 : "");
471 }
472 }
473 return true;
474}
475
477 int var) const {
478 CHECK(RefIsPositive(var));
479 if (!ConstraintVariableGraphIsUpToDate()) return false;
480 if (var_to_num_linear1_[var] == 0) return false;
481 return var_to_num_linear1_[var] == var_to_constraints_[var].size() ||
482 (var_to_constraints_[var].contains(kObjectiveConstraint) &&
483 var_to_num_linear1_[var] + 1 == var_to_constraints_[var].size());
484}
485
487 int var) const {
488 if (!ConstraintVariableGraphIsUpToDate()) return false;
489 if (var_to_num_linear1_[var] == 0) return false;
490 CHECK(RefIsPositive(var));
491 return var_to_num_linear1_[var] + 1 == var_to_constraints_[var].size();
492}
493
495 Domain result;
496 if (RefIsPositive(ref)) {
497 result = domains_[ref];
498 } else {
499 result = domains_[PositiveRef(ref)].Negation();
500 }
501 return result;
502}
503
504bool PresolveContext::DomainContains(int ref, int64_t value) const {
505 if (!RefIsPositive(ref)) {
506 return domains_[PositiveRef(ref)].Contains(-value);
507 }
508 return domains_[ref].Contains(value);
509}
510
512 int64_t value) const {
513 CHECK_LE(expr.vars_size(), 1);
514 if (IsFixed(expr)) {
515 return FixedValue(expr) == value;
516 }
517 if (value > MaxOf(expr)) return false;
518 if (value < MinOf(expr)) return false;
519
520 // We assume expression is validated for overflow initially, and the code
521 // below should be overflow safe.
522 if ((value - expr.offset()) % expr.coeffs(0) != 0) return false;
523 return DomainContains(expr.vars(0), (value - expr.offset()) / expr.coeffs(0));
524}
525
526ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWith(
527 int ref, const Domain& domain, bool* domain_modified) {
528 DCHECK(!DomainIsEmpty(ref));
529 const int var = PositiveRef(ref);
530
531 if (RefIsPositive(ref)) {
532 if (domains_[var].IsIncludedIn(domain)) {
533 return true;
534 }
535 domains_[var] = domains_[var].IntersectionWith(domain);
536 } else {
537 const Domain temp = domain.Negation();
538 if (domains_[var].IsIncludedIn(temp)) {
539 return true;
540 }
541 domains_[var] = domains_[var].IntersectionWith(temp);
542 }
543
544 if (domain_modified != nullptr) {
545 *domain_modified = true;
546 }
547 modified_domains.Set(var);
548 if (domains_[var].IsEmpty()) {
550 absl::StrCat("var #", ref, " as empty domain after intersecting with ",
551 domain.ToString()));
552 }
553
554 solution_crush_.SetOrUpdateVarToDomain(var, domains_[var]);
555
556 // Propagate the domain of the representative right away.
557 // Note that the recursive call should only by one level deep.
559 if (r.representative == var) return true;
561 DomainOf(var)
562 .AdditionWith(Domain(-r.offset))
563 .InverseMultiplicationBy(r.coeff),
564 /*domain_modified=*/nullptr);
565}
566
567ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWith(
568 const LinearExpressionProto& expr, const Domain& domain,
569 bool* domain_modified) {
570 if (expr.vars().empty()) {
571 if (domain.Contains(expr.offset())) {
572 return true;
573 } else {
574 return NotifyThatModelIsUnsat(absl::StrCat(
576 " as empty domain after intersecting with ", domain.ToString()));
577 }
578 }
579 if (expr.vars().size() == 1) { // Affine
580 return IntersectDomainWith(expr.vars(0),
581 domain.AdditionWith(Domain(-expr.offset()))
583 domain_modified);
584 }
585
586 // We don't do anything for longer expression for now.
587 return true;
588}
589
590ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralToFalse(int lit) {
591 const int var = PositiveRef(lit);
592 const int64_t value = RefIsPositive(lit) ? 0 : 1;
593 return IntersectDomainWith(var, Domain(value));
594}
595
596ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralToTrue(int lit) {
597 return SetLiteralToFalse(NegatedRef(lit));
598}
599
601 const ConstraintProto& ct = working_model->constraints(index);
602 if (ct.constraint_case() ==
604 return true;
605 }
606 for (const int literal : ct.enforcement_literal()) {
607 if (LiteralIsFalse(literal)) return true;
608 }
609 return false;
610}
611
613 const ConstraintProto& ct = working_model->constraints(ct_ref);
614 bool contains_one_free_literal = false;
615 for (const int literal : ct.enforcement_literal()) {
616 if (LiteralIsFalse(literal)) return false;
617 if (!LiteralIsTrue(literal)) contains_one_free_literal = true;
618 }
619 return contains_one_free_literal;
620}
621
622void PresolveContext::UpdateRuleStats(const std::string& name, int num_times) {
623 // Hack: we don't want to count TODO rules as this is used to decide if
624 // we loop again.
625 const bool is_todo = name.size() >= 4 && name.substr(0, 4) == "TODO";
626 if (!is_todo) num_presolve_operations += num_times;
627
628 if (logger_->LoggingIsEnabled()) {
629 if (VLOG_IS_ON(1)) {
630 int level = is_todo ? 3 : 2;
631 if (std::abs(num_presolve_operations -
632 params_.debug_max_num_presolve_operations()) <= 100) {
633 level = 1;
634 }
635 VLOG(level) << num_presolve_operations << " : " << name;
636 }
637
638 stats_by_rule_name_[name] += num_times;
639 }
640}
641
642void PresolveContext::UpdateLinear1Usage(const ConstraintProto& ct, int c) {
643 const int old_var = constraint_to_linear1_var_[c];
644 if (old_var >= 0) {
645 var_to_num_linear1_[old_var]--;
646 DCHECK_GE(var_to_num_linear1_[old_var], 0);
647 }
649 ct.linear().vars().size() == 1) {
650 const int var = PositiveRef(ct.linear().vars(0));
651 constraint_to_linear1_var_[c] = var;
652 var_to_num_linear1_[var]++;
653 } else {
654 constraint_to_linear1_var_[c] = -1;
655 }
656}
657
658void PresolveContext::MaybeResizeIntervalData() {
659 // Lazy allocation so that we only do that if there are some interval.
660 const int num_constraints = constraint_to_vars_.size();
661 if (constraint_to_intervals_.size() != num_constraints) {
662 constraint_to_intervals_.resize(num_constraints);
663 interval_usage_.resize(num_constraints);
664 }
665}
666
667void PresolveContext::AddVariableUsage(int c) {
668 const ConstraintProto& ct = working_model->constraints(c);
669
670 constraint_to_vars_[c] = UsedVariables(ct);
671 for (const int v : constraint_to_vars_[c]) {
672 DCHECK_LT(v, var_to_constraints_.size());
673 DCHECK(!VariableWasRemoved(v));
674 var_to_constraints_[v].insert(c);
675 }
676
677 std::vector<int> used_interval = UsedIntervals(ct);
678 if (!used_interval.empty()) {
679 MaybeResizeIntervalData();
680 constraint_to_intervals_[c].swap(used_interval);
681 for (const int i : constraint_to_intervals_[c]) interval_usage_[i]++;
682 }
683
684 UpdateLinear1Usage(ct, c);
685
686#ifdef CHECK_HINT
687 // Crash if the loaded hint is infeasible for this constraint.
688 // This is helpful to debug a wrong presolve that kill a feasible solution.
689 if (working_model->has_solution_hint() &&
690 solution_crush_.SolutionIsLoaded() &&
692 solution_crush_.GetVarValues())) {
693 LOG(FATAL) << "Hint infeasible for constraint #" << c << " : "
694 << ct.ShortDebugString();
695 }
696#endif
697}
698
699void PresolveContext::EraseFromVarToConstraint(int var, int c) {
700 var_to_constraints_[var].erase(c);
701 if (var_to_constraints_[var].size() <= 3) {
703 }
704}
705
707 if (is_unsat_) return;
708 DCHECK_EQ(constraint_to_vars_.size(), working_model->constraints_size());
709 const ConstraintProto& ct = working_model->constraints(c);
710
711 // We don't optimize the interval usage as this is not super frequent.
712 std::vector<int> used_interval = UsedIntervals(ct);
713 if (c < constraint_to_intervals_.size() || !used_interval.empty()) {
714 MaybeResizeIntervalData();
715 for (const int i : constraint_to_intervals_[c]) interval_usage_[i]--;
716 constraint_to_intervals_[c].swap(used_interval);
717 for (const int i : constraint_to_intervals_[c]) interval_usage_[i]++;
718 }
719
720 // For the variables, we avoid an erase() followed by an insert() for the
721 // variables that didn't change.
722 std::vector<int> new_usage = UsedVariables(ct);
723 const absl::Span<const int> old_usage = constraint_to_vars_[c];
724 const int old_size = old_usage.size();
725 int i = 0;
726 for (const int var : new_usage) {
727 DCHECK(!VariableWasRemoved(var));
728 while (i < old_size && old_usage[i] < var) {
729 EraseFromVarToConstraint(old_usage[i], c);
730 ++i;
731 }
732 if (i < old_size && old_usage[i] == var) {
733 ++i;
734 } else {
735 var_to_constraints_[var].insert(c);
736 }
737 }
738 for (; i < old_size; ++i) {
739 EraseFromVarToConstraint(old_usage[i], c);
740 }
741 constraint_to_vars_[c].swap(new_usage);
742
743 UpdateLinear1Usage(ct, c);
744
745#ifdef CHECK_HINT
746 // Crash if the loaded hint is infeasible for this constraint.
747 // This is helpful to debug a wrong presolve that kill a feasible solution.
748 if (working_model->has_solution_hint() &&
749 solution_crush_.SolutionIsLoaded() &&
751 solution_crush_.GetVarValues())) {
752 LOG(FATAL) << "Hint infeasible for constraint #" << c << " : "
753 << ct.ShortDebugString();
754 }
755#endif
756}
757
759 if (is_unsat_) return true; // We do not care in this case.
760 return constraint_to_vars_.size() == working_model->constraints_size();
761}
762
764 if (is_unsat_) return;
765 const int old_size = constraint_to_vars_.size();
766 const int new_size = working_model->constraints_size();
767 DCHECK_LE(old_size, new_size);
768 constraint_to_vars_.resize(new_size);
769 constraint_to_linear1_var_.resize(new_size, -1);
770 for (int c = old_size; c < new_size; ++c) {
771 AddVariableUsage(c);
772 }
773}
774
776 if (is_unsat_) return false; // We do not care in this case.
777 if (params_.keep_all_feasible_solutions_in_presolve()) return false;
778
779 // We can leave non-optimal stuff around if we reach the time limit.
780 if (time_limit_->LimitReached()) return false;
781
782 for (int var = 0; var < working_model->variables_size(); ++var) {
783 if (VariableIsNotUsedAnymore(var)) continue;
784 if (IsFixed(var)) continue;
785 const auto& constraints = VarToConstraints(var);
786 if (constraints.size() == 1 &&
787 constraints.contains(kAffineRelationConstraint) &&
788 GetAffineRelation(var).representative != var) {
789 return true;
790 }
791 }
792 return false;
793}
794
795// TODO(user): Also test var_to_constraints_ !!
797 // We do not care in these cases.
798 if (is_unsat_) return true;
799 if (time_limit_->LimitReached()) return true;
800
801 if (var_to_constraints_.size() != working_model->variables_size()) {
802 LOG(INFO) << "Wrong var_to_constraints_ size!";
803 return false;
804 }
805 if (constraint_to_vars_.size() != working_model->constraints_size()) {
806 LOG(INFO) << "Wrong constraint_to_vars size!";
807 return false;
808 }
809 std::vector<int> linear1_count(var_to_constraints_.size(), 0);
810 for (int c = 0; c < constraint_to_vars_.size(); ++c) {
811 const ConstraintProto& ct = working_model->constraints(c);
812 if (constraint_to_vars_[c] != UsedVariables(ct)) {
813 LOG(INFO) << "Wrong variables usage for constraint: \n"
815 << " old_size: " << constraint_to_vars_[c].size();
816 return false;
817 }
819 ct.linear().vars().size() == 1) {
820 linear1_count[PositiveRef(ct.linear().vars(0))]++;
821 if (constraint_to_linear1_var_[c] != PositiveRef(ct.linear().vars(0))) {
822 LOG(INFO) << "Wrong variables for linear1: \n"
824 << " saved_var: " << constraint_to_linear1_var_[c];
825 return false;
826 }
827 }
828 }
829 int num_in_objective = 0;
830 for (int v = 0; v < var_to_constraints_.size(); ++v) {
831 if (linear1_count[v] != var_to_num_linear1_[v]) {
832 LOG(INFO) << "Variable " << v << " has wrong linear1 count!"
833 << " stored: " << var_to_num_linear1_[v]
834 << " actual: " << linear1_count[v];
835 return false;
836 }
837 if (var_to_constraints_[v].contains(kObjectiveConstraint)) {
838 ++num_in_objective;
839 if (!objective_map_.contains(v)) {
840 LOG(INFO) << "Variable " << v
841 << " is marked as part of the objective but isn't.";
842 return false;
843 }
844 }
845 }
846 if (num_in_objective != objective_map_.size()) {
847 LOG(INFO) << "Not all variables are marked as part of the objective";
848 return false;
849 }
850
851 return true;
852}
853
854// If a Boolean variable (one with domain [0, 1]) appear in this affine
855// equivalence class, then we want its representative to be Boolean. Note that
856// this is always possible because a Boolean variable can never be equal to a
857// multiple of another if std::abs(coeff) is greater than 1 and if it is not
858// fixed to zero. This is important because it allows to simply use the same
859// representative for any referenced literals.
860//
861// Note(user): When both domain contains [0,1] and later the wrong variable
862// become usable as boolean, then we have a bug. Because of that, the code
863// for GetLiteralRepresentative() is not as simple as it should be.
864bool PresolveContext::AddRelation(int x, int y, int64_t c, int64_t o,
865 AffineRelation* repo) {
866 // When the coefficient is larger than one, then if later one variable becomes
867 // Boolean, it must be the representative.
868 if (std::abs(c) != 1) return repo->TryAdd(x, y, c, o);
869
870 CHECK(!VariableWasRemoved(x));
871 CHECK(!VariableWasRemoved(y));
872
873 // To avoid integer overflow, we always want to use the representative with
874 // the smallest domain magnitude. Otherwise we might express a variable in say
875 // [0, 3] as ([x, x + 3] - x) for an arbitrary large x, and substituting
876 // something like this in a linear expression could break our overflow
877 // precondition.
878 //
879 // Note that if either rep_x or rep_y can be used as a literal, then it will
880 // also be the variable with the smallest domain magnitude (1 or 0 if fixed).
881 const int rep_x = repo->Get(x).representative;
882 const int rep_y = repo->Get(y).representative;
883 const int64_t m_x = std::max(std::abs(MinOf(rep_x)), std::abs(MaxOf(rep_x)));
884 const int64_t m_y = std::max(std::abs(MinOf(rep_y)), std::abs(MaxOf(rep_y)));
885 bool allow_rep_x = m_x < m_y;
886 bool allow_rep_y = m_y < m_x;
887 if (m_x == m_y) {
888 // If both magnitude are the same, we prefer a positive domain.
889 // This is important so we don't use [-1, 0] as a representative for [0, 1].
890 allow_rep_x = MinOf(rep_x) >= MinOf(rep_y);
891 allow_rep_y = MinOf(rep_y) >= MinOf(rep_x);
892 }
893 if (allow_rep_x && allow_rep_y) {
894 // If both representative are okay, we force the choice to the variable
895 // with lower index. This is needed because we have two "equivalence"
896 // relations, and we want the same representative in both.
897 if (rep_x < rep_y) {
898 allow_rep_y = false;
899 } else {
900 allow_rep_x = false;
901 }
902 }
903 return repo->TryAdd(x, y, c, o, allow_rep_x, allow_rep_y);
904}
905
907 DCHECK(RefIsPositive(var));
909 if (r.representative == var) return true;
911}
912
913bool PresolveContext::PropagateAffineRelation(int var, int rep, int64_t coeff,
914 int64_t offset) {
915 DCHECK(RefIsPositive(var));
916 DCHECK(RefIsPositive(rep));
917 DCHECK(!DomainIsEmpty(var));
918 DCHECK(!DomainIsEmpty(rep));
919
920 // Propagate domains both ways.
921 // var = coeff * rep + offset
922 if (!IntersectDomainWith(rep, DomainOf(var)
923 .AdditionWith(Domain(-offset))
924 .InverseMultiplicationBy(coeff))) {
925 return false;
926 }
928 var,
929 DomainOf(rep).MultiplicationBy(coeff).AdditionWith(Domain(offset)))) {
930 return false;
931 }
932
933 return true;
934}
935
937 for (auto& ref_map : var_to_constraints_) {
938 ref_map.erase(kAffineRelationConstraint);
939 }
940}
941
943 if (!VariableIsUnique(var)) {
944 return;
945 }
947 if (var == r.representative) {
948 return;
949 }
950 DCHECK(VarToConstraints(var).contains(kAffineRelationConstraint));
952 // Add relation with current representative to the mapping model.
953 ConstraintProto* ct = NewMappingConstraint(__FILE__, __LINE__);
954 auto* arg = ct->mutable_linear();
955 arg->add_vars(var);
956 arg->add_coeffs(1);
957 arg->add_vars(r.representative);
958 arg->add_coeffs(-r.coeff);
959 arg->add_domain(r.offset);
960 arg->add_domain(r.offset);
962}
963
964// We only call that for a non representative variable that is only used in
965// the kAffineRelationConstraint. Such variable can be ignored and should never
966// be seen again in the presolve.
968 const int rep = GetAffineRelation(var).representative;
969
970 CHECK(RefIsPositive(var));
971 CHECK_NE(var, rep);
972 CHECK_EQ(var_to_constraints_[var].size(), 1);
973 CHECK(var_to_constraints_[var].contains(kAffineRelationConstraint));
974 CHECK(var_to_constraints_[rep].contains(kAffineRelationConstraint));
975
976 // We shouldn't reuse this variable again!
978
979 // We do not call EraseFromVarToConstraint() on purpose here since the
980 // variable is removed.
981 var_to_constraints_[var].erase(kAffineRelationConstraint);
982 affine_relations_.IgnoreFromClassSize(var);
983
984 // If the representative is left alone, we can remove it from the special
985 // affine relation constraint too.
986 if (affine_relations_.ClassSize(rep) == 1) {
987 EraseFromVarToConstraint(rep, kAffineRelationConstraint);
988 }
989
990 if (VLOG_IS_ON(2)) {
991 LOG(INFO) << "Removing affine relation: " << AffineRelationDebugString(var);
992 }
993}
994
996 const int var = GetAffineRelation(ref).representative;
997 const int64_t min = MinOf(var);
998 if (min == 0 || IsFixed(var)) return; // Nothing to do.
999
1000 const int new_var = NewIntVar(DomainOf(var).AdditionWith(Domain(-min)));
1001 CHECK(StoreAffineRelation(var, new_var, 1, min, /*debug_no_recursion=*/true));
1002 UpdateRuleStats("variables: canonicalize domain");
1004}
1005
1007 SolverLogger* logger, CpModelProto* proto) {
1008 DCHECK(proto->has_floating_point_objective());
1009 DCHECK(!proto->has_objective());
1010 const auto& objective = proto->floating_point_objective();
1011 std::vector<std::pair<int, double>> terms;
1012 for (int i = 0; i < objective.vars_size(); ++i) {
1013 DCHECK(RefIsPositive(objective.vars(i)));
1014 terms.push_back({objective.vars(i), objective.coeffs(i)});
1015 }
1016 const double offset = objective.offset();
1017 const bool maximize = objective.maximize();
1019
1020 return ScaleAndSetObjective(params, terms, offset, maximize, proto, logger);
1021}
1022
1024 int64_t mod, int64_t rhs) {
1025 CHECK_NE(mod, 0);
1026 CHECK_NE(coeff, 0);
1027
1028 const int64_t gcd = std::gcd(coeff, mod);
1029 if (gcd != 1) {
1030 if (rhs % gcd != 0) {
1032 absl::StrCat("Infeasible ", coeff, " * X = ", rhs, " % ", mod));
1033 }
1034 coeff /= gcd;
1035 mod /= gcd;
1036 rhs /= gcd;
1037 }
1038
1039 // We just abort in this case as there is no point introducing a new variable.
1040 if (std::abs(mod) == 1) return true;
1041
1042 int var = ref;
1043 if (!RefIsPositive(var)) {
1044 var = NegatedRef(ref);
1045 coeff = -coeff;
1046 rhs = -rhs;
1047 }
1048
1049 // From var * coeff % mod = rhs
1050 // We have var = mod * X + offset.
1051 const int64_t offset = ProductWithModularInverse(coeff, mod, rhs);
1052
1053 // Lets create a new integer variable and add the affine relation.
1054 const Domain new_domain =
1056 if (new_domain.IsEmpty()) {
1058 "Empty domain in CanonicalizeAffineVariable()");
1059 }
1060 if (new_domain.IsFixed()) {
1061 UpdateRuleStats("variables: fixed value due to affine relation");
1062 return IntersectDomainWith(
1063 var, new_domain.ContinuousMultiplicationBy(mod).AdditionWith(
1064 Domain(offset)));
1065 }
1066
1067 // We make sure the new variable has a domain starting at zero to minimize
1068 // future overflow issues. If it end up Boolean, it is also nice to be able to
1069 // use it as such.
1070 //
1071 // A potential problem with this is that it messes up the natural variable
1072 // order chosen by the modeler. We try to correct that when mapping variables
1073 // at the end of the presolve.
1074 const int64_t min_value = new_domain.Min();
1075 const int new_var = NewIntVar(new_domain.AdditionWith(Domain(-min_value)));
1076 if (!working_model->variables(var).name().empty()) {
1077 working_model->mutable_variables(new_var)->set_name(
1078 working_model->variables(var).name());
1079 }
1080 CHECK(StoreAffineRelation(var, new_var, mod, offset + mod * min_value,
1081 /*debug_no_recursion=*/true));
1082 UpdateRuleStats("variables: canonicalize affine domain");
1084 return true;
1085}
1086
1087bool PresolveContext::StoreAffineRelation(int var_x, int var_y, int64_t coeff,
1088 int64_t offset,
1089 bool debug_no_recursion) {
1090 DCHECK(RefIsPositive(var_x));
1091 DCHECK(RefIsPositive(var_y));
1092 DCHECK_NE(coeff, 0);
1093 if (is_unsat_) return false;
1094
1095 // Sets var_y's value to the solution of
1096 // "var_x's value - coeff * var_y's value = offset".
1097 solution_crush_.SetVarToLinearConstraintSolution(1, {var_x, var_y},
1098 {1, -coeff}, offset);
1099
1100 // TODO(user): I am not 100% sure why, but sometimes the representative is
1101 // fixed but that is not propagated to var_x or var_y and this causes issues.
1102 if (!PropagateAffineRelation(var_x)) return false;
1103 if (!PropagateAffineRelation(var_y)) return false;
1104 if (!PropagateAffineRelation(var_x, var_y, coeff, offset)) return false;
1105
1106 if (IsFixed(var_x)) {
1107 const int64_t lhs = DomainOf(var_x).FixedValue() - offset;
1108 if (lhs % std::abs(coeff) != 0) {
1109 return NotifyThatModelIsUnsat();
1110 }
1111 UpdateRuleStats("affine: fixed");
1112 return IntersectDomainWith(var_y, Domain(lhs / coeff));
1113 }
1114
1115 if (IsFixed(var_y)) {
1116 const int64_t value_x = DomainOf(var_y).FixedValue() * coeff + offset;
1117 UpdateRuleStats("affine: fixed");
1118 return IntersectDomainWith(var_x, Domain(value_x));
1119 }
1120
1121 // If both are already in the same class, we need to make sure the relations
1122 // are compatible.
1125 if (rx.representative == ry.representative) {
1126 // x = rx.coeff * rep + rx.offset;
1127 // y = ry.coeff * rep + ry.offset;
1128 // And x == coeff * ry.coeff * rep + (coeff * ry.offset + offset).
1129 //
1130 // So we get the relation a * rep == b with a and b defined here:
1131 const int64_t a = coeff * ry.coeff - rx.coeff;
1132 const int64_t b = coeff * ry.offset + offset - rx.offset;
1133 if (a == 0) {
1134 if (b != 0) return NotifyThatModelIsUnsat();
1135 return true;
1136 }
1137 if (b % a != 0) {
1138 return NotifyThatModelIsUnsat();
1139 }
1140 UpdateRuleStats("affine: unique solution");
1141 const int64_t unique_value = -b / a;
1142 if (!IntersectDomainWith(rx.representative, Domain(unique_value))) {
1143 return false;
1144 }
1145 if (!IntersectDomainWith(var_x,
1146 Domain(unique_value * rx.coeff + rx.offset))) {
1147 return false;
1148 }
1149 if (!IntersectDomainWith(var_y,
1150 Domain(unique_value * ry.coeff + ry.offset))) {
1151 return false;
1152 }
1153 return true;
1154 }
1155
1156 // var_x = coeff * var_y + offset;
1157 // rx.coeff * rep_x + rx.offset =
1158 // coeff * (ry.coeff * rep_y + ry.offset) + offset
1159 //
1160 // We have a * rep_x + b * rep_y == o
1161 int64_t a = rx.coeff;
1162 int64_t b = -coeff * ry.coeff;
1163 int64_t o = coeff * ry.offset + offset - rx.offset;
1164 CHECK_NE(a, 0);
1165 CHECK_NE(b, 0);
1166 {
1167 const int64_t gcd = std::gcd(std::abs(a), std::abs(b));
1168 if (gcd != 1) {
1169 a /= gcd;
1170 b /= gcd;
1171 if (o % gcd != 0) return NotifyThatModelIsUnsat();
1172 o /= gcd;
1173 }
1174 }
1175
1176 // In this (rare) case, we need to canonicalize one of the variable that will
1177 // become the representative for both.
1178 if (std::abs(a) > 1 && std::abs(b) > 1) {
1179 UpdateRuleStats("affine: created common representative");
1180 if (!CanonicalizeAffineVariable(rx.representative, a, std::abs(b),
1181 offset)) {
1182 return false;
1183 }
1184
1185 // Re-add the relation now that a will resolve to a multiple of b.
1186 return StoreAffineRelation(var_x, var_y, coeff, offset,
1187 /*debug_no_recursion=*/true);
1188 }
1189
1190 // Canonicalize from (a * rep_x + b * rep_y = o) to (x = c * y + o).
1191 int x, y;
1192 int64_t c;
1193 bool negate = false;
1194 if (std::abs(a) == 1) {
1195 x = rx.representative;
1196 y = ry.representative;
1197 c = -b;
1198 negate = a < 0;
1199 } else {
1200 CHECK_EQ(std::abs(b), 1);
1201 x = ry.representative;
1202 y = rx.representative;
1203 c = -a;
1204 negate = b < 0;
1205 }
1206 if (negate) {
1207 c = -c;
1208 o = -o;
1209 }
1210 CHECK(RefIsPositive(x));
1211 CHECK(RefIsPositive(y));
1212
1213 // Lets propagate domains first.
1215 y, DomainOf(x).AdditionWith(Domain(-o)).InverseMultiplicationBy(c))) {
1216 return false;
1217 }
1219 x,
1220 DomainOf(y).ContinuousMultiplicationBy(c).AdditionWith(Domain(o)))) {
1221 return false;
1222 }
1223
1224 // To avoid corner cases where replacing x by y in a linear expression
1225 // can cause overflow, we might want to canonicalize y first to avoid
1226 // cases like x = c * [large_value, ...] - large_value.
1227 //
1228 // TODO(user): we can do better for overflow by not always choosing the
1229 // min at zero, do the best things if it becomes needed.
1230 if (std::abs(o) > std::max(std::abs(MinOf(x)), std::abs(MaxOf(x)))) {
1231 // Both these function recursively call StoreAffineRelation() but shouldn't
1232 // be able to cascade (CHECKED).
1233 CHECK(!debug_no_recursion);
1235 return StoreAffineRelation(x, y, c, o, /*debug_no_recursion=*/true);
1236 }
1237
1238 // TODO(user): can we force the rep and remove GetAffineRelation()?
1239 CHECK(AddRelation(x, y, c, o, &affine_relations_));
1240 UpdateRuleStats("affine: new relation");
1241
1242 // Lets propagate again the new relation. We might as well do it as early
1243 // as possible and not all call site do it.
1244 //
1245 // TODO(user): I am not sure this is needed given the propagation above.
1246 if (!PropagateAffineRelation(var_x)) return false;
1247 if (!PropagateAffineRelation(var_y)) return false;
1248
1249 // These maps should only contains representative, so only need to remap
1250 // either x or y.
1251 const int rep = GetAffineRelation(x).representative;
1252
1253 // The domain didn't change, but this notification allows to re-process any
1254 // constraint containing these variables. Note that we do not need to
1255 // retrigger a propagation of the constraint containing a variable whose
1256 // representative didn't change.
1257 if (x != rep) modified_domains.Set(x);
1258 if (y != rep) modified_domains.Set(y);
1259
1260 var_to_constraints_[x].insert(kAffineRelationConstraint);
1261 var_to_constraints_[y].insert(kAffineRelationConstraint);
1262 return true;
1263}
1264
1266 int ref_a, int ref_b) {
1267 if (is_unsat_) return false;
1268
1269 CHECK(!VariableWasRemoved(ref_a));
1270 CHECK(!VariableWasRemoved(ref_b));
1271 CHECK(!DomainOf(ref_a).IsEmpty());
1272 CHECK(!DomainOf(ref_b).IsEmpty());
1273 CHECK(CanBeUsedAsLiteral(ref_a));
1274 CHECK(CanBeUsedAsLiteral(ref_b));
1275
1276 if (ref_a == ref_b) return true;
1277 if (ref_a == NegatedRef(ref_b)) {
1278 is_unsat_ = true;
1279 return false;
1280 }
1281
1282 const int var_a = PositiveRef(ref_a);
1283 const int var_b = PositiveRef(ref_b);
1284 if (RefIsPositive(ref_a) == RefIsPositive(ref_b)) {
1285 // a = b
1286 return StoreAffineRelation(var_a, var_b, /*coeff=*/1, /*offset=*/0);
1287 }
1288 // a = 1 - b
1289 return StoreAffineRelation(var_a, var_b, /*coeff=*/-1, /*offset=*/1);
1290}
1291
1294
1295 CHECK(CanBeUsedAsLiteral(ref));
1297 // Note(user): This can happen is some corner cases where the affine
1298 // relation where added before the variable became usable as Boolean. When
1299 // this is the case, the domain will be of the form [x, x + 1] and should be
1300 // later remapped to a Boolean variable.
1301 return ref;
1302 }
1303
1304 // We made sure that the affine representative can always be used as a
1305 // literal. However, if some variable are fixed, we might not have only
1306 // (coeff=1 offset=0) or (coeff=-1 offset=1) and we might have something like
1307 // (coeff=8 offset=0) which is only valid for both variable at zero...
1308 //
1309 // What is sure is that depending on the value, only one mapping can be valid
1310 // because r.coeff can never be zero.
1311 const bool positive_possible = (r.offset == 0 || r.coeff + r.offset == 1);
1312 const bool negative_possible = (r.offset == 1 || r.coeff + r.offset == 0);
1313 DCHECK_NE(positive_possible, negative_possible);
1314 if (RefIsPositive(ref)) {
1315 return positive_possible ? r.representative : NegatedRef(r.representative);
1316 } else {
1317 return positive_possible ? NegatedRef(r.representative) : r.representative;
1318 }
1319}
1320
1321// This makes sure that the affine relation only uses one of the
1322// representative from the var_equiv_relations_.
1324 AffineRelation::Relation r = affine_relations_.Get(PositiveRef(ref));
1325 if (!RefIsPositive(ref)) {
1326 r.coeff *= -1;
1327 r.offset *= -1;
1328 }
1329 return r;
1330}
1331
1332std::string PresolveContext::RefDebugString(int ref) const {
1333 return absl::StrCat(RefIsPositive(ref) ? "X" : "-X", PositiveRef(ref),
1334 DomainOf(ref).ToString());
1335}
1336
1339 return absl::StrCat(RefDebugString(ref), " = ", r.coeff, " * ",
1340 RefDebugString(r.representative), " + ", r.offset);
1341}
1342
1344 domains_.clear();
1345 modified_domains.ResetAllToFalse();
1346 var_with_reduced_small_degree.ResetAllToFalse();
1347 var_to_constraints_.clear();
1348 var_to_num_linear1_.clear();
1349 objective_map_.clear();
1350 DCHECK(!solution_crush_.SolutionIsLoaded());
1351}
1352
1353// Create the internal structure for any new variables in working_model.
1355 const int new_size = working_model->variables().size();
1356 DCHECK_GE(new_size, domains_.size());
1357 if (domains_.size() == new_size) return;
1358
1359 modified_domains.Resize(new_size);
1360 var_with_reduced_small_degree.Resize(new_size);
1361 var_to_constraints_.resize(new_size);
1362 var_to_num_linear1_.resize(new_size);
1363
1364 // We mark the domain as modified so we will look at these new variable during
1365 // our presolve loop.
1366 const int old_size = domains_.size();
1367 domains_.resize(new_size);
1368 for (int i = old_size; i < new_size; ++i) {
1369 modified_domains.Set(i);
1370 domains_[i] = ReadDomainFromProto(working_model->variables(i));
1371 if (domains_[i].IsEmpty()) {
1372 is_unsat_ = true;
1373 return;
1374 }
1375 }
1376
1377 // We resize the hint too even if not loaded.
1378 solution_crush_.Resize(new_size);
1379}
1380
1382 const int num_vars = working_model->variables().size();
1383 if (working_model->has_solution_hint() || num_vars == 0) {
1384 const auto hint_proto = working_model->solution_hint();
1385 absl::flat_hash_map<int, int64_t> hint_values;
1386 int num_changes = 0;
1387 for (int i = 0; i < hint_proto.vars().size(); ++i) {
1388 const int var = hint_proto.vars(i);
1389 if (!RefIsPositive(var)) break; // Abort. Shouldn't happen.
1390 const int64_t hint_value = hint_proto.values(i);
1391 const int64_t clamped_hint_value = DomainOf(var).ClosestValue(hint_value);
1392 if (clamped_hint_value != hint_value) {
1393 ++num_changes;
1394 }
1395 hint_values[var] = clamped_hint_value;
1396 }
1397 if (num_changes > 0) {
1398 UpdateRuleStats("hint: moved var hint within its domain.", num_changes);
1399 }
1400 for (int i = 0; i < num_vars; ++i) {
1401 if (!hint_values.contains(i) && IsFixed(i)) {
1402 hint_values[i] = FixedValue(i);
1403 }
1404 }
1405 solution_crush_.LoadSolution(num_vars, hint_values);
1406 }
1407}
1408
1410 CHECK(RefIsPositive(var));
1411 CHECK_EQ(DomainOf(var).Size(), 2);
1412 const int64_t var_min = MinOf(var);
1413 const int64_t var_max = MaxOf(var);
1414
1415 if (is_unsat_) return;
1416
1417 absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
1418
1419 // Find encoding for min if present.
1420 auto min_it = var_map.find(var_min);
1421 if (min_it != var_map.end()) {
1422 const int old_var = PositiveRef(min_it->second.Get(this));
1423 if (removed_variables_.contains(old_var)) {
1424 var_map.erase(min_it);
1425 min_it = var_map.end();
1426 }
1427 }
1428
1429 // Find encoding for max if present.
1430 auto max_it = var_map.find(var_max);
1431 if (max_it != var_map.end()) {
1432 const int old_var = PositiveRef(max_it->second.Get(this));
1433 if (removed_variables_.contains(old_var)) {
1434 var_map.erase(max_it);
1435 max_it = var_map.end();
1436 }
1437 }
1438
1439 // Insert missing encoding.
1440 int min_literal;
1441 int max_literal;
1442 if (min_it != var_map.end() && max_it != var_map.end()) {
1443 min_literal = min_it->second.Get(this);
1444 max_literal = max_it->second.Get(this);
1445 if (min_literal != NegatedRef(max_literal)) {
1446 UpdateRuleStats("variables with 2 values: merge encoding literals");
1447 if (!StoreBooleanEqualityRelation(min_literal, NegatedRef(max_literal))) {
1448 return;
1449 }
1450 }
1451 min_literal = GetLiteralRepresentative(min_literal);
1452 max_literal = GetLiteralRepresentative(max_literal);
1453 if (!IsFixed(min_literal)) CHECK_EQ(min_literal, NegatedRef(max_literal));
1454 } else if (min_it != var_map.end() && max_it == var_map.end()) {
1455 UpdateRuleStats("variables with 2 values: register other encoding");
1456 min_literal = min_it->second.Get(this);
1457 max_literal = NegatedRef(min_literal);
1458 var_map[var_max] = SavedLiteral(max_literal);
1459 } else if (min_it == var_map.end() && max_it != var_map.end()) {
1460 UpdateRuleStats("variables with 2 values: register other encoding");
1461 max_literal = max_it->second.Get(this);
1462 min_literal = NegatedRef(max_literal);
1463 var_map[var_min] = SavedLiteral(min_literal);
1464 } else {
1465 UpdateRuleStats("variables with 2 values: create encoding literal");
1466 max_literal = NewBoolVar("var with 2 values");
1467 solution_crush_.MaybeSetLiteralToValueEncoding(max_literal, var, var_max);
1468 min_literal = NegatedRef(max_literal);
1469 var_map[var_min] = SavedLiteral(min_literal);
1470 var_map[var_max] = SavedLiteral(max_literal);
1471 }
1472
1473 if (IsFixed(min_literal) || IsFixed(max_literal)) {
1474 CHECK(IsFixed(min_literal));
1475 CHECK(IsFixed(max_literal));
1476 UpdateRuleStats("variables with 2 values: fixed encoding");
1477 if (LiteralIsTrue(min_literal)) {
1478 return static_cast<void>(IntersectDomainWith(var, Domain(var_min)));
1479 } else {
1480 return static_cast<void>(IntersectDomainWith(var, Domain(var_max)));
1481 }
1482 }
1483
1484 // Add affine relation.
1485 if (GetAffineRelation(var).representative != PositiveRef(min_literal)) {
1486 UpdateRuleStats("variables with 2 values: new affine relation");
1487 if (RefIsPositive(max_literal)) {
1488 (void)StoreAffineRelation(var, PositiveRef(max_literal),
1489 var_max - var_min, var_min);
1490 } else {
1491 (void)StoreAffineRelation(var, PositiveRef(max_literal),
1492 var_min - var_max, var_max);
1493 }
1494 }
1495}
1496
1497bool PresolveContext::InsertVarValueEncodingInternal(int literal, int var,
1498 int64_t value,
1499 bool add_constraints) {
1500 DCHECK(RefIsPositive(var));
1501 DCHECK(!VariableWasRemoved(literal));
1502 DCHECK(!VariableWasRemoved(var));
1503 if (is_unsat_) return false;
1504 absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
1505
1506 // The code below is not 100% correct if this is not the case.
1507 if (!DomainOf(var).Contains(value)) {
1508 return SetLiteralToFalse(literal);
1509 }
1510 if (DomainOf(var).IsFixed()) {
1511 return SetLiteralToTrue(literal);
1512 }
1513 if (LiteralIsTrue(literal)) {
1514 return IntersectDomainWith(var, Domain(value));
1515 }
1516 if (LiteralIsFalse(literal)) {
1517 return IntersectDomainWith(var, Domain(value).Complement());
1518 }
1519
1520 // If an encoding already exist, make the two Boolean equals.
1521 const auto [it, inserted] =
1522 var_map.insert(std::make_pair(value, SavedLiteral(literal)));
1523 if (!inserted) {
1524 const int previous_literal = it->second.Get(this);
1525
1526 // Ticky and rare: I have only observed this on the LNS of
1527 // radiation_m18_12_05_sat.fzn. The value was encoded, but maybe we never
1528 // used the involved variables / constraints, so it was removed (with the
1529 // encoding constraints) from the model already! We have to be careful.
1530 if (VariableWasRemoved(previous_literal)) {
1531 it->second = SavedLiteral(literal);
1532 } else {
1533 if (literal != previous_literal) {
1535 "variables: merge equivalent var value encoding literals");
1536 if (!StoreBooleanEqualityRelation(literal, previous_literal)) {
1537 return false;
1538 }
1539 }
1540 }
1541 return true;
1542 }
1543
1544 if (DomainOf(var).Size() == 2) {
1545 if (!CanBeUsedAsLiteral(var)) {
1546 // TODO(user): There is a bug here if the var == value was not in the
1547 // domain, it will just be ignored.
1549 if (is_unsat_) return false;
1550
1551 if (IsFixed(var)) {
1552 if (FixedValue(var) == value) {
1553 return SetLiteralToTrue(literal);
1554 } else {
1555 return SetLiteralToFalse(literal);
1556 }
1557 }
1558
1559 // We should have a Boolean now.
1560 CanonicalizeEncoding(&var, &value);
1561 }
1562
1563 CHECK(CanBeUsedAsLiteral(var));
1564 if (value == 0) {
1565 if (!StoreBooleanEqualityRelation(literal, NegatedRef(var))) {
1566 return false;
1567 }
1568 } else {
1569 CHECK_EQ(value, 1);
1570 if (!StoreBooleanEqualityRelation(literal, var)) return false;
1571 }
1572 } else if (add_constraints) {
1573 UpdateRuleStats("variables: add encoding constraint");
1574 AddImplyInDomain(literal, var, Domain(value));
1575 AddImplyInDomain(NegatedRef(literal), var, Domain(value).Complement());
1576 }
1577
1578 // The canonicalization might have proven UNSAT.
1579 return !ModelIsUnsat();
1580}
1581
1582bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var,
1583 int64_t value, bool imply_eq) {
1584 if (is_unsat_) return false;
1585 DCHECK(RefIsPositive(var));
1586
1587 // Creates the linking sets on demand.
1588 // Insert the enforcement literal in the half encoding map.
1589 auto& direct_set = imply_eq ? eq_half_encoding_ : neq_half_encoding_;
1590 auto insert_result = direct_set.insert({{literal, var}, value});
1591 if (!insert_result.second) {
1592 if (insert_result.first->second != value && imply_eq) {
1593 UpdateRuleStats("variables: detect half reified incompatible value");
1594 return SetLiteralToFalse(literal);
1595 }
1596 return false; // Already there.
1597 }
1598 if (imply_eq) {
1599 // We are adding b => x=v. Check if we already have ~b => x=u.
1600 auto negated_encoding = direct_set.find({NegatedRef(literal), var});
1601 if (negated_encoding != direct_set.end()) {
1602 if (negated_encoding->second == value) {
1604 "variables: both boolean and its negation imply same equality");
1605 if (!IntersectDomainWith(var, Domain(value))) {
1606 return false;
1607 }
1608 } else {
1609 const int64_t other_value = negated_encoding->second;
1610 // b => var == value
1611 // !b => var == other_value
1612 // var = (value - other_value) * b + other_value
1614 "variables: both boolean and its negation fix the same variable");
1615 if (RefIsPositive(literal)) {
1616 StoreAffineRelation(var, literal, value - other_value, other_value);
1617 } else {
1618 StoreAffineRelation(var, NegatedRef(literal), other_value - value,
1619 value);
1620 }
1621 }
1622 }
1623 }
1624 VLOG(2) << "Collect lit(" << literal << ") implies var(" << var
1625 << (imply_eq ? ") == " : ") != ") << value;
1626 UpdateRuleStats("variables: detect half reified value encoding");
1627
1628 // Note(user): We don't expect a lot of literals in these sets, so doing
1629 // a scan should be okay.
1630 auto& other_set = imply_eq ? neq_half_encoding_ : eq_half_encoding_;
1631 auto it = other_set.find({NegatedRef(literal), var});
1632 if (it != other_set.end() && it->second == value) {
1633 UpdateRuleStats("variables: detect fully reified value encoding");
1634 const int imply_eq_literal = imply_eq ? literal : NegatedRef(literal);
1635 if (!InsertVarValueEncodingInternal(imply_eq_literal, var, value,
1636 /*add_constraints=*/false)) {
1637 return false;
1638 }
1639 }
1640
1641 return true;
1642}
1643
1644bool PresolveContext::CanonicalizeEncoding(int* ref, int64_t* value) {
1645 const AffineRelation::Relation r = GetAffineRelation(*ref);
1646 if ((*value - r.offset) % r.coeff != 0) return false;
1647 *ref = r.representative;
1648 *value = (*value - r.offset) / r.coeff;
1649 return true;
1650}
1651
1653 int64_t value) {
1654 if (!CanonicalizeEncoding(&var, &value) || !DomainOf(var).Contains(value)) {
1655 return SetLiteralToFalse(literal);
1656 }
1657 literal = GetLiteralRepresentative(literal);
1658 if (!InsertVarValueEncodingInternal(literal, var, value,
1659 /*add_constraints=*/true)) {
1660 return false;
1661 }
1662
1663 eq_half_encoding_.insert({{literal, var}, value});
1664 neq_half_encoding_.insert({{NegatedRef(literal), var}, value});
1665
1666 solution_crush_.MaybeSetLiteralToValueEncoding(literal, var, value);
1667 return true;
1668}
1669
1671 int64_t value) {
1672 if (!CanonicalizeEncoding(&var, &value) || !DomainOf(var).Contains(value)) {
1673 // The literal cannot be true.
1674 return SetLiteralToFalse(literal);
1675 }
1676 literal = GetLiteralRepresentative(literal);
1677 return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/true);
1678}
1679
1681 int64_t value) {
1682 if (!CanonicalizeEncoding(&var, &value) || !DomainOf(var).Contains(value)) {
1683 // The constraint is trivial.
1684 return false;
1685 }
1686 literal = GetLiteralRepresentative(literal);
1687 return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/false);
1688}
1689
1690bool PresolveContext::HasVarValueEncoding(int ref, int64_t value,
1691 int* literal) {
1692 CHECK(!VariableWasRemoved(ref));
1693 if (!CanonicalizeEncoding(&ref, &value)) return false;
1694 DCHECK(RefIsPositive(ref));
1695
1696 if (!DomainOf(ref).Contains(value)) {
1697 if (literal != nullptr) *literal = GetFalseLiteral();
1698 return true;
1699 }
1700
1701 if (CanBeUsedAsLiteral(ref)) {
1702 if (literal != nullptr) {
1703 *literal = value == 1 ? ref : NegatedRef(ref);
1704 }
1705 return true;
1706 }
1707
1708 const auto first_it = encoding_.find(ref);
1709 if (first_it == encoding_.end()) return false;
1710 const auto it = first_it->second.find(value);
1711 if (it == first_it->second.end()) return false;
1712
1713 if (VariableWasRemoved(it->second.Get(this))) return false;
1714 if (literal != nullptr) {
1715 *literal = it->second.Get(this);
1716 }
1717 return true;
1718}
1719
1721 const int var = PositiveRef(ref);
1722 const int64_t size = domains_[var].Size();
1723 if (size <= 2) return true;
1724 const auto& it = encoding_.find(var);
1725 return it == encoding_.end() ? false : size <= it->second.size();
1726}
1727
1729 CHECK_LE(expr.vars_size(), 1);
1730 if (IsFixed(expr)) return true;
1731 return IsFullyEncoded(expr.vars(0));
1732}
1733
1735 CHECK(!VariableWasRemoved(ref));
1736 if (!CanonicalizeEncoding(&ref, &value)) return GetFalseLiteral();
1737
1738 // Positive after CanonicalizeEncoding().
1739 const int var = ref;
1740
1741 // Returns the false literal if the value is not in the domain.
1742 if (!domains_[var].Contains(value)) {
1743 return GetFalseLiteral();
1744 }
1745
1746 // Return the literal itself if this was called or canonicalized to a Boolean.
1747 if (CanBeUsedAsLiteral(ref)) {
1748 return value == 1 ? ref : NegatedRef(ref);
1749 }
1750
1751 // Returns the associated literal if already present.
1752 absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
1753 auto it = var_map.find(value);
1754 if (it != var_map.end()) {
1755 const int lit = it->second.Get(this);
1756 if (VariableWasRemoved(lit)) {
1757 // If the variable was already removed, for now we create a new one.
1758 // This should be rare hopefully.
1759 var_map.erase(value);
1760 } else {
1761 return lit;
1762 }
1763 }
1764
1765 // Special case for fixed domains.
1766 if (domains_[var].Size() == 1) {
1767 const int true_literal = GetTrueLiteral();
1768 var_map[value] = SavedLiteral(true_literal);
1769 return true_literal;
1770 }
1771
1772 // Special case for domains of size 2.
1773 const int64_t var_min = MinOf(var);
1774 const int64_t var_max = MaxOf(var);
1775 if (domains_[var].Size() == 2) {
1776 // Checks if the other value is already encoded.
1777 const int64_t other_value = value == var_min ? var_max : var_min;
1778 auto other_it = var_map.find(other_value);
1779 if (other_it != var_map.end()) {
1780 const int literal = NegatedRef(other_it->second.Get(this));
1781 if (VariableWasRemoved(literal)) {
1782 // If the variable was already removed, for now we create a new one.
1783 // This should be rare hopefully.
1784 var_map.erase(other_value);
1785 } else {
1786 // Update the encoding map. The domain could have been reduced to size
1787 // two after the creation of the first literal.
1788 var_map[value] = SavedLiteral(literal);
1789 return literal;
1790 }
1791 }
1792
1793 if (var_min == 0 && var_max == 1) {
1794 const int representative = GetLiteralRepresentative(var);
1795 var_map[1] = SavedLiteral(representative);
1796 var_map[0] = SavedLiteral(NegatedRef(representative));
1797 return value == 1 ? representative : NegatedRef(representative);
1798 } else {
1799 const int literal = NewBoolVar("integer encoding");
1800 if (!InsertVarValueEncoding(literal, var, var_max)) {
1801 return GetFalseLiteral();
1802 }
1803 const int representative = GetLiteralRepresentative(literal);
1804 return value == var_max ? representative : NegatedRef(representative);
1805 }
1806 }
1807
1808 const int literal = NewBoolVar("integer encoding");
1809 if (!InsertVarValueEncoding(literal, var, value)) {
1810 return GetFalseLiteral();
1811 }
1812 return GetLiteralRepresentative(literal);
1813}
1814
1816 const LinearExpressionProto& expr, int64_t value) {
1817 DCHECK_LE(expr.vars_size(), 1);
1818 if (IsFixed(expr)) {
1819 if (FixedValue(expr) == value) {
1820 return GetTrueLiteral();
1821 } else {
1822 return GetFalseLiteral();
1823 }
1824 }
1825
1826 if ((value - expr.offset()) % expr.coeffs(0) != 0) {
1827 return GetFalseLiteral();
1828 }
1829
1830 return GetOrCreateVarValueEncoding(expr.vars(0),
1831 (value - expr.offset()) / expr.coeffs(0));
1832}
1833
1835 const CpObjectiveProto& obj = working_model->objective();
1836
1837 // We do some small canonicalization here
1838 objective_proto_is_up_to_date_ = false;
1839
1840 objective_offset_ = obj.offset();
1841 objective_scaling_factor_ = obj.scaling_factor();
1842 if (objective_scaling_factor_ == 0.0) {
1843 objective_scaling_factor_ = 1.0;
1844 }
1845
1846 objective_integer_before_offset_ = obj.integer_before_offset();
1847 objective_integer_after_offset_ = obj.integer_after_offset();
1848 objective_integer_scaling_factor_ = obj.integer_scaling_factor();
1849 if (objective_integer_scaling_factor_ == 0) {
1850 objective_integer_scaling_factor_ = 1;
1851 }
1852
1853 if (!obj.domain().empty()) {
1854 // We might relax this in CanonicalizeObjective() when we will compute
1855 // the possible objective domain from the domains of the variables.
1856 objective_domain_is_constraining_ = true;
1857 objective_domain_ = ReadDomainFromProto(obj);
1858 } else {
1859 objective_domain_is_constraining_ = false;
1860 objective_domain_ = Domain::AllValues();
1861 }
1862
1863 // This is an upper bound of the higher magnitude that can be reach by
1864 // summing an objective partial sum. Because of the model validation, this
1865 // shouldn't overflow, and we make sure it stays this way.
1866 objective_overflow_detection_ = std::abs(objective_integer_before_offset_);
1867 int64_t fixed_terms = 0;
1868
1869 objective_map_.clear();
1870 for (int i = 0; i < obj.vars_size(); ++i) {
1871 int var = obj.vars(i);
1872 int64_t coeff = obj.coeffs(i);
1873
1874 // TODO(user): There should be no negative reference here !
1875 if (!RefIsPositive(var)) {
1876 var = NegatedRef(var);
1877 coeff = -coeff;
1878 }
1879
1880 // We remove fixed terms as we read the objective. This can help a lot on
1881 // LNS problems with a large proportions of fixed terms.
1882 if (IsFixed(var)) {
1883 fixed_terms += FixedValue(var) * coeff;
1884 continue;
1885 }
1886
1887 const int64_t var_max_magnitude =
1888 std::max(std::abs(MinOf(var)), std::abs(MaxOf(var)));
1889 objective_overflow_detection_ += var_max_magnitude * std::abs(coeff);
1890
1891 objective_map_[var] += RefIsPositive(var) ? coeff : -coeff;
1892 if (objective_map_[var] == 0) {
1894 } else {
1895 var_to_constraints_[var].insert(kObjectiveConstraint);
1896 }
1897 }
1898
1899 if (fixed_terms != 0) {
1900 AddToObjectiveOffset(fixed_terms);
1901 }
1902}
1903
1905 const auto it = objective_map_.find(var);
1906 if (it == objective_map_.end()) return true;
1907 const int64_t coeff = it->second;
1908
1909 // If a variable only appear in objective, we can fix it!
1910 // Note that we don't care if it was in affine relation, because if none
1911 // of the relations are left, then we can still fix it.
1912 if (params_.cp_model_presolve() &&
1913 !params_.keep_all_feasible_solutions_in_presolve() &&
1914 !objective_domain_is_constraining_ &&
1916 var_to_constraints_[var].size() == 1 &&
1917 var_to_constraints_[var].contains(kObjectiveConstraint)) {
1918 UpdateRuleStats("objective: variable not used elsewhere");
1919 if (coeff > 0) {
1920 if (!IntersectDomainWith(var, Domain(MinOf(var)))) {
1921 return false;
1922 }
1923 } else {
1924 if (!IntersectDomainWith(var, Domain(MaxOf(var)))) {
1925 return false;
1926 }
1927 }
1928 }
1929
1930 if (IsFixed(var)) {
1931 AddToObjectiveOffset(coeff * MinOf(var));
1933 return true;
1934 }
1935
1937 if (r.representative == var) return true;
1938
1940
1941 // After we removed the variable from the objective it might have become a
1942 // unused affine. Add it to the list of variables to check so we reprocess it.
1943 modified_domains.Set(var);
1944
1945 // Do the substitution.
1946 AddToObjectiveOffset(coeff * r.offset);
1947 const int64_t new_coeff = objective_map_[r.representative] += coeff * r.coeff;
1948
1949 // Process new term.
1950 if (new_coeff == 0) {
1952 } else {
1953 var_to_constraints_[r.representative].insert(kObjectiveConstraint);
1954 if (IsFixed(r.representative)) {
1957 }
1958 }
1959 return true;
1960}
1961
1962bool PresolveContext::CanonicalizeObjective(bool simplify_domain) {
1963 objective_proto_is_up_to_date_ = false;
1964
1965 // We replace each entry by its affine representative.
1966 // Note that the non-deterministic loop is fine, but because we iterate
1967 // one the map while modifying it, it is safer to do a copy rather than to
1968 // try to handle that in one pass.
1969 tmp_entries_.clear();
1970 for (const auto& entry : objective_map_) {
1971 tmp_entries_.push_back(entry);
1972 }
1973
1974 // TODO(user): This is a bit duplicated with the presolve linear code.
1975 // We also do not propagate back any domain restriction from the objective to
1976 // the variables if any.
1977 for (const auto& entry : tmp_entries_) {
1978 if (!CanonicalizeOneObjectiveVariable(entry.first)) {
1979 return NotifyThatModelIsUnsat("canonicalize objective one term");
1980 }
1981 }
1982
1983 Domain implied_domain(0);
1984 int64_t gcd(0);
1985
1986 // We need to sort the entries to be deterministic.
1987 tmp_entries_.clear();
1988 for (const auto& entry : objective_map_) {
1989 tmp_entries_.push_back(entry);
1990 }
1991 std::sort(tmp_entries_.begin(), tmp_entries_.end());
1992 for (const auto& entry : tmp_entries_) {
1993 const int var = entry.first;
1994 const int64_t coeff = entry.second;
1995 gcd = std::gcd(gcd, std::abs(coeff));
1996 implied_domain =
1997 implied_domain.AdditionWith(DomainOf(var).MultiplicationBy(coeff))
1999 }
2000
2001 // This is the new domain.
2002 // Note that the domain never include the offset.
2003 objective_domain_ = objective_domain_.IntersectionWith(implied_domain);
2004
2005 // Depending on the use case, we cannot do that.
2006 if (simplify_domain) {
2007 objective_domain_ =
2008 objective_domain_.SimplifyUsingImpliedDomain(implied_domain);
2009 }
2010
2011 // Maybe divide by GCD.
2012 if (gcd > 1) {
2013 for (auto& entry : objective_map_) {
2014 entry.second /= gcd;
2015 }
2016 objective_domain_ = objective_domain_.InverseMultiplicationBy(gcd);
2017 if (objective_domain_.IsEmpty()) {
2018 return NotifyThatModelIsUnsat("empty objective domain");
2019 }
2020
2021 objective_offset_ /= static_cast<double>(gcd);
2022 objective_scaling_factor_ *= static_cast<double>(gcd);
2023
2024 // We update the integer offsets accordingly.
2025 //
2026 // We compute the old "a * objective_scaling_factor_ + b" offset and rewrite
2027 // it in term of the new "objective_scaling_factor_".
2028 const absl::int128 offset =
2029 absl::int128(objective_integer_before_offset_) *
2030 absl::int128(objective_integer_scaling_factor_) +
2031 absl::int128(objective_integer_after_offset_);
2032 objective_integer_scaling_factor_ *= gcd;
2033 objective_integer_before_offset_ = static_cast<int64_t>(
2034 offset / absl::int128(objective_integer_scaling_factor_));
2035 objective_integer_after_offset_ = static_cast<int64_t>(
2036 offset % absl::int128(objective_integer_scaling_factor_));
2037
2038 // It is important to update the implied_domain for the "is constraining"
2039 // test below.
2040 implied_domain = implied_domain.InverseMultiplicationBy(gcd);
2041 }
2042
2043 if (objective_domain_.IsEmpty()) {
2044 return NotifyThatModelIsUnsat("empty objective domain");
2045 }
2046
2047 // Detect if the objective domain do not limit the "optimal" objective value.
2048 // If this is true, then we can apply any reduction that reduce the objective
2049 // value without any issues.
2050 objective_domain_is_constraining_ =
2051 !implied_domain
2052 .IntersectionWith(Domain(std::numeric_limits<int64_t>::min(),
2053 objective_domain_.Max()))
2054 .IsIncludedIn(objective_domain_);
2055 return true;
2056}
2057
2059 CHECK_EQ(objective_map_.size(), 1);
2060 const int var = objective_map_.begin()->first;
2061 const int64_t coeff = objective_map_.begin()->second;
2062
2063 // Transfer all the info to the domain of var.
2064 if (!IntersectDomainWith(var,
2065 objective_domain_.InverseMultiplicationBy(coeff))) {
2066 return false;
2067 }
2068
2069 // Recompute a correct and non-constraining objective domain.
2070 objective_proto_is_up_to_date_ = false;
2071 objective_domain_ = DomainOf(var).ContinuousMultiplicationBy(coeff);
2072 objective_domain_is_constraining_ = false;
2073 return true;
2074}
2075
2077 objective_proto_is_up_to_date_ = false;
2078 const int var = PositiveRef(ref);
2079 objective_map_.erase(var);
2080 EraseFromVarToConstraint(var, kObjectiveConstraint);
2081}
2082
2083void PresolveContext::AddToObjective(int var, int64_t value) {
2084 CHECK(RefIsPositive(var));
2085 objective_proto_is_up_to_date_ = false;
2086 int64_t& map_ref = objective_map_[var];
2087 map_ref += value;
2088 if (map_ref == 0) {
2090 } else {
2091 var_to_constraints_[var].insert(kObjectiveConstraint);
2092 }
2093}
2094
2095void PresolveContext::AddLiteralToObjective(int ref, int64_t value) {
2096 objective_proto_is_up_to_date_ = false;
2097 const int var = PositiveRef(ref);
2098 int64_t& map_ref = objective_map_[var];
2099 if (RefIsPositive(ref)) {
2100 map_ref += value;
2101 } else {
2102 AddToObjectiveOffset(value);
2103 map_ref -= value;
2104 }
2105 if (map_ref == 0) {
2107 } else {
2108 var_to_constraints_[var].insert(kObjectiveConstraint);
2109 }
2110}
2111
2113 objective_proto_is_up_to_date_ = false;
2114 const int64_t temp = CapAdd(objective_integer_before_offset_, delta);
2115 if (temp == std::numeric_limits<int64_t>::min()) return false;
2116 if (temp == std::numeric_limits<int64_t>::max()) return false;
2117 objective_integer_before_offset_ = temp;
2118
2119 // Tricky: The objective domain is without the offset, so we need to shift it.
2120 objective_offset_ += static_cast<double>(delta);
2121 objective_domain_ = objective_domain_.AdditionWith(Domain(-delta));
2122 return true;
2123}
2124
2126 int var_in_equality, int64_t coeff_in_equality,
2127 const ConstraintProto& equality) {
2128 objective_proto_is_up_to_date_ = false;
2129 CHECK(equality.enforcement_literal().empty());
2130 CHECK(RefIsPositive(var_in_equality));
2131
2132 // We can only "easily" substitute if the objective coefficient is a multiple
2133 // of the one in the constraint.
2134 const int64_t coeff_in_objective = objective_map_.at(var_in_equality);
2135 CHECK_NE(coeff_in_equality, 0);
2136 CHECK_EQ(coeff_in_objective % coeff_in_equality, 0);
2137
2138 const int64_t multiplier = coeff_in_objective / coeff_in_equality;
2139
2140 // Abort if the new objective seems to violate our overflow preconditions.
2141 int64_t change = 0;
2142 for (int i = 0; i < equality.linear().vars().size(); ++i) {
2143 int var = equality.linear().vars(i);
2144 if (PositiveRef(var) == var_in_equality) continue;
2145 int64_t coeff = equality.linear().coeffs(i);
2146 change +=
2147 std::abs(coeff) * std::max(std::abs(MinOf(var)), std::abs(MaxOf(var)));
2148 }
2149 const int64_t new_value =
2150 CapAdd(CapProd(std::abs(multiplier), change),
2151 objective_overflow_detection_ -
2152 std::abs(coeff_in_equality) *
2153 std::max(std::abs(MinOf(var_in_equality)),
2154 std::abs(MaxOf(var_in_equality))));
2155 if (new_value == std::numeric_limits<int64_t>::max()) return false;
2156 objective_overflow_detection_ = new_value;
2157
2158 // Compute the objective offset change.
2159 Domain offset = ReadDomainFromProto(equality.linear());
2160 DCHECK_EQ(offset.Min(), offset.Max());
2161 bool exact = true;
2162 offset = offset.MultiplicationBy(multiplier, &exact);
2163 CHECK(exact);
2164 CHECK(!offset.IsEmpty());
2165
2166 // We also need to make sure the integer_offset will not overflow.
2167 if (!AddToObjectiveOffset(offset.Min())) return false;
2168
2169 // Perform the substitution.
2170 for (int i = 0; i < equality.linear().vars().size(); ++i) {
2171 int var = equality.linear().vars(i);
2172 int64_t coeff = equality.linear().coeffs(i);
2173 if (!RefIsPositive(var)) {
2174 var = NegatedRef(var);
2175 coeff = -coeff;
2176 }
2177 if (var == var_in_equality) continue;
2178
2179 int64_t& map_ref = objective_map_[var];
2180 map_ref -= coeff * multiplier;
2181
2182 if (map_ref == 0) {
2184 } else {
2185 var_to_constraints_[var].insert(kObjectiveConstraint);
2186 }
2187 }
2188
2189 RemoveVariableFromObjective(var_in_equality);
2190
2191 // Because we can assume that the constraint we used was constraining
2192 // (otherwise it would have been removed), the objective domain should be now
2193 // constraining.
2194 objective_domain_is_constraining_ = true;
2195
2196 if (objective_domain_.IsEmpty()) {
2197 return NotifyThatModelIsUnsat();
2198 }
2199 return true;
2200}
2201
2203 absl::Span<const int> exactly_one) {
2204 if (objective_map_.empty()) return false;
2205 if (exactly_one.empty()) return false;
2206
2207 int64_t min_coeff = std::numeric_limits<int64_t>::max();
2208 for (const int ref : exactly_one) {
2209 const auto it = objective_map_.find(PositiveRef(ref));
2210 if (it == objective_map_.end()) return false;
2211
2212 const int64_t coeff = it->second;
2213 if (RefIsPositive(ref)) {
2214 min_coeff = std::min(min_coeff, coeff);
2215 } else {
2216 // Objective = coeff * var = coeff * (1 - ref);
2217 min_coeff = std::min(min_coeff, -coeff);
2218 }
2219 }
2220
2221 return ShiftCostInExactlyOne(exactly_one, min_coeff);
2222}
2223
2224bool PresolveContext::ShiftCostInExactlyOne(absl::Span<const int> exactly_one,
2225 int64_t shift) {
2226 if (shift == 0) return true;
2227
2228 // We have to be careful because shifting cost like this might increase the
2229 // min/max possible activity of the sum.
2230 //
2231 // TODO(user): Be more precise with this objective_overflow_detection_ and
2232 // always keep it up to date on each offset / coeff change.
2233 int64_t sum = 0;
2234 int64_t new_sum = 0;
2235 for (const int ref : exactly_one) {
2236 const int var = PositiveRef(ref);
2237 const int64_t obj = ObjectiveCoeff(var);
2238 sum = CapAdd(sum, std::abs(obj));
2239
2240 const int64_t new_obj = RefIsPositive(ref) ? obj - shift : obj + shift;
2241 new_sum = CapAdd(new_sum, std::abs(new_obj));
2242 }
2243 if (AtMinOrMaxInt64(new_sum)) return false;
2244 if (new_sum > sum) {
2245 const int64_t new_value =
2246 CapAdd(objective_overflow_detection_, new_sum - sum);
2247 if (AtMinOrMaxInt64(new_value)) return false;
2248 objective_overflow_detection_ = new_value;
2249 }
2250
2251 int64_t offset = shift;
2252 objective_proto_is_up_to_date_ = false;
2253 for (const int ref : exactly_one) {
2254 const int var = PositiveRef(ref);
2255
2256 // The value will be zero if it wasn't present.
2257 int64_t& map_ref = objective_map_[var];
2258 if (map_ref == 0) {
2259 var_to_constraints_[var].insert(kObjectiveConstraint);
2260 }
2261 if (RefIsPositive(ref)) {
2262 map_ref -= shift;
2263 if (map_ref == 0) {
2265 }
2266 } else {
2267 // Term = coeff * (1 - X) = coeff - coeff * X;
2268 // So -coeff -> -coeff -shift
2269 // And Term = coeff + shift - shift - (coeff + shift) * X
2270 // = (coeff + shift) * (1 - X) - shift;
2271 map_ref += shift;
2272 if (map_ref == 0) {
2274 }
2275 offset -= shift;
2276 }
2277 }
2278
2279 // Note that the domain never include the offset, so we need to update it.
2280 if (offset != 0) AddToObjectiveOffset(offset);
2281
2282 // When we shift the cost using an exactly one, our objective implied bounds
2283 // might be more or less precise. If the objective domain is not constraining
2284 // (and thus just constraining the upper bound), we relax it to make sure its
2285 // stay "non constraining".
2286 //
2287 // TODO(user): This is a bit hacky, find a nicer way.
2288 if (!objective_domain_is_constraining_) {
2289 objective_domain_ =
2290 Domain(std::numeric_limits<int64_t>::min(), objective_domain_.Max());
2291 }
2292
2293 return true;
2294}
2295
2297 if (objective_proto_is_up_to_date_) return;
2298 objective_proto_is_up_to_date_ = true;
2299
2300 // We need to sort the entries to be deterministic.
2301 // Note that --cpu_profile shows it is slightly faster to only compare key.
2302 tmp_entries_.clear();
2303 tmp_entries_.reserve(objective_map_.size());
2304 for (const auto& entry : objective_map_) {
2305 tmp_entries_.push_back(entry);
2306 }
2307 std::sort(tmp_entries_.begin(), tmp_entries_.end(),
2308 [](const std::pair<int, int64_t>& a,
2309 const std::pair<int, int64_t>& b) { return a.first < b.first; });
2310
2311 CpObjectiveProto* mutable_obj = working_model->mutable_objective();
2312 mutable_obj->set_offset(objective_offset_);
2313 mutable_obj->set_scaling_factor(objective_scaling_factor_);
2314 mutable_obj->set_integer_before_offset(objective_integer_before_offset_);
2315 mutable_obj->set_integer_after_offset(objective_integer_after_offset_);
2316 if (objective_integer_scaling_factor_ == 1) {
2317 mutable_obj->set_integer_scaling_factor(0); // Default.
2318 } else {
2319 mutable_obj->set_integer_scaling_factor(objective_integer_scaling_factor_);
2320 }
2321 FillDomainInProto(objective_domain_, mutable_obj);
2322 mutable_obj->clear_vars();
2323 mutable_obj->clear_coeffs();
2324 for (const auto& entry : tmp_entries_) {
2325 mutable_obj->add_vars(entry.first);
2326 mutable_obj->add_coeffs(entry.second);
2327 }
2328}
2329
2331 for (int i = 0; i < working_model->variables_size(); ++i) {
2332 FillDomainInProto(DomainOf(i), working_model->mutable_variables(i));
2333 }
2334}
2335
2337 const LinearExpressionProto& time_i, const LinearExpressionProto& time_j,
2338 int active_i, int active_j) {
2339 CHECK(!LiteralIsFalse(active_i));
2340 CHECK(!LiteralIsFalse(active_j));
2341 DCHECK(ExpressionIsAffine(time_i));
2342 DCHECK(ExpressionIsAffine(time_j));
2343
2344 const std::tuple<int, int64_t, int, int64_t, int64_t, int, int> key =
2345 GetReifiedPrecedenceKey(time_i, time_j, active_i, active_j);
2346 const auto& it = reified_precedences_cache_.find(key);
2347 if (it != reified_precedences_cache_.end()) return it->second;
2348
2349 const int result = NewBoolVar("precedences");
2350 reified_precedences_cache_[key] = result;
2351
2352 solution_crush_.SetVarToReifiedPrecedenceLiteral(result, time_i, time_j,
2353 active_i, active_j);
2354
2355 if (!IsFixed(time_i) && !IsFixed(time_j)) {
2357 {time_i.vars(0), time_j.vars(0)},
2358 {-time_i.coeffs(0), time_j.coeffs(0)}));
2359 }
2360
2361 // result => (time_i <= time_j) && active_i && active_j.
2362 ConstraintProto* const lesseq = working_model->add_constraints();
2363 lesseq->add_enforcement_literal(result);
2364 if (!IsFixed(time_i)) {
2365 lesseq->mutable_linear()->add_vars(time_i.vars(0));
2366 lesseq->mutable_linear()->add_coeffs(-time_i.coeffs(0));
2367 }
2368 if (!IsFixed(time_j)) {
2369 lesseq->mutable_linear()->add_vars(time_j.vars(0));
2370 lesseq->mutable_linear()->add_coeffs(time_j.coeffs(0));
2371 }
2372
2373 const int64_t offset =
2374 (IsFixed(time_i) ? FixedValue(time_i) : time_i.offset()) -
2375 (IsFixed(time_j) ? FixedValue(time_j) : time_j.offset());
2376 lesseq->mutable_linear()->add_domain(offset);
2377 lesseq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::max());
2379
2380 if (!LiteralIsTrue(active_i)) {
2381 AddImplication(result, active_i);
2382 }
2383 if (!LiteralIsTrue(active_j) && active_i != active_j) {
2384 AddImplication(result, active_j);
2385 }
2386
2387 // Not(result) && active_i && active_j => (time_i > time_j)
2388 {
2389 ConstraintProto* const greater = working_model->add_constraints();
2390 if (!IsFixed(time_i)) {
2391 greater->mutable_linear()->add_vars(time_i.vars(0));
2392 greater->mutable_linear()->add_coeffs(-time_i.coeffs(0));
2393 }
2394 if (!IsFixed(time_j)) {
2395 greater->mutable_linear()->add_vars(time_j.vars(0));
2396 greater->mutable_linear()->add_coeffs(time_j.coeffs(0));
2397 }
2398 greater->mutable_linear()->add_domain(std::numeric_limits<int64_t>::min());
2399 greater->mutable_linear()->add_domain(offset - 1);
2400
2401 greater->add_enforcement_literal(NegatedRef(result));
2402 if (!LiteralIsTrue(active_i)) {
2403 greater->add_enforcement_literal(active_i);
2404 }
2405 if (!LiteralIsTrue(active_j) && active_i != active_j) {
2406 greater->add_enforcement_literal(active_j);
2407 }
2409 }
2410
2411 // This is redundant but should improves performance.
2412 //
2413 // If GetOrCreateReifiedPrecedenceLiteral(time_j, time_i, active_j, active_i)
2414 // (the reverse precedence) has been called too, then we can link the two
2415 // precedence literals, and the two active literals together.
2416 const auto& rev_it = reified_precedences_cache_.find(
2417 GetReifiedPrecedenceKey(time_j, time_i, active_j, active_i));
2418 if (rev_it != reified_precedences_cache_.end()) {
2419 auto* const bool_or = working_model->add_constraints()->mutable_bool_or();
2420 bool_or->add_literals(result);
2421 bool_or->add_literals(rev_it->second);
2422 if (!LiteralIsTrue(active_i)) {
2423 bool_or->add_literals(NegatedRef(active_i));
2424 }
2425 if (!LiteralIsTrue(active_j)) {
2426 bool_or->add_literals(NegatedRef(active_j));
2427 }
2428 }
2429
2430 return result;
2431}
2432
2433std::tuple<int, int64_t, int, int64_t, int64_t, int, int>
2435 const LinearExpressionProto& time_j,
2436 int active_i, int active_j) {
2437 const int var_i =
2438 IsFixed(time_i) ? std::numeric_limits<int>::min() : time_i.vars(0);
2439 const int64_t coeff_i = IsFixed(time_i) ? 0 : time_i.coeffs(0);
2440 const int var_j =
2441 IsFixed(time_j) ? std::numeric_limits<int>::min() : time_j.vars(0);
2442 const int64_t coeff_j = IsFixed(time_j) ? 0 : time_j.coeffs(0);
2443 const int64_t offset =
2444 (IsFixed(time_i) ? FixedValue(time_i) : time_i.offset()) -
2445 (IsFixed(time_j) ? FixedValue(time_j) : time_j.offset());
2446 // In all formulas, active_i and active_j are symmetrical, we can sort the
2447 // active literals.
2448 if (active_j < active_i) std::swap(active_i, active_j);
2449 return std::make_tuple(var_i, coeff_i, var_j, coeff_j, offset, active_i,
2450 active_j);
2451}
2452
2454 reified_precedences_cache_.clear();
2455}
2456
2458 SOLVER_LOG(logger_, "");
2459 SOLVER_LOG(logger_, "Presolve summary:");
2460 SOLVER_LOG(logger_, " - ", NumAffineRelations(),
2461 " affine relations were detected.");
2462 absl::btree_map<std::string, int> sorted_rules(stats_by_rule_name_.begin(),
2463 stats_by_rule_name_.end());
2464 for (const auto& entry : sorted_rules) {
2465 if (entry.second == 1) {
2466 SOLVER_LOG(logger_, " - rule '", entry.first, "' was applied 1 time.");
2467 } else {
2468 SOLVER_LOG(logger_, " - rule '", entry.first, "' was applied ",
2469 FormatCounter(entry.second), " times.");
2470 }
2471 }
2472}
2473
2474// Load the constraints in a local model.
2475//
2476// TODO(user): The model we load does not contain affine relations! But
2477// ideally we should be able to remove all of them once we allow more complex
2478// constraints to contains linear expression.
2479//
2480// TODO(user): remove code duplication with cp_model_solver. Here we also do
2481// not run the heuristic to decide which variable to fully encode.
2482//
2483// TODO(user): Maybe do not load slow to propagate constraints? for instance
2484// we do not use any linear relaxation here.
2485bool LoadModelForProbing(PresolveContext* context, Model* local_model) {
2486 if (context->ModelIsUnsat()) return false;
2487
2488 // Update the domain in the current CpModelProto.
2489 context->WriteVariableDomainsToProto();
2490 const CpModelProto& model_proto = *(context->working_model);
2491 // Adapt some of the parameters during this probing phase.
2492 SatParameters local_params = context->params();
2493 local_params.set_use_implied_bounds(false);
2494 return LoadModelForPresolve(model_proto, std::move(local_params), context,
2495 local_model, "probing");
2496}
2497
2498bool LoadModelForPresolve(const CpModelProto& model_proto, SatParameters params,
2499 PresolveContext* context, Model* local_model,
2500 absl::string_view name_for_logging) {
2501 *local_model->GetOrCreate<SatParameters>() = std::move(params);
2502 local_model->GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(
2503 context->time_limit());
2504 local_model->Register<ModelRandomGenerator>(context->random());
2505 auto* encoder = local_model->GetOrCreate<IntegerEncoder>();
2507 auto* mapping = local_model->GetOrCreate<CpModelMapping>();
2508
2509 // Important: Because the model_proto do not contains affine relation or the
2510 // objective, we cannot call DetectOptionalVariables() ! This might wrongly
2511 // detect optionality and derive bad conclusion.
2512 LoadVariables(model_proto, /*view_all_booleans_as_integers=*/false,
2513 local_model);
2514 ExtractEncoding(model_proto, local_model);
2515 auto* sat_solver = local_model->GetOrCreate<SatSolver>();
2516 if (sat_solver->ModelIsUnsat()) {
2517 return context->NotifyThatModelIsUnsat(
2518 absl::StrCat("Initial loading for ", name_for_logging));
2519 }
2520 for (const ConstraintProto& ct : model_proto.constraints()) {
2521 if (mapping->ConstraintIsAlreadyLoaded(&ct)) continue;
2522 CHECK(LoadConstraint(ct, local_model));
2523 if (sat_solver->ModelIsUnsat()) {
2524 return context->NotifyThatModelIsUnsat(
2525 absl::StrCat("after loading constraint during ", name_for_logging,
2526 " ", ProtobufShortDebugString(ct)));
2527 }
2528 }
2529 encoder->AddAllImplicationsBetweenAssociatedLiterals();
2530 if (sat_solver->ModelIsUnsat()) return false;
2531 if (!sat_solver->Propagate()) {
2532 return context->NotifyThatModelIsUnsat(
2533 "during probing initial propagation");
2534 }
2535
2536 return true;
2537}
2538
2539template <typename ProtoWithVarsAndCoeffs, typename PresolveContextT>
2541 absl::Span<const int> enforcements, ProtoWithVarsAndCoeffs* proto,
2542 int64_t* offset, std::vector<std::pair<int, int64_t>>* tmp_terms,
2543 PresolveContextT* context) {
2544 // First regroup the terms on the same variables and sum the fixed ones.
2545 //
2546 // TODO(user): Add a quick pass to skip most of the work below if the
2547 // constraint is already in canonical form?
2548 tmp_terms->clear();
2549 int64_t sum_of_fixed_terms = 0;
2550 bool remapped = false;
2551 const int old_size = proto->vars().size();
2552 DCHECK_EQ(old_size, proto->coeffs().size());
2553 for (int i = 0; i < old_size; ++i) {
2554 // Remove fixed variable and take affine representative.
2555 //
2556 // Note that we need to do that before we test for equality with an
2557 // enforcement (they should already have been mapped).
2558 int new_var;
2559 int64_t new_coeff;
2560 {
2561 const int ref = proto->vars(i);
2562 const int var = PositiveRef(ref);
2563 const int64_t coeff =
2564 RefIsPositive(ref) ? proto->coeffs(i) : -proto->coeffs(i);
2565 if (coeff == 0) continue;
2566
2567 if (context->IsFixed(var)) {
2568 sum_of_fixed_terms += coeff * context->FixedValue(var);
2569 continue;
2570 }
2571
2572 const AffineRelation::Relation r = context->GetAffineRelation(var);
2573 if (r.representative != var) {
2574 remapped = true;
2575 sum_of_fixed_terms += coeff * r.offset;
2576 }
2577
2578 new_var = r.representative;
2579 new_coeff = coeff * r.coeff;
2580 }
2581
2582 // TODO(user): Avoid the quadratic loop for the corner case of many
2583 // enforcement literal (this should be pretty rare though).
2584 bool removed = false;
2585 for (const int enf : enforcements) {
2586 if (new_var == PositiveRef(enf)) {
2587 if (RefIsPositive(enf)) {
2588 // If the constraint is enforced, we can assume the variable is at 1.
2589 sum_of_fixed_terms += new_coeff;
2590 } else {
2591 // We can assume the variable is at zero.
2592 }
2593 removed = true;
2594 break;
2595 }
2596 }
2597 if (removed) {
2598 context->UpdateRuleStats("linear: enforcement literal in expression");
2599 continue;
2600 }
2601
2602 tmp_terms->push_back({new_var, new_coeff});
2603 }
2604 proto->clear_vars();
2605 proto->clear_coeffs();
2606 std::sort(tmp_terms->begin(), tmp_terms->end());
2607 int current_var = 0;
2608 int64_t current_coeff = 0;
2609 for (const auto& entry : *tmp_terms) {
2610 CHECK(RefIsPositive(entry.first));
2611 if (entry.first == current_var) {
2612 current_coeff += entry.second;
2613 } else {
2614 if (current_coeff != 0) {
2615 proto->add_vars(current_var);
2616 proto->add_coeffs(current_coeff);
2617 }
2618 current_var = entry.first;
2619 current_coeff = entry.second;
2620 }
2621 }
2622 if (current_coeff != 0) {
2623 proto->add_vars(current_var);
2624 proto->add_coeffs(current_coeff);
2625 }
2626 if (remapped) {
2627 context->UpdateRuleStats("linear: remapped using affine relations");
2628 }
2629 if (proto->vars().size() < old_size) {
2630 context->UpdateRuleStats("linear: fixed or dup variables");
2631 }
2632 *offset = sum_of_fixed_terms;
2633 return remapped || proto->vars().size() < old_size;
2634}
2635
2636namespace {
2637bool CanonicalizeLinearExpressionNoContext(absl::Span<const int> enforcements,
2638 LinearConstraintProto* proto) {
2639 struct DummyContext {
2640 bool IsFixed(int /*var*/) const { return false; }
2641 int64_t FixedValue(int /*var*/) const { return 0; }
2642 AffineRelation::Relation GetAffineRelation(int var) const {
2643 return {var, 1, 0};
2644 }
2645 void UpdateRuleStats(absl::string_view /*rule*/) const {}
2646 } dummy_context;
2647 int64_t offset = 0;
2648 std::vector<std::pair<int, int64_t>> tmp_terms;
2649 const bool result = CanonicalizeLinearExpressionInternal(
2650 enforcements, proto, &offset, &tmp_terms, &dummy_context);
2651 if (offset != 0) {
2652 FillDomainInProto(ReadDomainFromProto(*proto).AdditionWith(Domain(-offset)),
2653 proto);
2654 }
2655 return result;
2656}
2657} // namespace
2658
2660 int64_t offset = 0;
2661 const bool result = CanonicalizeLinearExpressionInternal(
2662 ct->enforcement_literal(), ct->mutable_linear(), &offset, &tmp_terms_,
2663 this);
2664 const auto [min_activity, max_activity] = ComputeMinMaxActivity(ct->linear());
2665 const Domain implied = Domain(min_activity, max_activity);
2666 const Domain original_domain =
2668 const Domain tight_domain = implied.IntersectionWith(original_domain);
2669 if (tight_domain.IsEmpty()) {
2670 // Canonicalization is not the right place to handle unsat constraints.
2671 // Let's just replace the domain by one that is overflow-safe.
2672 const Domain bad_domain = Domain(implied.Max() + 1, implied.Max() + 2);
2673 FillDomainInProto(bad_domain, ct->mutable_linear());
2674 } else {
2675 FillDomainInProto(tight_domain, ct->mutable_linear());
2676 }
2677 return result;
2678}
2679
2681 absl::Span<const int> enforcements, LinearExpressionProto* expr) {
2682 int64_t offset = 0;
2683 const bool result = CanonicalizeLinearExpressionInternal(
2684 enforcements, expr, &offset, &tmp_terms_, this);
2685 expr->set_offset(expr->offset() + offset);
2686 return result;
2687}
2688
2690 int line) {
2691 const int c = mapping_model->constraints().size();
2692 ConstraintProto* new_ct = mapping_model->add_constraints();
2693 if (absl::GetFlag(FLAGS_cp_model_debug_postsolve)) {
2694 new_ct->set_name(absl::StrCat("#", c, " ", file, ":", line));
2695 }
2696 return new_ct;
2697}
2698
2700 const ConstraintProto& base_ct, absl::string_view file, int line) {
2701 const int c = mapping_model->constraints().size();
2702 ConstraintProto* new_ct = mapping_model->add_constraints();
2703 *new_ct = base_ct;
2704 if (absl::GetFlag(FLAGS_cp_model_debug_postsolve)) {
2705 new_ct->set_name(absl::StrCat("#c", c, " ", file, ":", line));
2706 }
2707 return new_ct;
2708}
2709
2711 const PresolveContext* context,
2712 std::vector<int>* variable_mapping,
2713 CpModelProto* mini_model) {
2714 mini_model->Clear();
2715
2716 *mini_model->add_constraints() = ct;
2717
2718 absl::flat_hash_map<int, int> inverse_interval_map;
2719 for (const int i : UsedIntervals(ct)) {
2720 auto [it, inserted] =
2721 inverse_interval_map.insert({i, mini_model->constraints_size()});
2722 if (inserted) {
2723 const ConstraintProto& itv_ct = context->working_model->constraints(i);
2724 *mini_model->add_constraints() = itv_ct;
2725
2726 // Now add end = start + size for the interval. This is not strictly
2727 // necessary but it makes the presolve more powerful.
2728 ConstraintProto* linear = mini_model->add_constraints();
2730 LinearConstraintProto* mutable_linear = linear->mutable_linear();
2731 const IntervalConstraintProto& itv = itv_ct.interval();
2732
2733 mutable_linear->add_domain(0);
2734 mutable_linear->add_domain(0);
2735 AddLinearExpressionToLinearConstraint(itv.start(), 1, mutable_linear);
2736 AddLinearExpressionToLinearConstraint(itv.size(), 1, mutable_linear);
2737 AddLinearExpressionToLinearConstraint(itv.end(), -1, mutable_linear);
2738 CanonicalizeLinearExpressionNoContext(itv_ct.enforcement_literal(),
2739 mutable_linear);
2740 }
2741 }
2742
2743 absl::flat_hash_map<int, int> inverse_variable_map;
2744 for (const ConstraintProto& cur_ct : mini_model->constraints()) {
2745 for (const int v : UsedVariables(cur_ct)) {
2746 auto [it, inserted] =
2747 inverse_variable_map.insert({v, mini_model->variables_size()});
2748 if (inserted) {
2749 FillDomainInProto(context->DomainOf(v), mini_model->add_variables());
2750 }
2751 }
2752 }
2753
2754 variable_mapping->resize(inverse_variable_map.size());
2755 for (const auto& [k, v] : inverse_variable_map) {
2756 (*variable_mapping)[v] = k;
2757 }
2758 const auto mapping_function = [&inverse_variable_map](int* i) {
2759 const bool is_positive = RefIsPositive(*i);
2760 const int positive_ref = is_positive ? *i : NegatedRef(*i);
2761
2762 const auto it = inverse_variable_map.find(positive_ref);
2763 DCHECK(it != inverse_variable_map.end());
2764 *i = is_positive ? it->second : NegatedRef(it->second);
2765 };
2766 const auto interval_mapping_function = [&inverse_interval_map](int* i) {
2767 const auto it = inverse_interval_map.find(*i);
2768 DCHECK(it != inverse_interval_map.end());
2769 *i = it->second;
2770 };
2771 for (ConstraintProto& ct : *mini_model->mutable_constraints()) {
2772 ApplyToAllVariableIndices(mapping_function, &ct);
2773 ApplyToAllLiteralIndices(mapping_function, &ct);
2774 ApplyToAllIntervalIndices(interval_mapping_function, &ct);
2778 for (LinearExpressionProto& expr : *node_exprs.mutable_exprs()) {
2779 if (expr.vars().empty()) continue;
2780 DCHECK_EQ(expr.vars().size(), 1);
2781 const int ref = expr.vars(0);
2782 const auto it = inverse_variable_map.find(PositiveRef(ref));
2783 if (it == inverse_variable_map.end()) {
2784 expr.clear_vars();
2785 expr.clear_coeffs();
2786 continue;
2787 }
2788 const int image = it->second;
2789 expr.set_vars(0, RefIsPositive(ref) ? image : NegatedRef(image));
2790 }
2791 }
2792 }
2793 }
2794}
2795
2798 const absl::Span<const int64_t> hint = solution_crush_.GetVarValues();
2799 if (hint.size() != working_model->variables().size()) return false;
2800 return SolutionIsFeasible(*working_model, hint);
2801}
2802
2803} // namespace sat
2804} // namespace operations_research
bool TryAdd(int x, int y, int64_t coeff, int64_t offset)
Domain MultiplicationBy(int64_t coeff, bool *exact=nullptr) const
Domain IntersectionWith(const Domain &domain) const
Domain ContinuousMultiplicationBy(int64_t coeff) const
bool Contains(int64_t value) const
Domain AdditionWith(const Domain &domain) const
bool IsIncludedIn(const Domain &domain) const
Domain InverseMultiplicationBy(int64_t coeff) const
int64_t ClosestValue(int64_t wanted) const
::operations_research::sat::BoolArgumentProto *PROTOBUF_NONNULL mutable_bool_and()
::int32_t enforcement_literal(int index) const
const ::operations_research::sat::LinearConstraintProto & linear() const
const ::operations_research::sat::IntervalConstraintProto & interval() const
::operations_research::sat::LinearConstraintProto *PROTOBUF_NONNULL mutable_linear()
::operations_research::sat::RoutesConstraintProto *PROTOBUF_NONNULL mutable_routes()
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_enforcement_literal()
void set_name(Arg_ &&arg, Args_... args)
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL mutable_constraints(int index)
bool has_floating_point_objective() const
.operations_research.sat.FloatObjectiveProto floating_point_objective = 9;
const ::operations_research::sat::FloatObjectiveProto & floating_point_objective() const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
bool has_objective() const
.operations_research.sat.CpObjectiveProto objective = 4;
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
int constraints_size() const
repeated .operations_research.sat.ConstraintProto constraints = 3;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL add_variables()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL add_constraints()
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
int vars_size() const
repeated int32 vars = 1;
const ::operations_research::sat::LinearExpressionProto & size() const
const ::operations_research::sat::LinearExpressionProto & end() const
const ::operations_research::sat::LinearExpressionProto & start() const
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_coeffs()
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_vars()
int vars_size() const
repeated int32 vars = 1;
void Register(T *non_owned_class)
Definition model.h:177
ABSL_MUST_USE_RESULT bool CanonicalizeObjective(bool simplify_domain=true)
bool ExpressionIsSingleVariable(const LinearExpressionProto &expr) const
Returns true iff the expr is of the form 1 * var + 0.
bool CanonicalizeAffineVariable(int ref, int64_t coeff, int64_t mod, int64_t rhs)
ABSL_MUST_USE_RESULT bool IntersectDomainWith(int ref, const Domain &domain, bool *domain_modified=nullptr)
bool ExpressionIsALiteral(const LinearExpressionProto &expr, int *literal=nullptr) const
Returns true iff the expr is a literal (x or not(x)).
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64_t value)
void ClearStats()
Clears the "rules" statistics.
bool StoreAffineRelation(int var_x, int var_y, int64_t coeff, int64_t offset, bool debug_no_recursion=false)
SparseBitset< int > modified_domains
Each time a domain is modified this is set to true.
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
int NewIntVarWithDefinition(const Domain &domain, absl::Span< const std::pair< int, int64_t > > definition, bool append_constraint_to_mapping_model=false)
bool DomainIsEmpty(int ref) const
Helpers to query the current domain of a variable.
ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective(int var_in_equality, int64_t coeff_in_equality, const ConstraintProto &equality)
bool IntervalIsConstant(int ct_ref) const
Helper to query the state of an interval.
int NewIntVar(const Domain &domain)
Helpers to adds new variables to the presolved model.
bool ShiftCostInExactlyOne(absl::Span< const int > exactly_one, int64_t shift)
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
Returns false if the 'lit' doesn't have the desired value in the domain.
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(absl::string_view message="")
int GetOrCreateVarValueEncoding(int ref, int64_t value)
ABSL_MUST_USE_RESULT bool CanonicalizeOneObjectiveVariable(int var)
std::string IntervalDebugString(int ct_ref) const
bool ExpressionIsAffineBoolean(const LinearExpressionProto &expr) const
bool VariableIsOnlyUsedInLinear1AndOneExtraConstraint(int var) const
bool StoreBooleanEqualityRelation(int ref_a, int ref_b)
void AddImplyInDomain(int b, int x, const Domain &domain)
b => (x ∈ domain).
bool VariableIsOnlyUsedInEncodingAndMaybeInObjective(int var) const
std::tuple< int, int64_t, int, int64_t, int64_t, int, int > GetReifiedPrecedenceKey(const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)
std::pair< int64_t, int64_t > ComputeMinMaxActivity(const ProtoWithVarsAndCoeffs &proto) const
int NewBoolVar(absl::string_view source)
void LogInfo()
Logs stats to the logger.
void ClearPrecedenceCache()
Clear the precedence cache.
int NewBoolVarWithClause(absl::Span< const int > clause)
bool HasVarValueEncoding(int ref, int64_t value, int *literal=nullptr)
void RemoveVariableFromObjective(int ref)
Allows to manipulate the objective coefficients.
std::optional< int64_t > FixedValueOrNullopt(const LinearExpressionProto &expr) const
This is faster than testing IsFixed() + FixedValue().
Domain DomainSuperSetOf(const LinearExpressionProto &expr) const
Return a super-set of the domain of the linear expression.
void InitializeNewDomains()
Creates the internal structure for any new variables in working_model.
bool VariableIsNotUsedAnymore(int ref) const
Returns true if this ref no longer appears in the model.
bool VariableIsUnique(int ref) const
Returns true if this ref only appear in one constraint.
ConstraintProto * NewMappingConstraint(absl::string_view file, int line)
int GetLiteralRepresentative(int ref) const
Returns the representative of a literal.
int GetOrCreateAffineValueEncoding(const LinearExpressionProto &expr, int64_t value)
int LiteralForExpressionMax(const LinearExpressionProto &expr) const
bool CanonicalizeLinearExpression(absl::Span< const int > enforcements, LinearExpressionProto *expr)
void UpdateRuleStats(const std::string &name, int num_times=1)
AffineRelation::Relation GetAffineRelation(int ref) const
Returns the representative of ref under the affine relations.
void AddToObjective(int var, int64_t value)
const absl::flat_hash_set< int > & VarToConstraints(int var) const
std::string RefDebugString(int ref) const
To facilitate debugging.
void AddLiteralToObjective(int ref, int64_t value)
bool InsertVarValueEncoding(int literal, int var, int64_t value)
void UpdateNewConstraintsVariableUsage()
Calls UpdateConstraintVariableUsage() on all newly created constraints.
int NumAffineRelations() const
Used for statistics.
std::string AffineRelationDebugString(int ref) const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64_t value)
bool ExploitExactlyOneInObjective(absl::Span< const int > exactly_one)
bool DomainContains(int ref, int64_t value) const
int NewBoolVarWithConjunction(absl::Span< const int > conjunction)
int GetOrCreateReifiedPrecedenceLiteral(const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)
bool CanonicalizeLinearConstraint(ConstraintProto *ct)
::operations_research::sat::RoutesConstraintProto_NodeExpressions *PROTOBUF_NONNULL mutable_dimensions(int index)
RoutesConstraintProto_NodeExpressions NodeExpressions
nested types -------------------------------------------------—
int Get(PresolveContext *context) const
Definition file.cc:326
bool CanonicalizeLinearExpressionInternal(absl::Span< const int > enforcements, ProtoWithVarsAndCoeffs *proto, int64_t *offset, std::vector< std::pair< int, int64_t > > *tmp_terms, PresolveContextT *context)
bool LoadModelForProbing(PresolveContext *context, Model *local_model)
bool SolutionIsFeasible(const CpModelProto &model, absl::Span< const int64_t > variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
int64_t ProductWithModularInverse(int64_t coeff, int64_t mod, int64_t rhs)
Definition util.cc:182
bool ConstraintIsFeasible(const CpModelProto &model, const ConstraintProto &constraint, absl::Span< const int64_t > variable_values)
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void LoadVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
bool ScaleFloatingPointObjective(const SatParameters &params, SolverLogger *logger, CpModelProto *proto)
bool ScaleAndSetObjective(const SatParameters &params, absl::Span< const std::pair< int, double > > objective, double objective_offset, bool maximize, CpModelProto *cp_model, SolverLogger *logger)
Definition lp_utils.cc:1355
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset, std::pair< int64_t, int64_t > *implied_domain)
bool ExpressionIsAffine(const LinearExpressionProto &expr)
Checks if the expression is affine or constant.
constexpr int kAffineRelationConstraint
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
Definition util.cc:44
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
constexpr int kObjectiveConstraint
We use some special constraint index in our variable <-> constraint graph.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
void CreateValidModelWithSingleConstraint(const ConstraintProto &ct, const PresolveContext *context, std::vector< int > *variable_mapping, CpModelProto *mini_model)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool LoadModelForPresolve(const CpModelProto &model_proto, SatParameters params, PresolveContext *context, Model *local_model, absl::string_view name_for_logging)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
In SWIG mode, we don't want anything besides these top-level includes.
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
int64_t CapAdd(int64_t x, int64_t y)
std::string ProtobufShortDebugString(const P &message)
Definition proto_utils.h:46
int64_t CapProd(int64_t x, int64_t y)
std::string ProtobufDebugString(const P &message)
Definition proto_utils.h:31
absl::string_view ToString(MPSolver::OptimizationProblemType optimization_problem_type)
ABSL_FLAG(bool, cp_model_debug_postsolve, false, "DEBUG ONLY. When set to true, the mapping_model.proto will contains " "file:line of the code that created that constraint. This is helpful " "for debugging postsolve")
Definition model.h:51
#define SOLVER_LOG(logger,...)
Definition logging.h:110