Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_expand.cc
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <algorithm>
17#include <cstdint>
18#include <deque>
19#include <limits>
20#include <optional>
21#include <string>
22#include <utility>
23#include <vector>
24
25#include "absl/algorithm/container.h"
26#include "absl/container/btree_map.h"
27#include "absl/container/flat_hash_map.h"
28#include "absl/container/flat_hash_set.h"
29#include "absl/container/inlined_vector.h"
30#include "absl/log/check.h"
31#include "absl/meta/type_traits.h"
32#include "absl/strings/str_cat.h"
33#include "absl/types/span.h"
34#include "google/protobuf/message.h"
45#include "ortools/sat/util.h"
48
49namespace operations_research {
50namespace sat {
51namespace {
52
53// Different encoding that support general demands. This is usually a pretty bad
54// encoding, at least until we improve the solver on such models.
55void ExpandReservoirUsingCircuit(int64_t sum_of_positive_demand,
56 int64_t sum_of_negative_demand,
57 ConstraintProto* reservoir_ct,
58 PresolveContext* context) {
59 const ReservoirConstraintProto& reservoir = reservoir_ct->reservoir();
60 const int num_events = reservoir.time_exprs_size();
61
62 // The encoding will create a circuit constraint, and one integer variable per
63 // event (representing the level at that event time).
64 CircuitConstraintProto* circuit =
65 context->working_model->add_constraints()->mutable_circuit();
66
67 const int64_t var_min =
68 std::max(reservoir.min_level(), sum_of_negative_demand);
69 const int64_t var_max =
70 std::min(reservoir.max_level(), sum_of_positive_demand);
71 std::vector<int> level_vars(num_events);
72 for (int i = 0; i < num_events; ++i) {
73 level_vars[i] = context->NewIntVar(Domain(var_min, var_max));
74 }
75
76 // For the corner case where all events are absent, we need a potential
77 // self-arc on the start/end circuit node.
78 {
79 const int all_inactive = context->NewBoolVar("reservoir expansion");
80 circuit->add_tails(num_events);
81 circuit->add_heads(num_events);
82 circuit->add_literals(all_inactive);
83 }
84
85 for (int i = 0; i < num_events; ++i) {
86 if (!reservoir.active_literals().empty()) {
87 // Add self arc to represent absence.
88 circuit->add_tails(i);
89 circuit->add_heads(i);
90 circuit->add_literals(NegatedRef(reservoir.active_literals(i)));
91 }
92
93 // We need an extra circuit node for start/end of circuit.
94 // We use the available index 'num_events'.
95 {
96 // Circuit starts at i, level_vars[i] == demand_expr[i].
97 const int start_var = context->NewBoolVar("reservoir expansion");
98 circuit->add_tails(num_events);
99 circuit->add_heads(i);
100 circuit->add_literals(start_var);
101
102 // Add enforced linear for demand.
103 {
104 ConstraintProto* new_ct = context->working_model->add_constraints();
105 new_ct->add_enforcement_literal(start_var);
106 LinearConstraintProto* lin = new_ct->mutable_linear();
107 lin->add_domain(0);
108 lin->add_domain(0);
109 lin->add_vars(level_vars[i]);
110 lin->add_coeffs(1);
111 AddLinearExpressionToLinearConstraint(reservoir.level_changes(i), -1,
112 lin);
113 context->CanonicalizeLinearConstraint(new_ct);
114 }
115
116 // Circuit ends at i, no extra constraint there.
117 const int end_var = context->NewBoolVar("reservoir expansion");
118 circuit->add_tails(i);
119 circuit->add_heads(num_events);
120 circuit->add_literals(end_var);
121 }
122
123 for (int j = 0; j < num_events; ++j) {
124 if (i == j) continue;
125
126 // If arc_i_j is true then:
127 // - active_i is true (enforced by circuit).
128 // - active_j is true (enforced by circuit).
129 // - time_i <= time_j
130 // - level_j == level_i + demand_j
131 //
132 // TODO(user): Unfortunately we cannot share these literal between
133 // reservoir except if the set of time point is exactly the same!
134 // otherwise if we miss one, then A "after" B in one circuit do not
135 // implies that there is no C in between in another!
136 const int arc_i_j = context->NewBoolVar("reservoir expansion");
137 circuit->add_tails(i);
138 circuit->add_heads(j);
139 circuit->add_literals(arc_i_j);
140
141 // Add enforced linear for time.
142 {
143 ConstraintProto* new_ct = context->working_model->add_constraints();
144 new_ct->add_enforcement_literal(arc_i_j);
145 LinearConstraintProto* lin = new_ct->mutable_linear();
146 lin->add_domain(0);
147 lin->add_domain(std::numeric_limits<int64_t>::max());
148 AddLinearExpressionToLinearConstraint(reservoir.time_exprs(j), 1, lin);
149 AddLinearExpressionToLinearConstraint(reservoir.time_exprs(i), -1, lin);
150 context->CanonicalizeLinearConstraint(new_ct);
151 }
152
153 // Add enforced linear for demand.
154 {
155 ConstraintProto* new_ct = context->working_model->add_constraints();
156 new_ct->add_enforcement_literal(arc_i_j);
157 LinearConstraintProto* lin = new_ct->mutable_linear();
158 lin->add_domain(0);
159 lin->add_domain(0);
160 lin->add_vars(level_vars[j]);
161 lin->add_coeffs(1);
162 lin->add_vars(level_vars[i]);
163 lin->add_coeffs(-1);
164 AddLinearExpressionToLinearConstraint(reservoir.level_changes(j), -1,
165 lin);
166 context->CanonicalizeLinearConstraint(new_ct);
167 }
168 }
169 }
170 context->solution_crush().SetReservoirCircuitVars(reservoir, var_min, var_max,
171 level_vars, *circuit);
172
173 reservoir_ct->Clear();
174 context->UpdateRuleStats("reservoir: expanded using circuit.");
175}
176
177void ExpandReservoirUsingPrecedences(bool max_level_is_constraining,
178 bool min_level_is_constraining,
179 ConstraintProto* reservoir_ct,
180 PresolveContext* context) {
181 const ReservoirConstraintProto& reservoir = reservoir_ct->reservoir();
182 const int num_events = reservoir.time_exprs_size();
183 const int true_literal = context->GetTrueLiteral();
184 const auto is_active_literal = [&reservoir, true_literal](int index) {
185 if (reservoir.active_literals_size() == 0) return true_literal;
186 return reservoir.active_literals(index);
187 };
188
189 // Constrains the running level to be consistent at all time_exprs.
190 // For this we only add a constraint at the time a given demand take place.
191 for (int i = 0; i < num_events; ++i) {
192 const int active_i = is_active_literal(i);
193 if (context->LiteralIsFalse(active_i)) continue;
194
195 const int64_t demand_i = context->FixedValue(reservoir.level_changes(i));
196 if (demand_i == 0) continue;
197
198 // No need for some constraints if the reservoir is just constrained in
199 // one direction.
200 if (demand_i > 0 && !max_level_is_constraining) continue;
201 if (demand_i < 0 && !min_level_is_constraining) continue;
202
203 ConstraintProto* new_cumul = context->working_model->add_constraints();
204 LinearConstraintProto* new_linear = new_cumul->mutable_linear();
205 int64_t offset = 0;
206
207 // Add contributions from events that happened at time_j <= time_i.
208 const LinearExpressionProto& time_i = reservoir.time_exprs(i);
209 for (int j = 0; j < num_events; ++j) {
210 if (i == j) continue;
211 const int active_j = is_active_literal(j);
212 if (context->LiteralIsFalse(active_j)) continue;
213 const int64_t demand_j = context->FixedValue(reservoir.level_changes(j));
214 if (demand_j == 0) continue;
215
216 // Get or create the literal equivalent to
217 // active_i && active_j && time[j] <= time[i].
218 //
219 // TODO(user): we could get rid of active_i in the equivalence above.
220 // Experiments when we have enough benchmarks.
221 const LinearExpressionProto& time_j = reservoir.time_exprs(j);
222 const int j_lesseq_i = context->GetOrCreateReifiedPrecedenceLiteral(
223 time_j, time_i, active_j, active_i);
224 AddWeightedLiteralToLinearConstraint(j_lesseq_i, demand_j, new_linear,
225 &offset);
226 }
227
228 // Add contribution from event i.
229 //
230 // TODO(user): Alternatively we can mark the whole constraint as enforced
231 // only if active_i is true. Experiments with both version, right now we
232 // miss enough benchmarks to conclude.
233 AddWeightedLiteralToLinearConstraint(active_i, demand_i, new_linear,
234 &offset);
235
236 // Note that according to the sign of demand_i, we only need one side.
237 // We apply the offset here to make sure we use int64_t min and max.
238 if (demand_i > 0) {
239 new_linear->add_domain(std::numeric_limits<int64_t>::min());
240 new_linear->add_domain(reservoir.max_level() - offset);
241 } else {
242 new_linear->add_domain(reservoir.min_level() - offset);
243 new_linear->add_domain(std::numeric_limits<int64_t>::max());
244 }
245
246 // Canonicalize the newly created constraint.
247 context->CanonicalizeLinearConstraint(new_cumul);
248
249 DCHECK(!PossibleIntegerOverflow(*context->working_model, new_linear->vars(),
250 new_linear->coeffs()));
251 }
252
253 reservoir_ct->Clear();
254 context->UpdateRuleStats("reservoir: expanded using precedences");
255}
256
257void ExpandReservoir(ConstraintProto* reservoir_ct, PresolveContext* context) {
258 if (reservoir_ct->reservoir().min_level() >
259 reservoir_ct->reservoir().max_level()) {
260 VLOG(1) << "Empty level domain in reservoir constraint.";
261 return (void)context->NotifyThatModelIsUnsat();
262 }
263
264 const ReservoirConstraintProto& reservoir = reservoir_ct->reservoir();
265 const int num_events = reservoir.time_exprs_size();
266
267 int num_positives = 0;
268 int num_negatives = 0;
269 bool all_demands_are_fixed = true;
270 int64_t sum_of_positive_demand = 0;
271 int64_t sum_of_negative_demand = 0;
272 for (const LinearExpressionProto& demand_expr : reservoir.level_changes()) {
273 if (!context->IsFixed(demand_expr)) {
274 all_demands_are_fixed = false;
275 }
276 const int64_t max_demand = context->MaxOf(demand_expr);
277 if (max_demand > 0) {
278 num_positives++;
279 sum_of_positive_demand += max_demand;
280 }
281 const int64_t min_demand = context->MinOf(demand_expr);
282 if (min_demand < 0) {
283 num_negatives++;
284 sum_of_negative_demand += min_demand;
285 }
286 }
287
288 if (sum_of_negative_demand >= reservoir.min_level() &&
289 sum_of_positive_demand <= reservoir.max_level()) {
290 context->UpdateRuleStats("reservoir: always true");
291 reservoir_ct->Clear();
292 return;
293 }
294
295 // If all level_changes have the same sign, we do not care about the order,
296 // just the sum. We might need to create intermediate variable for quadratic
297 // terms though.
298 if (num_negatives == 0 || num_positives == 0) {
299 const int true_literal = context->GetTrueLiteral();
300 ConstraintProto* new_ct = context->working_model->add_constraints();
301 LinearConstraintProto* sum = new_ct->mutable_linear();
302 for (int i = 0; i < num_events; ++i) {
303 const int active = reservoir.active_literals().empty()
304 ? true_literal
305 : reservoir.active_literals(i);
306 const LinearExpressionProto& demand = reservoir.level_changes(i);
307 if (context->IsFixed(demand)) {
308 const int64_t change = context->FixedValue(reservoir.level_changes(i));
309 if (RefIsPositive(active)) {
310 sum->add_vars(active);
311 sum->add_coeffs(change);
312 } else {
313 // Add (1 - not(active)) * level_change.
314 sum->add_vars(true_literal);
315 sum->add_coeffs(change);
316 sum->add_vars(NegatedRef(active));
317 sum->add_coeffs(-change);
318 }
319 } else if (context->LiteralIsTrue(active)) {
321 } else {
322 const int new_var = context->NewIntVar(
323 Domain(context->MinOf(demand), context->MaxOf(demand))
324 .UnionWith(Domain(0)));
325 sum->add_vars(new_var);
326 sum->add_coeffs(1);
327
328 // Active => new_var == demand.
329 {
330 ConstraintProto* demand_ct =
331 context->working_model->add_constraints();
332 demand_ct->add_enforcement_literal(active);
333 LinearConstraintProto* lin = demand_ct->mutable_linear();
334 lin->add_domain(0);
335 lin->add_domain(0);
336 lin->add_vars(new_var);
337 lin->add_coeffs(1);
339 context->CanonicalizeLinearConstraint(demand_ct);
340 context->solution_crush().SetVarToLinearExpressionIf(new_var, demand,
341 active);
342 }
343
344 // not(active) => new_var == 0.
345 context->AddImplyInDomain(NegatedRef(active), new_var, Domain(0));
346 context->solution_crush().SetVarToValueIf(new_var, 0,
347 NegatedRef(active));
348 }
349 }
350 sum->add_domain(reservoir.min_level());
351 sum->add_domain(reservoir.max_level());
352 context->CanonicalizeLinearConstraint(new_ct);
353
354 context->UpdateRuleStats("reservoir: simple expansion with sum");
355 reservoir_ct->Clear();
356 return;
357 }
358
359 // Call the correct expansion according to our parameter.
360 if (context->params().expand_reservoir_using_circuit()) {
361 ExpandReservoirUsingCircuit(sum_of_positive_demand, sum_of_negative_demand,
362 reservoir_ct, context);
363 } else {
364 // This one is the faster option usually.
365 if (all_demands_are_fixed) {
366 ExpandReservoirUsingPrecedences(
367 sum_of_positive_demand > reservoir_ct->reservoir().max_level(),
368 sum_of_negative_demand < reservoir_ct->reservoir().min_level(),
369 reservoir_ct, context);
370 } else {
371 context->UpdateRuleStats(
372 "reservoir: skipped expansion due to variable demands");
373 }
374 }
375}
376
377// This is mainly used for testing the reservoir implementation.
378void EncodeCumulativeAsReservoir(ConstraintProto* ct,
379 PresolveContext* context) {
380 if (!context->IsFixed(ct->cumulative().capacity())) {
381 context->UpdateRuleStats(
382 "cumulative -> reservoir: expansion is not supported with variable "
383 "capacity.");
384 return;
385 }
386
387 // Note that we know that the min_level can never go below zero, so we can
388 // just ignore this part of the constraint here.
389 ConstraintProto reservoir_ct;
390 auto* reservoir = reservoir_ct.mutable_reservoir();
391 reservoir->set_min_level(std::numeric_limits<int64_t>::min());
392 reservoir->set_max_level(context->FixedValue(ct->cumulative().capacity()));
393
394 const int true_literal = context->GetTrueLiteral();
395 const int num_intervals = ct->cumulative().intervals().size();
396 for (int i = 0; i < num_intervals; ++i) {
397 const auto& interval_ct =
398 context->working_model->constraints(ct->cumulative().intervals(i));
399 const auto& interval = interval_ct.interval();
400 *reservoir->add_time_exprs() = interval.start();
401 *reservoir->add_time_exprs() = interval.end();
402
403 const LinearExpressionProto& demand = ct->cumulative().demands(i);
404 *reservoir->add_level_changes() = demand;
405 LinearExpressionProto& negated = *reservoir->add_level_changes();
406 negated.set_offset(-demand.offset());
407 for (int j = 0; j < demand.vars().size(); ++j) {
408 negated.add_vars(demand.vars(j));
409 negated.add_coeffs(-demand.coeffs(j));
410 }
411
412 if (interval_ct.enforcement_literal().empty()) {
413 reservoir->add_active_literals(true_literal);
414 reservoir->add_active_literals(true_literal);
415 } else {
416 CHECK_EQ(interval_ct.enforcement_literal().size(), 1);
417 reservoir->add_active_literals(interval_ct.enforcement_literal(0));
418 reservoir->add_active_literals(interval_ct.enforcement_literal(0));
419 }
420 }
421
422 // Now expand it and clear the cumulative.
423 ct->Clear();
424 context->UpdateRuleStats("cumulative: expanded into reservoir");
425 ExpandReservoir(&reservoir_ct, context);
426}
427
428void ExpandIntMod(ConstraintProto* ct, PresolveContext* context) {
429 const LinearArgumentProto& int_mod = ct->int_mod();
430 const LinearExpressionProto& mod_expr = int_mod.exprs(1);
431 if (context->IsFixed(mod_expr)) return;
432
433 const LinearExpressionProto& expr = int_mod.exprs(0);
434 const LinearExpressionProto& target_expr = int_mod.target();
435
436 // We reduce the domain of target_expr to avoid later overflow.
437 if (!context->IntersectDomainWith(
438 target_expr, context->DomainSuperSetOf(expr).PositiveModuloBySuperset(
439 context->DomainSuperSetOf(mod_expr)))) {
440 return;
441 }
442
443 // Create a new constraint with the same enforcement as ct.
444 auto new_enforced_constraint = [&]() {
445 ConstraintProto* new_ct = context->working_model->add_constraints();
446 *new_ct->mutable_enforcement_literal() = ct->enforcement_literal();
447 return new_ct;
448 };
449
450 // div_expr = expr / mod_expr.
451 const int div_var = context->NewIntVar(
452 context->DomainSuperSetOf(expr).PositiveDivisionBySuperset(
453 context->DomainSuperSetOf(mod_expr)));
454 LinearExpressionProto div_expr;
455 div_expr.add_vars(div_var);
456 div_expr.add_coeffs(1);
457
458 LinearArgumentProto* const div_proto =
459 new_enforced_constraint()->mutable_int_div();
460 *div_proto->mutable_target() = div_expr;
461 *div_proto->add_exprs() = expr;
462 *div_proto->add_exprs() = mod_expr;
463
464 // Create prod_expr = div_expr * mod_expr.
465 const Domain prod_domain =
466 context->DomainOf(div_var)
467 .ContinuousMultiplicationBy(context->DomainSuperSetOf(mod_expr))
468 .IntersectionWith(context->DomainSuperSetOf(expr).AdditionWith(
469 context->DomainSuperSetOf(target_expr).Negation()));
470 const int prod_var = context->NewIntVar(prod_domain);
471 LinearExpressionProto prod_expr;
472 prod_expr.add_vars(prod_var);
473 prod_expr.add_coeffs(1);
474
475 LinearArgumentProto* const int_prod =
476 new_enforced_constraint()->mutable_int_prod();
477 *int_prod->mutable_target() = prod_expr;
478 *int_prod->add_exprs() = div_expr;
479 *int_prod->add_exprs() = mod_expr;
480
481 // expr - prod_expr = target_expr.
482 LinearConstraintProto* const lin =
483 new_enforced_constraint()->mutable_linear();
484 lin->add_domain(0);
485 lin->add_domain(0);
487 AddLinearExpressionToLinearConstraint(prod_expr, -1, lin);
488 AddLinearExpressionToLinearConstraint(target_expr, -1, lin);
489
490 context->solution_crush().SetIntModExpandedVars(*ct, div_var, prod_var,
491 context->MinOf(div_var),
492 context->MinOf(prod_var));
493 ct->Clear();
494 context->UpdateRuleStats("int_mod: expanded");
495}
496
497void ExpandIntProd(ConstraintProto* ct, PresolveContext* context) {
498 if (ct->int_prod().exprs_size() <= 2) return;
499 std::deque<LinearExpressionProto> terms(
500 {ct->int_prod().exprs().begin(), ct->int_prod().exprs().end()});
501 std::vector<int> new_vars;
502 while (terms.size() > 2) {
503 const LinearExpressionProto& left = terms[0];
504 const LinearExpressionProto& right = terms[1];
505 const Domain new_domain =
506 context->DomainSuperSetOf(left).ContinuousMultiplicationBy(
507 context->DomainSuperSetOf(right));
508 const int new_var = context->NewIntVar(new_domain);
509 new_vars.push_back(new_var);
510 LinearArgumentProto* const int_prod =
511 context->working_model->add_constraints()->mutable_int_prod();
512 *int_prod->add_exprs() = left;
513 *int_prod->add_exprs() = right;
514 int_prod->mutable_target()->add_vars(new_var);
515 int_prod->mutable_target()->add_coeffs(1);
516 terms.pop_front();
517 terms.front() = int_prod->target();
518 }
519
520 LinearArgumentProto* const final_int_prod =
521 context->working_model->add_constraints()->mutable_int_prod();
522 *final_int_prod->add_exprs() = terms[0];
523 *final_int_prod->add_exprs() = terms[1];
524 *final_int_prod->mutable_target() = ct->int_prod().target();
525
526 context->solution_crush().SetIntProdExpandedVars(ct->int_prod(), new_vars);
527 context->UpdateRuleStats(absl::StrCat(
528 "int_prod: expanded int_prod with arity ", ct->int_prod().exprs_size()));
529 ct->Clear();
530}
531
532void ExpandInverse(ConstraintProto* ct, PresolveContext* context) {
533 const auto& f_direct = ct->inverse().f_direct();
534 const auto& f_inverse = ct->inverse().f_inverse();
535 const int n = f_direct.size();
536 CHECK_EQ(n, f_inverse.size());
537
538 // Make sure the domains are included in [0, n - 1).
539 // Note that if a variable and its negation appear, the domains will be set to
540 // zero here.
541 //
542 // TODO(user): Add support for UNSAT at expansion. This should create empty
543 // domain if UNSAT, so it should still work correctly.
544 absl::flat_hash_set<int> used_variables;
545 for (const int ref : f_direct) {
546 used_variables.insert(PositiveRef(ref));
547 if (!context->IntersectDomainWith(ref, Domain(0, n - 1))) {
548 VLOG(1) << "Empty domain for a variable in ExpandInverse()";
549 return;
550 }
551 }
552 for (const int ref : f_inverse) {
553 used_variables.insert(PositiveRef(ref));
554 if (!context->IntersectDomainWith(ref, Domain(0, n - 1))) {
555 VLOG(1) << "Empty domain for a variable in ExpandInverse()";
556 return;
557 }
558 }
559
560 // If we have duplicate variables, we make sure the domain are reduced
561 // as the loop below might not detect incompatibilities.
562 if (used_variables.size() != 2 * n) {
563 for (int i = 0; i < n; ++i) {
564 for (int j = 0; j < n; ++j) {
565 // Note that if we don't have the same sign, both domain are at zero.
566 if (PositiveRef(f_direct[i]) != PositiveRef(f_inverse[j])) continue;
567
568 // We can't have i or j as value if i != j.
569 if (i == j) continue;
570 if (!context->IntersectDomainWith(
571 f_direct[i], Domain::FromValues({i, j}).Complement())) {
572 return;
573 }
574 }
575 }
576 }
577
578 // Reduce the domains of each variable by checking that the inverse value
579 // exists.
580 std::vector<int64_t> possible_values;
581
582 // Propagate from one vector to its counterpart.
583 const auto filter_inverse_domain =
584 [context, n, &possible_values](const auto& direct, const auto& inverse) {
585 // Propagate from the inverse vector to the direct vector.
586 for (int i = 0; i < n; ++i) {
587 possible_values.clear();
588 const Domain domain = context->DomainOf(direct[i]);
589 bool removed_value = false;
590 for (const int64_t j : domain.Values()) {
591 if (context->DomainOf(inverse[j]).Contains(i)) {
592 possible_values.push_back(j);
593 } else {
594 removed_value = true;
595 }
596 }
597 if (removed_value) {
598 if (!context->IntersectDomainWith(
599 direct[i], Domain::FromValues(possible_values))) {
600 VLOG(1) << "Empty domain for a variable in ExpandInverse()";
601 return false;
602 }
603 }
604 }
605 return true;
606 };
607
608 // Note that this should reach the fixed point in one pass.
609 // However, if we have duplicate variable, I am not sure.
610 if (!filter_inverse_domain(f_direct, f_inverse)) return;
611 if (!filter_inverse_domain(f_inverse, f_direct)) return;
612
613 // Expand the inverse constraint by associating literal to var == value
614 // and sharing them between the direct and inverse variables.
615 //
616 // Note that this is only correct because the domain are tight now.
617 for (int i = 0; i < n; ++i) {
618 const int f_i = f_direct[i];
619 for (const int64_t j : context->DomainOf(f_i).Values()) {
620 // We have f[i] == j <=> r[j] == i;
621 const int r_j = f_inverse[j];
622 int r_j_i;
623 if (context->HasVarValueEncoding(r_j, i, &r_j_i)) {
624 if (!context->InsertVarValueEncoding(r_j_i, f_i, j)) {
625 return;
626 }
627 } else {
628 const int f_i_j = context->GetOrCreateVarValueEncoding(f_i, j);
629 if (!context->InsertVarValueEncoding(f_i_j, r_j, i)) {
630 return;
631 }
632 }
633 }
634 }
635
636 ct->Clear();
637 context->UpdateRuleStats("inverse: expanded");
638}
639
640void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
641 const int num_exprs = ct->lin_max().exprs().size();
642 if (num_exprs < 2) return;
643
644 // We have a special treatment for Abs, Earliness, Tardiness, and all
645 // affine_max where there is only one variable present in all the expressions.
646 if (ExpressionsContainsOnlyOneVar(ct->lin_max().exprs())) return;
647
648 // We will create 2 * num_exprs constraints for target = max(a1, ..., an).
649
650 // First.
651 // - target >= ai
652 for (const LinearExpressionProto& expr : ct->lin_max().exprs()) {
653 ConstraintProto* new_ct = context->working_model->add_constraints();
654 LinearConstraintProto* lin = new_ct->mutable_linear();
655 lin->add_domain(0);
656 lin->add_domain(std::numeric_limits<int64_t>::max());
657 AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin);
659 context->CanonicalizeLinearConstraint(new_ct);
660 }
661
662 // Second, for each expr, create a new boolean bi, and add bi => target <= ai
663 // With exactly_one(bi)
664 std::vector<int> enforcement_literals;
665 enforcement_literals.reserve(num_exprs);
666 if (num_exprs == 2) {
667 const int new_bool = context->NewBoolVar("lin max expansion");
668 enforcement_literals.push_back(new_bool);
669 enforcement_literals.push_back(NegatedRef(new_bool));
670 } else {
671 ConstraintProto* exactly_one = context->working_model->add_constraints();
672 for (int i = 0; i < num_exprs; ++i) {
673 const int new_bool = context->NewBoolVar("lin max expansion");
674 exactly_one->mutable_exactly_one()->add_literals(new_bool);
675 enforcement_literals.push_back(new_bool);
676 }
677 }
678
679 for (int i = 0; i < num_exprs; ++i) {
680 ConstraintProto* new_ct = context->working_model->add_constraints();
681 new_ct->add_enforcement_literal(enforcement_literals[i]);
682 LinearConstraintProto* lin = new_ct->mutable_linear();
683 lin->add_domain(std::numeric_limits<int64_t>::min());
684 lin->add_domain(0);
685 AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin);
686 AddLinearExpressionToLinearConstraint(ct->lin_max().exprs(i), -1, lin);
687 context->CanonicalizeLinearConstraint(new_ct);
688 }
689
690 context->solution_crush().SetLinMaxExpandedVars(ct->lin_max(),
691 enforcement_literals);
692 context->UpdateRuleStats("lin_max: expanded lin_max");
693 ct->Clear();
694}
695
696// A[V] == V means for all i, V == i => A_i == i
697void ExpandElementWhenTargetShareVarWithIndex(ConstraintProto* ct,
698 PresolveContext* context) {
699 const ElementConstraintProto& element = ct->element();
700
701 const LinearExpressionProto& index = element.linear_index();
702 DCHECK_EQ(index.vars_size(), 1);
703 const int index_var = index.vars(0);
704 const LinearExpressionProto& target = element.linear_target();
705 DCHECK_EQ(target.vars_size(), 1);
706 DCHECK_EQ(target.vars(0), index_var);
707
708 for (const int64_t v : context->DomainOf(index_var).Values()) {
709 const int64_t index_value = AffineExpressionValueAt(index, v);
710 const int64_t target_value = AffineExpressionValueAt(target, v);
711 const LinearExpressionProto& expr = element.exprs(index_value);
712 ConstraintProto* imply = context->working_model->add_constraints();
714 context->GetOrCreateVarValueEncoding(index_var, v));
715 imply->mutable_linear()->add_domain(target_value);
716 imply->mutable_linear()->add_domain(target_value);
717 AddLinearExpressionToLinearConstraint(expr, 1, imply->mutable_linear());
718 context->CanonicalizeLinearConstraint(imply);
719 }
720
721 context->UpdateRuleStats(
722 "element: expanded when the index and the target share the same var");
723 ct->Clear();
724}
725
726// Special case if the array of the element is filled with constant values.
727void ExpandConstantArrayElement(ConstraintProto* ct, PresolveContext* context) {
728 const ElementConstraintProto& element = ct->element();
729 const LinearExpressionProto& index = element.linear_index();
730 DCHECK_EQ(index.vars_size(), 1);
731 const int index_var = index.vars(0);
732 const LinearExpressionProto& target = element.linear_target();
733
734 // Index and target domain have been reduced before calling this function.
735 const Domain index_var_domain = context->DomainOf(index_var);
736 const Domain target_domain = context->DomainSuperSetOf(target);
737
738 // This BoolOrs implements the deduction that if all index literals pointing
739 // to the same value in the constant array are false, then this value is no
740 // no longer valid for the target variable. They are created only for values
741 // that have multiples literals supporting them.
742 absl::btree_map<int64_t, std::vector<int>> supports;
743 for (const int64_t v : index_var_domain.Values()) {
744 const int64_t index_value = AffineExpressionValueAt(index, v);
745 const int64_t expr_value = context->FixedValue(element.exprs(index_value));
746 supports[expr_value].push_back(v);
747 }
748
749 // While this is not strictly needed since all value in the index will be
750 // covered, it allows to easily detect this fact in the presolve.
751 //
752 // TODO(user): Do we need the support part ? Is this discovered by probing?
753 auto* exactly_one =
754 context->working_model->add_constraints()->mutable_exactly_one();
755 for (const auto& [expr_value, support] : supports) {
756 const int target_literal =
757 context->GetOrCreateAffineValueEncoding(target, expr_value);
758 // not(indices supporting value) -> target != value
759 BoolArgumentProto* bool_or =
760 context->working_model->add_constraints()->mutable_bool_or();
761 bool_or->add_literals(NegatedRef(target_literal));
762 for (const int64_t v : support) {
763 const int index_literal =
764 context->GetOrCreateVarValueEncoding(index_var, v);
765 bool_or->add_literals(index_literal);
766
767 // index == v => target == value
768 context->AddImplication(index_literal, target_literal);
769
770 // Helps presolve.
771 exactly_one->add_literals(index_literal);
772 }
773 }
774
775 context->UpdateRuleStats("element: expanded value element");
776 ct->Clear();
777}
778
779// General element when the array contains non fixed variables.
780void ExpandVariableElement(ConstraintProto* ct, PresolveContext* context) {
781 const ElementConstraintProto& element = ct->element();
782 const LinearExpressionProto& index = element.linear_index();
783 DCHECK_EQ(index.vars_size(), 1);
784 const int index_var = index.vars(0);
785 const Domain index_var_domain = context->DomainOf(index_var);
786 const LinearExpressionProto& target = element.linear_target();
787
788 BoolArgumentProto* exactly_one =
789 context->working_model->add_constraints()->mutable_exactly_one();
790
791 for (const int64_t v : index_var_domain.Values()) {
792 const int64_t index_value = AffineExpressionValueAt(index, v);
793 DCHECK_GE(index_value, 0);
794 DCHECK_LT(index_value, element.exprs_size());
795 const int index_lit = context->GetOrCreateVarValueEncoding(index_var, v);
796 exactly_one->add_literals(index_lit);
797
798 ConstraintProto* const imply = context->working_model->add_constraints();
799 imply->add_enforcement_literal(index_lit);
800 imply->mutable_linear()->add_domain(0);
801 imply->mutable_linear()->add_domain(0);
802 AddLinearExpressionToLinearConstraint(target, -1, imply->mutable_linear());
803 AddLinearExpressionToLinearConstraint(ct->element().exprs(index_value), 1,
804 imply->mutable_linear());
805 context->CanonicalizeLinearConstraint(imply);
806
807 // Note that this should have been checked at model validation.
808 DCHECK(!PossibleIntegerOverflow(*context->working_model,
809 imply->mutable_linear()->vars(),
810 imply->mutable_linear()->coeffs()))
811 << google::protobuf::ShortFormat(*imply);
812 }
813
814 context->UpdateRuleStats("element: expanded");
815 ct->Clear();
816}
817
818void ExpandElement(ConstraintProto* ct, PresolveContext* context) {
819 const ElementConstraintProto& element = ct->element();
820
821 const LinearExpressionProto& index = element.linear_index();
822 const LinearExpressionProto& target = element.linear_target();
823 const int size = element.exprs_size();
824
825 // Reduce the domain of the index to be compatible with the array of
826 // variables. Note that the element constraint is 0 based.
827 if (!context->IntersectDomainWith(index, Domain(0, size - 1))) {
828 VLOG(1) << "Empty domain for the index variable in ExpandElement()";
829 return;
830 }
831
832 if (context->IsFixed(index)) {
833 ConstraintProto* const eq = context->working_model->add_constraints();
834 eq->mutable_linear()->add_domain(0);
835 eq->mutable_linear()->add_domain(0);
836 AddLinearExpressionToLinearConstraint(target, 1, eq->mutable_linear());
838 ct->element().exprs(context->FixedValue(index)), -1,
839 eq->mutable_linear());
840 context->CanonicalizeLinearConstraint(eq);
841 context->UpdateRuleStats("element: expanded with fixed index");
842 ct->Clear();
843 return;
844 }
845
846 // Special case when index.var = target.var.
847 if (index.vars_size() == 1 && target.vars_size() == 1 &&
848 index.vars(0) == target.vars(0)) {
849 ExpandElementWhenTargetShareVarWithIndex(ct, context);
850 return;
851 }
852
853 // Checks if all elements are constant.
854 bool all_constants = true;
855 for (const int64_t v : context->DomainOf(index.vars(0)).Values()) {
856 const int64_t index_value = AffineExpressionValueAt(index, v);
857 if (!context->IsFixed(element.exprs(index_value))) {
858 all_constants = false;
859 break;
860 }
861 }
862
863 if (all_constants) {
864 ExpandConstantArrayElement(ct, context);
865 } else {
866 ExpandVariableElement(ct, context);
867 }
868}
869
870// Adds clauses so that literals[i] true <=> encoding[values[i]] true.
871// This also implicitly use the fact that exactly one alternative is true.
872void LinkLiteralsAndValues(absl::Span<const int> literals,
873 absl::Span<const int64_t> values,
874 const absl::flat_hash_map<int64_t, int>& encoding,
875 PresolveContext* context) {
876 CHECK_EQ(literals.size(), values.size());
877
878 // We use a map to make this method deterministic.
879 //
880 // TODO(user): Make sure this does not appear in the profile.
881 absl::btree_map<int, std::vector<int>> encoding_lit_to_support;
882
883 // If a value is false (i.e not possible), then the tuple with this
884 // value is false too (i.e not possible). Conversely, if the tuple is
885 // selected, the value must be selected.
886 for (int i = 0; i < values.size(); ++i) {
887 encoding_lit_to_support[encoding.at(values[i])].push_back(literals[i]);
888 }
889
890 // If all tuples supporting a value are false, then this value must be
891 // false.
892 for (const auto& [encoding_lit, support] : encoding_lit_to_support) {
893 CHECK(!support.empty());
894 if (support.size() == 1) {
895 if (!context->StoreBooleanEqualityRelation(encoding_lit, support[0])) {
896 return;
897 }
898 } else {
899 BoolArgumentProto* bool_or =
900 context->working_model->add_constraints()->mutable_bool_or();
901 bool_or->add_literals(NegatedRef(encoding_lit));
902 for (const int lit : support) {
903 bool_or->add_literals(lit);
904 context->AddImplication(lit, encoding_lit);
905 }
906 }
907 }
908}
909
910// Add the constraint literal => one_of(encoding[v]), for v in reachable_values.
911// Note that all possible values are the ones appearing in encoding.
912void AddImplyInReachableValues(int literal,
913 std::vector<int64_t>& reachable_values,
914 const absl::flat_hash_map<int64_t, int> encoding,
915 PresolveContext* context) {
916 gtl::STLSortAndRemoveDuplicates(&reachable_values);
917 if (reachable_values.size() == encoding.size()) return; // No constraint.
918 if (reachable_values.size() <= encoding.size() / 2) {
919 // Bool or encoding.
920 ConstraintProto* ct = context->working_model->add_constraints();
921 ct->add_enforcement_literal(literal);
922 BoolArgumentProto* bool_or = ct->mutable_bool_or();
923 for (const int64_t v : reachable_values) {
924 bool_or->add_literals(encoding.at(v));
925 }
926 } else {
927 // Bool and encoding.
928 absl::flat_hash_set<int64_t> set(reachable_values.begin(),
929 reachable_values.end());
930 ConstraintProto* ct = context->working_model->add_constraints();
931 ct->add_enforcement_literal(literal);
932 BoolArgumentProto* bool_and = ct->mutable_bool_and();
933 for (const auto [value, literal] : encoding) {
934 if (!set.contains(value)) {
935 bool_and->add_literals(NegatedRef(literal));
936 }
937 }
938 }
939}
940
941void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
942 AutomatonConstraintProto& proto = *ct->mutable_automaton();
943
944 if (proto.exprs_size() == 0) {
945 const int64_t initial_state = proto.starting_state();
946 for (const int64_t final_state : proto.final_states()) {
947 if (initial_state == final_state) {
948 context->UpdateRuleStats("automaton: empty and trivially feasible");
949 ct->Clear();
950 return;
951 }
952 }
953 return (void)context->NotifyThatModelIsUnsat(
954 "automaton: empty with an initial state not in the final states.");
955 } else if (proto.transition_label_size() == 0) {
956 return (void)context->NotifyThatModelIsUnsat(
957 "automaton: non-empty with no transition.");
958 }
959
960 std::vector<absl::flat_hash_set<int64_t>> reachable_states;
961 std::vector<absl::flat_hash_set<int64_t>> reachable_labels;
962 PropagateAutomaton(proto, *context, &reachable_states, &reachable_labels);
963
964 // We will model at each time step the current automaton state using Boolean
965 // variables. We will have n+1 time step. At time zero, we start in the
966 // initial state, and at time n we should be in one of the final states. We
967 // don't need to create Booleans at times when there is just one possible
968 // state (like at time zero).
969 absl::flat_hash_map<int64_t, int> encoding;
970 absl::flat_hash_map<int64_t, int> in_encoding;
971 absl::flat_hash_map<int64_t, int> out_encoding;
972 bool removed_values = false;
973
974 const int n = proto.exprs_size();
975 std::vector<SolutionCrush::StateVar> new_state_vars;
976 std::vector<SolutionCrush::TransitionVar> new_transition_vars;
977 for (int time = 0; time < n; ++time) {
978 if (context->time_limit()->LimitReached()) return;
979 // All these vectors have the same size. We will use them to enforce a
980 // local table constraint representing one step of the automaton at the
981 // given time.
982 std::vector<int64_t> in_states;
983 std::vector<int64_t> labels;
984 std::vector<int64_t> out_states;
985 absl::flat_hash_set<int64_t> still_reachable_after_domain_change;
986 for (int i = 0; i < proto.transition_label_size(); ++i) {
987 const int64_t tail = proto.transition_tail(i);
988 const int64_t label = proto.transition_label(i);
989 const int64_t head = proto.transition_head(i);
990
991 if (!reachable_states[time].contains(tail)) continue;
992 if (!reachable_states[time + 1].contains(head)) continue;
993 if (!context->DomainContains(proto.exprs(time), label)) continue;
994
995 still_reachable_after_domain_change.insert(head);
996 // TODO(user): if this transition correspond to just one in-state or
997 // one-out state or one variable value, we could reuse the corresponding
998 // Boolean variable instead of creating a new one!
999 in_states.push_back(tail);
1000 labels.push_back(label);
1001
1002 // On the last step we don't need to distinguish the output states, so
1003 // we use zero.
1004 out_states.push_back(time + 1 == n ? 0 : head);
1005 }
1006
1007 reachable_states[time + 1] = still_reachable_after_domain_change;
1008
1009 // Deal with single tuple.
1010 const int num_tuples = in_states.size();
1011 if (num_tuples == 1) {
1012 if (!context->IntersectDomainWith(proto.exprs(time),
1013 Domain(labels.front()))) {
1014 VLOG(1) << "Infeasible automaton.";
1015 return;
1016 }
1017
1018 // Tricky: when the same variable is used more than once, the propagation
1019 // above might not reach the fixed point, so we do need to fix literal
1020 // at false.
1021 std::vector<int> at_false;
1022 for (const auto [value, literal] : in_encoding) {
1023 if (value != in_states[0]) {
1024 if (!context->SetLiteralToFalse(literal)) return;
1025 }
1026 }
1027
1028 in_encoding.clear();
1029 continue;
1030 }
1031
1032 // Fully encode vars[time].
1033 {
1034 std::vector<int64_t> transitions = labels;
1035 const LinearExpressionProto& expr = proto.exprs(time);
1036 gtl::STLSortAndRemoveDuplicates(&transitions);
1037
1038 encoding.clear();
1039 if (!context->IntersectDomainWith(expr, Domain::FromValues(transitions),
1040 &removed_values)) {
1041 VLOG(1) << "Infeasible automaton.";
1042 return;
1043 }
1044
1045 // Fully encode the variable.
1046 // We can leave the encoding empty for fixed vars.
1047 if (!context->IsFixed(expr)) {
1048 const int var = expr.vars(0);
1049 for (const int64_t v : context->DomainOf(var).Values()) {
1050 encoding[AffineExpressionValueAt(expr, v)] =
1051 context->GetOrCreateVarValueEncoding(var, v);
1052 }
1053 }
1054 }
1055
1056 // Count how many time each value appear.
1057 // We use this to reuse literals if possible.
1058 absl::flat_hash_map<int64_t, int> in_count;
1059 absl::flat_hash_map<int64_t, int> transition_count;
1060 absl::flat_hash_map<int64_t, int> out_count;
1061 for (int i = 0; i < num_tuples; ++i) {
1062 in_count[in_states[i]]++;
1063 transition_count[labels[i]]++;
1064 out_count[out_states[i]]++;
1065 }
1066
1067 // For each possible out states, create one Boolean variable.
1068 //
1069 // TODO(user): Add exactly one?
1070 {
1071 std::vector<int64_t> states = out_states;
1073
1074 out_encoding.clear();
1075 if (states.size() == 2) {
1076 const int var = context->NewBoolVar("automaton expansion");
1077 new_state_vars.push_back({var, time + 1, states[0]});
1078 out_encoding[states[0]] = var;
1079 out_encoding[states[1]] = NegatedRef(var);
1080 } else if (states.size() > 2) {
1081 struct UniqueDetector {
1082 void Set(int64_t v) {
1083 if (!is_unique) return;
1084 if (is_set) {
1085 if (v != value) is_unique = false;
1086 } else {
1087 is_set = true;
1088 value = v;
1089 }
1090 }
1091 bool is_set = false;
1092 bool is_unique = true;
1093 int64_t value = 0;
1094 };
1095
1096 // Optimization to detect if we have an in state that is only matched to
1097 // a single out state. Same with transition.
1098 absl::flat_hash_map<int64_t, UniqueDetector> out_to_in;
1099 absl::flat_hash_map<int64_t, UniqueDetector> out_to_transition;
1100 for (int i = 0; i < num_tuples; ++i) {
1101 out_to_in[out_states[i]].Set(in_states[i]);
1102 out_to_transition[out_states[i]].Set(labels[i]);
1103 }
1104
1105 for (const int64_t state : states) {
1106 // If we have a relation in_state <=> out_state, then we can reuse
1107 // the in Boolean and do not need to create a new one.
1108 if (!in_encoding.empty() && out_to_in[state].is_unique) {
1109 const int64_t unique_in = out_to_in[state].value;
1110 if (in_count[unique_in] == out_count[state]) {
1111 out_encoding[state] = in_encoding[unique_in];
1112 continue;
1113 }
1114 }
1115
1116 // Same if we have an unique transition value that correspond only to
1117 // this state.
1118 if (!encoding.empty() && out_to_transition[state].is_unique) {
1119 const int64_t unique_transition = out_to_transition[state].value;
1120 if (transition_count[unique_transition] == out_count[state]) {
1121 out_encoding[state] = encoding[unique_transition];
1122 continue;
1123 }
1124 }
1125
1126 out_encoding[state] = context->NewBoolVar("automaton expansion");
1127 new_state_vars.push_back({out_encoding[state], time + 1, state});
1128 }
1129 }
1130 }
1131
1132 // Simple encoding. This is enough to properly enforce the constraint, but
1133 // it propagate less. It creates a lot less Booleans though. Note that we
1134 // use implicit "exactly one" on the encoding and do not add any extra
1135 // exactly one if the simple encoding is used.
1136 //
1137 // We currently decide which encoding to use depending on the number of new
1138 // literals needed by the "heavy" encoding compared to the number of states
1139 // and labels. When the automaton is small, using the full encoding is
1140 // better, see for instance on rotating-workforce_Example789 were the simple
1141 // encoding make the problem hard to solve but the full encoding allow the
1142 // solver to solve it in a couple of seconds!
1143 //
1144 // Note that both encoding create about the same number of constraints.
1145 const int num_involved_variables =
1146 in_encoding.size() + encoding.size() + out_encoding.size();
1147 const bool use_light_encoding = (num_tuples > num_involved_variables);
1148 if (use_light_encoding && !in_encoding.empty() && !encoding.empty() &&
1149 !out_encoding.empty()) {
1150 // Part 1: If a in_state is selected, restrict the set of possible labels.
1151 // We also restrict the set of possible out states, but this is not needed
1152 // for correctness.
1153 absl::flat_hash_map<int64_t, std::vector<int64_t>> in_to_label;
1154 absl::flat_hash_map<int64_t, std::vector<int64_t>> in_to_out;
1155 for (int i = 0; i < num_tuples; ++i) {
1156 in_to_label[in_states[i]].push_back(labels[i]);
1157 in_to_out[in_states[i]].push_back(out_states[i]);
1158 }
1159 // Sort the pairs to make the order deterministic.
1160 std::vector<std::pair<int64_t, int>> in_to_label_pairs(
1161 in_encoding.begin(), in_encoding.end());
1162 absl::c_sort(in_to_label_pairs);
1163 for (const auto [in_value, in_literal] : in_to_label_pairs) {
1164 AddImplyInReachableValues(in_literal, in_to_label[in_value], encoding,
1165 context);
1166 AddImplyInReachableValues(in_literal, in_to_out[in_value], out_encoding,
1167 context);
1168 }
1169
1170 // Part2, add all 3-clauses: (in_state, label) => out_state.
1171 for (int i = 0; i < num_tuples; ++i) {
1172 auto* bool_or =
1173 context->working_model->add_constraints()->mutable_bool_or();
1174 bool_or->add_literals(NegatedRef(in_encoding.at(in_states[i])));
1175 bool_or->add_literals(NegatedRef(encoding.at(labels[i])));
1176 bool_or->add_literals(out_encoding.at(out_states[i]));
1177 }
1178
1179 in_encoding.swap(out_encoding);
1180 out_encoding.clear();
1181 continue;
1182 }
1183
1184 // Create the tuple literals.
1185 //
1186 // TODO(user): Call and use the same heuristics as the table constraint to
1187 // expand this small table with 3 columns (i.e. compress, negate, etc...).
1188 std::vector<int> tuple_literals;
1189 if (num_tuples == 2) {
1190 const int bool_var = context->NewBoolVar("automaton expansion");
1191 new_transition_vars.push_back({bool_var, time, in_states[0], labels[0]});
1192 tuple_literals.push_back(bool_var);
1193 tuple_literals.push_back(NegatedRef(bool_var));
1194 } else {
1195 // Note that we do not need the ExactlyOneConstraint(tuple_literals)
1196 // because it is already implicitly encoded since we have exactly one
1197 // transition value. But adding one seems to help.
1198 BoolArgumentProto* exactly_one =
1199 context->working_model->add_constraints()->mutable_exactly_one();
1200 for (int i = 0; i < num_tuples; ++i) {
1201 int tuple_literal;
1202 if (in_count[in_states[i]] == 1 && !in_encoding.empty()) {
1203 tuple_literal = in_encoding[in_states[i]];
1204 } else if (transition_count[labels[i]] == 1 && !encoding.empty()) {
1205 tuple_literal = encoding[labels[i]];
1206 } else if (out_count[out_states[i]] == 1 && !out_encoding.empty()) {
1207 tuple_literal = out_encoding[out_states[i]];
1208 } else {
1209 tuple_literal = context->NewBoolVar("automaton expansion");
1210 new_transition_vars.push_back(
1211 {tuple_literal, time, in_states[i], labels[i]});
1212 }
1213
1214 tuple_literals.push_back(tuple_literal);
1215 exactly_one->add_literals(tuple_literal);
1216 }
1217 }
1218
1219 if (!in_encoding.empty()) {
1220 LinkLiteralsAndValues(tuple_literals, in_states, in_encoding, context);
1221 }
1222 if (!encoding.empty()) {
1223 LinkLiteralsAndValues(tuple_literals, labels, encoding, context);
1224 }
1225 if (!out_encoding.empty()) {
1226 LinkLiteralsAndValues(tuple_literals, out_states, out_encoding, context);
1227 }
1228
1229 in_encoding.swap(out_encoding);
1230 out_encoding.clear();
1231 }
1232
1233 context->solution_crush().SetAutomatonExpandedVars(proto, new_state_vars,
1234 new_transition_vars);
1235 if (removed_values) {
1236 context->UpdateRuleStats("automaton: reduced variable domains");
1237 }
1238 context->UpdateRuleStats("automaton: expanded");
1239 ct->Clear();
1240}
1241
1242bool TableIsInCanonicalForm(ConstraintProto* ct) {
1243 TableConstraintProto& table = *ct->mutable_table();
1244 if (!table.vars().empty()) {
1245 LOG(ERROR) << "Table is in the legacy format.";
1246 return false;
1247 }
1248 if (table.values().empty()) {
1249 if (table.exprs().empty()) {
1250 return true;
1251 }
1252 if (table.exprs_size() != 1) {
1253 LOG(ERROR) << "Table is empty but has more than one expression.";
1254 return false;
1255 }
1256 if (table.exprs(0).offset() != 0) {
1257 LOG(ERROR) << "Table is empty but has an expression with a non-zero "
1258 "offset.";
1259 return false;
1260 }
1261 if (!table.exprs(0).vars().empty()) {
1262 LOG(ERROR) << "Table is empty but has an expression with a non-constant "
1263 "coefficient.";
1264 return false;
1265 }
1266 return true;
1267 }
1268 for (const LinearExpressionProto& expr : table.exprs()) {
1269 if (expr.offset() != 0) {
1270 LOG(ERROR) << "Expression contains an non-zero offset.";
1271 return false;
1272 }
1273 if (expr.coeffs().size() == 1 && expr.coeffs(0) != 1) {
1274 LOG(ERROR) << "Expression contains a single variable with a coefficient "
1275 "different from 1.";
1276 return false;
1277 }
1278 if (expr.vars().empty()) {
1279 LOG(ERROR) << "Constant expression.";
1280 return false;
1281 }
1282 }
1283 return true;
1284}
1285
1286void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) {
1287 DCHECK(TableIsInCanonicalForm(ct));
1288 TableConstraintProto& table = *ct->mutable_table();
1289 if (table.values().empty()) { // Early exit.
1290 context->UpdateRuleStats("table: empty negated constraint");
1291 ct->Clear();
1292 return;
1293 }
1294
1295 const int num_exprs = table.exprs_size();
1296 DCHECK_GT(num_exprs, 0);
1297 const int num_original_tuples = table.values_size() / num_exprs;
1298 std::vector<std::vector<int64_t>> tuples(num_original_tuples);
1299 int count = 0;
1300 for (int i = 0; i < num_original_tuples; ++i) {
1301 for (int j = 0; j < num_exprs; ++j) {
1302 tuples[i].push_back(table.values(count++));
1303 }
1304 }
1305
1306 // Compress tuples.
1307 std::vector<int64_t> domain_sizes;
1308 for (int i = 0; i < num_exprs; ++i) {
1309 domain_sizes.push_back(context->DomainOf(table.exprs(i).vars(0)).Size());
1310 }
1311 CompressTuples(domain_sizes, &tuples);
1312
1313 // For each tuple, forbid the variables values to be this tuple.
1314 std::vector<int> clause;
1315 for (const std::vector<int64_t>& tuple : tuples) {
1316 clause.clear();
1317 for (int i = 0; i < num_exprs; ++i) {
1318 const int64_t value = tuple[i];
1319 if (value == kTableAnyValue) continue;
1320
1321 const int literal =
1322 context->GetOrCreateVarValueEncoding(table.exprs(i).vars(0), value);
1323 clause.push_back(NegatedRef(literal));
1324 }
1325
1326 // Note: if the clause is empty, then the model is infeasible.
1327 ConstraintProto* tuple_ct = context->working_model->add_constraints();
1328 *tuple_ct->mutable_enforcement_literal() = ct->enforcement_literal();
1329 BoolArgumentProto* bool_or = tuple_ct->mutable_bool_or();
1330 for (const int lit : clause) {
1331 bool_or->add_literals(lit);
1332 }
1333 }
1334 context->UpdateRuleStats("table: expanded negated constraint");
1335 ct->Clear();
1336}
1337
1338// Add the implications and clauses to link one variable (i.e. column) of a
1339// table to the literals controlling if the tuples are possible or not.
1340//
1341// We list for each tuple the possible values the variable can take.
1342// If the list is empty, then this encode "any value".
1343void ProcessOneCompressedColumn(
1344 int variable, absl::Span<const int> tuple_literals,
1345 absl::Span<const absl::InlinedVector<int64_t, 2>> values,
1346 std::optional<int> table_is_active_literal, PresolveContext* context) {
1347 DCHECK_EQ(tuple_literals.size(), values.size());
1348
1349 // Collect pairs of value-literal.
1350 // Add the constraint literal => one of values.
1351 //
1352 // TODO(user): If we have n - 1 values, we could add the constraint that
1353 // tuple literal => not(last_value) instead?
1354 std::vector<std::pair<int64_t, int>> pairs;
1355 std::vector<int> any_values_literals;
1356 for (int i = 0; i < values.size(); ++i) {
1357 if (values[i].empty()) {
1358 any_values_literals.push_back(tuple_literals[i]);
1359 continue;
1360 }
1361
1362 ConstraintProto* ct = context->working_model->add_constraints();
1363 ct->add_enforcement_literal(tuple_literals[i]);
1364
1365 // It is slightly better to use a bool_and if size is 1 instead of
1366 // reconverting it at a later stage.
1367 auto* literals =
1368 values[i].size() == 1 ? ct->mutable_bool_and() : ct->mutable_bool_or();
1369 for (const int64_t v : values[i]) {
1370 DCHECK(context->DomainContains(variable, v));
1371 literals->add_literals(context->GetOrCreateVarValueEncoding(variable, v));
1372 pairs.emplace_back(v, tuple_literals[i]);
1373 }
1374 }
1375
1376 // Regroup literal with the same value and add for each the clause: If all the
1377 // tuples containing a value are false, then this value must be false too.
1378 std::vector<int> selected;
1379 std::sort(pairs.begin(), pairs.end());
1380 for (int i = 0; i < pairs.size();) {
1381 selected.clear();
1382 const int64_t value = pairs[i].first;
1383 for (; i < pairs.size() && pairs[i].first == value; ++i) {
1384 selected.push_back(pairs[i].second);
1385 }
1386
1387 // A value is supported if one tuple is still active, or a covering 'any'
1388 // tuple is still active, or the table can still be inactive.
1389 BoolArgumentProto* no_support =
1390 context->working_model->add_constraints()->mutable_bool_or();
1391 for (const int lit : selected) {
1392 no_support->add_literals(lit);
1393 }
1394 for (const int lit : any_values_literals) {
1395 no_support->add_literals(lit);
1396 }
1397 if (table_is_active_literal.has_value()) {
1398 no_support->add_literals(NegatedRef(table_is_active_literal.value()));
1399 }
1400
1401 // And the "value" literal.
1402 const int value_literal =
1403 context->GetOrCreateVarValueEncoding(variable, value);
1404 no_support->add_literals(NegatedRef(value_literal));
1405 }
1406}
1407
1408// Simpler encoding for table constraints with 2 variables.
1409void AddSizeTwoTable(
1410 absl::Span<const int> vars, absl::Span<const std::vector<int64_t>> tuples,
1411 absl::Span<const absl::flat_hash_set<int64_t>> values_per_var,
1412 PresolveContext* context) {
1413 CHECK_EQ(vars.size(), 2);
1414 const int left_var = vars[0];
1415 const int right_var = vars[1];
1416 if (context->DomainOf(left_var).IsFixed() ||
1417 context->DomainOf(right_var).IsFixed()) {
1418 // A table constraint with at most one variable not fixed is trivially
1419 // enforced after domain reduction.
1420 return;
1421 }
1422
1423 absl::btree_map<int, std::vector<int>> left_to_right;
1424 absl::btree_map<int, std::vector<int>> right_to_left;
1425
1426 for (const auto& tuple : tuples) {
1427 const int64_t left_value(tuple[0]);
1428 const int64_t right_value(tuple[1]);
1429 DCHECK(context->DomainContains(left_var, left_value));
1430 DCHECK(context->DomainContains(right_var, right_value));
1431
1432 const int left_literal =
1433 context->GetOrCreateVarValueEncoding(left_var, left_value);
1434 const int right_literal =
1435 context->GetOrCreateVarValueEncoding(right_var, right_value);
1436 left_to_right[left_literal].push_back(right_literal);
1437 right_to_left[right_literal].push_back(left_literal);
1438 }
1439
1440 int num_implications = 0;
1441 int num_clause_added = 0;
1442 int num_large_clause_added = 0;
1443 auto add_support_constraint =
1444 [context, &num_clause_added, &num_large_clause_added, &num_implications](
1445 int lit, absl::Span<const int> support_literals,
1446 int max_support_size) {
1447 if (support_literals.size() == max_support_size) return;
1448 if (support_literals.size() == 1) {
1449 context->AddImplication(lit, support_literals.front());
1450 num_implications++;
1451 } else {
1452 BoolArgumentProto* bool_or =
1453 context->working_model->add_constraints()->mutable_bool_or();
1454 for (const int support_literal : support_literals) {
1455 bool_or->add_literals(support_literal);
1456 }
1457 bool_or->add_literals(NegatedRef(lit));
1458 num_clause_added++;
1459 if (support_literals.size() > max_support_size / 2) {
1460 num_large_clause_added++;
1461 }
1462 }
1463 };
1464
1465 for (const auto& it : left_to_right) {
1466 add_support_constraint(it.first, it.second, values_per_var[1].size());
1467 }
1468 for (const auto& it : right_to_left) {
1469 add_support_constraint(it.first, it.second, values_per_var[0].size());
1470 }
1471 VLOG(2) << "Table: 2 variables, " << tuples.size() << " tuples encoded using "
1472 << num_clause_added << " clauses, including "
1473 << num_large_clause_added << " large clauses, " << num_implications
1474 << " implications";
1475}
1476
1477// A "WCSP" (weighted constraint programming) problem is usually encoded as
1478// a set of table, with one or more variable only there to carry a cost.
1479//
1480// If this is the case, we can do special presolving.
1481bool ReduceTableInPresenceOfUniqueVariableWithCosts(
1482 std::vector<int>* vars, std::vector<std::vector<int64_t>>* tuples,
1483 PresolveContext* context) {
1484 const int num_vars = vars->size();
1485
1486 std::vector<bool> only_here_and_in_objective(num_vars, false);
1487 std::vector<int64_t> objective_coeffs(num_vars, 0.0);
1488 std::vector<int> new_vars;
1489 std::vector<int> deleted_vars;
1490 for (int var_index = 0; var_index < num_vars; ++var_index) {
1491 const int var = (*vars)[var_index];
1492
1493 // We do not use VariableWithCostIsUniqueAndRemovable() since this one
1494 // return false if the objective is constraining but we don't care here.
1495 // Our transformation also do not loose solutions.
1496 if (context->VariableWithCostIsUnique(var)) {
1497 context->UpdateRuleStats("table: removed unused column with cost");
1498 only_here_and_in_objective[var_index] = true;
1499 objective_coeffs[var_index] =
1500 RefIsPositive(var) ? context->ObjectiveMap().at(var)
1501 : -context->ObjectiveMap().at(PositiveRef(var));
1502 context->RemoveVariableFromObjective(var);
1503 context->MarkVariableAsRemoved(var);
1504 deleted_vars.push_back(var);
1505 } else if (context->VarToConstraints(var).size() == 1) {
1506 // If there is no cost, we can remove that variable using the same code by
1507 // just setting the cost to zero.
1508 context->UpdateRuleStats("table: removed unused column");
1509 only_here_and_in_objective[var_index] = true;
1510 objective_coeffs[var_index] = 0;
1511 context->MarkVariableAsRemoved(var);
1512 deleted_vars.push_back(var);
1513 } else {
1514 new_vars.push_back(var);
1515 }
1516 }
1517 if (new_vars.size() == num_vars) return false;
1518
1519 // Rewrite the tuples.
1520 // put the cost last.
1521 int64_t min_cost = std::numeric_limits<int64_t>::max();
1522 std::vector<int64_t> temp;
1523 for (int i = 0; i < tuples->size(); ++i) {
1524 int64_t cost = 0;
1525 int new_size = 0;
1526 temp.clear();
1527 for (int var_index = 0; var_index < num_vars; ++var_index) {
1528 const int64_t value = (*tuples)[i][var_index];
1529 if (only_here_and_in_objective[var_index]) {
1530 temp.push_back(value);
1531 const int64_t objective_coeff = objective_coeffs[var_index];
1532 cost += value * objective_coeff;
1533 } else {
1534 (*tuples)[i][new_size++] = value;
1535 }
1536 }
1537 (*tuples)[i].resize(new_size);
1538 (*tuples)[i].push_back(cost);
1539 min_cost = std::min(min_cost, cost);
1540
1541 // Hack: we store the deleted value here so that we can properly encode
1542 // the postsolve constraints below.
1543 (*tuples)[i].insert((*tuples)[i].end(), temp.begin(), temp.end());
1544 }
1545
1546 // Remove tuples that only differ by their cost.
1547 // Make sure we will assign the proper value of the removed variable at
1548 // postsolve.
1549 {
1550 int new_size = 0;
1551 const int old_size = tuples->size();
1552 std::sort(tuples->begin(), tuples->end());
1553 for (int i = 0; i < tuples->size(); ++i) {
1554 // If the prefix (up to new_vars.size()) is the same, skip this tuple.
1555 if (new_size > 0) {
1556 bool skip = true;
1557 for (int var_index = 0; var_index < new_vars.size(); ++var_index) {
1558 if ((*tuples)[i][var_index] != (*tuples)[new_size - 1][var_index]) {
1559 skip = false;
1560 break;
1561 }
1562 }
1563 if (skip) continue;
1564 }
1565
1566 // If this tuple is selected, then fix the removed variable value in the
1567 // mapping model.
1568 for (int j = 0; j < deleted_vars.size(); ++j) {
1569 ConstraintProto* mapping_ct =
1570 context->NewMappingConstraint(__FILE__, __LINE__);
1571 for (int var_index = 0; var_index < new_vars.size(); ++var_index) {
1572 mapping_ct->add_enforcement_literal(
1573 context->GetOrCreateVarValueEncoding(new_vars[var_index],
1574 (*tuples)[i][var_index]));
1575 }
1576 LinearConstraintProto* new_lin = mapping_ct->mutable_linear();
1577 new_lin->add_vars(deleted_vars[j]);
1578 new_lin->add_coeffs(1);
1579 new_lin->add_domain((*tuples)[i][new_vars.size() + 1 + j]);
1580 new_lin->add_domain((*tuples)[i][new_vars.size() + 1 + j]);
1581 }
1582 (*tuples)[i].resize(new_vars.size() + 1);
1583 (*tuples)[new_size++] = (*tuples)[i];
1584 }
1585 tuples->resize(new_size);
1586 if (new_size < old_size) {
1587 context->UpdateRuleStats(
1588 "table: removed duplicate tuples with different costs");
1589 }
1590 }
1591
1592 if (min_cost > 0) {
1593 context->AddToObjectiveOffset(min_cost);
1594 context->UpdateRuleStats("table: transferred min_cost to objective offset");
1595 for (int i = 0; i < tuples->size(); ++i) {
1596 (*tuples)[i].back() -= min_cost;
1597 }
1598 }
1599
1600 // This comes from the WCSP litterature. Basically, if by fixing a variable to
1601 // a value, we have only tuples with a non-zero cost, we can substract the
1602 // minimum cost of these tuples and transfer it to the variable cost.
1603 //
1604 // TODO(user): Doing this before table compression can prevent good
1605 // compression. We should probably exploit this during compression to make
1606 // sure we compress as much as possible, and once compressed, do it again. Or
1607 // do it in a more general IP settings when one literal implies that a set of
1608 // literals with >0 cost are in EXO. We can transfer the min of their cost to
1609 // that Boolean.
1610 if (/*DISABLES CODE*/ (false)) {
1611 for (int var_index = 0; var_index < new_vars.size(); ++var_index) {
1612 absl::flat_hash_map<int64_t, int64_t> value_to_min_cost;
1613 const int num_tuples = tuples->size();
1614 for (int i = 0; i < num_tuples; ++i) {
1615 const int64_t v = (*tuples)[i][var_index];
1616 const int64_t cost = (*tuples)[i].back();
1617 auto insert = value_to_min_cost.insert({v, cost});
1618 if (!insert.second) {
1619 insert.first->second = std::min(insert.first->second, cost);
1620 }
1621 }
1622 for (int i = 0; i < num_tuples; ++i) {
1623 const int64_t v = (*tuples)[i][var_index];
1624 (*tuples)[i].back() -= value_to_min_cost.at(v);
1625 }
1626 for (const auto entry : value_to_min_cost) {
1627 if (entry.second == 0) continue;
1628 context->UpdateRuleStats("table: transferred cost to encoding");
1629 const int value_literal = context->GetOrCreateVarValueEncoding(
1630 new_vars[var_index], entry.first);
1631 context->AddLiteralToObjective(value_literal, entry.second);
1632 }
1633 }
1634 }
1635
1636 context->UpdateRuleStats(absl::StrCat(
1637 "table: expansion with column(s) only in objective. Arity = ",
1638 new_vars.size()));
1639
1640 *vars = new_vars;
1641 return true;
1642}
1643
1644// Important: the table and variable domains must be pre-solved before this
1645// is called. Some checks will fail otherwise.
1646void CompressAndExpandPositiveTable(ConstraintProto* ct,
1647 bool last_column_is_cost,
1648 absl::Span<const int> vars,
1649 std::vector<std::vector<int64_t>>* tuples,
1650 PresolveContext* context) {
1651 const int num_tuples_before_compression = tuples->size();
1652
1653 // If the last column is actually the tuple cost, we compress the table like
1654 // if this was a normal variable, but afterwards we treat it differently.
1655 std::vector<int64_t> domain_sizes;
1656 for (const int var : vars) {
1657 domain_sizes.push_back(context->DomainOf(var).Size());
1658 }
1659 if (last_column_is_cost) {
1660 domain_sizes.push_back(std::numeric_limits<int64_t>::max());
1661 }
1662
1663 // We start by compressing the table with kTableAnyValue only.
1664 const int compression_level = context->params().table_compression_level();
1665 if (compression_level > 0) {
1666 CompressTuples(domain_sizes, tuples);
1667 }
1668 const int num_tuples_after_first_compression = tuples->size();
1669
1670 // Tricky: If the table is big, it is better to compress it as much as
1671 // possible to reduce the number of created booleans. Otherwise, the more
1672 // verbose encoding can lead to better linear relaxation. Probably because the
1673 // tuple literal can encode each variable as sum literal * value. Also because
1674 // we have more direct implied bounds, which might lead to better cuts.
1675 //
1676 // For instance, on lot_sizing_cp_pigment15c.psp, compressing the table more
1677 // is a lot worse (at least until we can produce better cut).
1678 //
1679 // TODO(user): Tweak the heuristic, maybe compute the reduction achieve and
1680 // decide based on that.
1681 std::vector<std::vector<absl::InlinedVector<int64_t, 2>>> compressed_table;
1682 if (compression_level > 2 ||
1683 (compression_level == 2 && num_tuples_after_first_compression > 1000)) {
1684 compressed_table = FullyCompressTuples(domain_sizes, tuples);
1685 if (compressed_table.size() < num_tuples_before_compression) {
1686 context->UpdateRuleStats("table: fully compress tuples");
1687 }
1688 } else {
1689 // Convert the kTableAnyValue to an empty list format.
1690 for (int i = 0; i < tuples->size(); ++i) {
1691 compressed_table.push_back({});
1692 for (const int64_t v : (*tuples)[i]) {
1693 if (v == kTableAnyValue) {
1694 compressed_table.back().push_back({});
1695 } else {
1696 compressed_table.back().push_back({v});
1697 }
1698 }
1699 }
1700 if (compressed_table.size() < num_tuples_before_compression) {
1701 context->UpdateRuleStats("table: compress tuples");
1702 }
1703 }
1704
1705 VLOG(2) << "Table compression"
1706 << " var=" << vars.size()
1707 << " cost=" << domain_sizes.size() - vars.size()
1708 << " tuples= " << num_tuples_before_compression << " -> "
1709 << num_tuples_after_first_compression << " -> "
1710 << compressed_table.size();
1711
1712 // Affect mznc2017_aes_opt_r10 instance!
1713 std::sort(compressed_table.begin(), compressed_table.end());
1714
1715 const int num_vars = vars.size();
1716 if (compressed_table.size() == 1 && ct->enforcement_literal().empty()) {
1717 // Domains are propagated. We can remove the constraint.
1718 context->UpdateRuleStats("table: one tuple");
1719 if (last_column_is_cost) {
1720 // TODO(user): Because we transfer the cost, this should always be zero,
1721 // so not needed.
1722 context->AddToObjectiveOffset(compressed_table[0].back()[0]);
1723 }
1724 return;
1725 }
1726
1727 // Optimization. If a value is unique and appear alone in a cell, we can use
1728 // the encoding literal for this line tuple literal instead of creating a new
1729 // one.
1730 std::vector<bool> has_any(num_vars, false);
1731 std::vector<absl::flat_hash_map<int64_t, int>> var_index_to_value_count(
1732 num_vars);
1733 for (int i = 0; i < compressed_table.size(); ++i) {
1734 for (int var_index = 0; var_index < num_vars; ++var_index) {
1735 if (compressed_table[i][var_index].empty()) {
1736 has_any[var_index] = true;
1737 continue;
1738 }
1739 for (const int64_t v : compressed_table[i][var_index]) {
1740 DCHECK_NE(v, kTableAnyValue);
1741 DCHECK(context->DomainContains(vars[var_index], v));
1742 var_index_to_value_count[var_index][v]++;
1743 }
1744 }
1745 }
1746
1747 // Create one Boolean variable per tuple to indicate if it can still be
1748 // selected or not. Enforce an exactly one between them.
1749 BoolArgumentProto* exactly_one =
1750 context->working_model->add_constraints()->mutable_exactly_one();
1751
1752 std::optional<int> table_is_active_literal = std::nullopt;
1753 // Process enforcement literals.
1754 if (ct->enforcement_literal().size() == 1) {
1755 table_is_active_literal = ct->enforcement_literal(0);
1756 } else if (ct->enforcement_literal().size() > 1) {
1757 table_is_active_literal =
1758 context->NewBoolVarWithConjunction(ct->enforcement_literal());
1759
1760 // Adds table_is_active <=> and(enforcement_literals).
1761 BoolArgumentProto* bool_or =
1762 context->working_model->add_constraints()->mutable_bool_or();
1763 bool_or->add_literals(table_is_active_literal.value());
1764 for (const int lit : ct->enforcement_literal()) {
1765 context->AddImplication(table_is_active_literal.value(), lit);
1766 bool_or->add_literals(NegatedRef(lit));
1767 }
1768 }
1769 std::vector<int> existing_row_literals;
1770 std::vector<SolutionCrush::TableRowLiteral> new_row_literals;
1771 if (table_is_active_literal.has_value()) {
1772 const int inactive_lit = NegatedRef(table_is_active_literal.value());
1773 exactly_one->add_literals(inactive_lit);
1774 existing_row_literals.push_back(inactive_lit);
1775 }
1776
1777 int num_reused_variables = 0;
1778 std::vector<int> tuples_with_new_variable;
1779 std::vector<int> tuple_literals(compressed_table.size());
1780 for (int i = 0; i < compressed_table.size(); ++i) {
1781 bool create_new_var = true;
1782 for (int var_index = 0; var_index < num_vars; ++var_index) {
1783 if (has_any[var_index]) continue;
1784 if (compressed_table[i][var_index].size() != 1 ||
1785 !ct->enforcement_literal().empty()) {
1786 continue;
1787 }
1788 const int64_t v = compressed_table[i][var_index][0];
1789 if (var_index_to_value_count[var_index][v] != 1) continue;
1790
1791 ++num_reused_variables;
1792 create_new_var = false;
1793 tuple_literals[i] =
1794 context->GetOrCreateVarValueEncoding(vars[var_index], v);
1795 existing_row_literals.push_back(tuple_literals[i]);
1796 break;
1797 }
1798 if (create_new_var) {
1799 tuple_literals[i] = context->NewBoolVar("table expansion");
1800 new_row_literals.push_back({tuple_literals[i], compressed_table[i]});
1801 }
1802 exactly_one->add_literals(tuple_literals[i]);
1803 }
1804 if (num_reused_variables > 0) {
1805 context->UpdateRuleStats("table: reused literals");
1806 }
1807
1808 // Set the cost to the corresponding tuple literal. If there is more than one
1809 // cost, we just choose the first one which is the smallest one.
1810 if (last_column_is_cost) {
1811 for (int i = 0; i < tuple_literals.size(); ++i) {
1812 context->AddLiteralToObjective(tuple_literals[i],
1813 compressed_table[i].back()[0]);
1814 }
1815 }
1816
1817 std::vector<absl::InlinedVector<int64_t, 2>> column;
1818 for (int var_index = 0; var_index < num_vars; ++var_index) {
1819 if (context->IsFixed(vars[var_index])) continue;
1820
1821 column.clear();
1822 for (int i = 0; i < tuple_literals.size(); ++i) {
1823 column.push_back(compressed_table[i][var_index]);
1824 }
1825 ProcessOneCompressedColumn(vars[var_index], tuple_literals, column,
1826 table_is_active_literal, context);
1827 }
1828
1829 context->solution_crush().SetTableExpandedVars(vars, existing_row_literals,
1830 new_row_literals);
1831 context->UpdateRuleStats("table: expanded positive constraint");
1832}
1833
1834// TODO(user): reinvestigate ExploreSubsetOfVariablesAndAddNegatedTables.
1835//
1836// TODO(user): if 2 table constraints share the same valid prefix, the
1837// tuple literals can be reused.
1838//
1839// TODO(user): investigate different encoding for prefix tables. Maybe
1840// we can remove the need to create tuple literals.
1841void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) {
1842 DCHECK(TableIsInCanonicalForm(ct));
1843 const TableConstraintProto& table = ct->table();
1844 if (table.exprs().empty()) {
1845 CHECK(table.values().empty());
1846 context->UpdateRuleStats("table: empty trivial");
1847 ct->Clear();
1848 return;
1849 }
1850 const int num_exprs = table.exprs_size();
1851 const int num_original_tuples = table.values_size() / num_exprs;
1852
1853 // Read tuples flat array and recreate the vector of tuples.
1854 std::vector<int> vars;
1855 vars.reserve(table.exprs_size());
1856 if (table.values().empty()) {
1857 DCHECK(table.exprs_size() == 1 && table.exprs(0).vars().empty());
1858 } else {
1859 for (const LinearExpressionProto& expr : table.exprs()) {
1860 vars.push_back(expr.vars(0));
1861 }
1862 }
1863 std::vector<std::vector<int64_t>> tuples(num_original_tuples);
1864 int count = 0;
1865 for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
1866 for (int var_index = 0; var_index < num_exprs; ++var_index) {
1867 tuples[tuple_index].push_back(table.values(count++));
1868 }
1869 }
1870
1871 // Compute the set of possible values for each variable (from the table).
1872 // Remove invalid tuples along the way.
1873 std::vector<absl::flat_hash_set<int64_t>> values_per_var(num_exprs);
1874 int new_size = 0;
1875 for (int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
1876 bool keep = true;
1877 for (int var_index = 0; var_index < num_exprs; ++var_index) {
1878 const int64_t value = tuples[tuple_index][var_index];
1879 if (!context->DomainContains(vars[var_index], value)) {
1880 keep = false;
1881 break;
1882 }
1883 }
1884 if (keep) {
1885 for (int var_index = 0; var_index < num_exprs; ++var_index) {
1886 values_per_var[var_index].insert(tuples[tuple_index][var_index]);
1887 }
1888 std::swap(tuples[tuple_index], tuples[new_size]);
1889 new_size++;
1890 }
1891 }
1892 tuples.resize(new_size);
1893
1894 if (tuples.empty()) {
1895 if (ct->enforcement_literal().empty()) {
1896 context->UpdateRuleStats("table: empty");
1897 return (void)context->NotifyThatModelIsUnsat();
1898 } else {
1899 context->UpdateRuleStats("table: enforced and empty");
1900 BoolArgumentProto* bool_or =
1901 context->working_model->add_constraints()->mutable_bool_or();
1902 for (const int lit : ct->enforcement_literal()) {
1903 bool_or->add_literals(NegatedRef(lit));
1904 }
1905 ct->Clear();
1906 return;
1907 }
1908 }
1909
1910 // Update variable domains. It is redundant with presolve, but we could be
1911 // here with presolve = false.
1912 // Also counts the number of fixed variables.
1913 if (ct->enforcement_literal().empty()) {
1914 int num_fixed_variables = 0;
1915 for (int var_index = 0; var_index < num_exprs; ++var_index) {
1916 CHECK(context->IntersectDomainWith(
1917 vars[var_index],
1918 Domain::FromValues({values_per_var[var_index].begin(),
1919 values_per_var[var_index].end()})));
1920 if (context->DomainOf(vars[var_index]).IsFixed()) {
1921 num_fixed_variables++;
1922 }
1923 }
1924
1925 if (num_fixed_variables == num_exprs - 1) {
1926 context->UpdateRuleStats("table: one variable not fixed");
1927 ct->Clear();
1928 return;
1929 } else if (num_fixed_variables == num_exprs) {
1930 context->UpdateRuleStats("table: all variables fixed");
1931 ct->Clear();
1932 return;
1933 }
1934 }
1935
1936 // Tables with two variables do not need tuple literals.
1937 //
1938 // TODO(user): If there is an unique variable with cost, it is better to
1939 // detect it. But if the detection fail, we should still call
1940 // AddSizeTwoTable() unlike what happen here.
1941 if (num_exprs == 2 && !context->params().detect_table_with_cost() &&
1942 ct->enforcement_literal().empty()) {
1943 AddSizeTwoTable(vars, tuples, values_per_var, context);
1944 context->UpdateRuleStats(
1945 "table: expanded positive constraint with two variables");
1946 ct->Clear();
1947 return;
1948 }
1949
1950 bool last_column_is_cost = false;
1951 if (context->params().detect_table_with_cost() &&
1952 ct->enforcement_literal().empty()) {
1953 last_column_is_cost =
1954 ReduceTableInPresenceOfUniqueVariableWithCosts(&vars, &tuples, context);
1955 }
1956
1957 CompressAndExpandPositiveTable(ct, last_column_is_cost, vars, &tuples,
1958 context);
1959 ct->Clear();
1960}
1961
1962bool AllDiffShouldBeExpanded(const Domain& union_of_domains,
1963 ConstraintProto* ct, PresolveContext* context) {
1964 if (union_of_domains.Size() > context->params().max_alldiff_domain_size()) {
1965 return false;
1966 }
1967
1968 const AllDifferentConstraintProto& proto = *ct->mutable_all_diff();
1969 const int num_exprs = proto.exprs_size();
1970 int num_fully_encoded = 0;
1971 for (int i = 0; i < num_exprs; ++i) {
1972 if (context->IsFullyEncoded(proto.exprs(i))) {
1973 num_fully_encoded++;
1974 }
1975 }
1976
1977 if ((union_of_domains.Size() <= 2 * proto.exprs_size()) ||
1978 (union_of_domains.Size() <= 32)) {
1979 // Small domains.
1980 return true;
1981 }
1982
1983 if (num_fully_encoded == num_exprs) {
1984 // All variables fully encoded, and domains are small enough.
1985 return true;
1986 }
1987 return false;
1988}
1989
1990// Replaces a constraint literal => ax + by != cte by a set of clauses.
1991// This is performed if the domains are small enough, and the variables are
1992// fully encoded.
1993//
1994// We do it during the expansion as we want the first pass of the presolve to be
1995// complete.
1996void ExpandSomeLinearOfSizeTwo(ConstraintProto* ct, PresolveContext* context) {
1997 const LinearConstraintProto& arg = ct->linear();
1998 if (arg.vars_size() != 2) return;
1999
2000 const int var1 = arg.vars(0);
2001 const int var2 = arg.vars(1);
2002 if (context->IsFixed(var1) || context->IsFixed(var2)) return;
2003
2004 const int64_t coeff1 = arg.coeffs(0);
2005 const int64_t coeff2 = arg.coeffs(1);
2006 const Domain reachable_rhs_superset =
2007 context->DomainOf(var1)
2008 .MultiplicationBy(coeff1)
2009 .RelaxIfTooComplex()
2010 .AdditionWith(context->DomainOf(var2)
2011 .MultiplicationBy(coeff2)
2012 .RelaxIfTooComplex());
2013 const Domain infeasible_reachable_values =
2014 reachable_rhs_superset.IntersectionWith(
2015 ReadDomainFromProto(arg).Complement());
2016
2017 // We only deal with != cte constraints.
2018 if (infeasible_reachable_values.Size() != 1) return;
2019
2020 // coeff1 * v1 + coeff2 * v2 != cte.
2021 int64_t a = coeff1;
2022 int64_t b = coeff2;
2023 int64_t cte = infeasible_reachable_values.FixedValue();
2024 int64_t x0 = 0;
2025 int64_t y0 = 0;
2026 if (!SolveDiophantineEquationOfSizeTwo(a, b, cte, x0, y0)) {
2027 // no solution.
2028 context->UpdateRuleStats("linear: expand always feasible ax + by != cte");
2029 ct->Clear();
2030 return;
2031 }
2032 const Domain reduced_domain =
2033 context->DomainOf(var1)
2034 .AdditionWith(Domain(-x0))
2035 .InverseMultiplicationBy(b)
2036 .IntersectionWith(context->DomainOf(var2)
2037 .AdditionWith(Domain(-y0))
2038 .InverseMultiplicationBy(-a));
2039
2040 if (reduced_domain.Size() > 16) return;
2041
2042 // Check if all the needed values are encoded.
2043 // TODO(user): Do we force encoding for very small domains? Current
2044 // experiments says no, but revisit later.
2045 const int64_t size1 = context->DomainOf(var1).Size();
2046 const int64_t size2 = context->DomainOf(var2).Size();
2047 for (const int64_t z : reduced_domain.Values()) {
2048 const int64_t value1 = x0 + b * z;
2049 const int64_t value2 = y0 - a * z;
2050 DCHECK(context->DomainContains(var1, value1)) << "value1 = " << value1;
2051 DCHECK(context->DomainContains(var2, value2)) << "value2 = " << value2;
2052 DCHECK_EQ(coeff1 * value1 + coeff2 * value2,
2053 infeasible_reachable_values.FixedValue());
2054 // TODO(user): Presolve if one or two variables are Boolean.
2055 if (!context->HasVarValueEncoding(var1, value1, nullptr) || size1 == 2) {
2056 return;
2057 }
2058 if (!context->HasVarValueEncoding(var2, value2, nullptr) || size2 == 2) {
2059 return;
2060 }
2061 }
2062
2063 // All encoding literals already exist and the number of clauses to create
2064 // is small enough. We can encode the constraint using just clauses.
2065 for (const int64_t z : reduced_domain.Values()) {
2066 const int64_t value1 = x0 + b * z;
2067 const int64_t value2 = y0 - a * z;
2068 // We cannot have both lit1 and lit2 true.
2069 const int lit1 = context->GetOrCreateVarValueEncoding(var1, value1);
2070 const int lit2 = context->GetOrCreateVarValueEncoding(var2, value2);
2071 auto* bool_or =
2072 context->working_model->add_constraints()->mutable_bool_or();
2073 bool_or->add_literals(NegatedRef(lit1));
2074 bool_or->add_literals(NegatedRef(lit2));
2075 for (const int lit : ct->enforcement_literal()) {
2076 bool_or->add_literals(NegatedRef(lit));
2077 }
2078 }
2079
2080 context->UpdateRuleStats("linear: expand small ax + by != cte");
2081 ct->Clear();
2082}
2083
2084// Note that we used to do that at loading time, but we prefer to do that as
2085// part of the presolve so that all variables are available for sharing between
2086// subworkers and also are accessible by the linear relaxation.
2087//
2088// TODO(user): Note that currently both encoding introduce extra solutions
2089// if the constraint has some enforcement literal(). We can either fix this by
2090// supporting enumeration on a subset of variable. Or add extra constraint to
2091// fix all new Boolean to false if the initial constraint is not enforced.
2092void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
2093 PresolveContext* context) {
2094 // TODO(user): We treat the linear of size 1 differently because we need them
2095 // as is to recognize value encoding. Try to still creates needed Boolean now
2096 // so that we can share more between the different workers. Or revisit how
2097 // linear1 are propagated.
2098 if (ct->linear().domain().size() <= 2) return;
2099 if (ct->linear().vars().size() == 1) return;
2100
2101 const SatParameters& params = context->params();
2102 if (params.encode_complex_linear_constraint_with_integer()) {
2103 // Integer encoding.
2104 //
2105 // Here we add a slack with domain equal to rhs and transform
2106 // expr \in rhs to expr - slack = 0
2107 const Domain rhs = ReadDomainFromProto(ct->linear());
2108 const int slack = context->NewIntVar(rhs);
2109 context->solution_crush().SetVarToLinearExpression(
2110 slack, ct->linear().vars(), ct->linear().coeffs());
2111 ct->mutable_linear()->add_vars(slack);
2112 ct->mutable_linear()->add_coeffs(-1);
2113 ct->mutable_linear()->clear_domain();
2114 ct->mutable_linear()->add_domain(0);
2115 ct->mutable_linear()->add_domain(0);
2116 } else {
2117 // Boolean encoding.
2118 int single_bool;
2119 BoolArgumentProto* clause = nullptr;
2120 if (ct->enforcement_literal().empty() && ct->linear().domain_size() == 4) {
2121 // We cover the special case of no enforcement and two choices by creating
2122 // a single Boolean.
2123 single_bool = context->NewBoolVar("complex linear expansion");
2124 } else {
2125 clause = context->working_model->add_constraints()->mutable_bool_or();
2126 for (const int ref : ct->enforcement_literal()) {
2127 clause->add_literals(NegatedRef(ref));
2128 }
2129 }
2130
2131 // Save enforcement literals for the enumeration.
2132 const std::vector<int> enforcement_literals(
2133 ct->enforcement_literal().begin(), ct->enforcement_literal().end());
2134 ct->mutable_enforcement_literal()->Clear();
2135 std::vector<int> domain_literals;
2136 for (int i = 0; i < ct->linear().domain_size(); i += 2) {
2137 const int64_t lb = ct->linear().domain(i);
2138 const int64_t ub = ct->linear().domain(i + 1);
2139
2140 int subdomain_literal;
2141 if (clause != nullptr) {
2142 subdomain_literal = context->NewBoolVar("complex linear expansion");
2143 clause->add_literals(subdomain_literal);
2144 domain_literals.push_back(subdomain_literal);
2145 } else {
2146 if (i == 0) domain_literals.push_back(single_bool);
2147 subdomain_literal = i == 0 ? single_bool : NegatedRef(single_bool);
2148 }
2149
2150 // Create a new constraint which is a copy of the original, but with a
2151 // simple sub-domain and enforcement literal.
2152 ConstraintProto* new_ct = context->working_model->add_constraints();
2153 *new_ct = *ct;
2154 new_ct->add_enforcement_literal(subdomain_literal);
2155 FillDomainInProto(Domain(lb, ub), new_ct->mutable_linear());
2156 }
2157 context->solution_crush().SetLinearWithComplexDomainExpandedVars(
2158 ct->linear(), domain_literals);
2159
2160 // Make sure all booleans are tights when enumerating all solutions.
2161 if (context->params().enumerate_all_solutions() &&
2162 !enforcement_literals.empty()) {
2163 int linear_is_enforced;
2164 if (enforcement_literals.size() == 1) {
2165 linear_is_enforced = enforcement_literals[0];
2166 } else {
2167 linear_is_enforced = context->NewBoolVar("complex linear expansion");
2168 BoolArgumentProto* maintain_linear_is_enforced =
2169 context->working_model->add_constraints()->mutable_bool_or();
2170 for (const int e_lit : enforcement_literals) {
2171 context->AddImplication(NegatedRef(e_lit),
2172 NegatedRef(linear_is_enforced));
2173 maintain_linear_is_enforced->add_literals(NegatedRef(e_lit));
2174 }
2175 maintain_linear_is_enforced->add_literals(linear_is_enforced);
2176 context->solution_crush().SetVarToConjunction(linear_is_enforced,
2177 enforcement_literals);
2178 }
2179
2180 for (const int lit : domain_literals) {
2181 context->AddImplication(NegatedRef(linear_is_enforced),
2182 NegatedRef(lit));
2183 }
2184 }
2185 ct->Clear();
2186 }
2187
2188 context->UpdateRuleStats("linear: expanded complex rhs");
2189 context->InitializeNewDomains();
2190 context->UpdateNewConstraintsVariableUsage();
2191 context->UpdateConstraintVariableUsage(c);
2192}
2193
2194bool IsVarEqOrNeqValue(PresolveContext* context,
2195 const LinearConstraintProto& lin) {
2196 if (lin.vars_size() != 1) return false;
2197 const Domain rhs = ReadDomainFromProto(lin);
2198
2199 // This is literal => var == value.
2200 if (rhs.IsFixed()) return true;
2201
2202 // Is it literal => var != value ?
2203 const Domain not_implied =
2204 rhs.InverseMultiplicationBy(lin.coeffs(0))
2205 .Complement()
2206 .IntersectionWith(context->DomainOf(lin.vars(0)));
2207 if (not_implied.IsEmpty()) return false;
2208 return not_implied.IsFixed();
2209}
2210
2211// This method will scan all constraints of all variables appearing in an
2212// all_diff.
2213// There are 3 outcomes:
2214// - maybe expand to Boolean variables (depending on the size)
2215// - keep integer all_different constraint (and cuts)
2216// - expand and keep
2217//
2218// Expand is selected if the variable is fully encoded, or will be when
2219// expanding other constraints: index of element, table, automaton.
2220// It will check AllDiffShouldBeExpanded() before doing the actual expansion.
2221// Keep is forced is the variable appears in a linear equation with at least 3
2222// terms, and with a tight domain ( == cst).
2223// TODO(user): The above rule is complex. Revisit.
2224void ScanModelAndDecideAllDiffExpansion(
2225 ConstraintProto* all_diff_ct, PresolveContext* context,
2226 absl::flat_hash_set<int>& domain_of_var_is_used,
2227 absl::flat_hash_set<int>& bounds_of_var_are_used,
2228 absl::flat_hash_set<int>& processed_variables, bool& expand, bool& keep) {
2229 CHECK_EQ(all_diff_ct->constraint_case(), ConstraintProto::kAllDiff);
2230
2231 bool at_least_one_var_domain_is_used = false;
2232 bool at_least_one_var_bound_is_used = false;
2233
2234 // Scan variables.
2235 for (const LinearExpressionProto& expr : all_diff_ct->all_diff().exprs()) {
2236 // Skip constant expressions.
2237 if (expr.vars().empty()) continue;
2238 DCHECK_EQ(1, expr.vars_size());
2239 const int var = expr.vars(0);
2240 DCHECK(RefIsPositive(var));
2241 if (context->IsFixed(var)) continue;
2242
2243 bool at_least_one_var_domain_is_used = false;
2244 bool at_least_one_var_bound_is_used = false;
2245
2246 // Check cache.
2247 if (!processed_variables.insert(var).second) {
2248 at_least_one_var_domain_is_used = bounds_of_var_are_used.contains(var);
2249 at_least_one_var_bound_is_used = domain_of_var_is_used.contains(var);
2250 } else {
2251 bool domain_is_used = false;
2252 bool bounds_are_used = false;
2253
2254 // Note: Boolean constraints are ignored.
2255 for (const int ct_index : context->VarToConstraints(var)) {
2256 // Skip artificial constraints.
2257 if (ct_index < 0) continue;
2258
2259 const ConstraintProto& other_ct =
2260 context->working_model->constraints(ct_index);
2261 switch (other_ct.constraint_case()) {
2263 break;
2265 break;
2267 break;
2269 break;
2271 break;
2273 break;
2275 break;
2277 bounds_are_used = true;
2278 break;
2280 break;
2282 if (IsVarEqOrNeqValue(context, other_ct.linear()) &&
2283 var == other_ct.linear().vars(0)) {
2284 // Encoding literals.
2285 domain_is_used = true;
2286 } else if (other_ct.linear().vars_size() > 2 &&
2287 other_ct.linear().domain_size() == 2 &&
2288 other_ct.linear().domain(0) ==
2289 other_ct.linear().domain(1)) {
2290 // We assume all_diff cuts will only be useful if the linear
2291 // constraint has a fixed domain.
2292 bounds_are_used = true;
2293 }
2294 break;
2296 // We ignore all_diffs as we are trying to decide their expansion
2297 // from the rest of the model.
2298 break;
2300 break;
2302 // Note: elements should have been expanded.
2303 if (other_ct.element().index() == var) {
2304 domain_is_used = true;
2305 }
2306 break;
2308 break;
2310 break;
2312 domain_is_used = true;
2313 break;
2315 break;
2317 domain_is_used = true;
2318 break;
2320 domain_is_used = true;
2321 break;
2323 bounds_are_used = true;
2324 break;
2326 // Will be covered by the interval case.
2327 break;
2329 // Will be covered by the interval case.
2330 break;
2332 // Will be covered by the interval case.
2333 break;
2335 break;
2336 }
2337
2338 // Exit early.
2339 if (domain_is_used && bounds_are_used) break;
2340 } // Loop on other_ct.
2341
2342 // Update cache.
2343 if (domain_is_used) domain_of_var_is_used.insert(var);
2344 if (bounds_are_used) bounds_of_var_are_used.insert(var);
2345
2346 // Update the usage of the variable.
2347 at_least_one_var_domain_is_used |= domain_is_used;
2348 at_least_one_var_bound_is_used |= bounds_are_used;
2349 } // End of model scanning.
2350
2351 if (at_least_one_var_domain_is_used && at_least_one_var_bound_is_used) {
2352 break; // No need to scan the rest of the all_diff.
2353 }
2354 } // End of var processing.
2355
2356 expand = at_least_one_var_domain_is_used;
2357 keep = at_least_one_var_bound_is_used;
2358}
2359
2360void MaybeExpandAllDiff(ConstraintProto* ct, PresolveContext* context,
2361 absl::flat_hash_set<int>& domain_of_var_is_used,
2362 absl::flat_hash_set<int>& bounds_of_var_are_used,
2363 absl::flat_hash_set<int>& processed_variable) {
2364 const bool expand_all_diff_from_parameters =
2365 context->params().expand_alldiff_constraints();
2366 AllDifferentConstraintProto& proto = *ct->mutable_all_diff();
2367 if (proto.exprs_size() <= 1) return;
2368 if (context->ModelIsUnsat()) return;
2369
2370 bool keep_after_expansion = false;
2371 bool expand_all_diff_from_usage = false;
2372 ScanModelAndDecideAllDiffExpansion(
2373 ct, context, domain_of_var_is_used, bounds_of_var_are_used,
2374 processed_variable, expand_all_diff_from_usage, keep_after_expansion);
2375
2376 const int num_exprs = proto.exprs_size();
2377 Domain union_of_domains = context->DomainSuperSetOf(proto.exprs(0));
2378 for (int i = 1; i < num_exprs; ++i) {
2379 union_of_domains =
2380 union_of_domains.UnionWith(context->DomainSuperSetOf(proto.exprs(i)));
2381 }
2382
2383 const bool expand_all_diff_from_size =
2384 AllDiffShouldBeExpanded(union_of_domains, ct, context);
2385
2386 // Decide expansion:
2387 // - always expand if expand_all_diff_from_parameters
2388 // - expand if size is compatible (expand_all_diff_from_size) and
2389 // expansion is desired:
2390 // expand_all_diff_from_usage || !keep_after_expansion
2391 const bool should_expand =
2392 expand_all_diff_from_parameters ||
2393 (expand_all_diff_from_size &&
2394 (expand_all_diff_from_usage || !keep_after_expansion));
2395 if (!should_expand) return;
2396
2397 const bool is_a_permutation = num_exprs == union_of_domains.Size();
2398
2399 // Collect all possible variables that can take each value, and add one linear
2400 // equation per value stating that this value can be assigned at most once, or
2401 // exactly once in case of permutation.
2402 for (const int64_t v : union_of_domains.Values()) {
2403 // Collect references which domain contains v.
2404 std::vector<LinearExpressionProto> possible_exprs;
2405 int fixed_expression_count = 0;
2406 for (const LinearExpressionProto& expr : proto.exprs()) {
2407 if (!context->DomainContains(expr, v)) continue;
2408 possible_exprs.push_back(expr);
2409 if (context->IsFixed(expr)) {
2410 fixed_expression_count++;
2411 }
2412 }
2413
2414 if (fixed_expression_count > 1) {
2415 // Violates the definition of AllDifferent.
2416 return (void)context->NotifyThatModelIsUnsat();
2417 } else if (fixed_expression_count == 1) {
2418 // Remove values from other domains.
2419 for (const LinearExpressionProto& expr : possible_exprs) {
2420 if (context->IsFixed(expr)) continue;
2421 if (!context->IntersectDomainWith(expr, Domain(v).Complement())) {
2422 VLOG(1) << "Empty domain for a variable in MaybeExpandAllDiff()";
2423 return;
2424 }
2425 }
2426 }
2427
2428 BoolArgumentProto* at_most_or_equal_one =
2429 is_a_permutation
2430 ? context->working_model->add_constraints()->mutable_exactly_one()
2431 : context->working_model->add_constraints()->mutable_at_most_one();
2432 for (const LinearExpressionProto& expr : possible_exprs) {
2433 // The above propagation can remove a value after the expressions was
2434 // added to possible_exprs.
2435 if (!context->DomainContains(expr, v)) continue;
2436
2437 // If the expression is fixed, the created literal will be the true
2438 // literal. We still need to fail if two expressions are fixed to the same
2439 // value.
2440 const int encoding = context->GetOrCreateAffineValueEncoding(expr, v);
2441 at_most_or_equal_one->add_literals(encoding);
2442 }
2443 }
2444
2445 context->UpdateRuleStats(
2446 absl::StrCat("all_diff:", is_a_permutation ? " permutation" : "",
2447 " expanded", keep_after_expansion ? " and kept" : ""));
2448 if (!keep_after_expansion) ct->Clear();
2449}
2450
2451} // namespace
2452
2454 if (context->params().disable_constraint_expansion()) return;
2455 if (context->ModelIsUnsat()) return;
2456
2457 // None of the function here need to be run twice. This is because we never
2458 // create constraint that need to be expanded during presolve.
2459 if (context->ModelIsExpanded()) return;
2460
2461 // Make sure all domains are initialized.
2462 context->InitializeNewDomains();
2463 if (context->ModelIsUnsat()) return;
2464
2465 // Clear the precedence cache.
2466 context->ClearPrecedenceCache();
2467
2468 bool has_all_diffs = false;
2469
2470 // First pass: we look at constraints that may fully encode variables.
2471 for (int c = 0; c < context->working_model->constraints_size(); ++c) {
2472 ConstraintProto* const ct = context->working_model->mutable_constraints(c);
2473 bool skip = false;
2474 switch (ct->constraint_case()) {
2476 // If we only do expansion, we do that as part of the main loop.
2477 // This way we don't need to call FinalExpansionForLinearConstraint().
2478 if (ct->linear().domain().size() > 2 &&
2479 !context->params().cp_model_presolve()) {
2480 ExpandComplexLinearConstraint(c, ct, context);
2481 }
2482 break;
2484 if (context->params().expand_reservoir_constraints()) {
2485 ExpandReservoir(ct, context);
2486 }
2487 break;
2489 if (context->params().encode_cumulative_as_reservoir()) {
2490 EncodeCumulativeAsReservoir(ct, context);
2491 }
2492 break;
2494 ExpandIntMod(ct, context);
2495 break;
2497 ExpandIntProd(ct, context);
2498 break;
2500 ExpandElement(ct, context);
2501 break;
2503 ExpandInverse(ct, context);
2504 break;
2506 ExpandAutomaton(ct, context);
2507 break;
2509 if (!context->params().cp_model_presolve()) {
2510 CanonicalizeTable(context, ct);
2511 }
2512 if (ct->table().negated()) {
2513 ExpandNegativeTable(ct, context);
2514 } else {
2515 ExpandPositiveTable(ct, context);
2516 }
2517 break;
2519 if (ct->lin_max().exprs().size() <=
2521 ExpandLinMax(ct, context);
2522 }
2523 break;
2525 has_all_diffs = true;
2526 skip = true;
2527 break;
2528 default:
2529 skip = true;
2530 break;
2531 }
2532 if (skip) continue; // Nothing was done for this constraint.
2533
2534 // Update variable-constraint graph.
2538 }
2539
2540 // Early exit if the model is unsat.
2541 if (context->ModelIsUnsat()) {
2542 SOLVER_LOG(context->logger(), "UNSAT after expansion of ",
2544 return;
2545 }
2546 }
2547
2548 // Second pass. We may decide to expand constraints if all their variables
2549 // are fully encoded.
2550 //
2551 // Cache for variable scanning.
2552 absl::flat_hash_set<int> domain_of_var_is_used;
2553 absl::flat_hash_set<int> bounds_of_var_are_used;
2554 absl::flat_hash_set<int> processed_variables;
2555 for (int i = 0; i < context->working_model->constraints_size(); ++i) {
2556 ConstraintProto* const ct = context->working_model->mutable_constraints(i);
2557 bool skip = false;
2558 switch (ct->constraint_case()) {
2560 MaybeExpandAllDiff(ct, context, domain_of_var_is_used,
2561 bounds_of_var_are_used, processed_variables);
2562 break;
2564 ExpandSomeLinearOfSizeTwo(ct, context);
2565 break;
2566 default:
2567 skip = true;
2568 break;
2569 }
2570
2571 if (skip) continue; // Nothing was done for this constraint.
2572
2573 // Update variable-constraint graph.
2577 }
2578
2579 // Early exit if the model is unsat.
2580 if (context->ModelIsUnsat()) {
2581 SOLVER_LOG(context->logger(), "UNSAT after expansion of ",
2583 return;
2584 }
2585 }
2586
2587 // The precedence cache can become invalid during presolve as it does not
2588 // handle variable substitution. It is safer just to clear it at the end
2589 // of the expansion phase.
2590 context->ClearPrecedenceCache();
2591
2592 // Make sure the context is consistent.
2593 context->InitializeNewDomains();
2594
2595 // Update any changed domain from the context.
2596 for (int i = 0; i < context->working_model->variables_size(); ++i) {
2597 FillDomainInProto(context->DomainOf(i),
2598 context->working_model->mutable_variables(i));
2599 }
2600
2601 context->NotifyThatModelIsExpanded();
2602}
2603
2605 if (context->params().disable_constraint_expansion()) return;
2606 if (context->ModelIsUnsat()) return;
2607 for (int c = 0; c < context->working_model->constraints_size(); ++c) {
2608 ConstraintProto* const ct = context->working_model->mutable_constraints(c);
2609 switch (ct->constraint_case()) {
2611 if (ct->linear().domain().size() > 2) {
2612 ExpandComplexLinearConstraint(c, ct, context);
2613 }
2614 break;
2615 default:
2616 break;
2617 }
2618 }
2619}
2620
2621} // namespace sat
2622} // namespace operations_research
static Domain FromValues(std::vector< int64_t > values)
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 1;
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
const ::operations_research::sat::TableConstraintProto & table() const
const ::operations_research::sat::LinearConstraintProto & linear() const
::operations_research::sat::ReservoirConstraintProto *PROTOBUF_NONNULL mutable_reservoir()
const ::operations_research::sat::LinearArgumentProto & lin_max() const
::operations_research::sat::LinearConstraintProto *PROTOBUF_NONNULL mutable_linear()
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_enforcement_literal()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL mutable_constraints(int index)
int constraints_size() const
repeated .operations_research.sat.ConstraintProto constraints = 3;
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL mutable_variables(int index)
::operations_research::sat::LinearExpressionProto *PROTOBUF_NONNULL mutable_target()
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
::operations_research::sat::LinearExpressionProto *PROTOBUF_NONNULL add_exprs()
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
void ClearPrecedenceCache()
Clear the precedence cache.
void InitializeNewDomains()
Creates the internal structure for any new variables in working_model.
void UpdateNewConstraintsVariableUsage()
Calls UpdateConstraintVariableUsage() on all newly created constraints.
int time_exprs_size() const
repeated .operations_research.sat.LinearExpressionProto time_exprs = 3;
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 4;
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:55
constexpr int64_t kTableAnyValue
void CompressTuples(absl::Span< const int64_t > domain_sizes, std::vector< std::vector< int64_t > > *tuples)
void ExpandCpModel(PresolveContext *context)
bool SolveDiophantineEquationOfSizeTwo(int64_t &a, int64_t &b, int64_t &cte, int64_t &x0, int64_t &y0)
Definition util.cc:204
std::vector< std::vector< absl::InlinedVector< int64_t, 2 > > > FullyCompressTuples(absl::Span< const int64_t > domain_sizes, std::vector< std::vector< int64_t > > *tuples)
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset, std::pair< int64_t, int64_t > *implied_domain)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
void FinalExpansionForLinearConstraint(PresolveContext *context)
int64_t AffineExpressionValueAt(const LinearExpressionProto &expr, int64_t value)
Evaluates an affine expression at the given value.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
bool ExpressionsContainsOnlyOneVar(const ExpressionList &exprs)
Returns true if there exactly one variable appearing in all the expressions.
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
void PropagateAutomaton(const AutomatonConstraintProto &proto, const PresolveContext &context, std::vector< absl::flat_hash_set< int64_t > > *states, std::vector< absl::flat_hash_set< int64_t > > *labels)
Fills and propagates the set of reachable states/labels.
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff, LinearConstraintProto *linear, int64_t *offset)
void CanonicalizeTable(PresolveContext *context, ConstraintProto *ct)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
std::string ProtobufShortDebugString(const P &message)
Definition proto_utils.h:46
#define SOLVER_LOG(logger,...)
Definition logging.h:110