OR-Tools  8.2
linear_relaxation.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 <vector>
17 
18 #include "absl/container/flat_hash_set.h"
20 #include "ortools/base/stl_util.h"
21 #include "ortools/sat/cp_model.pb.h"
23 #include "ortools/sat/integer.h"
27 #include "ortools/sat/sat_base.h"
29 
30 namespace operations_research {
31 namespace sat {
32 
33 bool AppendFullEncodingRelaxation(IntegerVariable var, const Model& model,
34  LinearRelaxation* relaxation) {
35  const auto* encoder = model.Get<IntegerEncoder>();
36  if (encoder == nullptr) return false;
37  if (!encoder->VariableIsFullyEncoded(var)) return false;
38 
39  const auto& encoding = encoder->FullDomainEncoding(var);
40  const IntegerValue var_min = model.Get<IntegerTrail>()->LowerBound(var);
41 
42  LinearConstraintBuilder at_least_one(&model, IntegerValue(1),
44  LinearConstraintBuilder encoding_ct(&model, var_min, var_min);
45  encoding_ct.AddTerm(var, IntegerValue(1));
46 
47  // Create the constraint if all literal have a view.
48  std::vector<Literal> at_most_one;
49 
50  for (const auto value_literal : encoding) {
51  const Literal lit = value_literal.literal;
52  const IntegerValue delta = value_literal.value - var_min;
53  DCHECK_GE(delta, IntegerValue(0));
54  at_most_one.push_back(lit);
55  if (!at_least_one.AddLiteralTerm(lit, IntegerValue(1))) return false;
56  if (delta != IntegerValue(0)) {
57  if (!encoding_ct.AddLiteralTerm(lit, -delta)) return false;
58  }
59  }
60 
61  relaxation->linear_constraints.push_back(at_least_one.Build());
62  relaxation->linear_constraints.push_back(encoding_ct.Build());
63  relaxation->at_most_ones.push_back(at_most_one);
64  return true;
65 }
66 
67 namespace {
68 
69 // TODO(user): Not super efficient.
70 std::pair<IntegerValue, IntegerValue> GetMinAndMaxNotEncoded(
71  IntegerVariable var,
72  const absl::flat_hash_set<IntegerValue>& encoded_values,
73  const Model& model) {
74  const auto* domains = model.Get<IntegerDomains>();
75  if (domains == nullptr || var >= domains->size()) {
77  }
78 
79  // The domain can be large, but the list of values shouldn't, so this
80  // runs in O(encoded_values.size());
81  IntegerValue min = kMaxIntegerValue;
82  for (const ClosedInterval interval : (*domains)[var]) {
83  for (IntegerValue v(interval.start); v <= interval.end; ++v) {
84  if (!gtl::ContainsKey(encoded_values, v)) {
85  min = v;
86  break;
87  }
88  }
89  if (min != kMaxIntegerValue) break;
90  }
91 
92  IntegerValue max = kMinIntegerValue;
93  const auto& domain = (*domains)[var];
94  for (int i = domain.NumIntervals() - 1; i >= 0; --i) {
95  const ClosedInterval interval = domain[i];
96  for (IntegerValue v(interval.end); v >= interval.start; --v) {
97  if (!gtl::ContainsKey(encoded_values, v)) {
98  max = v;
99  break;
100  }
101  }
102  if (max != kMinIntegerValue) break;
103  }
104 
105  return {min, max};
106 }
107 
108 } // namespace
109 
110 void AppendPartialEncodingRelaxation(IntegerVariable var, const Model& model,
111  LinearRelaxation* relaxation) {
112  const auto* encoder = model.Get<IntegerEncoder>();
113  const auto* integer_trail = model.Get<IntegerTrail>();
114  if (encoder == nullptr || integer_trail == nullptr) return;
115 
116  const std::vector<IntegerEncoder::ValueLiteralPair>& encoding =
117  encoder->PartialDomainEncoding(var);
118  if (encoding.empty()) return;
119 
120  std::vector<Literal> at_most_one_ct;
121  absl::flat_hash_set<IntegerValue> encoded_values;
122  for (const auto value_literal : encoding) {
123  const Literal literal = value_literal.literal;
124 
125  // Note that we skip pairs that do not have an Integer view.
126  if (encoder->GetLiteralView(literal) == kNoIntegerVariable &&
127  encoder->GetLiteralView(literal.Negated()) == kNoIntegerVariable) {
128  continue;
129  }
130 
131  at_most_one_ct.push_back(literal);
132  encoded_values.insert(value_literal.value);
133  }
134  if (encoded_values.empty()) return;
135 
136  // TODO(user): The PartialDomainEncoding() function automatically exclude
137  // values that are no longer in the initial domain, so we could be a bit
138  // tighter here. That said, this is supposed to be called just after the
139  // presolve, so it shouldn't really matter.
140  const auto pair = GetMinAndMaxNotEncoded(var, encoded_values, model);
141  if (pair.first == kMaxIntegerValue) {
142  // TODO(user): try to remove the duplication with
143  // AppendFullEncodingRelaxation()? actually I am not sure we need the other
144  // function since this one is just more general.
145  LinearConstraintBuilder exactly_one_ct(&model, IntegerValue(1),
146  IntegerValue(1));
147  LinearConstraintBuilder encoding_ct(&model, IntegerValue(0),
148  IntegerValue(0));
149  encoding_ct.AddTerm(var, IntegerValue(1));
150  for (const auto value_literal : encoding) {
151  const Literal lit = value_literal.literal;
152  CHECK(exactly_one_ct.AddLiteralTerm(lit, IntegerValue(1)));
153  CHECK(
154  encoding_ct.AddLiteralTerm(lit, IntegerValue(-value_literal.value)));
155  }
156  relaxation->linear_constraints.push_back(exactly_one_ct.Build());
157  relaxation->linear_constraints.push_back(encoding_ct.Build());
158  return;
159  }
160 
161  // min + sum li * (xi - min) <= var.
162  const IntegerValue d_min = pair.first;
163  LinearConstraintBuilder lower_bound_ct(&model, d_min, kMaxIntegerValue);
164  lower_bound_ct.AddTerm(var, IntegerValue(1));
165  for (const auto value_literal : encoding) {
166  CHECK(lower_bound_ct.AddLiteralTerm(value_literal.literal,
167  d_min - value_literal.value));
168  }
169 
170  // var <= max + sum li * (xi - max).
171  const IntegerValue d_max = pair.second;
172  LinearConstraintBuilder upper_bound_ct(&model, kMinIntegerValue, d_max);
173  upper_bound_ct.AddTerm(var, IntegerValue(1));
174  for (const auto value_literal : encoding) {
175  CHECK(upper_bound_ct.AddLiteralTerm(value_literal.literal,
176  d_max - value_literal.value));
177  }
178 
179  // Note that empty/trivial constraints will be filtered later.
180  relaxation->at_most_ones.push_back(at_most_one_ct);
181  relaxation->linear_constraints.push_back(lower_bound_ct.Build());
182  relaxation->linear_constraints.push_back(upper_bound_ct.Build());
183 }
184 
186  const Model& model,
187  LinearRelaxation* relaxation) {
188  const auto* integer_trail = model.Get<IntegerTrail>();
189  const auto* encoder = model.Get<IntegerEncoder>();
190  if (integer_trail == nullptr || encoder == nullptr) return;
191 
192  const std::map<IntegerValue, Literal>& greater_than_encoding =
193  encoder->PartialGreaterThanEncoding(var);
194  if (greater_than_encoding.empty()) return;
195 
196  // Start by the var >= side.
197  // And also add the implications between used literals.
198  {
199  IntegerValue prev_used_bound = integer_trail->LowerBound(var);
200  LinearConstraintBuilder lb_constraint(&model, prev_used_bound,
202  lb_constraint.AddTerm(var, IntegerValue(1));
203  LiteralIndex prev_literal_index = kNoLiteralIndex;
204  for (const auto entry : greater_than_encoding) {
205  if (entry.first <= prev_used_bound) continue;
206 
207  const LiteralIndex literal_index = entry.second.Index();
208  const IntegerValue diff = prev_used_bound - entry.first;
209 
210  // Skip the entry if the literal doesn't have a view.
211  if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue;
212  if (prev_literal_index != kNoLiteralIndex) {
213  // Add var <= prev_var, which is the same as var + not(prev_var) <= 1
214  relaxation->at_most_ones.push_back(
215  {Literal(literal_index), Literal(prev_literal_index).Negated()});
216  }
217  prev_used_bound = entry.first;
218  prev_literal_index = literal_index;
219  }
220  relaxation->linear_constraints.push_back(lb_constraint.Build());
221  }
222 
223  // Do the same for the var <= side by using NegationOfVar().
224  // Note that we do not need to add the implications between literals again.
225  {
226  IntegerValue prev_used_bound = integer_trail->LowerBound(NegationOf(var));
227  LinearConstraintBuilder lb_constraint(&model, prev_used_bound,
229  lb_constraint.AddTerm(var, IntegerValue(-1));
230  for (const auto entry :
231  encoder->PartialGreaterThanEncoding(NegationOf(var))) {
232  if (entry.first <= prev_used_bound) continue;
233  const IntegerValue diff = prev_used_bound - entry.first;
234 
235  // Skip the entry if the literal doesn't have a view.
236  if (!lb_constraint.AddLiteralTerm(entry.second, diff)) continue;
237  prev_used_bound = entry.first;
238  }
239  relaxation->linear_constraints.push_back(lb_constraint.Build());
240  }
241 }
242 
243 namespace {
244 // Adds enforcing_lit => target <= bounding_var to relaxation.
245 void AppendEnforcedUpperBound(const Literal enforcing_lit,
246  const IntegerVariable target,
247  const IntegerVariable bounding_var, Model* model,
248  LinearRelaxation* relaxation) {
249  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
250  const IntegerValue max_target_value = integer_trail->UpperBound(target);
251  const IntegerValue min_var_value = integer_trail->LowerBound(bounding_var);
252  const IntegerValue max_term_value = max_target_value - min_var_value;
253  LinearConstraintBuilder lc(model, kMinIntegerValue, max_term_value);
254  lc.AddTerm(target, IntegerValue(1));
255  lc.AddTerm(bounding_var, IntegerValue(-1));
256  CHECK(lc.AddLiteralTerm(enforcing_lit, max_term_value));
257  relaxation->linear_constraints.push_back(lc.Build());
258 }
259 
260 // Adds {enforcing_lits} => rhs_domain_min <= expr <= rhs_domain_max.
261 // Requires expr offset to be 0.
262 void AppendEnforcedLinearExpression(
263  const std::vector<Literal>& enforcing_literals,
264  const LinearExpression& expr, const IntegerValue rhs_domain_min,
265  const IntegerValue rhs_domain_max, const Model& model,
266  LinearRelaxation* relaxation) {
267  CHECK_EQ(expr.offset, IntegerValue(0));
268  const LinearExpression canonical_expr = CanonicalizeExpr(expr);
269  const IntegerTrail* integer_trail = model.Get<IntegerTrail>();
270  const IntegerValue min_expr_value =
271  LinExprLowerBound(canonical_expr, *integer_trail);
272 
273  if (rhs_domain_min > min_expr_value) {
274  // And(ei) => terms >= rhs_domain_min
275  // <=> Sum_i (~ei * (rhs_domain_min - min_expr_value)) + terms >=
276  // rhs_domain_min
277  LinearConstraintBuilder lc(&model, rhs_domain_min, kMaxIntegerValue);
278  for (const Literal& literal : enforcing_literals) {
279  CHECK(lc.AddLiteralTerm(literal.Negated(),
280  rhs_domain_min - min_expr_value));
281  }
282  for (int i = 0; i < canonical_expr.vars.size(); i++) {
283  lc.AddTerm(canonical_expr.vars[i], canonical_expr.coeffs[i]);
284  }
285  relaxation->linear_constraints.push_back(lc.Build());
286  }
287  const IntegerValue max_expr_value =
288  LinExprUpperBound(canonical_expr, *integer_trail);
289  if (rhs_domain_max < max_expr_value) {
290  // And(ei) => terms <= rhs_domain_max
291  // <=> Sum_i (~ei * (rhs_domain_max - max_expr_value)) + terms <=
292  // rhs_domain_max
293  LinearConstraintBuilder lc(&model, kMinIntegerValue, rhs_domain_max);
294  for (const Literal& literal : enforcing_literals) {
295  CHECK(lc.AddLiteralTerm(literal.Negated(),
296  rhs_domain_max - max_expr_value));
297  }
298  for (int i = 0; i < canonical_expr.vars.size(); i++) {
299  lc.AddTerm(canonical_expr.vars[i], canonical_expr.coeffs[i]);
300  }
301  relaxation->linear_constraints.push_back(lc.Build());
302  }
303 }
304 
305 bool AllLiteralsHaveViews(const IntegerEncoder& encoder,
306  const std::vector<Literal>& literals) {
307  for (const Literal lit : literals) {
308  if (!encoder.LiteralOrNegationHasView(lit)) return false;
309  }
310  return true;
311 }
312 
313 } // namespace
314 
315 // Add a linear relaxation of the CP constraint to the set of linear
316 // constraints. The highest linearization_level is, the more types of constraint
317 // we encode. This method should be called only for linearization_level > 0.
318 //
319 // Note: IntProd is linearized dynamically using the cut generators.
320 //
321 // TODO(user): In full generality, we could encode all the constraint as an LP.
322 // TODO(user,user): Add unit tests for this method.
323 void TryToLinearizeConstraint(const CpModelProto& model_proto,
324  const ConstraintProto& ct, Model* model,
325  int linearization_level,
326  LinearRelaxation* relaxation) {
327  CHECK_EQ(model->GetOrCreate<SatSolver>()->CurrentDecisionLevel(), 0);
328  DCHECK_GT(linearization_level, 0);
329  auto* mapping = model->GetOrCreate<CpModelMapping>();
330  const auto& encoder = *model->GetOrCreate<IntegerEncoder>();
331  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
332  if (linearization_level < 2) return;
333  LinearConstraintBuilder lc(model, IntegerValue(1), kMaxIntegerValue);
334  for (const int enforcement_ref : ct.enforcement_literal()) {
335  CHECK(lc.AddLiteralTerm(mapping->Literal(NegatedRef(enforcement_ref)),
336  IntegerValue(1)));
337  }
338  for (const int ref : ct.bool_or().literals()) {
339  CHECK(lc.AddLiteralTerm(mapping->Literal(ref), IntegerValue(1)));
340  }
341  relaxation->linear_constraints.push_back(lc.Build());
342  } else if (ct.constraint_case() ==
343  ConstraintProto::ConstraintCase::kBoolAnd) {
344  // TODO(user): These constraints can be many, and if they are not regrouped
345  // in big at most ones, then they should probably only added lazily as cuts.
346  // Regroup this with future clique-cut separation logic.
347  if (linearization_level < 2) return;
348  if (!HasEnforcementLiteral(ct)) return;
349  if (ct.enforcement_literal().size() == 1) {
350  const Literal enforcement = mapping->Literal(ct.enforcement_literal(0));
351  for (const int ref : ct.bool_and().literals()) {
352  relaxation->at_most_ones.push_back(
353  {enforcement, mapping->Literal(ref).Negated()});
354  }
355  return;
356  }
357 
358  // Andi(e_i) => Andj(x_j)
359  // <=> num_rhs_terms <= Sum_j(x_j) + num_rhs_terms * Sum_i(~e_i)
360  int num_literals = ct.bool_and().literals_size();
361  LinearConstraintBuilder lc(model, IntegerValue(num_literals),
363  for (const int ref : ct.bool_and().literals()) {
364  CHECK(lc.AddLiteralTerm(mapping->Literal(ref), IntegerValue(1)));
365  }
366  for (const int enforcement_ref : ct.enforcement_literal()) {
367  CHECK(lc.AddLiteralTerm(mapping->Literal(NegatedRef(enforcement_ref)),
368  IntegerValue(num_literals)));
369  }
370  relaxation->linear_constraints.push_back(lc.Build());
371  } else if (ct.constraint_case() ==
372  ConstraintProto::ConstraintCase::kAtMostOne) {
373  if (HasEnforcementLiteral(ct)) return;
374  relaxation->at_most_ones.push_back(
375  mapping->Literals(ct.at_most_one().literals()));
376  } else if (ct.constraint_case() ==
377  ConstraintProto::ConstraintCase::kExactlyOne) {
378  if (HasEnforcementLiteral(ct)) return;
379  const std::vector<Literal> literals =
380  mapping->Literals(ct.exactly_one().literals());
381  if (linearization_level >= 2 || AllLiteralsHaveViews(encoder, literals)) {
382  LinearConstraintBuilder lc(model, IntegerValue(1), IntegerValue(1));
383  for (const Literal lit : literals) {
384  CHECK(lc.AddLiteralTerm(lit, IntegerValue(1)));
385  }
386  relaxation->linear_constraints.push_back(lc.Build());
387  } else if (linearization_level == 1) {
388  // We just encode the at most one part that might be partially linearized
389  // later.
390  relaxation->at_most_ones.push_back(literals);
391  }
392  } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMax) {
393  if (HasEnforcementLiteral(ct)) return;
394  const IntegerVariable target = mapping->Integer(ct.int_max().target());
395  const std::vector<IntegerVariable> vars =
396  mapping->Integers(ct.int_max().vars());
397  AppendMaxRelaxation(target, vars, linearization_level, model, relaxation);
398 
399  } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMin) {
400  if (HasEnforcementLiteral(ct)) return;
401  const IntegerVariable negative_target =
402  NegationOf(mapping->Integer(ct.int_min().target()));
403  const std::vector<IntegerVariable> negative_vars =
404  NegationOf(mapping->Integers(ct.int_min().vars()));
405  AppendMaxRelaxation(negative_target, negative_vars, linearization_level,
406  model, relaxation);
407  } else if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
408  AppendLinearConstraintRelaxation(ct, linearization_level, *model,
409  relaxation);
410  } else if (ct.constraint_case() ==
411  ConstraintProto::ConstraintCase::kCircuit) {
412  if (HasEnforcementLiteral(ct)) return;
413  const int num_arcs = ct.circuit().literals_size();
414  CHECK_EQ(num_arcs, ct.circuit().tails_size());
415  CHECK_EQ(num_arcs, ct.circuit().heads_size());
416 
417  // Each node must have exactly one incoming and one outgoing arc (note that
418  // it can be the unique self-arc of this node too).
419  std::map<int, std::vector<Literal>> incoming_arc_constraints;
420  std::map<int, std::vector<Literal>> outgoing_arc_constraints;
421  for (int i = 0; i < num_arcs; i++) {
422  const Literal arc = mapping->Literal(ct.circuit().literals(i));
423  const int tail = ct.circuit().tails(i);
424  const int head = ct.circuit().heads(i);
425 
426  // Make sure this literal has a view.
428  outgoing_arc_constraints[tail].push_back(arc);
429  incoming_arc_constraints[head].push_back(arc);
430  }
431  for (const auto* node_map :
432  {&outgoing_arc_constraints, &incoming_arc_constraints}) {
433  for (const auto& entry : *node_map) {
434  const std::vector<Literal>& exactly_one = entry.second;
435  if (exactly_one.size() > 1) {
436  LinearConstraintBuilder at_least_one_lc(model, IntegerValue(1),
438  for (const Literal l : exactly_one) {
439  CHECK(at_least_one_lc.AddLiteralTerm(l, IntegerValue(1)));
440  }
441 
442  // We separate the two constraints.
443  relaxation->at_most_ones.push_back(exactly_one);
444  relaxation->linear_constraints.push_back(at_least_one_lc.Build());
445  }
446  }
447  }
448  } else if (ct.constraint_case() ==
449  ConstraintProto::ConstraintCase::kElement) {
450  const IntegerVariable index = mapping->Integer(ct.element().index());
451  const IntegerVariable target = mapping->Integer(ct.element().target());
452  const std::vector<IntegerVariable> vars =
453  mapping->Integers(ct.element().vars());
454 
455  // We only relax the case where all the vars are constant.
456  // target = sum (index == i) * fixed_vars[i].
457  LinearConstraintBuilder constraint(model, IntegerValue(0), IntegerValue(0));
458  constraint.AddTerm(target, IntegerValue(-1));
459  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
460  for (const auto literal_value : model->Add(FullyEncodeVariable((index)))) {
461  const IntegerVariable var = vars[literal_value.value.value()];
462  if (!model->Get(IsFixed(var))) return;
463 
464  // Make sure this literal has a view.
465  model->Add(NewIntegerVariableFromLiteral(literal_value.literal));
466  CHECK(constraint.AddLiteralTerm(literal_value.literal,
467  integer_trail->LowerBound(var)));
468  }
469 
470  relaxation->linear_constraints.push_back(constraint.Build());
471  } else if (ct.constraint_case() ==
472  ConstraintProto::ConstraintCase::kInterval) {
473  // If the interval is using views, then the linear equation is already
474  // present in the model.
475  if (linearization_level < 2) return;
476  if (ct.interval().has_start_view()) return;
477  const IntegerVariable start = mapping->Integer(ct.interval().start());
478  const IntegerVariable size = mapping->Integer(ct.interval().size());
479  const IntegerVariable end = mapping->Integer(ct.interval().end());
480  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
481  const bool size_is_fixed = integer_trail->IsFixed(size);
482  const IntegerValue rhs =
483  size_is_fixed ? -integer_trail->LowerBound(size) : IntegerValue(0);
484  LinearConstraintBuilder lc(model, rhs, rhs);
485  lc.AddTerm(start, IntegerValue(1));
486  if (!size_is_fixed) {
487  lc.AddTerm(size, IntegerValue(1));
488  }
489  lc.AddTerm(end, IntegerValue(-1));
490  if (HasEnforcementLiteral(ct)) {
491  LinearConstraint tmp_lc = lc.Build();
492  LinearExpression expr;
493  expr.coeffs = tmp_lc.coeffs;
494  expr.vars = tmp_lc.vars;
495  AppendEnforcedLinearExpression(
496  mapping->Literals(ct.enforcement_literal()), expr, tmp_lc.ub,
497  tmp_lc.ub, *model, relaxation);
498  } else {
499  relaxation->linear_constraints.push_back(lc.Build());
500  }
501  } else if (ct.constraint_case() ==
502  ConstraintProto::ConstraintCase::kNoOverlap) {
503  AppendNoOverlapRelaxation(model_proto, ct, linearization_level, model,
504  relaxation);
505  } else if (ct.constraint_case() ==
506  ConstraintProto::ConstraintCase::kCumulative) {
507  AppendCumulativeRelaxation(model_proto, ct, linearization_level, model,
508  relaxation);
509  }
510 }
511 
512 // TODO(user): Use affine demand.
513 void AddCumulativeCut(const std::vector<IntervalVariable>& intervals,
514  const std::vector<IntegerVariable>& demands,
515  IntegerValue capacity_upper_bound, Model* model,
516  LinearRelaxation* relaxation) {
517  // TODO(user): Keep a map intervals -> helper, or ct_index->helper to avoid
518  // creating many helpers for the same constraint.
519  auto* helper = new SchedulingConstraintHelper(intervals, model);
520  model->TakeOwnership(helper);
521  const int num_intervals = helper->NumTasks();
522 
523  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
524 
525  IntegerValue min_of_starts = kMaxIntegerValue;
526  IntegerValue max_of_ends = kMinIntegerValue;
527 
528  int num_variable_sizes = 0;
529  int num_optionals = 0;
530 
531  for (int index = 0; index < num_intervals; ++index) {
532  min_of_starts = std::min(min_of_starts, helper->StartMin(index));
533  max_of_ends = std::max(max_of_ends, helper->EndMax(index));
534 
535  if (helper->IsOptional(index)) {
536  num_optionals++;
537  }
538 
539  if (!helper->SizeIsFixed(index) ||
540  (!demands.empty() && !integer_trail->IsFixed(demands[index]))) {
541  num_variable_sizes++;
542  }
543  }
544 
545  VLOG(2) << "Span [" << min_of_starts << ".." << max_of_ends << "] with "
546  << num_optionals << " optional intervals, and " << num_variable_sizes
547  << " variable size intervals out of " << num_intervals
548  << " intervals";
549 
550  if (num_variable_sizes + num_optionals == 0) return;
551 
552  const IntegerVariable span_start =
553  integer_trail->AddIntegerVariable(min_of_starts, max_of_ends);
554  const IntegerVariable span_size = integer_trail->AddIntegerVariable(
555  IntegerValue(0), max_of_ends - min_of_starts);
556  const IntegerVariable span_end =
557  integer_trail->AddIntegerVariable(min_of_starts, max_of_ends);
558 
559  IntervalVariable span_var;
560  if (num_optionals < num_intervals) {
561  span_var = model->Add(NewInterval(span_start, span_end, span_size));
562  } else {
563  const Literal span_lit = Literal(model->Add(NewBooleanVariable()), true);
564  span_var = model->Add(
565  NewOptionalInterval(span_start, span_end, span_size, span_lit));
566  }
567 
568  model->Add(SpanOfIntervals(span_var, intervals));
569 
570  LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
571  lc.AddTerm(span_size, -capacity_upper_bound);
572  for (int i = 0; i < num_intervals; ++i) {
573  const IntegerValue demand_lower_bound =
574  demands.empty() ? IntegerValue(1)
575  : integer_trail->LowerBound(demands[i]);
576  const bool demand_is_fixed =
577  demands.empty() || integer_trail->IsFixed(demands[i]);
578  if (!helper->IsOptional(i)) {
579  if (helper->SizeIsFixed(i) && !demands.empty()) {
580  lc.AddTerm(demands[i], helper->SizeMin(i));
581  } else if (demand_is_fixed) {
582  lc.AddTerm(helper->Sizes()[i], demand_lower_bound);
583  } else { // demand and size are not fixed.
584  DCHECK(!demands.empty());
585  // We use McCormick equation.
586  // demand * size = (demand_min + delta_d) * (size_min + delta_s) =
587  // demand_min * size_min + delta_d * size_min +
588  // delta_s * demand_min + delta_s * delta_d
589  // which is >= (by ignoring the quatratic term)
590  // demand_min * size + size_min * demand - demand_min * size_min
591  lc.AddTerm(helper->Sizes()[i], demand_lower_bound);
592  lc.AddTerm(demands[i], helper->SizeMin(i));
593  lc.AddConstant(-helper->SizeMin(i) * demand_lower_bound);
594  }
595  } else {
596  if (!lc.AddLiteralTerm(helper->PresenceLiteral(i),
597  helper->SizeMin(i) * demand_lower_bound)) {
598  return;
599  }
600  }
601  }
602  relaxation->linear_constraints.push_back(lc.Build());
603 }
604 
605 void AppendCumulativeRelaxation(const CpModelProto& model_proto,
606  const ConstraintProto& ct,
607  int linearization_level, Model* model,
608  LinearRelaxation* relaxation) {
609  CHECK(ct.has_cumulative());
610  if (linearization_level < 2) return;
611  if (HasEnforcementLiteral(ct)) return;
612 
613  auto* mapping = model->GetOrCreate<CpModelMapping>();
614  const std::vector<IntegerVariable> demands =
615  mapping->Integers(ct.cumulative().demands());
616  std::vector<IntervalVariable> intervals =
617  mapping->Intervals(ct.cumulative().intervals());
618  const IntegerValue capacity_upper_bound =
619  model->GetOrCreate<IntegerTrail>()->UpperBound(
620  mapping->Integer(ct.cumulative().capacity()));
621  AddCumulativeCut(intervals, demands, capacity_upper_bound, model, relaxation);
622 }
623 
624 void AppendNoOverlapRelaxation(const CpModelProto& model_proto,
625  const ConstraintProto& ct,
626  int linearization_level, Model* model,
627  LinearRelaxation* relaxation) {
628  CHECK(ct.has_no_overlap());
629  if (linearization_level < 2) return;
630  if (HasEnforcementLiteral(ct)) return;
631 
632  auto* mapping = model->GetOrCreate<CpModelMapping>();
633  std::vector<IntervalVariable> intervals =
634  mapping->Intervals(ct.no_overlap().intervals());
635  AddCumulativeCut(intervals, /*demands=*/{},
636  /*capacity_upper_bound=*/IntegerValue(1), model, relaxation);
637 }
638 
639 void AppendMaxRelaxation(IntegerVariable target,
640  const std::vector<IntegerVariable>& vars,
641  int linearization_level, Model* model,
642  LinearRelaxation* relaxation) {
643  // Case X = max(X_1, X_2, ..., X_N)
644  // Part 1: Encode X >= max(X_1, X_2, ..., X_N)
645  for (const IntegerVariable var : vars) {
646  // This deal with the corner case X = max(X, Y, Z, ..) !
647  // Note that this can be presolved into X >= Y, X >= Z, ...
648  if (target == var) continue;
649  LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
650  lc.AddTerm(var, IntegerValue(1));
651  lc.AddTerm(target, IntegerValue(-1));
652  relaxation->linear_constraints.push_back(lc.Build());
653  }
654 
655  // Part 2: Encode upper bound on X.
656  if (linearization_level < 2) return;
657  GenericLiteralWatcher* watcher = model->GetOrCreate<GenericLiteralWatcher>();
658  // For size = 2, we do this with 1 less variable.
659  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
660  if (vars.size() == 2) {
661  IntegerVariable y = model->Add(NewIntegerVariable(0, 1));
662  const Literal y_lit =
663  encoder->GetOrCreateLiteralAssociatedToEquality(y, IntegerValue(1));
664  AppendEnforcedUpperBound(y_lit, target, vars[0], model, relaxation);
665 
666  // TODO(user,user): It makes more sense to use ConditionalLowerOrEqual()
667  // here, but that degrades perf on the road*.fzn problem. Understand why.
668  IntegerSumLE* upper_bound1 = new IntegerSumLE(
669  {y_lit}, {target, vars[0]}, {IntegerValue(1), IntegerValue(-1)},
670  IntegerValue(0), model);
671  upper_bound1->RegisterWith(watcher);
672  model->TakeOwnership(upper_bound1);
673  AppendEnforcedUpperBound(y_lit.Negated(), target, vars[1], model,
674  relaxation);
675  IntegerSumLE* upper_bound2 = new IntegerSumLE(
676  {y_lit.Negated()}, {target, vars[1]},
677  {IntegerValue(1), IntegerValue(-1)}, IntegerValue(0), model);
678  upper_bound2->RegisterWith(watcher);
679  model->TakeOwnership(upper_bound2);
680  return;
681  }
682  // For each X_i, we encode y_i => X <= X_i. And at least one of the y_i is
683  // true. Note that the correct y_i will be chosen because of the first part in
684  // linearlization (X >= X_i).
685  // TODO(user): Only lower bound is needed, experiment.
686  LinearConstraintBuilder lc_exactly_one(model, IntegerValue(1),
687  IntegerValue(1));
688  std::vector<Literal> exactly_one_literals;
689  exactly_one_literals.reserve(vars.size());
690  for (const IntegerVariable var : vars) {
691  if (target == var) continue;
692  // y => X <= X_i.
693  // <=> max_term_value * y + X - X_i <= max_term_value.
694  // where max_tern_value is X_ub - X_i_lb.
695  IntegerVariable y = model->Add(NewIntegerVariable(0, 1));
696  const Literal y_lit =
697  encoder->GetOrCreateLiteralAssociatedToEquality(y, IntegerValue(1));
698 
699  AppendEnforcedUpperBound(y_lit, target, var, model, relaxation);
700  IntegerSumLE* upper_bound_constraint = new IntegerSumLE(
701  {y_lit}, {target, var}, {IntegerValue(1), IntegerValue(-1)},
702  IntegerValue(0), model);
703  upper_bound_constraint->RegisterWith(watcher);
704  model->TakeOwnership(upper_bound_constraint);
705  exactly_one_literals.push_back(y_lit);
706 
707  CHECK(lc_exactly_one.AddLiteralTerm(y_lit, IntegerValue(1)));
708  }
709  model->Add(ExactlyOneConstraint(exactly_one_literals));
710  relaxation->linear_constraints.push_back(lc_exactly_one.Build());
711 }
712 
713 std::vector<IntegerVariable> AppendLinMaxRelaxation(
714  IntegerVariable target, const std::vector<LinearExpression>& exprs,
715  Model* model, LinearRelaxation* relaxation) {
716  // We want to linearize X = max(exprs[1], exprs[2], ..., exprs[d]).
717  // Part 1: Encode X >= max(exprs[1], exprs[2], ..., exprs[d])
718  for (const LinearExpression& expr : exprs) {
720  for (int i = 0; i < expr.vars.size(); ++i) {
721  lc.AddTerm(expr.vars[i], expr.coeffs[i]);
722  }
723  lc.AddTerm(target, IntegerValue(-1));
724  relaxation->linear_constraints.push_back(lc.Build());
725  }
726 
727  // Part 2: Encode upper bound on X.
728 
729  // Add linking constraint to the CP solver
730  // sum zi = 1 and for all i, zi => max = expr_i.
731  const int num_exprs = exprs.size();
732  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
733  GenericLiteralWatcher* watcher = model->GetOrCreate<GenericLiteralWatcher>();
734 
735  // TODO(user): For the case where num_exprs = 2, Create only one z var.
736  std::vector<IntegerVariable> z_vars;
737  std::vector<Literal> z_lits;
738  z_vars.reserve(num_exprs);
739  z_lits.reserve(num_exprs);
740  LinearConstraintBuilder lc_exactly_one(model, IntegerValue(1),
741  IntegerValue(1));
742  std::vector<Literal> exactly_one_literals;
743  for (int i = 0; i < num_exprs; ++i) {
744  IntegerVariable z = model->Add(NewIntegerVariable(0, 1));
745  z_vars.push_back(z);
746  const Literal z_lit =
747  encoder->GetOrCreateLiteralAssociatedToEquality(z, IntegerValue(1));
748  z_lits.push_back(z_lit);
749  LinearExpression local_expr;
750  local_expr.vars = NegationOf(exprs[i].vars);
751  local_expr.vars.push_back(target);
752  local_expr.coeffs = exprs[i].coeffs;
753  local_expr.coeffs.push_back(IntegerValue(1));
754  IntegerSumLE* upper_bound = new IntegerSumLE(
755  {z_lit}, local_expr.vars, local_expr.coeffs, exprs[i].offset, model);
756  upper_bound->RegisterWith(watcher);
757  model->TakeOwnership(upper_bound);
758 
759  CHECK(lc_exactly_one.AddLiteralTerm(z_lit, IntegerValue(1)));
760  }
761  model->Add(ExactlyOneConstraint(z_lits));
762 
763  // For the relaxation, we use different constraints with a stronger linear
764  // relaxation as explained in the .h
765  // TODO(user): Consider passing the x_vars to this method instead of
766  // computing it here.
767  std::vector<IntegerVariable> x_vars;
768  for (int i = 0; i < num_exprs; ++i) {
769  x_vars.insert(x_vars.end(), exprs[i].vars.begin(), exprs[i].vars.end());
770  }
772  // All expressions should only contain positive variables.
773  DCHECK(std::all_of(x_vars.begin(), x_vars.end(), [](IntegerVariable var) {
774  return VariableIsPositive(var);
775  }));
776 
777  std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
778  num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
779 
780  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
781  for (int i = 0; i < num_exprs; ++i) {
782  for (int j = 0; j < num_exprs; ++j) {
783  if (i == j) continue;
784  for (const IntegerVariable x_var : x_vars) {
785  const IntegerValue lb = integer_trail->LevelZeroLowerBound(x_var);
786  const IntegerValue ub = integer_trail->LevelZeroUpperBound(x_var);
787  const IntegerValue diff =
788  GetCoefficient(x_var, exprs[j]) - GetCoefficient(x_var, exprs[i]);
789  sum_of_max_corner_diff[i][j] += std::max(diff * lb, diff * ub);
790  }
791  }
792  }
793  for (int i = 0; i < num_exprs; ++i) {
794  LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
795  lc.AddTerm(target, IntegerValue(1));
796  for (int j = 0; j < exprs[i].vars.size(); ++j) {
797  lc.AddTerm(exprs[i].vars[j], -exprs[i].coeffs[j]);
798  }
799  for (int j = 0; j < num_exprs; ++j) {
800  CHECK(lc.AddLiteralTerm(z_lits[j],
801  -exprs[j].offset - sum_of_max_corner_diff[i][j]));
802  }
803  relaxation->linear_constraints.push_back(lc.Build());
804  }
805 
806  relaxation->linear_constraints.push_back(lc_exactly_one.Build());
807  return z_vars;
808 }
809 
810 void AppendLinearConstraintRelaxation(const ConstraintProto& constraint_proto,
811  const int linearization_level,
812  const Model& model,
813  LinearRelaxation* relaxation) {
814  auto* mapping = model.Get<CpModelMapping>();
815 
816  // Note that we ignore the holes in the domain.
817  //
818  // TODO(user): In LoadLinearConstraint() we already created intermediate
819  // Booleans for each disjoint interval, we should reuse them here if
820  // possible.
821  //
822  // TODO(user): process the "at most one" part of a == 1 separately?
823  const IntegerValue rhs_domain_min =
824  IntegerValue(constraint_proto.linear().domain(0));
825  const IntegerValue rhs_domain_max =
826  IntegerValue(constraint_proto.linear().domain(
827  constraint_proto.linear().domain_size() - 1));
828  if (rhs_domain_min == kint64min && rhs_domain_max == kint64max) return;
829 
830  if (!HasEnforcementLiteral(constraint_proto)) {
831  LinearConstraintBuilder lc(&model, rhs_domain_min, rhs_domain_max);
832  for (int i = 0; i < constraint_proto.linear().vars_size(); i++) {
833  const int ref = constraint_proto.linear().vars(i);
834  const int64 coeff = constraint_proto.linear().coeffs(i);
835  lc.AddTerm(mapping->Integer(ref), IntegerValue(coeff));
836  }
837  relaxation->linear_constraints.push_back(lc.Build());
838  return;
839  }
840 
841  // Reified version.
842  if (linearization_level < 2) return;
843 
844  // We linearize fully reified constraints of size 1 all together for a given
845  // variable. But we need to process half-reified ones.
846  if (!mapping->IsHalfEncodingConstraint(&constraint_proto) &&
847  constraint_proto.linear().vars_size() <= 1) {
848  return;
849  }
850 
851  std::vector<Literal> enforcing_literals;
852  enforcing_literals.reserve(constraint_proto.enforcement_literal_size());
853  for (const int enforcement_ref : constraint_proto.enforcement_literal()) {
854  enforcing_literals.push_back(mapping->Literal(enforcement_ref));
855  }
856  LinearExpression expr;
857  expr.vars.reserve(constraint_proto.linear().vars_size());
858  expr.coeffs.reserve(constraint_proto.linear().vars_size());
859  for (int i = 0; i < constraint_proto.linear().vars_size(); i++) {
860  int ref = constraint_proto.linear().vars(i);
861  IntegerValue coeff(constraint_proto.linear().coeffs(i));
862  if (!RefIsPositive(ref)) {
863  ref = PositiveRef(ref);
864  coeff = -coeff;
865  }
866  const IntegerVariable int_var = mapping->Integer(ref);
867  expr.vars.push_back(int_var);
868  expr.coeffs.push_back(coeff);
869  }
870  AppendEnforcedLinearExpression(enforcing_literals, expr, rhs_domain_min,
871  rhs_domain_max, model, relaxation);
872 }
873 
874 } // namespace sat
875 } // 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 CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
std::vector< IntegerVariable > Integers(const List &list) const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
Definition: integer.cc:248
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
Definition: integer.cc:106
void RegisterWith(GenericLiteralWatcher *watcher)
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition: integer.h:1355
IntegerVariable AddIntegerVariable(IntegerValue lower_bound, IntegerValue upper_bound)
Definition: integer.cc:603
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1350
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff)
void AddTerm(IntegerVariable var, IntegerValue coeff)
Literal(int signed_value)
Definition: sat_base.h:68
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
CpModelProto const * model_proto
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1467
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::vector< IntegerVariable > AppendLinMaxRelaxation(IntegerVariable target, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:876
void AppendLinearConstraintRelaxation(const ConstraintProto &constraint_proto, const int linearization_level, const Model &model, LinearRelaxation *relaxation)
bool RefIsPositive(int ref)
const LiteralIndex kNoLiteralIndex(-1)
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
Definition: intervals.h:662
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
bool HasEnforcementLiteral(const ConstraintProto &ct)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >Model *)> FullyEncodeVariable(IntegerVariable var)
Definition: integer.h:1587
bool AppendFullEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
const IntegerVariable kNoIntegerVariable(-1)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
Definition: intervals.h:632
LinearExpression CanonicalizeExpr(const LinearExpression &expr)
void AppendMaxRelaxation(IntegerVariable target, const std::vector< IntegerVariable > &vars, int linearization_level, Model *model, LinearRelaxation *relaxation)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
Definition: integer.h:1444
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1426
IntegerValue GetCoefficient(const IntegerVariable var, const LinearExpression &expr)
void TryToLinearizeConstraint(const CpModelProto &model_proto, const ConstraintProto &ct, Model *model, int linearization_level, LinearRelaxation *relaxation)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
void AppendPartialEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> SpanOfIntervals(IntervalVariable span, const std::vector< IntervalVariable > &intervals)
void AddCumulativeCut(const std::vector< IntervalVariable > &intervals, const std::vector< IntegerVariable > &demands, IntegerValue capacity_upper_bound, Model *model, LinearRelaxation *relaxation)
void AppendNoOverlapRelaxation(const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1479
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
void AppendCumulativeRelaxation(const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 delta
Definition: resource.cc:1684
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
std::vector< IntegerVariable > vars
std::vector< std::vector< Literal > > at_most_ones
std::vector< LinearConstraint > linear_constraints