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"
23#include "ortools/sat/cp_model.pb.h"
26#include "ortools/sat/util.h"
29
30namespace operations_research {
31namespace sat {
32namespace {
33
34void 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.
135void 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
142void 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
218void 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
237void 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.
251void 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
303void 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
339void 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
392void 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
481void 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.
674void 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
723void 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
906void 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
956void 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.
978void 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.
1029void 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
1097void 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
1321void 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
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
void ExpandCpModel(PresolveContext *context)
bool RefIsPositive(int ref)
void CompressTuples(absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 > > *tuples)
Definition: sat/util.cc:112
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapProd(int64 x, int64 y)
int64 CapSub(int64 x, int64 y)
std::string ProtobufShortDebugString(const P &message)
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