OR-Tools  8.2
cp_model_expand.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 <map>
17 
18 #include "absl/container/flat_hash_map.h"
19 #include "ortools/base/hash.h"
20 #include "ortools/base/map_util.h"
21 #include "ortools/base/stl_util.h"
23 #include "ortools/sat/cp_model.pb.h"
26 #include "ortools/sat/util.h"
29 
30 namespace operations_research {
31 namespace sat {
32 namespace {
33 
34 void ExpandReservoir(ConstraintProto* ct, PresolveContext* context) {
35  if (ct->reservoir().min_level() > ct->reservoir().max_level()) {
36  VLOG(1) << "Empty level domain in reservoir constraint.";
37  return (void)context->NotifyThatModelIsUnsat();
38  }
39 
40  const ReservoirConstraintProto& reservoir = ct->reservoir();
41  const int num_events = reservoir.times_size();
42 
43  const int true_literal = context->GetOrCreateConstantVar(1);
44 
45  const auto is_active_literal = [&reservoir, true_literal](int index) {
46  if (reservoir.actives_size() == 0) return true_literal;
47  return reservoir.actives(index);
48  };
49 
50  int num_positives = 0;
51  int num_negatives = 0;
52  for (const int64 demand : reservoir.demands()) {
53  if (demand > 0) {
54  num_positives++;
55  } else if (demand < 0) {
56  num_negatives++;
57  }
58  }
59 
60  if (num_positives > 0 && num_negatives > 0) {
61  // Creates Boolean variables equivalent to (start[i] <= start[j]) i != j
62  for (int i = 0; i < num_events - 1; ++i) {
63  const int active_i = is_active_literal(i);
64  if (context->LiteralIsFalse(active_i)) continue;
65  const int time_i = reservoir.times(i);
66 
67  for (int j = i + 1; j < num_events; ++j) {
68  const int active_j = is_active_literal(j);
69  if (context->LiteralIsFalse(active_j)) continue;
70  const int time_j = reservoir.times(j);
71 
72  const int i_lesseq_j = context->GetOrCreateReifiedPrecedenceLiteral(
73  time_i, time_j, active_i, active_j);
74  context->working_model->mutable_variables(i_lesseq_j)
75  ->set_name(absl::StrCat(i, " before ", j));
76  const int j_lesseq_i = context->GetOrCreateReifiedPrecedenceLiteral(
77  time_j, time_i, active_j, active_i);
78  context->working_model->mutable_variables(j_lesseq_i)
79  ->set_name(absl::StrCat(j, " before ", i));
80  }
81  }
82 
83  // Constrains the running level to be consistent at all times.
84  // For this we only add a constraint at the time a given demand
85  // take place. We also have a constraint for time zero if needed
86  // (added below).
87  for (int i = 0; i < num_events; ++i) {
88  const int active_i = is_active_literal(i);
89  if (context->LiteralIsFalse(active_i)) continue;
90  const int time_i = reservoir.times(i);
91 
92  // Accumulates demands of all predecessors.
93  ConstraintProto* const level = context->working_model->add_constraints();
94  level->add_enforcement_literal(active_i);
95 
96  // Add contributions from previous events.
97  for (int j = 0; j < num_events; ++j) {
98  if (i == j) continue;
99  const int active_j = is_active_literal(j);
100  if (context->LiteralIsFalse(active_j)) continue;
101 
102  const int time_j = reservoir.times(j);
103  level->mutable_linear()->add_vars(
104  context->GetOrCreateReifiedPrecedenceLiteral(time_j, time_i,
105  active_j, active_i));
106  level->mutable_linear()->add_coeffs(reservoir.demands(j));
107  }
108 
109  // Accounts for own demand in the domain of the sum.
110  const int64 demand_i = reservoir.demands(i);
111  level->mutable_linear()->add_domain(
112  CapSub(reservoir.min_level(), demand_i));
113  level->mutable_linear()->add_domain(
114  CapSub(reservoir.max_level(), demand_i));
115  }
116  } else {
117  // If all demands have the same sign, we do not care about the order, just
118  // the sum.
119  auto* const sum =
120  context->working_model->add_constraints()->mutable_linear();
121  for (int i = 0; i < num_events; ++i) {
122  sum->add_vars(is_active_literal(i));
123  sum->add_coeffs(reservoir.demands(i));
124  }
125  sum->add_domain(reservoir.min_level());
126  sum->add_domain(reservoir.max_level());
127  }
128 
129  ct->Clear();
130  context->UpdateRuleStats("reservoir: expanded");
131 }
132 
133 // This is not an "expansion" per say, but just a mandatory presolve step to
134 // satisfy preconditions assumed by the rest of the code.
135 void ExpandIntDiv(ConstraintProto* ct, PresolveContext* context) {
136  const int divisor = ct->int_div().vars(1);
137  if (!context->IntersectDomainWith(divisor, Domain(0).Complement())) {
138  return (void)context->NotifyThatModelIsUnsat();
139  }
140 }
141 
142 void ExpandIntMod(ConstraintProto* ct, PresolveContext* context) {
143  const IntegerArgumentProto& int_mod = ct->int_mod();
144  const int var = int_mod.vars(0);
145  const int mod_var = int_mod.vars(1);
146  const int target_var = int_mod.target();
147 
148  const int64 mod_lb = context->MinOf(mod_var);
149  CHECK_GE(mod_lb, 1);
150  const int64 mod_ub = context->MaxOf(mod_var);
151 
152  const int64 var_lb = context->MinOf(var);
153  const int64 var_ub = context->MaxOf(var);
154 
155  // Compute domains of var / mod_var.
156  const int div_var =
157  context->NewIntVar(Domain(var_lb / mod_ub, var_ub / mod_lb));
158 
159  auto add_enforcement_literal_if_needed = [&]() {
160  if (ct->enforcement_literal_size() == 0) return;
161  const int literal = ct->enforcement_literal(0);
162  ConstraintProto* const last = context->working_model->mutable_constraints(
163  context->working_model->constraints_size() - 1);
164  last->add_enforcement_literal(literal);
165  };
166 
167  // div = var / mod.
168  IntegerArgumentProto* const div_proto =
169  context->working_model->add_constraints()->mutable_int_div();
170  div_proto->set_target(div_var);
171  div_proto->add_vars(var);
172  div_proto->add_vars(mod_var);
173  add_enforcement_literal_if_needed();
174 
175  // Checks if mod is constant.
176  if (mod_lb == mod_ub) {
177  // var - div_var * mod = target.
178  LinearConstraintProto* const lin =
179  context->working_model->add_constraints()->mutable_linear();
180  lin->add_vars(int_mod.vars(0));
181  lin->add_coeffs(1);
182  lin->add_vars(div_var);
183  lin->add_coeffs(-mod_lb);
184  lin->add_vars(target_var);
185  lin->add_coeffs(-1);
186  lin->add_domain(0);
187  lin->add_domain(0);
188  add_enforcement_literal_if_needed();
189  } else {
190  // Create prod_var = div_var * mod.
191  const int prod_var = context->NewIntVar(
192  Domain(var_lb * mod_lb / mod_ub, var_ub * mod_ub / mod_lb));
193  IntegerArgumentProto* const int_prod =
194  context->working_model->add_constraints()->mutable_int_prod();
195  int_prod->set_target(prod_var);
196  int_prod->add_vars(div_var);
197  int_prod->add_vars(mod_var);
198  add_enforcement_literal_if_needed();
199 
200  // var - prod_var = target.
201  LinearConstraintProto* const lin =
202  context->working_model->add_constraints()->mutable_linear();
203  lin->add_vars(var);
204  lin->add_coeffs(1);
205  lin->add_vars(prod_var);
206  lin->add_coeffs(-1);
207  lin->add_vars(target_var);
208  lin->add_coeffs(-1);
209  lin->add_domain(0);
210  lin->add_domain(0);
211  add_enforcement_literal_if_needed();
212  }
213 
214  ct->Clear();
215  context->UpdateRuleStats("int_mod: expanded");
216 }
217 
218 void ExpandIntProdWithBoolean(int bool_ref, int int_ref, int product_ref,
219  PresolveContext* context) {
220  ConstraintProto* const one = context->working_model->add_constraints();
221  one->add_enforcement_literal(bool_ref);
222  one->mutable_linear()->add_vars(int_ref);
223  one->mutable_linear()->add_coeffs(1);
224  one->mutable_linear()->add_vars(product_ref);
225  one->mutable_linear()->add_coeffs(-1);
226  one->mutable_linear()->add_domain(0);
227  one->mutable_linear()->add_domain(0);
228 
229  ConstraintProto* const zero = context->working_model->add_constraints();
230  zero->add_enforcement_literal(NegatedRef(bool_ref));
231  zero->mutable_linear()->add_vars(product_ref);
232  zero->mutable_linear()->add_coeffs(1);
233  zero->mutable_linear()->add_domain(0);
234  zero->mutable_linear()->add_domain(0);
235 }
236 
237 void AddXEqualYOrXEqualZero(int x_eq_y, int x, int y,
238  PresolveContext* context) {
239  ConstraintProto* equality = context->working_model->add_constraints();
240  equality->add_enforcement_literal(x_eq_y);
241  equality->mutable_linear()->add_vars(x);
242  equality->mutable_linear()->add_coeffs(1);
243  equality->mutable_linear()->add_vars(y);
244  equality->mutable_linear()->add_coeffs(-1);
245  equality->mutable_linear()->add_domain(0);
246  equality->mutable_linear()->add_domain(0);
247  context->AddImplyInDomain(NegatedRef(x_eq_y), x, {0, 0});
248 }
249 
250 // a_ref spans across 0, b_ref does not.
251 void ExpandIntProdWithOneAcrossZero(int a_ref, int b_ref, int product_ref,
252  PresolveContext* context) {
253  DCHECK_LT(context->MinOf(a_ref), 0);
254  DCHECK_GT(context->MaxOf(a_ref), 0);
255  DCHECK(context->MinOf(b_ref) >= 0 || context->MaxOf(b_ref) <= 0);
256 
257  // Split the domain of a in two, controlled by a new literal.
258  const int a_is_positive = context->NewBoolVar();
259  context->AddImplyInDomain(a_is_positive, a_ref, {0, kint64max});
260  context->AddImplyInDomain(NegatedRef(a_is_positive), a_ref, {kint64min, -1});
261  const int pos_a_ref = context->NewIntVar({0, context->MaxOf(a_ref)});
262  AddXEqualYOrXEqualZero(a_is_positive, pos_a_ref, a_ref, context);
263 
264  const int neg_a_ref = context->NewIntVar({context->MinOf(a_ref), 0});
265  AddXEqualYOrXEqualZero(NegatedRef(a_is_positive), neg_a_ref, a_ref, context);
266 
267  // Create product with the positive part ofa_ref.
268  const bool b_is_positive = context->MinOf(b_ref) >= 0;
269  const Domain pos_a_product_domain =
270  b_is_positive ? Domain({0, context->MaxOf(product_ref)})
271  : Domain({context->MinOf(product_ref), 0});
272  const int pos_a_product = context->NewIntVar(pos_a_product_domain);
273  IntegerArgumentProto* pos_product =
274  context->working_model->add_constraints()->mutable_int_prod();
275  pos_product->set_target(pos_a_product);
276  pos_product->add_vars(pos_a_ref);
277  pos_product->add_vars(b_ref);
278 
279  // Create product with the negative part of a_ref.
280  const Domain neg_a_product_domain =
281  b_is_positive ? Domain({context->MinOf(product_ref), 0})
282  : Domain({0, context->MaxOf(product_ref)});
283  const int neg_a_product = context->NewIntVar(neg_a_product_domain);
284  IntegerArgumentProto* neg_product =
285  context->working_model->add_constraints()->mutable_int_prod();
286  neg_product->set_target(neg_a_product);
287  neg_product->add_vars(neg_a_ref);
288  neg_product->add_vars(b_ref);
289 
290  // Link back to the original product.
291  LinearConstraintProto* lin =
292  context->working_model->add_constraints()->mutable_linear();
293  lin->add_vars(product_ref);
294  lin->add_coeffs(-1);
295  lin->add_vars(pos_a_product);
296  lin->add_coeffs(1);
297  lin->add_vars(neg_a_product);
298  lin->add_coeffs(1);
299  lin->add_domain(0);
300  lin->add_domain(0);
301 }
302 
303 void ExpandIntProdWithTwoAcrossZero(int a_ref, int b_ref, int product_ref,
304  PresolveContext* context) {
305  // Split a_ref domain in two, controlled by a new literal.
306  const int a_is_positive = context->NewBoolVar();
307  context->AddImplyInDomain(a_is_positive, a_ref, {0, kint64max});
308  context->AddImplyInDomain(NegatedRef(a_is_positive), a_ref, {kint64min, -1});
309  const int64 min_of_a = context->MinOf(a_ref);
310  const int64 max_of_a = context->MaxOf(a_ref);
311 
312  const int pos_a_ref = context->NewIntVar({0, max_of_a});
313  AddXEqualYOrXEqualZero(a_is_positive, pos_a_ref, a_ref, context);
314 
315  const int neg_a_ref = context->NewIntVar({min_of_a, 0});
316  AddXEqualYOrXEqualZero(NegatedRef(a_is_positive), neg_a_ref, a_ref, context);
317 
318  // Create product with two sub parts of a_ref.
319  const int pos_product_ref =
320  context->NewIntVar(context->DomainOf(product_ref));
321  ExpandIntProdWithOneAcrossZero(b_ref, pos_a_ref, pos_product_ref, context);
322  const int neg_product_ref =
323  context->NewIntVar(context->DomainOf(product_ref));
324  ExpandIntProdWithOneAcrossZero(b_ref, neg_a_ref, neg_product_ref, context);
325 
326  // Link back to the original product.
327  LinearConstraintProto* lin =
328  context->working_model->add_constraints()->mutable_linear();
329  lin->add_vars(product_ref);
330  lin->add_coeffs(-1);
331  lin->add_vars(pos_product_ref);
332  lin->add_coeffs(1);
333  lin->add_vars(neg_product_ref);
334  lin->add_coeffs(1);
335  lin->add_domain(0);
336  lin->add_domain(0);
337 }
338 
339 void ExpandIntProd(ConstraintProto* ct, PresolveContext* context) {
340  const IntegerArgumentProto& int_prod = ct->int_prod();
341  if (int_prod.vars_size() != 2) return;
342  const int a = int_prod.vars(0);
343  const int b = int_prod.vars(1);
344  const int p = int_prod.target();
345  const bool a_is_boolean =
346  RefIsPositive(a) && context->MinOf(a) == 0 && context->MaxOf(a) == 1;
347  const bool b_is_boolean =
348  RefIsPositive(b) && context->MinOf(b) == 0 && context->MaxOf(b) == 1;
349 
350  // We expand if exactly one of {a, b} is Boolean. If both are Boolean, it
351  // will be presolved into a better version.
352  if (a_is_boolean && !b_is_boolean) {
353  ExpandIntProdWithBoolean(a, b, p, context);
354  ct->Clear();
355  context->UpdateRuleStats("int_prod: expanded product with Boolean var");
356  return;
357  }
358  if (b_is_boolean && !a_is_boolean) {
359  ExpandIntProdWithBoolean(b, a, p, context);
360  ct->Clear();
361  context->UpdateRuleStats("int_prod: expanded product with Boolean var");
362  return;
363  }
364 
365  const bool a_span_across_zero =
366  context->MinOf(a) < 0 && context->MaxOf(a) > 0;
367  const bool b_span_across_zero =
368  context->MinOf(b) < 0 && context->MaxOf(b) > 0;
369  if (a_span_across_zero && !b_span_across_zero) {
370  ExpandIntProdWithOneAcrossZero(a, b, p, context);
371  ct->Clear();
372  context->UpdateRuleStats(
373  "int_prod: expanded product with general integer variables");
374  return;
375  }
376  if (!a_span_across_zero && b_span_across_zero) {
377  ExpandIntProdWithOneAcrossZero(b, a, p, context);
378  ct->Clear();
379  context->UpdateRuleStats(
380  "int_prod: expanded product with general integer variables");
381  return;
382  }
383  if (a_span_across_zero && b_span_across_zero) {
384  ExpandIntProdWithTwoAcrossZero(a, b, p, context);
385  ct->Clear();
386  context->UpdateRuleStats(
387  "int_prod: expanded product with general integer variables");
388  return;
389  }
390 }
391 
392 void ExpandInverse(ConstraintProto* ct, PresolveContext* context) {
393  const int size = ct->inverse().f_direct().size();
394  CHECK_EQ(size, ct->inverse().f_inverse().size());
395 
396  // Make sure the domains are included in [0, size - 1).
397  //
398  // TODO(user): Add support for UNSAT at expansion. This should create empty
399  // domain if UNSAT, so it should still work correctly.
400  for (const int ref : ct->inverse().f_direct()) {
401  if (!context->IntersectDomainWith(ref, Domain(0, size - 1))) {
402  VLOG(1) << "Empty domain for a variable in ExpandInverse()";
403  return;
404  }
405  }
406  for (const int ref : ct->inverse().f_inverse()) {
407  if (!context->IntersectDomainWith(ref, Domain(0, size - 1))) {
408  VLOG(1) << "Empty domain for a variable in ExpandInverse()";
409  return;
410  }
411  }
412 
413  // Reduce the domains of each variable by checking that the inverse value
414  // exists.
415  std::vector<int64> possible_values;
416  // Propagate from one vector to its counterpart.
417  // Note this reaches the fixpoint as there is a one to one mapping between
418  // (variable-value) pairs in each vector.
419  const auto filter_inverse_domain = [context, size, &possible_values](
420  const auto& direct,
421  const auto& inverse) {
422  // Propagate for the inverse vector to the direct vector.
423  for (int i = 0; i < size; ++i) {
424  possible_values.clear();
425  const Domain domain = context->DomainOf(direct[i]);
426  bool removed_value = false;
427  for (const ClosedInterval& interval : domain) {
428  for (int64 j = interval.start; j <= interval.end; ++j) {
429  if (context->DomainOf(inverse[j]).Contains(i)) {
430  possible_values.push_back(j);
431  } else {
432  removed_value = true;
433  }
434  }
435  }
436  if (removed_value) {
437  if (!context->IntersectDomainWith(
438  direct[i], Domain::FromValues(possible_values))) {
439  VLOG(1) << "Empty domain for a variable in ExpandInverse()";
440  return false;
441  }
442  }
443  }
444  return true;
445  };
446 
447  if (!filter_inverse_domain(ct->inverse().f_direct(),
448  ct->inverse().f_inverse())) {
449  return;
450  }
451 
452  if (!filter_inverse_domain(ct->inverse().f_inverse(),
453  ct->inverse().f_direct())) {
454  return;
455  }
456 
457  // Expand the inverse constraint by associating literal to var == value
458  // and sharing them between the direct and inverse variables.
459  for (int i = 0; i < size; ++i) {
460  const int f_i = ct->inverse().f_direct(i);
461  const Domain domain = context->DomainOf(f_i);
462  for (const ClosedInterval& interval : domain) {
463  for (int64 j = interval.start; j <= interval.end; ++j) {
464  // We have f[i] == j <=> r[j] == i;
465  const int r_j = ct->inverse().f_inverse(j);
466  int r_j_i;
467  if (context->HasVarValueEncoding(r_j, i, &r_j_i)) {
468  context->InsertVarValueEncoding(r_j_i, f_i, j);
469  } else {
470  const int f_i_j = context->GetOrCreateVarValueEncoding(f_i, j);
471  context->InsertVarValueEncoding(f_i_j, r_j, i);
472  }
473  }
474  }
475  }
476 
477  ct->Clear();
478  context->UpdateRuleStats("inverse: expanded");
479 }
480 
481 void ExpandElement(ConstraintProto* ct, PresolveContext* context) {
482  const ElementConstraintProto& element = ct->element();
483  const int index_ref = element.index();
484  const int target_ref = element.target();
485  const int size = element.vars_size();
486 
487  if (!context->IntersectDomainWith(index_ref, Domain(0, size - 1))) {
488  VLOG(1) << "Empty domain for the index variable in ExpandElement()";
489  return (void)context->NotifyThatModelIsUnsat();
490  }
491 
492  bool all_constants = true;
493  absl::flat_hash_map<int64, int> constant_var_values_usage;
494  std::vector<int64> constant_var_values;
495  std::vector<int64> invalid_indices;
496  Domain index_domain = context->DomainOf(index_ref);
497  Domain target_domain = context->DomainOf(target_ref);
498  for (const ClosedInterval& interval : index_domain) {
499  for (int64 v = interval.start; v <= interval.end; ++v) {
500  const int var = element.vars(v);
501  const Domain var_domain = context->DomainOf(var);
502  if (var_domain.IntersectionWith(target_domain).IsEmpty()) {
503  invalid_indices.push_back(v);
504  continue;
505  }
506  if (var_domain.Min() != var_domain.Max()) {
507  all_constants = false;
508  break;
509  }
510 
511  const int64 value = var_domain.Min();
512  if (constant_var_values_usage[value]++ == 0) {
513  constant_var_values.push_back(value);
514  }
515  }
516  }
517 
518  if (!invalid_indices.empty() && target_ref != index_ref) {
519  if (!context->IntersectDomainWith(
520  index_ref, Domain::FromValues(invalid_indices).Complement())) {
521  VLOG(1) << "No compatible variable domains in ExpandElement()";
522  return (void)context->NotifyThatModelIsUnsat();
523  }
524 
525  // Re-read the domain.
526  index_domain = context->DomainOf(index_ref);
527  }
528 
529  // This BoolOrs implements the deduction that if all index literals pointing
530  // to the same values in the constant array are false, then this value is no
531  // no longer valid for the target variable. They are created only for values
532  // that have multiples literals supporting them.
533  // Order is not important.
534  absl::flat_hash_map<int64, BoolArgumentProto*> supports;
535  if (all_constants && target_ref != index_ref) {
536  if (!context->IntersectDomainWith(
537  target_ref, Domain::FromValues(constant_var_values))) {
538  VLOG(1) << "Empty domain for the target variable in ExpandElement()";
539  return;
540  }
541 
542  target_domain = context->DomainOf(target_ref);
543  if (target_domain.Size() == 1) {
544  context->UpdateRuleStats("element: one value array");
545  ct->Clear();
546  return;
547  }
548 
549  for (const ClosedInterval& interval : target_domain) {
550  for (int64 v = interval.start; v <= interval.end; ++v) {
551  const int usage = gtl::FindOrDie(constant_var_values_usage, v);
552  if (usage > 1) {
553  const int lit = context->GetOrCreateVarValueEncoding(target_ref, v);
554  BoolArgumentProto* const support =
555  context->working_model->add_constraints()->mutable_bool_or();
556  supports[v] = support;
557  support->add_literals(NegatedRef(lit));
558  }
559  }
560  }
561  }
562 
563  // While this is not stricly needed since all value in the index will be
564  // covered, it allows to easily detect this fact in the presolve.
565  auto* bool_or = context->working_model->add_constraints()->mutable_bool_or();
566 
567  for (const ClosedInterval& interval : index_domain) {
568  for (int64 v = interval.start; v <= interval.end; ++v) {
569  const int var = element.vars(v);
570  const int index_lit = context->GetOrCreateVarValueEncoding(index_ref, v);
571  const Domain var_domain = context->DomainOf(var);
572 
573  bool_or->add_literals(index_lit);
574 
575  if (target_ref == index_ref) {
576  // This adds extra code. But this information is really important,
577  // and hard to retrieve once lost.
578  context->AddImplyInDomain(index_lit, var, Domain(v));
579  } else if (target_domain.Size() == 1) {
580  // TODO(user): If we know all variables are different, then this
581  // becomes an equivalence.
582  context->AddImplyInDomain(index_lit, var, target_domain);
583  } else if (var_domain.Size() == 1) {
584  if (all_constants) {
585  const int64 value = var_domain.Min();
586  if (constant_var_values_usage[value] > 1) {
587  // The encoding literal for 'value' of the target_ref has been
588  // created before.
589  const int target_lit =
590  context->GetOrCreateVarValueEncoding(target_ref, value);
591  context->AddImplication(index_lit, target_lit);
592  gtl::FindOrDie(supports, value)->add_literals(index_lit);
593  } else {
594  // Try to reuse the literal of the index.
595  context->InsertVarValueEncoding(index_lit, target_ref, value);
596  }
597  } else {
598  context->AddImplyInDomain(index_lit, target_ref, var_domain);
599  }
600  } else {
601  ConstraintProto* const ct = context->working_model->add_constraints();
602  ct->add_enforcement_literal(index_lit);
603  ct->mutable_linear()->add_vars(var);
604  ct->mutable_linear()->add_coeffs(1);
605  ct->mutable_linear()->add_vars(target_ref);
606  ct->mutable_linear()->add_coeffs(-1);
607  ct->mutable_linear()->add_domain(0);
608  ct->mutable_linear()->add_domain(0);
609  }
610  }
611  }
612 
613  if (all_constants) {
614  const int64 var_min = target_domain.Min();
615 
616  // Scan all values to find the one with the most literals attached.
617  int64 most_frequent_value = kint64max;
618  int usage = -1;
619  for (const auto it : constant_var_values_usage) {
620  if (it.second > usage ||
621  (it.second == usage && it.first < most_frequent_value)) {
622  usage = it.second;
623  most_frequent_value = it.first;
624  }
625  }
626 
627  // Add a linear constraint. This helps the linear relaxation.
628  //
629  // We try to minimize the size of the linear constraint (if the gain is
630  // meaningful compared to using the min that has the advantage that all
631  // coefficients are positive).
632  // TODO(user): Benchmark if using base is always beneficial.
633  // TODO(user): Try not to create this if max_usage == 1.
634  const int64 base =
635  usage > 2 && usage > size / 10 ? most_frequent_value : var_min;
636  if (base != var_min) {
637  VLOG(3) << "expand element: choose " << base << " with usage " << usage
638  << " over " << var_min << " among " << size << " values.";
639  }
640 
641  LinearConstraintProto* const linear =
642  context->working_model->add_constraints()->mutable_linear();
643  int64 rhs = -base;
644  linear->add_vars(target_ref);
645  linear->add_coeffs(-1);
646  for (const ClosedInterval& interval : index_domain) {
647  for (int64 v = interval.start; v <= interval.end; ++v) {
648  const int ref = element.vars(v);
649  const int index_lit =
650  context->GetOrCreateVarValueEncoding(index_ref, v);
651  const int64 delta = context->DomainOf(ref).Min() - base;
652  if (RefIsPositive(index_lit)) {
653  linear->add_vars(index_lit);
654  linear->add_coeffs(delta);
655  } else {
656  linear->add_vars(NegatedRef(index_lit));
657  linear->add_coeffs(-delta);
658  rhs -= delta;
659  }
660  }
661  }
662  linear->add_domain(rhs);
663  linear->add_domain(rhs);
664 
665  context->UpdateRuleStats("element: expanded value element");
666  } else {
667  context->UpdateRuleStats("element: expanded");
668  }
669  ct->Clear();
670 }
671 
672 // Adds clauses so that literals[i] true <=> encoding[value[i]] true.
673 // This also implicitly use the fact that exactly one alternative is true.
674 void LinkLiteralsAndValues(
675  const std::vector<int>& value_literals, const std::vector<int64>& values,
676  const absl::flat_hash_map<int64, int>& target_encoding,
677  PresolveContext* context) {
678  CHECK_EQ(value_literals.size(), values.size());
679 
680  // TODO(user): Make sure this does not appear in the profile.
681  // We use a map to make this method deterministic.
682  std::map<int, std::vector<int>> value_literals_per_target_literal;
683 
684  // If a value is false (i.e not possible), then the tuple with this
685  // value is false too (i.e not possible). Conversely, if the tuple is
686  // selected, the value must be selected.
687  for (int i = 0; i < values.size(); ++i) {
688  const int64 v = values[i];
689  CHECK(target_encoding.contains(v));
690  const int lit = gtl::FindOrDie(target_encoding, v);
691  value_literals_per_target_literal[lit].push_back(value_literals[i]);
692  }
693 
694  // If all tuples supporting a value are false, then this value must be
695  // false.
696  for (const auto& it : value_literals_per_target_literal) {
697  const int target_literal = it.first;
698  switch (it.second.size()) {
699  case 0: {
700  if (!context->SetLiteralToFalse(target_literal)) {
701  return;
702  }
703  break;
704  }
705  case 1: {
706  context->StoreBooleanEqualityRelation(target_literal,
707  it.second.front());
708  break;
709  }
710  default: {
711  BoolArgumentProto* const bool_or =
712  context->working_model->add_constraints()->mutable_bool_or();
713  bool_or->add_literals(NegatedRef(target_literal));
714  for (const int value_literal : it.second) {
715  bool_or->add_literals(value_literal);
716  context->AddImplication(value_literal, target_literal);
717  }
718  }
719  }
720  }
721 }
722 
723 void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
724  AutomatonConstraintProto& proto = *ct->mutable_automaton();
725 
726  if (proto.vars_size() == 0) {
727  const int64 initial_state = proto.starting_state();
728  for (const int64 final_state : proto.final_states()) {
729  if (initial_state == final_state) {
730  context->UpdateRuleStats("automaton: empty constraint");
731  ct->Clear();
732  return;
733  }
734  }
735  // The initial state is not in the final state. The model is unsat.
736  return (void)context->NotifyThatModelIsUnsat();
737  } else if (proto.transition_label_size() == 0) {
738  // Not transitions. The constraint is infeasible.
739  return (void)context->NotifyThatModelIsUnsat();
740  }
741 
742  const int n = proto.vars_size();
743  const std::vector<int> vars = {proto.vars().begin(), proto.vars().end()};
744 
745  // Compute the set of reachable state at each time point.
746  const absl::flat_hash_set<int64> final_states(
747  {proto.final_states().begin(), proto.final_states().end()});
748  std::vector<absl::flat_hash_set<int64>> reachable_states(n + 1);
749  reachable_states[0].insert(proto.starting_state());
750 
751  // Forward pass.
752  for (int time = 0; time < n; ++time) {
753  for (int t = 0; t < proto.transition_tail_size(); ++t) {
754  const int64 tail = proto.transition_tail(t);
755  const int64 label = proto.transition_label(t);
756  const int64 head = proto.transition_head(t);
757  if (!reachable_states[time].contains(tail)) continue;
758  if (!context->DomainContains(vars[time], label)) continue;
759  if (time == n - 1 && !final_states.contains(head)) continue;
760  reachable_states[time + 1].insert(head);
761  }
762  }
763 
764  // Backward pass.
765  for (int time = n - 1; time >= 0; --time) {
766  absl::flat_hash_set<int64> new_set;
767  for (int t = 0; t < proto.transition_tail_size(); ++t) {
768  const int64 tail = proto.transition_tail(t);
769  const int64 label = proto.transition_label(t);
770  const int64 head = proto.transition_head(t);
771 
772  if (!reachable_states[time].contains(tail)) continue;
773  if (!context->DomainContains(vars[time], label)) continue;
774  if (!reachable_states[time + 1].contains(head)) continue;
775  new_set.insert(tail);
776  }
777  reachable_states[time].swap(new_set);
778  }
779 
780  // We will model at each time step the current automaton state using Boolean
781  // variables. We will have n+1 time step. At time zero, we start in the
782  // initial state, and at time n we should be in one of the final states. We
783  // don't need to create Booleans at at time when there is just one possible
784  // state (like at time zero).
785  absl::flat_hash_map<int64, int> encoding;
786  absl::flat_hash_map<int64, int> in_encoding;
787  absl::flat_hash_map<int64, int> out_encoding;
788  bool removed_values = false;
789 
790  for (int time = 0; time < n; ++time) {
791  // All these vector have the same size. We will use them to enforce a
792  // local table constraint representing one step of the automaton at the
793  // given time.
794  std::vector<int64> in_states;
795  std::vector<int64> transition_values;
796  std::vector<int64> out_states;
797  for (int i = 0; i < proto.transition_label_size(); ++i) {
798  const int64 tail = proto.transition_tail(i);
799  const int64 label = proto.transition_label(i);
800  const int64 head = proto.transition_head(i);
801 
802  if (!reachable_states[time].contains(tail)) continue;
803  if (!reachable_states[time + 1].contains(head)) continue;
804  if (!context->DomainContains(vars[time], label)) continue;
805 
806  // TODO(user): if this transition correspond to just one in-state or
807  // one-out state or one variable value, we could reuse the corresponding
808  // Boolean variable instead of creating a new one!
809  in_states.push_back(tail);
810  transition_values.push_back(label);
811 
812  // On the last step we don't need to distinguish the output states, so
813  // we use zero.
814  out_states.push_back(time + 1 == n ? 0 : head);
815  }
816 
817  std::vector<int> tuple_literals;
818  if (transition_values.size() == 1) {
819  bool tmp_removed_values = false;
820  tuple_literals.push_back(context->GetOrCreateConstantVar(1));
821  CHECK_EQ(reachable_states[time + 1].size(), 1);
822  if (!context->IntersectDomainWith(vars[time],
823  Domain(transition_values.front()),
824  &tmp_removed_values)) {
825  return (void)context->NotifyThatModelIsUnsat();
826  }
827  in_encoding.clear();
828  continue;
829  } else if (transition_values.size() == 2) {
830  const int bool_var = context->NewBoolVar();
831  tuple_literals.push_back(bool_var);
832  tuple_literals.push_back(NegatedRef(bool_var));
833  } else {
834  // Note that we do not need the ExactlyOneConstraint(tuple_literals)
835  // because it is already implicitly encoded since we have exactly one
836  // transition value.
837  LinearConstraintProto* const exactly_one =
838  context->working_model->add_constraints()->mutable_linear();
839  exactly_one->add_domain(1);
840  exactly_one->add_domain(1);
841  for (int i = 0; i < transition_values.size(); ++i) {
842  const int tuple_literal = context->NewBoolVar();
843  tuple_literals.push_back(tuple_literal);
844  exactly_one->add_vars(tuple_literal);
845  exactly_one->add_coeffs(1);
846  }
847  }
848 
849  // Fully encode vars[time].
850  {
851  std::vector<int64> s = transition_values;
853 
854  encoding.clear();
855  if (!context->IntersectDomainWith(vars[time], Domain::FromValues(s),
856  &removed_values)) {
857  return (void)context->NotifyThatModelIsUnsat();
858  }
859 
860  // Fully encode the variable.
861  for (const ClosedInterval& interval : context->DomainOf(vars[time])) {
862  for (int64 v = interval.start; v <= interval.end; ++v) {
863  encoding[v] = context->GetOrCreateVarValueEncoding(vars[time], v);
864  }
865  }
866  }
867 
868  // For each possible out states, create one Boolean variable.
869  {
870  std::vector<int64> s = out_states;
872 
873  out_encoding.clear();
874  if (s.size() == 2) {
875  const int var = context->NewBoolVar();
876  out_encoding[s.front()] = var;
877  out_encoding[s.back()] = NegatedRef(var);
878  } else if (s.size() > 2) {
879  for (const int64 state : s) {
880  out_encoding[state] = context->NewBoolVar();
881  }
882  }
883  }
884 
885  if (!in_encoding.empty()) {
886  LinkLiteralsAndValues(tuple_literals, in_states, in_encoding, context);
887  }
888  if (!encoding.empty()) {
889  LinkLiteralsAndValues(tuple_literals, transition_values, encoding,
890  context);
891  }
892  if (!out_encoding.empty()) {
893  LinkLiteralsAndValues(tuple_literals, out_states, out_encoding, context);
894  }
895  in_encoding.swap(out_encoding);
896  out_encoding.clear();
897  }
898 
899  if (removed_values) {
900  context->UpdateRuleStats("automaton: reduced variable domains");
901  }
902  context->UpdateRuleStats("automaton: expanded");
903  ct->Clear();
904 }
905 
906 void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) {
907  TableConstraintProto& table = *ct->mutable_table();
908  const int num_vars = table.vars_size();
909  const int num_original_tuples = table.values_size() / num_vars;
910  std::vector<std::vector<int64>> tuples(num_original_tuples);
911  int count = 0;
912  for (int i = 0; i < num_original_tuples; ++i) {
913  for (int j = 0; j < num_vars; ++j) {
914  tuples[i].push_back(table.values(count++));
915  }
916  }
917 
918  if (tuples.empty()) { // Early exit.
919  context->UpdateRuleStats("table: empty negated constraint");
920  ct->Clear();
921  return;
922  }
923 
924  // Compress tuples.
925  const int64 any_value = kint64min;
926  std::vector<int64> domain_sizes;
927  for (int i = 0; i < num_vars; ++i) {
928  domain_sizes.push_back(context->DomainOf(table.vars(i)).Size());
929  }
930  CompressTuples(domain_sizes, any_value, &tuples);
931 
932  // For each tuple, forbid the variables values to be this tuple.
933  std::vector<int> clause;
934  for (const std::vector<int64>& tuple : tuples) {
935  clause.clear();
936  for (int i = 0; i < num_vars; ++i) {
937  const int64 value = tuple[i];
938  if (value == any_value) continue;
939 
940  const int literal =
941  context->GetOrCreateVarValueEncoding(table.vars(i), value);
942  clause.push_back(NegatedRef(literal));
943  }
944  if (!clause.empty()) {
945  BoolArgumentProto* bool_or =
946  context->working_model->add_constraints()->mutable_bool_or();
947  for (const int lit : clause) {
948  bool_or->add_literals(lit);
949  }
950  }
951  }
952  context->UpdateRuleStats("table: expanded negated constraint");
953  ct->Clear();
954 }
955 
956 void ExpandLinMin(ConstraintProto* ct, PresolveContext* context) {
957  ConstraintProto* const lin_max = context->working_model->add_constraints();
958  for (int i = 0; i < ct->enforcement_literal_size(); ++i) {
959  lin_max->add_enforcement_literal(ct->enforcement_literal(i));
960  }
961 
962  // Target
963  SetToNegatedLinearExpression(ct->lin_min().target(),
964  lin_max->mutable_lin_max()->mutable_target());
965 
966  for (int i = 0; i < ct->lin_min().exprs_size(); ++i) {
967  LinearExpressionProto* const expr = lin_max->mutable_lin_max()->add_exprs();
968  SetToNegatedLinearExpression(ct->lin_min().exprs(i), expr);
969  }
970  ct->Clear();
971 }
972 
973 // Add the implications and clauses to link one variable of a table to the
974 // literals controling if the tuples are possible or not. The parallel vectors
975 // (tuple_literals, values) contains all valid projected tuples. The
976 // tuples_with_any vector provides a list of tuple_literals that will support
977 // any value.
978 void ProcessOneVariable(const std::vector<int>& tuple_literals,
979  const std::vector<int64>& values, int variable,
980  const std::vector<int>& tuples_with_any,
981  PresolveContext* context) {
982  VLOG(2) << "Process var(" << variable << ") with domain "
983  << context->DomainOf(variable) << " and " << values.size()
984  << " active tuples, and " << tuples_with_any.size() << " any tuples";
985  CHECK_EQ(tuple_literals.size(), values.size());
986  std::vector<std::pair<int64, int>> pairs;
987 
988  // Collect pairs of value-literal.
989  for (int i = 0; i < values.size(); ++i) {
990  const int64 value = values[i];
991  CHECK(context->DomainContains(variable, value));
992  pairs.emplace_back(value, tuple_literals[i]);
993  }
994 
995  // Regroup literal with the same value and add for each the clause: If all the
996  // tuples containing a value are false, then this value must be false too.
997  std::vector<int> selected;
998  std::sort(pairs.begin(), pairs.end());
999  for (int i = 0; i < pairs.size();) {
1000  selected.clear();
1001  const int64 value = pairs[i].first;
1002  for (; i < pairs.size() && pairs[i].first == value; ++i) {
1003  selected.push_back(pairs[i].second);
1004  }
1005 
1006  CHECK(!selected.empty() || !tuples_with_any.empty());
1007  if (selected.size() == 1 && tuples_with_any.empty()) {
1008  context->InsertVarValueEncoding(selected.front(), variable, value);
1009  } else {
1010  const int value_literal =
1011  context->GetOrCreateVarValueEncoding(variable, value);
1012  BoolArgumentProto* no_support =
1013  context->working_model->add_constraints()->mutable_bool_or();
1014  for (const int lit : selected) {
1015  no_support->add_literals(lit);
1016  context->AddImplication(lit, value_literal);
1017  }
1018  for (const int lit : tuples_with_any) {
1019  no_support->add_literals(lit);
1020  }
1021 
1022  // And the "value" literal.
1023  no_support->add_literals(NegatedRef(value_literal));
1024  }
1025  }
1026 }
1027 
1028 // Simpler encoding for table constraints with 2 variables.
1029 void AddSizeTwoTable(
1030  const std::vector<int>& vars, const std::vector<std::vector<int64>>& tuples,
1031  const std::vector<absl::flat_hash_set<int64>>& values_per_var,
1032  PresolveContext* context) {
1033  CHECK_EQ(vars.size(), 2);
1034  const int left_var = vars[0];
1035  const int right_var = vars[1];
1036  if (context->DomainOf(left_var).Size() == 1 ||
1037  context->DomainOf(right_var).Size() == 1) {
1038  // A table constraint with at most one variable not fixed is trivially
1039  // enforced after domain reduction.
1040  return;
1041  }
1042 
1043  std::map<int, std::vector<int>> left_to_right;
1044  std::map<int, std::vector<int>> right_to_left;
1045 
1046  for (const auto& tuple : tuples) {
1047  const int64 left_value(tuple[0]);
1048  const int64 right_value(tuple[1]);
1049  CHECK(context->DomainContains(left_var, left_value));
1050  CHECK(context->DomainContains(right_var, right_value));
1051 
1052  const int left_literal =
1053  context->GetOrCreateVarValueEncoding(left_var, left_value);
1054  const int right_literal =
1055  context->GetOrCreateVarValueEncoding(right_var, right_value);
1056  left_to_right[left_literal].push_back(right_literal);
1057  right_to_left[right_literal].push_back(left_literal);
1058  }
1059 
1060  int num_implications = 0;
1061  int num_clause_added = 0;
1062  int num_large_clause_added = 0;
1063  auto add_support_constraint =
1064  [context, &num_clause_added, &num_large_clause_added, &num_implications](
1065  int lit, const std::vector<int>& support_literals,
1066  int max_support_size) {
1067  if (support_literals.size() == max_support_size) return;
1068  if (support_literals.size() == 1) {
1069  context->AddImplication(lit, support_literals.front());
1070  num_implications++;
1071  } else {
1072  BoolArgumentProto* bool_or =
1073  context->working_model->add_constraints()->mutable_bool_or();
1074  for (const int support_literal : support_literals) {
1075  bool_or->add_literals(support_literal);
1076  }
1077  bool_or->add_literals(NegatedRef(lit));
1078  num_clause_added++;
1079  if (support_literals.size() > max_support_size / 2) {
1080  num_large_clause_added++;
1081  }
1082  }
1083  };
1084 
1085  for (const auto& it : left_to_right) {
1086  add_support_constraint(it.first, it.second, values_per_var[1].size());
1087  }
1088  for (const auto& it : right_to_left) {
1089  add_support_constraint(it.first, it.second, values_per_var[0].size());
1090  }
1091  VLOG(2) << "Table: 2 variables, " << tuples.size() << " tuples encoded using "
1092  << num_clause_added << " clauses, including "
1093  << num_large_clause_added << " large clauses, " << num_implications
1094  << " implications";
1095 }
1096 
1097 void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) {
1098  const TableConstraintProto& table = ct->table();
1099  const std::vector<int> vars(table.vars().begin(), table.vars().end());
1100  const int num_vars = table.vars_size();
1101  const int num_original_tuples = table.values_size() / num_vars;
1102 
1103  // Read tuples flat array and recreate the vector of tuples.
1104  std::vector<std::vector<int64>> tuples(num_original_tuples);
1105  int count = 0;
1106  for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
1107  for (int var_index = 0; var_index < num_vars; ++var_index) {
1108  tuples[tuple_index].push_back(table.values(count++));
1109  }
1110  }
1111 
1112  // Compute the set of possible values for each variable (from the table).
1113  // Remove invalid tuples along the way.
1114  std::vector<absl::flat_hash_set<int64>> values_per_var(num_vars);
1115  int new_size = 0;
1116  for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
1117  bool keep = true;
1118  for (int var_index = 0; var_index < num_vars; ++var_index) {
1119  const int64 value = tuples[tuple_index][var_index];
1120  if (!context->DomainContains(vars[var_index], value)) {
1121  keep = false;
1122  break;
1123  }
1124  }
1125  if (keep) {
1126  for (int var_index = 0; var_index < num_vars; ++var_index) {
1127  values_per_var[var_index].insert(tuples[tuple_index][var_index]);
1128  }
1129  std::swap(tuples[tuple_index], tuples[new_size]);
1130  new_size++;
1131  }
1132  }
1133  tuples.resize(new_size);
1134  const int num_valid_tuples = tuples.size();
1135 
1136  if (tuples.empty()) {
1137  context->UpdateRuleStats("table: empty");
1138  return (void)context->NotifyThatModelIsUnsat();
1139  }
1140 
1141  // Update variable domains. It is redundant with presolve, but we could be
1142  // here with presolve = false.
1143  // Also counts the number of fixed variables.
1144  int num_fixed_variables = 0;
1145  for (int var_index = 0; var_index < num_vars; ++var_index) {
1146  CHECK(context->IntersectDomainWith(
1147  vars[var_index],
1148  Domain::FromValues({values_per_var[var_index].begin(),
1149  values_per_var[var_index].end()})));
1150  if (context->DomainOf(vars[var_index]).Size() == 1) {
1151  num_fixed_variables++;
1152  }
1153  }
1154 
1155  if (num_fixed_variables == num_vars - 1) {
1156  context->UpdateRuleStats("table: one variable not fixed");
1157  ct->Clear();
1158  return;
1159  } else if (num_fixed_variables == num_vars) {
1160  context->UpdateRuleStats("table: all variables fixed");
1161  ct->Clear();
1162  return;
1163  }
1164 
1165  // Tables with two variables do not need tuple literals.
1166  if (num_vars == 2) {
1167  AddSizeTwoTable(vars, tuples, values_per_var, context);
1168  context->UpdateRuleStats(
1169  "table: expanded positive constraint with two variables");
1170  ct->Clear();
1171  return;
1172  }
1173 
1174  // It is easier to compute this before compression, as compression will merge
1175  // tuples.
1176  int num_prefix_tuples = 0;
1177  {
1178  absl::flat_hash_set<absl::Span<const int64>> prefixes;
1179  for (const std::vector<int64>& tuple : tuples) {
1180  prefixes.insert(absl::MakeSpan(tuple.data(), num_vars - 1));
1181  }
1182  num_prefix_tuples = prefixes.size();
1183  }
1184 
1185  // TODO(user): reinvestigate ExploreSubsetOfVariablesAndAddNegatedTables.
1186 
1187  // Compress tuples.
1188  const int64 any_value = kint64min;
1189  std::vector<int64> domain_sizes;
1190  for (int i = 0; i < num_vars; ++i) {
1191  domain_sizes.push_back(values_per_var[i].size());
1192  }
1193  CompressTuples(domain_sizes, any_value, &tuples);
1194  const int num_compressed_tuples = tuples.size();
1195 
1196  if (num_compressed_tuples == 1) {
1197  // Domains are propagated. We can remove the constraint.
1198  context->UpdateRuleStats("table: one tuple");
1199  ct->Clear();
1200  return;
1201  }
1202 
1203  // Detect if prefix tuples are all different.
1204  const bool prefixes_are_all_different = num_prefix_tuples == num_valid_tuples;
1205  if (prefixes_are_all_different) {
1206  context->UpdateRuleStats(
1207  "TODO table: last value implied by previous values");
1208  }
1209  // TODO(user): if 2 table constraints share the same valid prefix, the
1210  // tuple literals can be reused.
1211  // TODO(user): investigate different encoding for prefix tables. Maybe
1212  // we can remove the need to create tuple literals.
1213 
1214  // Debug message to log the status of the expansion.
1215  if (VLOG_IS_ON(2)) {
1216  // Compute the maximum number of prefix tuples.
1217  int64 max_num_prefix_tuples = 1;
1218  for (int var_index = 0; var_index + 1 < num_vars; ++var_index) {
1219  max_num_prefix_tuples =
1220  CapProd(max_num_prefix_tuples, values_per_var[var_index].size());
1221  }
1222 
1223  std::string message =
1224  absl::StrCat("Table: ", num_vars,
1225  " variables, original tuples = ", num_original_tuples);
1226  if (num_valid_tuples != num_original_tuples) {
1227  absl::StrAppend(&message, ", valid tuples = ", num_valid_tuples);
1228  }
1229  if (prefixes_are_all_different) {
1230  if (num_prefix_tuples < max_num_prefix_tuples) {
1231  absl::StrAppend(&message, ", partial prefix = ", num_prefix_tuples, "/",
1232  max_num_prefix_tuples);
1233  } else {
1234  absl::StrAppend(&message, ", full prefix = true");
1235  }
1236  } else {
1237  absl::StrAppend(&message, ", num prefix tuples = ", num_prefix_tuples);
1238  }
1239  if (num_compressed_tuples != num_valid_tuples) {
1240  absl::StrAppend(&message,
1241  ", compressed tuples = ", num_compressed_tuples);
1242  }
1243  VLOG(2) << message;
1244  }
1245 
1246  // Log if we have only two tuples.
1247  if (num_compressed_tuples == 2) {
1248  context->UpdateRuleStats("TODO table: two tuples");
1249  }
1250 
1251  // Create one Boolean variable per tuple to indicate if it can still be
1252  // selected or not. Note that we don't enforce exactly one tuple to be
1253  // selected as this is costly.
1254  //
1255  // TODO(user): Investigate adding the at_most_one if the number of tuples
1256  // is small.
1257  // TODO(user): Investigate it we could recover a linear constraint:
1258  // var = sum(tuple_literals[i] * values[i])
1259  // It could be done here or along the deductions grouping.
1260  std::vector<int> tuple_literals(num_compressed_tuples);
1261  BoolArgumentProto* at_least_one_tuple =
1262  context->working_model->add_constraints()->mutable_bool_or();
1263 
1264  // If we want to enumerate all solutions, we should not add new variables that
1265  // can take more than one value for a given feasible solution, otherwise we
1266  // will have a lot more solution than needed.
1267  //
1268  // TODO(user): Alternatively, we could mark those variable so that their
1269  // value do not count when excluding solution, but we do not have a
1270  // mecanism for that yet. It might not be easy to track them down when we
1271  // replace them with equivalent variable too.
1272  //
1273  // TODO(user): We use keep_all_feasible_solutions as a proxy for enumerate
1274  // all solution, but the concept are slightly different though.
1275  BoolArgumentProto* at_most_one_tuple = nullptr;
1276  if (context->keep_all_feasible_solutions) {
1277  at_most_one_tuple =
1278  context->working_model->add_constraints()->mutable_at_most_one();
1279  }
1280 
1281  for (int var_index = 0; var_index < num_compressed_tuples; ++var_index) {
1282  tuple_literals[var_index] = context->NewBoolVar();
1283  at_least_one_tuple->add_literals(tuple_literals[var_index]);
1284  if (at_most_one_tuple != nullptr) {
1285  at_most_one_tuple->add_literals(tuple_literals[var_index]);
1286  }
1287  }
1288 
1289  std::vector<int> active_tuple_literals;
1290  std::vector<int64> active_values;
1291  std::vector<int> any_tuple_literals;
1292  for (int var_index = 0; var_index < num_vars; ++var_index) {
1293  if (values_per_var[var_index].size() == 1) continue;
1294 
1295  active_tuple_literals.clear();
1296  active_values.clear();
1297  any_tuple_literals.clear();
1298  for (int tuple_index = 0; tuple_index < tuple_literals.size();
1299  ++tuple_index) {
1300  const int64 value = tuples[tuple_index][var_index];
1301  const int tuple_literal = tuple_literals[tuple_index];
1302 
1303  if (value == any_value) {
1304  any_tuple_literals.push_back(tuple_literal);
1305  } else {
1306  active_tuple_literals.push_back(tuple_literal);
1307  active_values.push_back(value);
1308  }
1309  }
1310 
1311  if (!active_tuple_literals.empty()) {
1312  ProcessOneVariable(active_tuple_literals, active_values, vars[var_index],
1313  any_tuple_literals, context);
1314  }
1315  }
1316 
1317  context->UpdateRuleStats("table: expanded positive constraint");
1318  ct->Clear();
1319 }
1320 
1321 void ExpandAllDiff(bool expand_non_permutations, ConstraintProto* ct,
1322  PresolveContext* context) {
1323  AllDifferentConstraintProto& proto = *ct->mutable_all_diff();
1324  if (proto.vars_size() <= 2) return;
1325 
1326  const int num_vars = proto.vars_size();
1327 
1328  Domain union_of_domains = context->DomainOf(proto.vars(0));
1329  for (int i = 1; i < num_vars; ++i) {
1330  union_of_domains =
1331  union_of_domains.UnionWith(context->DomainOf(proto.vars(i)));
1332  }
1333 
1334  const bool is_permutation = proto.vars_size() == union_of_domains.Size();
1335 
1336  if (!is_permutation && !expand_non_permutations) return;
1337 
1338  // Collect all possible variables that can take each value, and add one linear
1339  // equation per value stating that this value can be assigned at most once, or
1340  // exactly once in case of permutation.
1341  for (const ClosedInterval& interval : union_of_domains) {
1342  for (int64 v = interval.start; v <= interval.end; ++v) {
1343  // Collect references which domain contains v.
1344  std::vector<int> possible_refs;
1345  int fixed_variable_count = 0;
1346  for (const int ref : proto.vars()) {
1347  if (!context->DomainContains(ref, v)) continue;
1348  possible_refs.push_back(ref);
1349  if (context->DomainOf(ref).Size() == 1) {
1350  fixed_variable_count++;
1351  }
1352  }
1353 
1354  if (fixed_variable_count > 1) {
1355  // Violates the definition of AllDifferent.
1356  return (void)context->NotifyThatModelIsUnsat();
1357  } else if (fixed_variable_count == 1) {
1358  // Remove values from other domains.
1359  for (const int ref : possible_refs) {
1360  if (context->DomainOf(ref).Size() == 1) continue;
1361  if (!context->IntersectDomainWith(ref, Domain(v).Complement())) {
1362  VLOG(1) << "Empty domain for a variable in ExpandAllDiff()";
1363  return;
1364  }
1365  }
1366  }
1367 
1368  LinearConstraintProto* at_most_or_equal_one =
1369  context->working_model->add_constraints()->mutable_linear();
1370  int lb = is_permutation ? 1 : 0;
1371  int ub = 1;
1372  for (const int ref : possible_refs) {
1373  DCHECK(context->DomainContains(ref, v));
1374  DCHECK_GT(context->DomainOf(ref).Size(), 1);
1375  const int encoding = context->GetOrCreateVarValueEncoding(ref, v);
1376  if (RefIsPositive(encoding)) {
1377  at_most_or_equal_one->add_vars(encoding);
1378  at_most_or_equal_one->add_coeffs(1);
1379  } else {
1380  at_most_or_equal_one->add_vars(PositiveRef(encoding));
1381  at_most_or_equal_one->add_coeffs(-1);
1382  lb--;
1383  ub--;
1384  }
1385  }
1386  at_most_or_equal_one->add_domain(lb);
1387  at_most_or_equal_one->add_domain(ub);
1388  }
1389  }
1390  if (is_permutation) {
1391  context->UpdateRuleStats("alldiff: permutation expanded");
1392  } else {
1393  context->UpdateRuleStats("alldiff: expanded");
1394  }
1395  ct->Clear();
1396 }
1397 
1398 } // namespace
1399 
1401  if (context->params().disable_constraint_expansion()) return;
1402 
1403  if (context->ModelIsUnsat()) return;
1404 
1405  // Make sure all domains are initialized.
1406  context->InitializeNewDomains();
1407 
1408  // Clear the precedence cache.
1409  context->ClearPrecedenceCache();
1410 
1411  const int num_constraints = context->working_model->constraints_size();
1412  for (int i = 0; i < num_constraints; ++i) {
1413  ConstraintProto* const ct = context->working_model->mutable_constraints(i);
1414  bool skip = false;
1415  switch (ct->constraint_case()) {
1416  case ConstraintProto::ConstraintCase::kReservoir:
1417  if (context->params().expand_reservoir_constraints()) {
1418  ExpandReservoir(ct, context);
1419  }
1420  break;
1421  case ConstraintProto::ConstraintCase::kIntMod:
1422  ExpandIntMod(ct, context);
1423  break;
1424  case ConstraintProto::ConstraintCase::kIntDiv:
1425  ExpandIntDiv(ct, context);
1426  break;
1427  case ConstraintProto::ConstraintCase::kIntProd:
1428  ExpandIntProd(ct, context);
1429  break;
1430  case ConstraintProto::ConstraintCase::kLinMin:
1431  ExpandLinMin(ct, context);
1432  break;
1433  case ConstraintProto::ConstraintCase::kElement:
1434  if (context->params().expand_element_constraints()) {
1435  ExpandElement(ct, context);
1436  }
1437  break;
1438  case ConstraintProto::ConstraintCase::kInverse:
1439  ExpandInverse(ct, context);
1440  break;
1441  case ConstraintProto::ConstraintCase::kAutomaton:
1442  if (context->params().expand_automaton_constraints()) {
1443  ExpandAutomaton(ct, context);
1444  }
1445  break;
1446  case ConstraintProto::ConstraintCase::kTable:
1447  if (ct->table().negated()) {
1448  ExpandNegativeTable(ct, context);
1449  } else if (context->params().expand_table_constraints()) {
1450  ExpandPositiveTable(ct, context);
1451  }
1452  break;
1453  case ConstraintProto::ConstraintCase::kAllDiff:
1454  ExpandAllDiff(context->params().expand_alldiff_constraints(), ct,
1455  context);
1456  break;
1457  default:
1458  skip = true;
1459  break;
1460  }
1461  if (skip) continue; // Nothing was done for this constraint.
1462 
1463  // Update variable-contraint graph.
1464  context->UpdateNewConstraintsVariableUsage();
1465  if (ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
1466  context->UpdateConstraintVariableUsage(i);
1467  }
1468 
1469  // Early exit if the model is unsat.
1470  if (context->ModelIsUnsat()) {
1471  if (VLOG_IS_ON(1) || context->params().log_search_progress()) {
1472  LOG(INFO) << "UNSAT after expansion of "
1474  }
1475  return;
1476  }
1477  }
1478 
1479  // The precedence cache can become invalid during presolve as it does not
1480  // handle variable substitution. It is safer just to clear it at the end
1481  // of the expansion phase.
1482  context->ClearPrecedenceCache();
1483 
1484  // Make sure the context is consistent.
1485  context->InitializeNewDomains();
1486 
1487  // Update any changed domain from the context.
1488  for (int i = 0; i < context->working_model->variables_size(); ++i) {
1489  FillDomainInProto(context->DomainOf(i),
1490  context->working_model->mutable_variables(i));
1491  }
1492 }
1493 
1494 } // namespace sat
1495 } // namespace operations_research
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#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 VLOG(verboselevel)
Definition: base/logging.h:978
Domain Complement() const
Returns the set Int64 ∖ D.
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
CpModelProto proto
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
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
bool RefIsPositive(int ref)
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
void ExpandCpModel(PresolveContext *context)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
void CompressTuples(absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 >> *tuples)
Definition: sat/util.cc:112
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapSub(int64 x, int64 y)
std::string ProtobufShortDebugString(const P &message)
int64 CapProd(int64 x, int64 y)
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
int64 demand
Definition: resource.cc:123
int64 delta
Definition: resource.cc:1684
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
std::string message
Definition: trace.cc:395
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41