OR-Tools  8.2
presolve_context.cc
Go to the documentation of this file.
1 // Copyright 2010-2018 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 "ortools/base/map_util.h"
17 #include "ortools/base/mathutil.h"
20 
21 namespace operations_research {
22 namespace sat {
23 
25  return context->GetLiteralRepresentative(ref_);
26 }
27 
29  return context->GetVariableRepresentative(ref_);
30 }
31 
33 
34 int PresolveContext::NewIntVar(const Domain& domain) {
35  IntegerVariableProto* const var = working_model->add_variables();
36  FillDomainInProto(domain, var);
38  return working_model->variables_size() - 1;
39 }
40 
42 
44  if (!gtl::ContainsKey(constant_to_ref_, cst)) {
45  constant_to_ref_[cst] = SavedVariable(working_model->variables_size());
46  IntegerVariableProto* const var_proto = working_model->add_variables();
47  var_proto->add_domain(cst);
48  var_proto->add_domain(cst);
50  }
51  return constant_to_ref_[cst].Get(this);
52 }
53 
54 // a => b.
56  ConstraintProto* const ct = working_model->add_constraints();
57  ct->add_enforcement_literal(a);
58  ct->mutable_bool_and()->add_literals(b);
59 }
60 
61 // b => x in [lb, ub].
62 void PresolveContext::AddImplyInDomain(int b, int x, const Domain& domain) {
63  ConstraintProto* const imply = working_model->add_constraints();
64 
65  // Doing it like this seems to use slightly less memory.
66  // TODO(user): Find the best way to create such small proto.
67  imply->mutable_enforcement_literal()->Resize(1, b);
68  LinearConstraintProto* mutable_linear = imply->mutable_linear();
69  mutable_linear->mutable_vars()->Resize(1, x);
70  mutable_linear->mutable_coeffs()->Resize(1, 1);
71  FillDomainInProto(domain, mutable_linear);
72 }
73 
74 bool PresolveContext::DomainIsEmpty(int ref) const {
75  return domains[PositiveRef(ref)].IsEmpty();
76 }
77 
78 bool PresolveContext::IsFixed(int ref) const {
79  DCHECK_LT(PositiveRef(ref), domains.size());
80  DCHECK(!DomainIsEmpty(ref));
81  return domains[PositiveRef(ref)].IsFixed();
82 }
83 
85  const int var = PositiveRef(ref);
86  return domains[var].Min() >= 0 && domains[var].Max() <= 1;
87 }
88 
89 bool PresolveContext::LiteralIsTrue(int lit) const {
91  if (RefIsPositive(lit)) {
92  return domains[lit].Min() == 1;
93  } else {
94  return domains[PositiveRef(lit)].Max() == 0;
95  }
96 }
97 
98 bool PresolveContext::LiteralIsFalse(int lit) const {
100  if (RefIsPositive(lit)) {
101  return domains[lit].Max() == 0;
102  } else {
103  return domains[PositiveRef(lit)].Min() == 1;
104  }
105 }
106 
108  DCHECK(!DomainIsEmpty(ref));
109  return RefIsPositive(ref) ? domains[PositiveRef(ref)].Min()
110  : -domains[PositiveRef(ref)].Max();
111 }
112 
114  DCHECK(!DomainIsEmpty(ref));
115  return RefIsPositive(ref) ? domains[PositiveRef(ref)].Max()
116  : -domains[PositiveRef(ref)].Min();
117 }
118 
119 int64 PresolveContext::MinOf(const LinearExpressionProto& expr) const {
120  int64 result = expr.offset();
121  for (int i = 0; i < expr.vars_size(); ++i) {
122  const int64 coeff = expr.coeffs(i);
123  if (coeff > 0) {
124  result += coeff * MinOf(expr.vars(i));
125  } else {
126  result += coeff * MaxOf(expr.vars(i));
127  }
128  }
129  return result;
130 }
131 
132 int64 PresolveContext::MaxOf(const LinearExpressionProto& expr) const {
133  int64 result = expr.offset();
134  for (int i = 0; i < expr.vars_size(); ++i) {
135  const int64 coeff = expr.coeffs(i);
136  if (coeff > 0) {
137  result += coeff * MaxOf(expr.vars(i));
138  } else {
139  result += coeff * MinOf(expr.vars(i));
140  }
141  }
142  return result;
143 }
144 
145 // Important: To be sure a variable can be removed, we need it to not be a
146 // representative of both affine and equivalence relation.
147 bool PresolveContext::VariableIsNotRepresentativeOfEquivalenceClass(
148  int var) const {
150  if (affine_relations_.ClassSize(var) > 1 &&
151  affine_relations_.Get(var).representative == var) {
152  return false;
153  }
154  if (var_equiv_relations_.ClassSize(var) > 1 &&
155  var_equiv_relations_.Get(var).representative == var) {
156  return false;
157  }
158  return true;
159 }
160 
161 // Tricky: If this variable is equivalent to another one (but not the
162 // representative) and appear in just one constraint, then this constraint must
163 // be the affine defining one. And in this case the code using this function
164 // should do the proper stuff.
166  if (!ConstraintVariableGraphIsUpToDate()) return false;
167  const int var = PositiveRef(ref);
168  return var_to_constraints_[var].size() == 1 &&
169  VariableIsNotRepresentativeOfEquivalenceClass(var) &&
171 }
172 
173 // Tricky: Same remark as for VariableIsUniqueAndRemovable().
175  if (!ConstraintVariableGraphIsUpToDate()) return false;
176  const int var = PositiveRef(ref);
177  return !keep_all_feasible_solutions &&
178  var_to_constraints_[var].contains(kObjectiveConstraint) &&
179  var_to_constraints_[var].size() == 2 &&
180  VariableIsNotRepresentativeOfEquivalenceClass(var);
181 }
182 
183 // Here, even if the variable is equivalent to others, if its affine defining
184 // constraints where removed, then it is not needed anymore.
186  if (!ConstraintVariableGraphIsUpToDate()) return false;
187  return var_to_constraints_[PositiveRef(ref)].empty();
188 }
189 
191  removed_variables_.insert(PositiveRef(ref));
192 }
193 
194 // Note(user): I added an indirection and a function for this to be able to
195 // display debug information when this return false. This should actually never
196 // return false in the cases where it is used.
198  // It is okay to reuse removed fixed variable.
199  if (IsFixed(ref)) return false;
200  if (!removed_variables_.contains(PositiveRef(ref))) return false;
201  if (!var_to_constraints_[PositiveRef(ref)].empty()) {
202  LOG(INFO) << "Variable " << PositiveRef(ref)
203  << " was removed, yet it appears in some constraints!";
204  LOG(INFO) << "affine relation: "
206  for (const int c : var_to_constraints_[PositiveRef(ref)]) {
207  LOG(INFO) << "constraint #" << c << " : "
208  << (c >= 0 ? working_model->constraints(c).ShortDebugString()
209  : "");
210  }
211  }
212  return true;
213 }
214 
216  if (!ConstraintVariableGraphIsUpToDate()) return false;
217  const int var = PositiveRef(ref);
218  return var_to_num_linear1_[var] == var_to_constraints_[var].size();
219 }
220 
222  Domain result;
223  if (RefIsPositive(ref)) {
224  result = domains[ref];
225  } else {
226  result = domains[PositiveRef(ref)].Negation();
227  }
228  return result;
229 }
230 
232  if (!RefIsPositive(ref)) {
233  return domains[PositiveRef(ref)].Contains(-value);
234  }
235  return domains[ref].Contains(value);
236 }
237 
238 ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWith(
239  int ref, const Domain& domain, bool* domain_modified) {
240  DCHECK(!DomainIsEmpty(ref));
241  const int var = PositiveRef(ref);
242 
243  if (RefIsPositive(ref)) {
244  if (domains[var].IsIncludedIn(domain)) {
245  return true;
246  }
247  domains[var] = domains[var].IntersectionWith(domain);
248  } else {
249  const Domain temp = domain.Negation();
250  if (domains[var].IsIncludedIn(temp)) {
251  return true;
252  }
253  domains[var] = domains[var].IntersectionWith(temp);
254  }
255 
256  if (domain_modified != nullptr) {
257  *domain_modified = true;
258  }
260  if (domains[var].IsEmpty()) {
261  is_unsat = true;
262  return false;
263  }
264 
265  // Propagate the domain of the representative right away.
266  // Note that the recursive call should only by one level deep.
268  if (r.representative == var) return true;
270  DomainOf(var)
271  .AdditionWith(Domain(-r.offset))
273 }
274 
275 ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralToFalse(int lit) {
276  const int var = PositiveRef(lit);
277  const int64 value = RefIsPositive(lit) ? 0 : 1;
279 }
280 
281 ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralToTrue(int lit) {
282  return SetLiteralToFalse(NegatedRef(lit));
283 }
284 
285 void PresolveContext::UpdateRuleStats(const std::string& name, int num_times) {
286  if (enable_stats) {
287  VLOG(1) << num_presolve_operations << " : " << name;
288  stats_by_rule_name[name] += num_times;
289  }
290  num_presolve_operations += num_times;
291 }
292 
293 void PresolveContext::UpdateLinear1Usage(const ConstraintProto& ct, int c) {
294  const int old_var = constraint_to_linear1_var_[c];
295  if (old_var >= 0) {
296  var_to_num_linear1_[old_var]--;
297  }
298  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear &&
299  ct.linear().vars().size() == 1) {
300  const int var = PositiveRef(ct.linear().vars(0));
301  constraint_to_linear1_var_[c] = var;
302  var_to_num_linear1_[var]++;
303  }
304 }
305 
306 void PresolveContext::AddVariableUsage(int c) {
307  const ConstraintProto& ct = working_model->constraints(c);
308  constraint_to_vars_[c] = UsedVariables(ct);
309  constraint_to_intervals_[c] = UsedIntervals(ct);
310  for (const int v : constraint_to_vars_[c]) {
312  var_to_constraints_[v].insert(c);
313  }
314  for (const int i : constraint_to_intervals_[c]) interval_usage_[i]++;
315  UpdateLinear1Usage(ct, c);
316 }
317 
319  if (is_unsat) return;
320  DCHECK_EQ(constraint_to_vars_.size(), working_model->constraints_size());
321  const ConstraintProto& ct = working_model->constraints(c);
322 
323  // We don't optimize the interval usage as this is not super frequent.
324  for (const int i : constraint_to_intervals_[c]) interval_usage_[i]--;
325  constraint_to_intervals_[c] = UsedIntervals(ct);
326  for (const int i : constraint_to_intervals_[c]) interval_usage_[i]++;
327 
328  // For the variables, we avoid an erase() followed by an insert() for the
329  // variables that didn't change.
330  tmp_new_usage_ = UsedVariables(ct);
331  const std::vector<int>& old_usage = constraint_to_vars_[c];
332  const int old_size = old_usage.size();
333  int i = 0;
334  for (const int var : tmp_new_usage_) {
336  while (i < old_size && old_usage[i] < var) {
337  var_to_constraints_[old_usage[i]].erase(c);
338  ++i;
339  }
340  if (i < old_size && old_usage[i] == var) {
341  ++i;
342  } else {
343  var_to_constraints_[var].insert(c);
344  }
345  }
346  for (; i < old_size; ++i) var_to_constraints_[old_usage[i]].erase(c);
347  constraint_to_vars_[c] = tmp_new_usage_;
348 
349  UpdateLinear1Usage(ct, c);
350 }
351 
353  return constraint_to_vars_.size() == working_model->constraints_size();
354 }
355 
357  if (is_unsat) return;
358  const int old_size = constraint_to_vars_.size();
359  const int new_size = working_model->constraints_size();
360  CHECK_LE(old_size, new_size);
361  constraint_to_vars_.resize(new_size);
362  constraint_to_linear1_var_.resize(new_size, -1);
363  constraint_to_intervals_.resize(new_size);
364  interval_usage_.resize(new_size);
365  for (int c = old_size; c < new_size; ++c) {
366  AddVariableUsage(c);
367  }
368 }
369 
370 // TODO(user): Also test var_to_constraints_ !!
372  if (is_unsat) return true; // We do not care in this case.
373  if (constraint_to_vars_.size() != working_model->constraints_size()) {
374  LOG(INFO) << "Wrong constraint_to_vars size!";
375  return false;
376  }
377  for (int c = 0; c < constraint_to_vars_.size(); ++c) {
378  if (constraint_to_vars_[c] !=
379  UsedVariables(working_model->constraints(c))) {
380  LOG(INFO) << "Wrong variables usage for constraint: \n"
381  << ProtobufDebugString(working_model->constraints(c))
382  << "old_size: " << constraint_to_vars_[c].size();
383  return false;
384  }
385  }
386  int num_in_objective = 0;
387  for (int v = 0; v < var_to_constraints_.size(); ++v) {
388  if (var_to_constraints_[v].contains(kObjectiveConstraint)) {
389  ++num_in_objective;
390  if (!objective_map_.contains(v)) {
391  LOG(INFO) << "Variable " << v
392  << " is marked as part of the objective but isn't.";
393  return false;
394  }
395  }
396  }
397  if (num_in_objective != objective_map_.size()) {
398  LOG(INFO) << "Not all variables are marked as part of the objective";
399  return false;
400  }
401 
402  return true;
403 }
404 
405 // If a Boolean variable (one with domain [0, 1]) appear in this affine
406 // equivalence class, then we want its representative to be Boolean. Note that
407 // this is always possible because a Boolean variable can never be equal to a
408 // multiple of another if std::abs(coeff) is greater than 1 and if it is not
409 // fixed to zero. This is important because it allows to simply use the same
410 // representative for any referenced literals.
411 //
412 // Note(user): When both domain contains [0,1] and later the wrong variable
413 // become usable as boolean, then we have a bug. Because of that, the code
414 // for GetLiteralRepresentative() is not as simple as it should be.
415 bool PresolveContext::AddRelation(int x, int y, int64 c, int64 o,
416  AffineRelation* repo) {
417  // When the coefficient is larger than one, then if later one variable becomes
418  // Boolean, it must be the representative.
419  if (std::abs(c) != 1) return repo->TryAdd(x, y, c, o);
420 
423 
424  // To avoid integer overflow, we always want to use the representative with
425  // the smallest domain magnitude. Otherwise we might express a variable in say
426  // [0, 3] as ([x, x + 3] - x) for an arbitrary large x, and substituting
427  // something like this in a linear expression could break our overflow
428  // precondition.
429  //
430  // Note that if either rep_x or rep_y can be used as a literal, then it will
431  // also be the variable with the smallest domain magnitude (1 or 0 if fixed).
432  const int rep_x = repo->Get(x).representative;
433  const int rep_y = repo->Get(y).representative;
434  const int64 m_x = std::max(std::abs(MinOf(rep_x)), std::abs(MaxOf(rep_x)));
435  const int64 m_y = std::max(std::abs(MinOf(rep_y)), std::abs(MaxOf(rep_y)));
436  bool allow_rep_x = m_x < m_y;
437  bool allow_rep_y = m_y < m_x;
438  if (m_x == m_y) {
439  // If both magnitude are the same, we prefer a positive domain.
440  // This is important so we don't use [-1, 0] as a representative for [0, 1].
441  allow_rep_x = MinOf(rep_x) >= MinOf(rep_y);
442  allow_rep_y = MinOf(rep_y) >= MinOf(rep_x);
443  }
444  return repo->TryAdd(x, y, c, o, allow_rep_x, allow_rep_y);
445 }
446 
449  CHECK(IsFixed(var));
450  const int64 min = MinOf(var);
451  if (gtl::ContainsKey(constant_to_ref_, min)) {
452  const int rep = constant_to_ref_[min].Get(this);
453  if (RefIsPositive(rep)) {
454  if (rep != var) {
455  AddRelation(var, rep, 1, 0, &affine_relations_);
456  AddRelation(var, rep, 1, 0, &var_equiv_relations_);
457  }
458  } else {
459  if (PositiveRef(rep) == var) {
460  CHECK_EQ(min, 0);
461  } else {
462  AddRelation(var, PositiveRef(rep), -1, 0, &affine_relations_);
463  AddRelation(var, PositiveRef(rep), -1, 0, &var_equiv_relations_);
464  }
465  }
466  } else {
467  constant_to_ref_[min] = SavedVariable(var);
468  }
469 }
470 
472  const int var = PositiveRef(ref);
474  if (r.representative == var) return true;
475 
476  // Propagate domains both ways.
477  // var = coeff * rep + offset
479  DomainOf(var)
480  .AdditionWith(Domain(-r.offset))
482  return false;
483  }
486  .AdditionWith(Domain(r.offset)))) {
487  return false;
488  }
489 
490  return true;
491 }
492 
494  for (auto& ref_map : var_to_constraints_) {
495  ref_map.erase(kAffineRelationConstraint);
496  }
497 }
498 
499 // We only call that for a non representative variable that is only used in
500 // the kAffineRelationConstraint. Such variable can be ignored and should never
501 // be seen again in the presolve.
503  const int rep = GetAffineRelation(var).representative;
504 
506  CHECK_NE(var, rep);
507  CHECK_EQ(var_to_constraints_[var].size(), 1);
508  CHECK(var_to_constraints_[var].contains(kAffineRelationConstraint));
509  CHECK(var_to_constraints_[rep].contains(kAffineRelationConstraint));
510 
511  // We shouldn't reuse this variable again!
513 
514  var_to_constraints_[var].erase(kAffineRelationConstraint);
515  affine_relations_.IgnoreFromClassSize(var);
516  var_equiv_relations_.IgnoreFromClassSize(var);
517 
518  // If the representative is left alone, we can remove it from the special
519  // affine relation constraint too.
520  if (affine_relations_.ClassSize(rep) == 1 &&
521  var_equiv_relations_.ClassSize(rep) == 1) {
522  var_to_constraints_[rep].erase(kAffineRelationConstraint);
523  }
524 
525  if (VLOG_IS_ON(2)) {
526  LOG(INFO) << "Removing affine relation: " << AffineRelationDebugString(var);
527  }
528 }
529 
530 bool PresolveContext::StoreAffineRelation(int ref_x, int ref_y, int64 coeff,
531  int64 offset) {
532  CHECK_NE(coeff, 0);
533  if (is_unsat) return false;
534 
535  // TODO(user): I am not 100% sure why, but sometimes the representative is
536  // fixed but that is not propagated to ref_x or ref_y and this causes issues.
537  if (!PropagateAffineRelation(ref_x)) return true;
538  if (!PropagateAffineRelation(ref_y)) return true;
539 
540  if (IsFixed(ref_x)) {
541  const int64 lhs = DomainOf(ref_x).Min() - offset;
542  if (lhs % std::abs(coeff) != 0) {
543  is_unsat = true;
544  return true;
545  }
546  static_cast<void>(IntersectDomainWith(ref_y, Domain(lhs / coeff)));
547  UpdateRuleStats("affine: fixed");
548  return true;
549  }
550 
551  if (IsFixed(ref_y)) {
552  const int64 value_x = DomainOf(ref_y).Min() * coeff + offset;
553  static_cast<void>(IntersectDomainWith(ref_x, Domain(value_x)));
554  UpdateRuleStats("affine: fixed");
555  return true;
556  }
557 
558  // If both are already in the same class, we need to make sure the relations
559  // are compatible.
562  if (rx.representative == ry.representative) {
563  // x = rx.coeff * rep + rx.offset;
564  // y = ry.coeff * rep + ry.offset_y;
565  // And x == coeff * ry.coeff * rep + (coeff * ry.offset + offset).
566  //
567  // So we get the relation a * rep == b with a and b defined here:
568  const int64 a = coeff * ry.coeff - rx.coeff;
569  const int64 b = coeff * ry.offset + offset - rx.offset;
570  if (a == 0) {
571  if (b != 0) is_unsat = true;
572  return true;
573  }
574  if (b % a != 0) {
575  is_unsat = true;
576  return true;
577  }
578  UpdateRuleStats("affine: unique solution");
579  const int64 unique_value = -b / a;
580  if (!IntersectDomainWith(rx.representative, Domain(unique_value))) {
581  return true;
582  }
583  if (!IntersectDomainWith(ref_x,
584  Domain(unique_value * rx.coeff + rx.offset))) {
585  return true;
586  }
587  if (!IntersectDomainWith(ref_y,
588  Domain(unique_value * ry.coeff + ry.offset))) {
589  return true;
590  }
591  return true;
592  }
593 
594  const int x = PositiveRef(ref_x);
595  const int y = PositiveRef(ref_y);
596  const int64 c = RefIsPositive(ref_x) == RefIsPositive(ref_y) ? coeff : -coeff;
597  const int64 o = RefIsPositive(ref_x) ? offset : -offset;
598 
599  // TODO(user): can we force the rep and remove GetAffineRelation()?
600  bool added = AddRelation(x, y, c, o, &affine_relations_);
601  if ((c == 1 || c == -1) && o == 0) {
602  added |= AddRelation(x, y, c, o, &var_equiv_relations_);
603  }
604  if (added) {
605  UpdateRuleStats("affine: new relation");
606 
607  // Lets propagate again the new relation. We might as well do it as early
608  // as possible and not all call site do it.
609  if (!PropagateAffineRelation(ref_x)) return true;
610  if (!PropagateAffineRelation(ref_y)) return true;
611 
612  // These maps should only contains representative, so only need to remap
613  // either x or y.
614  const int rep = GetAffineRelation(x).representative;
615  if (x != rep) encoding_remap_queue_.push_back(x);
616  if (y != rep) encoding_remap_queue_.push_back(y);
617 
618  // The domain didn't change, but this notification allows to re-process any
619  // constraint containing these variables. Note that we do not need to
620  // retrigger a propagation of the constraint containing a variable whose
621  // representative didn't change.
622  if (x != rep) modified_domains.Set(x);
623  if (y != rep) modified_domains.Set(y);
624 
625  var_to_constraints_[x].insert(kAffineRelationConstraint);
626  var_to_constraints_[y].insert(kAffineRelationConstraint);
627  return true;
628  }
629 
630  UpdateRuleStats("affine: incompatible relation");
631  if (VLOG_IS_ON(1)) {
632  LOG(INFO) << "Cannot add relation " << DomainOf(ref_x) << " = " << coeff
633  << " * " << DomainOf(ref_y) << " + " << offset
634  << " because of incompatibilities with existing relation: ";
635  for (const int ref : {ref_x, ref_y}) {
636  const auto r = GetAffineRelation(ref);
637  LOG(INFO) << DomainOf(ref) << " = " << r.coeff << " * "
638  << DomainOf(r.representative) << " + " << r.offset;
639  }
640  }
641 
642  return false;
643 }
644 
646  if (is_unsat) return;
647 
648  CHECK(!VariableWasRemoved(ref_a));
649  CHECK(!VariableWasRemoved(ref_b));
650  CHECK(!DomainOf(ref_a).IsEmpty());
651  CHECK(!DomainOf(ref_b).IsEmpty());
652  CHECK(CanBeUsedAsLiteral(ref_a));
653  CHECK(CanBeUsedAsLiteral(ref_b));
654 
655  if (ref_a == ref_b) return;
656  if (ref_a == NegatedRef(ref_b)) {
657  is_unsat = true;
658  return;
659  }
660  const int var_a = PositiveRef(ref_a);
661  const int var_b = PositiveRef(ref_b);
662  if (RefIsPositive(ref_a) == RefIsPositive(ref_b)) {
663  // a = b
664  CHECK(StoreAffineRelation(var_a, var_b, /*coeff=*/1, /*offset=*/0));
665  } else {
666  // a = 1 - b
667  CHECK(StoreAffineRelation(var_a, var_b, /*coeff=*/-1, /*offset=*/1));
668  }
669 }
670 
671 bool PresolveContext::StoreAbsRelation(int target_ref, int ref) {
672  const auto insert_status = abs_relations_.insert(
673  std::make_pair(target_ref, SavedVariable(PositiveRef(ref))));
674  if (!insert_status.second) {
675  // Tricky: overwrite if the old value refer to a now unused variable.
676  const int candidate = insert_status.first->second.Get(this);
677  if (removed_variables_.contains(candidate)) {
678  insert_status.first->second = SavedVariable(PositiveRef(ref));
679  return true;
680  }
681  return false;
682  }
683  return true;
684 }
685 
686 bool PresolveContext::GetAbsRelation(int target_ref, int* ref) {
687  auto it = abs_relations_.find(target_ref);
688  if (it == abs_relations_.end()) return false;
689 
690  // Tricky: In some rare case the stored relation can refer to a deleted
691  // variable, so we need to ignore it.
692  //
693  // TODO(user): Incorporate this as part of SavedVariable/SavedLiteral so we
694  // make sure we never forget about this.
695  const int candidate = it->second.Get(this);
696  if (removed_variables_.contains(candidate)) {
697  abs_relations_.erase(it);
698  return false;
699  }
700  *ref = candidate;
701  return true;
702 }
703 
706 
709  // Note(user): This can happen is some corner cases where the affine
710  // relation where added before the variable became usable as Boolean. When
711  // this is the case, the domain will be of the form [x, x + 1] and should be
712  // later remapped to a Boolean variable.
713  return ref;
714  }
715 
716  // We made sure that the affine representative can always be used as a
717  // literal. However, if some variable are fixed, we might not have only
718  // (coeff=1 offset=0) or (coeff=-1 offset=1) and we might have something like
719  // (coeff=8 offset=0) which is only valid for both variable at zero...
720  //
721  // What is sure is that depending on the value, only one mapping can be valid
722  // because r.coeff can never be zero.
723  const bool positive_possible = (r.offset == 0 || r.coeff + r.offset == 1);
724  const bool negative_possible = (r.offset == 1 || r.coeff + r.offset == 0);
725  DCHECK_NE(positive_possible, negative_possible);
726  if (RefIsPositive(ref)) {
727  return positive_possible ? r.representative : NegatedRef(r.representative);
728  } else {
729  return positive_possible ? NegatedRef(r.representative) : r.representative;
730  }
731 }
732 
734  const AffineRelation::Relation r = var_equiv_relations_.Get(PositiveRef(ref));
735  CHECK_EQ(std::abs(r.coeff), 1);
736  CHECK_EQ(r.offset, 0);
737  return RefIsPositive(ref) == (r.coeff == 1) ? r.representative
739 }
740 
741 // This makes sure that the affine relation only uses one of the
742 // representative from the var_equiv_relations_.
744  AffineRelation::Relation r = affine_relations_.Get(PositiveRef(ref));
745  AffineRelation::Relation o = var_equiv_relations_.Get(r.representative);
747  if (o.coeff == -1) r.coeff = -r.coeff;
748  if (!RefIsPositive(ref)) {
749  r.coeff *= -1;
750  r.offset *= -1;
751  }
752  return r;
753 }
754 
755 std::string PresolveContext::RefDebugString(int ref) const {
756  return absl::StrCat(RefIsPositive(ref) ? "X" : "-X", PositiveRef(ref),
757  DomainOf(ref).ToString());
758 }
759 
760 std::string PresolveContext::AffineRelationDebugString(int ref) const {
762  return absl::StrCat(RefDebugString(ref), " = ", r.coeff, " * ",
763  RefDebugString(r.representative), " + ", r.offset);
764 }
765 
766 // Create the internal structure for any new variables in working_model.
768  for (int i = domains.size(); i < working_model->variables_size(); ++i) {
769  domains.emplace_back(ReadDomainFromProto(working_model->variables(i)));
770  if (domains.back().IsEmpty()) {
771  is_unsat = true;
772  return;
773  }
774  if (IsFixed(i)) ExploitFixedDomain(i);
775  }
776  modified_domains.Resize(domains.size());
777  var_to_constraints_.resize(domains.size());
778  var_to_num_linear1_.resize(domains.size());
779  var_to_ub_only_constraints.resize(domains.size());
780  var_to_lb_only_constraints.resize(domains.size());
781 }
782 
783 bool PresolveContext::RemapEncodingMaps() {
784  // TODO(user): for now, while the code works most of the time, it triggers
785  // weird side effect that causes some issues in some LNS presolve...
786  // We should continue the investigation before activating it.
787  //
788  // Note also that because all our encoding constraints are present in the
789  // model, they will be remapped, and the new mapping re-added again. So while
790  // the current code might not be efficient, it should eventually reach the
791  // same effect.
792  encoding_remap_queue_.clear();
793 
794  // Note that InsertVarValueEncodingInternal() will potentially add new entry
795  // to the encoding_ map, but for a different variables. So this code relies on
796  // the fact that the var_map shouldn't change content nor address of the
797  // "var_map" below while we iterate on them.
798  for (const int var : encoding_remap_queue_) {
801  if (r.representative == var) return true;
802  int num_remapping = 0;
803 
804  // Encoding.
805  {
806  const absl::flat_hash_map<int64, SavedLiteral>& var_map = encoding_[var];
807  for (const auto& entry : var_map) {
808  const int lit = entry.second.Get(this);
809  if (removed_variables_.contains(PositiveRef(lit))) continue;
810  if ((entry.first - r.offset) % r.coeff != 0) continue;
811  const int64 rep_value = (entry.first - r.offset) / r.coeff;
812  ++num_remapping;
813  InsertVarValueEncodingInternal(lit, r.representative, rep_value,
814  /*add_constraints=*/false);
815  if (is_unsat) return false;
816  }
817  encoding_.erase(var);
818  }
819 
820  // Eq half encoding.
821  {
822  const absl::flat_hash_map<int64, absl::flat_hash_set<int>>& var_map =
823  eq_half_encoding_[var];
824  for (const auto& entry : var_map) {
825  if ((entry.first - r.offset) % r.coeff != 0) continue;
826  const int64 rep_value = (entry.first - r.offset) / r.coeff;
827  for (int literal : entry.second) {
828  ++num_remapping;
829  InsertHalfVarValueEncoding(GetLiteralRepresentative(literal),
830  r.representative, rep_value,
831  /*imply_eq=*/true);
832  if (is_unsat) return false;
833  }
834  }
835  eq_half_encoding_.erase(var);
836  }
837 
838  // Neq half encoding.
839  {
840  const absl::flat_hash_map<int64, absl::flat_hash_set<int>>& var_map =
841  neq_half_encoding_[var];
842  for (const auto& entry : var_map) {
843  if ((entry.first - r.offset) % r.coeff != 0) continue;
844  const int64 rep_value = (entry.first - r.offset) / r.coeff;
845  for (int literal : entry.second) {
846  ++num_remapping;
847  InsertHalfVarValueEncoding(GetLiteralRepresentative(literal),
848  r.representative, rep_value,
849  /*imply_eq=*/false);
850  if (is_unsat) return false;
851  }
852  }
853  neq_half_encoding_.erase(var);
854  }
855 
856  if (num_remapping > 0) {
857  VLOG(1) << "Remapped " << num_remapping << " encodings due to " << var
858  << " -> " << r.representative << ".";
859  }
860  }
861  encoding_remap_queue_.clear();
862  return !is_unsat;
863 }
864 
867  CHECK_EQ(DomainOf(var).Size(), 2);
868  const int64 var_min = MinOf(var);
869  const int64 var_max = MaxOf(var);
870 
871  if (is_unsat) return;
872 
873  absl::flat_hash_map<int64, SavedLiteral>& var_map = encoding_[var];
874 
875  // Find encoding for min if present.
876  auto min_it = var_map.find(var_min);
877  if (min_it != var_map.end()) {
878  const int old_var = PositiveRef(min_it->second.Get(this));
879  if (removed_variables_.contains(old_var)) {
880  var_map.erase(min_it);
881  min_it = var_map.end();
882  }
883  }
884 
885  // Find encoding for max if present.
886  auto max_it = var_map.find(var_max);
887  if (max_it != var_map.end()) {
888  const int old_var = PositiveRef(max_it->second.Get(this));
889  if (removed_variables_.contains(old_var)) {
890  var_map.erase(max_it);
891  max_it = var_map.end();
892  }
893  }
894 
895  // Insert missing encoding.
896  int min_literal;
897  int max_literal;
898  if (min_it != var_map.end() && max_it != var_map.end()) {
899  min_literal = min_it->second.Get(this);
900  max_literal = max_it->second.Get(this);
901  if (min_literal != NegatedRef(max_literal)) {
902  UpdateRuleStats("variables with 2 values: merge encoding literals");
903  StoreBooleanEqualityRelation(min_literal, NegatedRef(max_literal));
904  if (is_unsat) return;
905  }
906  min_literal = GetLiteralRepresentative(min_literal);
907  max_literal = GetLiteralRepresentative(max_literal);
908  if (!IsFixed(min_literal)) CHECK_EQ(min_literal, NegatedRef(max_literal));
909  } else if (min_it != var_map.end() && max_it == var_map.end()) {
910  UpdateRuleStats("variables with 2 values: register other encoding");
911  min_literal = min_it->second.Get(this);
912  max_literal = NegatedRef(min_literal);
913  var_map[var_max] = SavedLiteral(max_literal);
914  } else if (min_it == var_map.end() && max_it != var_map.end()) {
915  UpdateRuleStats("variables with 2 values: register other encoding");
916  max_literal = max_it->second.Get(this);
917  min_literal = NegatedRef(max_literal);
918  var_map[var_min] = SavedLiteral(min_literal);
919  } else {
920  UpdateRuleStats("variables with 2 values: create encoding literal");
921  max_literal = NewBoolVar();
922  min_literal = NegatedRef(max_literal);
923  var_map[var_min] = SavedLiteral(min_literal);
924  var_map[var_max] = SavedLiteral(max_literal);
925  }
926 
927  if (IsFixed(min_literal) || IsFixed(max_literal)) {
928  CHECK(IsFixed(min_literal));
929  CHECK(IsFixed(max_literal));
930  UpdateRuleStats("variables with 2 values: fixed encoding");
931  if (LiteralIsTrue(min_literal)) {
932  return static_cast<void>(IntersectDomainWith(var, Domain(var_min)));
933  } else {
934  return static_cast<void>(IntersectDomainWith(var, Domain(var_max)));
935  }
936  }
937 
938  // Add affine relation.
939  if (GetAffineRelation(var).representative != PositiveRef(min_literal)) {
940  UpdateRuleStats("variables with 2 values: new affine relation");
941  if (RefIsPositive(max_literal)) {
943  var_max - var_min, var_min));
944  } else {
946  var_min - var_max, var_max));
947  }
948  }
949 }
950 
951 void PresolveContext::InsertVarValueEncodingInternal(int literal, int var,
952  int64 value,
953  bool add_constraints) {
956  absl::flat_hash_map<int64, SavedLiteral>& var_map = encoding_[var];
957 
958  // Ticky and rare: I have only observed this on the LNS of
959  // radiation_m18_12_05_sat.fzn. The value was encoded, but maybe we never
960  // used the involved variables / constraints, so it was removed (with the
961  // encoding constraints) from the model already! We have to be careful.
962  const auto it = var_map.find(value);
963  if (it != var_map.end()) {
964  const int old_var = PositiveRef(it->second.Get(this));
965  if (removed_variables_.contains(old_var)) {
966  var_map.erase(it);
967  }
968  }
969 
970  const auto insert =
971  var_map.insert(std::make_pair(value, SavedLiteral(literal)));
972 
973  // If an encoding already exist, make the two Boolean equals.
974  if (!insert.second) {
975  const int previous_literal = insert.first->second.Get(this);
976  CHECK(!VariableWasRemoved(previous_literal));
977  if (literal != previous_literal) {
979  "variables: merge equivalent var value encoding literals");
980  StoreBooleanEqualityRelation(literal, previous_literal);
981  }
982  return;
983  }
984 
985  if (DomainOf(var).Size() == 2) {
987  } else {
988  VLOG(2) << "Insert lit(" << literal << ") <=> var(" << var
989  << ") == " << value;
990  eq_half_encoding_[var][value].insert(literal);
991  neq_half_encoding_[var][value].insert(NegatedRef(literal));
992  if (add_constraints) {
993  UpdateRuleStats("variables: add encoding constraint");
994  AddImplyInDomain(literal, var, Domain(value));
995  AddImplyInDomain(NegatedRef(literal), var, Domain(value).Complement());
996  }
997  }
998 }
999 
1000 bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var,
1001  int64 value, bool imply_eq) {
1002  if (is_unsat) return false;
1004 
1005  // Creates the linking sets on demand.
1006  // Insert the enforcement literal in the half encoding map.
1007  auto& direct_set =
1008  imply_eq ? eq_half_encoding_[var][value] : neq_half_encoding_[var][value];
1009  if (!direct_set.insert(literal).second) return false; // Already there.
1010 
1011  VLOG(2) << "Collect lit(" << literal << ") implies var(" << var
1012  << (imply_eq ? ") == " : ") != ") << value;
1013  UpdateRuleStats("variables: detect half reified value encoding");
1014 
1015  // Note(user): We don't expect a lot of literals in these sets, so doing
1016  // a scan should be okay.
1017  auto& other_set =
1018  imply_eq ? neq_half_encoding_[var][value] : eq_half_encoding_[var][value];
1019  for (const int other : other_set) {
1020  if (GetLiteralRepresentative(other) != NegatedRef(literal)) continue;
1021 
1022  UpdateRuleStats("variables: detect fully reified value encoding");
1023  const int imply_eq_literal = imply_eq ? literal : NegatedRef(literal);
1024  InsertVarValueEncodingInternal(imply_eq_literal, var, value,
1025  /*add_constraints=*/false);
1026  break;
1027  }
1028 
1029  return true;
1030 }
1031 
1032 bool PresolveContext::CanonicalizeEncoding(int* ref, int64* value) {
1033  const AffineRelation::Relation r = GetAffineRelation(*ref);
1034  if ((*value - r.offset) % r.coeff != 0) return false;
1035  *ref = r.representative;
1036  *value = (*value - r.offset) / r.coeff;
1037  return true;
1038 }
1039 
1041  int64 value) {
1042  if (!RemapEncodingMaps()) return;
1043  if (!CanonicalizeEncoding(&ref, &value)) return;
1045  InsertVarValueEncodingInternal(literal, ref, value, /*add_constraints=*/true);
1046 }
1047 
1049  int64 value) {
1050  if (!RemapEncodingMaps()) return false;
1051  if (!CanonicalizeEncoding(&var, &value)) return false;
1053  return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/true);
1054 }
1055 
1057  int64 value) {
1058  if (!RemapEncodingMaps()) return false;
1059  if (!CanonicalizeEncoding(&var, &value)) return false;
1061  return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/false);
1062 }
1063 
1065  if (!RemapEncodingMaps()) return false;
1066  if (!CanonicalizeEncoding(&ref, &value)) return false;
1067  const absl::flat_hash_map<int64, SavedLiteral>& var_map = encoding_[ref];
1068  const auto it = var_map.find(value);
1069  if (it != var_map.end()) {
1070  if (literal != nullptr) {
1071  *literal = it->second.Get(this);
1072  }
1073  return true;
1074  }
1075  return false;
1076 }
1077 
1079  if (!RemapEncodingMaps()) return GetOrCreateConstantVar(0);
1080  if (!CanonicalizeEncoding(&ref, &value)) return GetOrCreateConstantVar(0);
1081 
1082  // Positive after CanonicalizeEncoding().
1083  const int var = ref;
1084 
1085  // Returns the false literal if the value is not in the domain.
1086  if (!domains[var].Contains(value)) {
1087  return GetOrCreateConstantVar(0);
1088  }
1089 
1090  // Returns the associated literal if already present.
1091  absl::flat_hash_map<int64, SavedLiteral>& var_map = encoding_[var];
1092  auto it = var_map.find(value);
1093  if (it != var_map.end()) {
1094  return it->second.Get(this);
1095  }
1096 
1097  // Special case for fixed domains.
1098  if (domains[var].Size() == 1) {
1099  const int true_literal = GetOrCreateConstantVar(1);
1100  var_map[value] = SavedLiteral(true_literal);
1101  return true_literal;
1102  }
1103 
1104  // Special case for domains of size 2.
1105  const int64 var_min = MinOf(var);
1106  const int64 var_max = MaxOf(var);
1107  if (domains[var].Size() == 2) {
1108  // Checks if the other value is already encoded.
1109  const int64 other_value = value == var_min ? var_max : var_min;
1110  auto other_it = var_map.find(other_value);
1111  if (other_it != var_map.end()) {
1112  // Update the encoding map. The domain could have been reduced to size
1113  // two after the creation of the first literal.
1114  const int literal = NegatedRef(other_it->second.Get(this));
1115  var_map[value] = SavedLiteral(literal);
1116  return literal;
1117  }
1118 
1119  if (var_min == 0 && var_max == 1) {
1121  var_map[1] = SavedLiteral(representative);
1122  var_map[0] = SavedLiteral(NegatedRef(representative));
1123  return value == 1 ? representative : NegatedRef(representative);
1124  } else {
1125  const int literal = NewBoolVar();
1126  InsertVarValueEncoding(literal, var, var_max);
1128  return value == var_max ? representative : NegatedRef(representative);
1129  }
1130  }
1131 
1132  const int literal = NewBoolVar();
1135 }
1136 
1138  const CpObjectiveProto& obj = working_model->objective();
1139 
1140  objective_offset_ = obj.offset();
1141  objective_scaling_factor_ = obj.scaling_factor();
1142  if (objective_scaling_factor_ == 0.0) {
1143  objective_scaling_factor_ = 1.0;
1144  }
1145  if (!obj.domain().empty()) {
1146  // We might relax this in CanonicalizeObjective() when we will compute
1147  // the possible objective domain from the domains of the variables.
1148  objective_domain_is_constraining_ = true;
1149  objective_domain_ = ReadDomainFromProto(obj);
1150  } else {
1151  objective_domain_is_constraining_ = false;
1152  objective_domain_ = Domain::AllValues();
1153  }
1154 
1155  // This is an upper bound of the higher magnitude that can be reach by
1156  // summing an objective partial sum. Because of the model validation, this
1157  // shouldn't overflow, and we make sure it stays this way.
1158  objective_overflow_detection_ = 0;
1159 
1160  objective_map_.clear();
1161  for (int i = 0; i < obj.vars_size(); ++i) {
1162  const int ref = obj.vars(i);
1163  int64 coeff = obj.coeffs(i);
1164  if (!RefIsPositive(ref)) coeff = -coeff;
1165  int var = PositiveRef(ref);
1166 
1167  objective_overflow_detection_ +=
1168  std::abs(coeff) * std::max(std::abs(MinOf(var)), std::abs(MaxOf(var)));
1169 
1170  objective_map_[var] += coeff;
1171  if (objective_map_[var] == 0) {
1172  objective_map_.erase(var);
1173  var_to_constraints_[var].erase(kObjectiveConstraint);
1174  } else {
1175  var_to_constraints_[var].insert(kObjectiveConstraint);
1176  }
1177  }
1178 }
1179 
1181  int64 offset_change = 0;
1182 
1183  // We replace each entry by its affine representative.
1184  // Note that the non-deterministic loop is fine, but because we iterate
1185  // one the map while modifying it, it is safer to do a copy rather than to
1186  // try to handle that in one pass.
1187  tmp_entries_.clear();
1188  for (const auto& entry : objective_map_) {
1189  tmp_entries_.push_back(entry);
1190  }
1191 
1192  // TODO(user): This is a bit duplicated with the presolve linear code.
1193  // We also do not propagate back any domain restriction from the objective to
1194  // the variables if any.
1195  for (const auto& entry : tmp_entries_) {
1196  const int var = entry.first;
1197  const auto it = objective_map_.find(var);
1198  if (it == objective_map_.end()) continue;
1199  const int64 coeff = it->second;
1200 
1201  // If a variable only appear in objective, we can fix it!
1202  // Note that we don't care if it was in affine relation, because if none
1203  // of the relations are left, then we can still fix it.
1204  if (!keep_all_feasible_solutions && !objective_domain_is_constraining_ &&
1206  var_to_constraints_[var].size() == 1 &&
1207  var_to_constraints_[var].contains(kObjectiveConstraint)) {
1208  UpdateRuleStats("objective: variable not used elsewhere");
1209  if (coeff > 0) {
1210  if (!IntersectDomainWith(var, Domain(MinOf(var)))) {
1211  return false;
1212  }
1213  } else {
1214  if (!IntersectDomainWith(var, Domain(MaxOf(var)))) {
1215  return false;
1216  }
1217  }
1218  }
1219 
1220  if (IsFixed(var)) {
1221  offset_change += coeff * MinOf(var);
1222  var_to_constraints_[var].erase(kObjectiveConstraint);
1223  objective_map_.erase(var);
1224  continue;
1225  }
1226 
1228  if (r.representative == var) continue;
1229 
1230  objective_map_.erase(var);
1231  var_to_constraints_[var].erase(kObjectiveConstraint);
1232 
1233  // Do the substitution.
1234  offset_change += coeff * r.offset;
1235  const int64 new_coeff = objective_map_[r.representative] += coeff * r.coeff;
1236 
1237  // Process new term.
1238  if (new_coeff == 0) {
1239  objective_map_.erase(r.representative);
1240  var_to_constraints_[r.representative].erase(kObjectiveConstraint);
1241  } else {
1242  var_to_constraints_[r.representative].insert(kObjectiveConstraint);
1243  if (IsFixed(r.representative)) {
1244  offset_change += new_coeff * MinOf(r.representative);
1245  var_to_constraints_[r.representative].erase(kObjectiveConstraint);
1246  objective_map_.erase(r.representative);
1247  }
1248  }
1249  }
1250 
1251  Domain implied_domain(0);
1252  int64 gcd(0);
1253 
1254  // We need to sort the entries to be deterministic.
1255  tmp_entries_.clear();
1256  for (const auto& entry : objective_map_) {
1257  tmp_entries_.push_back(entry);
1258  }
1259  std::sort(tmp_entries_.begin(), tmp_entries_.end());
1260  for (const auto& entry : tmp_entries_) {
1261  const int var = entry.first;
1262  const int64 coeff = entry.second;
1263  gcd = MathUtil::GCD64(gcd, std::abs(coeff));
1264  implied_domain =
1265  implied_domain.AdditionWith(DomainOf(var).MultiplicationBy(coeff))
1266  .RelaxIfTooComplex();
1267  }
1268 
1269  // This is the new domain.
1270  // Note that the domain never include the offset.
1271  objective_domain_ = objective_domain_.AdditionWith(Domain(-offset_change))
1272  .IntersectionWith(implied_domain);
1273  objective_domain_ =
1274  objective_domain_.SimplifyUsingImpliedDomain(implied_domain);
1275 
1276  // Updat the offset.
1277  objective_offset_ += offset_change;
1278 
1279  // Maybe divide by GCD.
1280  if (gcd > 1) {
1281  for (auto& entry : objective_map_) {
1282  entry.second /= gcd;
1283  }
1284  objective_domain_ = objective_domain_.InverseMultiplicationBy(gcd);
1285  objective_offset_ /= static_cast<double>(gcd);
1286  objective_scaling_factor_ *= static_cast<double>(gcd);
1287  }
1288 
1289  if (objective_domain_.IsEmpty()) return false;
1290 
1291  // Detect if the objective domain do not limit the "optimal" objective value.
1292  // If this is true, then we can apply any reduction that reduce the objective
1293  // value without any issues.
1294  objective_domain_is_constraining_ =
1295  !implied_domain
1296  .IntersectionWith(Domain(kint64min, objective_domain_.Max()))
1297  .IsIncludedIn(objective_domain_);
1298  return true;
1299 }
1300 
1302  int var_in_equality, int64 coeff_in_equality,
1303  const ConstraintProto& equality, std::vector<int>* new_vars_in_objective) {
1304  CHECK(equality.enforcement_literal().empty());
1305  CHECK(RefIsPositive(var_in_equality));
1306 
1307  if (new_vars_in_objective != nullptr) new_vars_in_objective->clear();
1308 
1309  // We can only "easily" substitute if the objective coefficient is a multiple
1310  // of the one in the constraint.
1311  const int64 coeff_in_objective =
1312  gtl::FindOrDie(objective_map_, var_in_equality);
1313  CHECK_NE(coeff_in_equality, 0);
1314  CHECK_EQ(coeff_in_objective % coeff_in_equality, 0);
1315  const int64 multiplier = coeff_in_objective / coeff_in_equality;
1316 
1317  // Abort if the new objective seems to violate our overflow preconditions.
1318  int64 change = 0;
1319  for (int i = 0; i < equality.linear().vars().size(); ++i) {
1320  int var = equality.linear().vars(i);
1321  if (PositiveRef(var) == var_in_equality) continue;
1322  int64 coeff = equality.linear().coeffs(i);
1323  change +=
1324  std::abs(coeff) * std::max(std::abs(MinOf(var)), std::abs(MaxOf(var)));
1325  }
1326  const int64 new_value =
1327  CapAdd(CapProd(std::abs(multiplier), change),
1328  objective_overflow_detection_ -
1329  std::abs(coeff_in_equality) *
1330  std::max(std::abs(MinOf(var_in_equality)),
1331  std::abs(MaxOf(var_in_equality))));
1332  if (new_value == kint64max) return false;
1333  objective_overflow_detection_ = new_value;
1334 
1335  for (int i = 0; i < equality.linear().vars().size(); ++i) {
1336  int var = equality.linear().vars(i);
1337  int64 coeff = equality.linear().coeffs(i);
1338  if (!RefIsPositive(var)) {
1339  var = NegatedRef(var);
1340  coeff = -coeff;
1341  }
1342  if (var == var_in_equality) continue;
1343 
1344  int64& map_ref = objective_map_[var];
1345  if (map_ref == 0 && new_vars_in_objective != nullptr) {
1346  new_vars_in_objective->push_back(var);
1347  }
1348  map_ref -= coeff * multiplier;
1349 
1350  if (map_ref == 0) {
1351  objective_map_.erase(var);
1352  var_to_constraints_[var].erase(kObjectiveConstraint);
1353  } else {
1354  var_to_constraints_[var].insert(kObjectiveConstraint);
1355  }
1356  }
1357 
1358  objective_map_.erase(var_in_equality);
1359  var_to_constraints_[var_in_equality].erase(kObjectiveConstraint);
1360 
1361  // Deal with the offset.
1362  Domain offset = ReadDomainFromProto(equality.linear());
1363  DCHECK_EQ(offset.Min(), offset.Max());
1364  bool exact = true;
1365  offset = offset.MultiplicationBy(multiplier, &exact);
1366  CHECK(exact);
1367  CHECK(!offset.IsEmpty());
1368 
1369  // Tricky: The objective domain is without the offset, so we need to shift it.
1370  objective_offset_ += static_cast<double>(offset.Min());
1371  objective_domain_ = objective_domain_.AdditionWith(Domain(-offset.Min()));
1372 
1373  // Because we can assume that the constraint we used was constraining
1374  // (otherwise it would have been removed), the objective domain should be now
1375  // constraining.
1376  objective_domain_is_constraining_ = true;
1377 
1378  if (objective_domain_.IsEmpty()) {
1379  return NotifyThatModelIsUnsat();
1380  }
1381  return true;
1382 }
1383 
1385  // We need to sort the entries to be deterministic.
1386  std::vector<std::pair<int, int64>> entries;
1387  for (const auto& entry : objective_map_) {
1388  entries.push_back(entry);
1389  }
1390  std::sort(entries.begin(), entries.end());
1391 
1392  CpObjectiveProto* mutable_obj = working_model->mutable_objective();
1393  mutable_obj->set_offset(objective_offset_);
1394  mutable_obj->set_scaling_factor(objective_scaling_factor_);
1395  FillDomainInProto(objective_domain_, mutable_obj);
1396  mutable_obj->clear_vars();
1397  mutable_obj->clear_coeffs();
1398  for (const auto& entry : entries) {
1399  mutable_obj->add_vars(entry.first);
1400  mutable_obj->add_coeffs(entry.second);
1401  }
1402 }
1403 
1405  int active_i,
1406  int active_j) {
1407  // Sort the active literals.
1408  if (active_j < active_i) std::swap(active_i, active_j);
1409 
1410  const std::tuple<int, int, int, int> key =
1411  std::make_tuple(time_i, time_j, active_i, active_j);
1412  const auto& it = reified_precedences_cache_.find(key);
1413  if (it != reified_precedences_cache_.end()) return it->second;
1414 
1415  const int result = NewBoolVar();
1416  reified_precedences_cache_[key] = result;
1417 
1418  // result => (time_i <= time_j) && active_i && active_j.
1419  ConstraintProto* const lesseq = working_model->add_constraints();
1420  lesseq->add_enforcement_literal(result);
1421  lesseq->mutable_linear()->add_vars(time_i);
1422  lesseq->mutable_linear()->add_vars(time_j);
1423  lesseq->mutable_linear()->add_coeffs(-1);
1424  lesseq->mutable_linear()->add_coeffs(1);
1425  lesseq->mutable_linear()->add_domain(0);
1426  lesseq->mutable_linear()->add_domain(kint64max);
1427  if (!LiteralIsTrue(active_i)) {
1428  AddImplication(result, active_i);
1429  }
1430  if (!LiteralIsTrue(active_j)) {
1431  AddImplication(result, active_j);
1432  }
1433 
1434  // Not(result) && active_i && active_j => (time_i > time_j)
1435  ConstraintProto* const greater = working_model->add_constraints();
1436  greater->mutable_linear()->add_vars(time_i);
1437  greater->mutable_linear()->add_vars(time_j);
1438  greater->mutable_linear()->add_coeffs(-1);
1439  greater->mutable_linear()->add_coeffs(1);
1440  greater->mutable_linear()->add_domain(kint64min);
1441  greater->mutable_linear()->add_domain(-1);
1442 
1443  // Manages enforcement literal.
1444  greater->add_enforcement_literal(NegatedRef(result));
1445  greater->add_enforcement_literal(active_i);
1446  greater->add_enforcement_literal(active_j);
1447 
1448  // This is redundant but should improves performance.
1449  //
1450  // If GetOrCreateReifiedPrecedenceLiteral(time_j, time_i, active_j, active_j)
1451  // (the reverse precedence) has been called too, then we can link the two
1452  // precedence literals, and the two active literals together.
1453  const auto& rev_it = reified_precedences_cache_.find(
1454  std::make_tuple(time_j, time_i, active_i, active_j));
1455  if (rev_it != reified_precedences_cache_.end()) {
1456  auto* const bool_or = working_model->add_constraints()->mutable_bool_or();
1457  bool_or->add_literals(result);
1458  bool_or->add_literals(rev_it->second);
1459  bool_or->add_literals(NegatedRef(active_i));
1460  bool_or->add_literals(NegatedRef(active_j));
1461  }
1462 
1463  return result;
1464 }
1465 
1467  reified_precedences_cache_.clear();
1468 }
1469 
1470 } // namespace sat
1471 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
#define VLOG(verboselevel)
Definition: base/logging.h:978
bool TryAdd(int x, int y, int64 coeff, int64 offset)
We call domain any subset of Int64 = [kint64min, kint64max].
static Domain AllValues()
Returns the full domain Int64.
Domain Negation() const
Returns {x ∈ Int64, ∃ e ∈ D, x = -e}.
bool IsIncludedIn(const Domain &domain) const
Returns true iff D is included in the given domain.
Domain MultiplicationBy(int64 coeff, bool *exact=nullptr) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e * coeff}.
Domain InverseMultiplicationBy(const int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
Domain AdditionWith(const Domain &domain) const
Returns {x ∈ Int64, ∃ a ∈ D, ∃ b ∈ domain, x = a + b}.
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
bool IsEmpty() const
Returns true if this is the empty set.
Domain RelaxIfTooComplex() const
If NumIntervals() is too large, this return a superset of the domain.
Domain SimplifyUsingImpliedDomain(const Domain &implied_domain) const
Advanced usage.
static int64 GCD64(int64 x, int64 y)
Definition: mathutil.h:107
void Set(IntegerType index)
Definition: bitset.h:803
void Resize(IntegerType size)
Definition: bitset.h:789
bool StoreAbsRelation(int target_ref, int ref)
ABSL_MUST_USE_RESULT bool IntersectDomainWith(int ref, const Domain &domain, bool *domain_modified=nullptr)
void InsertVarValueEncoding(int literal, int ref, int64 value)
std::vector< absl::flat_hash_set< int > > var_to_lb_only_constraints
int GetOrCreateVarValueEncoding(int ref, int64 value)
bool DomainContains(int ref, int64 value) const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value)
bool VariableWithCostIsUniqueAndRemovable(int ref) const
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value)
std::vector< absl::flat_hash_set< int > > var_to_ub_only_constraints
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(const std::string &message="")
bool HasVarValueEncoding(int ref, int64 value, int *literal=nullptr)
std::string AffineRelationDebugString(int ref) const
absl::flat_hash_map< std::string, int > stats_by_rule_name
void StoreBooleanEqualityRelation(int ref_a, int ref_b)
bool SubstituteVariableInObjective(int var_in_equality, int64 coeff_in_equality, const ConstraintProto &equality, std::vector< int > *new_vars_in_objective=nullptr)
void UpdateRuleStats(const std::string &name, int num_times=1)
ABSL_MUST_USE_RESULT bool CanonicalizeObjective()
AffineRelation::Relation GetAffineRelation(int ref) const
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
int GetOrCreateReifiedPrecedenceLiteral(int time_i, int time_j, int active_i, int active_j)
void AddImplyInDomain(int b, int x, const Domain &domain)
bool GetAbsRelation(int target_ref, int *ref)
bool StoreAffineRelation(int ref_x, int ref_y, int64 coeff, int64 offset)
int Get(PresolveContext *context) const
int Get(PresolveContext *context) const
const std::string name
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GurobiMPCallbackContext * context
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int INFO
Definition: log_severity.h:31
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
std::vector< int > UsedVariables(const ConstraintProto &ct)
bool RefIsPositive(int ref)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
constexpr int kAffineRelationConstraint
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
constexpr int kObjectiveConstraint
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
const absl::string_view ToString(MPSolver::OptimizationProblemType optimization_problem_type)
int64 CapAdd(int64 x, int64 y)
int64 CapProd(int64 x, int64 y)
std::string ProtobufDebugString(const P &message)
Literal literal
Definition: optimization.cc:84
ColIndex representative
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41