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"
38#include "ortools/sat/cp_model.pb.h"
43#include "ortools/sat/sat_parameters.pb.h"
55void ExpandReservoirUsingCircuit(int64_t sum_of_positive_demand,
56 int64_t sum_of_negative_demand,
57 ConstraintProto* reservoir_ct,
59 const ReservoirConstraintProto& reservoir = reservoir_ct->reservoir();
60 const int num_events = reservoir.time_exprs_size();
64 CircuitConstraintProto* circuit =
65 context->working_model->add_constraints()->mutable_circuit();
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));
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);
85 for (
int i = 0;
i < num_events; ++
i) {
86 if (!reservoir.active_literals().empty()) {
88 circuit->add_tails(
i);
89 circuit->add_heads(
i);
90 circuit->add_literals(
NegatedRef(reservoir.active_literals(
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);
104 ConstraintProto* new_ct = context->working_model->add_constraints();
105 new_ct->add_enforcement_literal(start_var);
106 LinearConstraintProto* lin = new_ct->mutable_linear();
109 lin->add_vars(level_vars[
i]);
113 context->CanonicalizeLinearConstraint(new_ct);
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);
123 for (
int j = 0; j < num_events; ++j) {
124 if (
i == j)
continue;
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);
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();
147 lin->add_domain(std::numeric_limits<int64_t>::max());
150 context->CanonicalizeLinearConstraint(new_ct);
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();
160 lin->add_vars(level_vars[j]);
162 lin->add_vars(level_vars[
i]);
166 context->CanonicalizeLinearConstraint(new_ct);
170 context->solution_crush().SetReservoirCircuitVars(reservoir, var_min, var_max,
171 level_vars, *circuit);
173 reservoir_ct->Clear();
174 context->UpdateRuleStats(
"reservoir: expanded using circuit.");
177void ExpandReservoirUsingPrecedences(
bool max_level_is_constraining,
178 bool min_level_is_constraining,
179 ConstraintProto* reservoir_ct,
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);
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;
195 const int64_t demand_i = context->FixedValue(reservoir.level_changes(
i));
196 if (demand_i == 0)
continue;
200 if (demand_i > 0 && !max_level_is_constraining)
continue;
201 if (demand_i < 0 && !min_level_is_constraining)
continue;
203 ConstraintProto* new_cumul = context->working_model->add_constraints();
204 LinearConstraintProto* new_linear = new_cumul->mutable_linear();
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;
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);
239 new_linear->add_domain(std::numeric_limits<int64_t>::min());
240 new_linear->add_domain(reservoir.max_level() - offset);
242 new_linear->add_domain(reservoir.min_level() - offset);
243 new_linear->add_domain(std::numeric_limits<int64_t>::max());
247 context->CanonicalizeLinearConstraint(new_cumul);
250 new_linear->coeffs()));
253 reservoir_ct->Clear();
254 context->UpdateRuleStats(
"reservoir: expanded using precedences");
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();
264 const ReservoirConstraintProto& reservoir = reservoir_ct->reservoir();
265 const int num_events = reservoir.time_exprs_size();
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;
276 const int64_t max_demand = context->MaxOf(demand_expr);
277 if (max_demand > 0) {
279 sum_of_positive_demand += max_demand;
281 const int64_t min_demand = context->MinOf(demand_expr);
282 if (min_demand < 0) {
284 sum_of_negative_demand += min_demand;
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();
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()
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));
310 sum->add_vars(active);
311 sum->add_coeffs(change);
314 sum->add_vars(true_literal);
315 sum->add_coeffs(change);
317 sum->add_coeffs(-change);
319 }
else if (context->LiteralIsTrue(active)) {
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);
330 ConstraintProto* demand_ct =
331 context->working_model->add_constraints();
332 demand_ct->add_enforcement_literal(active);
333 LinearConstraintProto* lin = demand_ct->mutable_linear();
336 lin->add_vars(new_var);
339 context->CanonicalizeLinearConstraint(demand_ct);
340 context->solution_crush().SetVarToLinearExpressionIf(new_var, demand,
345 context->AddImplyInDomain(
NegatedRef(active), new_var, Domain(0));
346 context->solution_crush().SetVarToValueIf(new_var, 0,
350 sum->add_domain(reservoir.min_level());
351 sum->add_domain(reservoir.max_level());
352 context->CanonicalizeLinearConstraint(new_ct);
354 context->UpdateRuleStats(
"reservoir: simple expansion with sum");
355 reservoir_ct->Clear();
360 if (context->params().expand_reservoir_using_circuit()) {
361 ExpandReservoirUsingCircuit(sum_of_positive_demand, sum_of_negative_demand,
362 reservoir_ct, context);
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);
371 context->UpdateRuleStats(
372 "reservoir: skipped expansion due to variable demands");
378void EncodeCumulativeAsReservoir(ConstraintProto* ct,
380 if (!context->IsFixed(ct->cumulative().capacity())) {
381 context->UpdateRuleStats(
382 "cumulative -> reservoir: expansion is not supported with variable "
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()));
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();
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));
412 if (interval_ct.enforcement_literal().empty()) {
413 reservoir->add_active_literals(true_literal);
414 reservoir->add_active_literals(true_literal);
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));
424 context->UpdateRuleStats(
"cumulative: expanded into reservoir");
425 ExpandReservoir(&reservoir_ct, 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;
433 const LinearExpressionProto& expr = int_mod.exprs(0);
434 const LinearExpressionProto& target_expr = int_mod.target();
437 if (!context->IntersectDomainWith(
438 target_expr, context->DomainSuperSetOf(expr).PositiveModuloBySuperset(
439 context->DomainSuperSetOf(mod_expr)))) {
444 auto new_enforced_constraint = [&]() {
445 ConstraintProto* new_ct = context->working_model->add_constraints();
446 *new_ct->mutable_enforcement_literal() = ct->enforcement_literal();
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);
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;
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);
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;
482 LinearConstraintProto*
const lin =
483 new_enforced_constraint()->mutable_linear();
490 context->solution_crush().SetIntModExpandedVars(*ct, div_var, prod_var,
491 context->MinOf(div_var),
492 context->MinOf(prod_var));
494 context->UpdateRuleStats(
"int_mod: expanded");
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);
517 terms.front() = int_prod->target();
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();
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()));
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());
544 absl::flat_hash_set<int> used_variables;
545 for (
const int ref : f_direct) {
547 if (!context->IntersectDomainWith(ref, Domain(0, n - 1))) {
548 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
552 for (
const int ref : f_inverse) {
554 if (!context->IntersectDomainWith(ref, Domain(0, n - 1))) {
555 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
562 if (used_variables.size() != 2 * n) {
563 for (
int i = 0;
i < n; ++
i) {
564 for (
int j = 0; j < n; ++j) {
569 if (
i == j)
continue;
570 if (!context->IntersectDomainWith(
580 std::vector<int64_t> possible_values;
583 const auto filter_inverse_domain =
584 [context, n, &possible_values](
const auto& direct,
const auto& inverse) {
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);
594 removed_value =
true;
598 if (!context->IntersectDomainWith(
600 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
610 if (!filter_inverse_domain(f_direct, f_inverse))
return;
611 if (!filter_inverse_domain(f_inverse, f_direct))
return;
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()) {
621 const int r_j = f_inverse[j];
623 if (context->HasVarValueEncoding(r_j,
i, &r_j_i)) {
624 if (!context->InsertVarValueEncoding(r_j_i, f_i, j)) {
628 const int f_i_j = context->GetOrCreateVarValueEncoding(f_i, j);
629 if (!context->InsertVarValueEncoding(f_i_j, r_j,
i)) {
637 context->UpdateRuleStats(
"inverse: expanded");
641 const int num_exprs = ct->lin_max().exprs().size();
642 if (num_exprs < 2)
return;
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();
656 lin->add_domain(std::numeric_limits<int64_t>::max());
659 context->CanonicalizeLinearConstraint(new_ct);
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));
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);
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());
687 context->CanonicalizeLinearConstraint(new_ct);
690 context->solution_crush().SetLinMaxExpandedVars(ct->lin_max(),
691 enforcement_literals);
692 context->UpdateRuleStats(
"lin_max: expanded lin_max");
697void ExpandElementWhenTargetShareVarWithIndex(ConstraintProto* ct,
699 const ElementConstraintProto& element = ct->element();
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);
708 for (
const int64_t v : context->DomainOf(index_var).Values()) {
711 const LinearExpressionProto& expr = element.exprs(index_value);
712 ConstraintProto* imply = context->working_model->add_constraints();
713 imply->add_enforcement_literal(
714 context->GetOrCreateVarValueEncoding(index_var, v));
715 imply->mutable_linear()->add_domain(target_value);
716 imply->mutable_linear()->add_domain(target_value);
718 context->CanonicalizeLinearConstraint(imply);
721 context->UpdateRuleStats(
722 "element: expanded when the index and the target share the same var");
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();
735 const Domain index_var_domain = context->DomainOf(index_var);
736 const Domain target_domain = context->DomainSuperSetOf(target);
742 absl::btree_map<int64_t, std::vector<int>> supports;
743 for (
const int64_t v : index_var_domain.Values()) {
745 const int64_t expr_value = context->FixedValue(element.exprs(index_value));
746 supports[expr_value].push_back(v);
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);
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);
768 context->AddImplication(index_literal, target_literal);
771 exactly_one->add_literals(index_literal);
775 context->UpdateRuleStats(
"element: expanded value element");
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();
788 BoolArgumentProto* exactly_one =
789 context->working_model->add_constraints()->mutable_exactly_one();
791 for (
const int64_t v : index_var_domain.Values()) {
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);
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);
804 imply->mutable_linear());
805 context->CanonicalizeLinearConstraint(imply);
809 imply->mutable_linear()->vars(),
810 imply->mutable_linear()->coeffs()))
811 << google::protobuf::ShortFormat(*imply);
814 context->UpdateRuleStats(
"element: expanded");
819 const ElementConstraintProto& element = ct->element();
821 const LinearExpressionProto& index = element.linear_index();
822 const LinearExpressionProto& target = element.linear_target();
823 const int size = element.exprs_size();
827 if (!context->IntersectDomainWith(index, Domain(0, size - 1))) {
828 VLOG(1) <<
"Empty domain for the index variable in ExpandElement()";
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);
838 ct->element().exprs(context->FixedValue(index)), -1,
839 eq->mutable_linear());
840 context->CanonicalizeLinearConstraint(eq);
841 context->UpdateRuleStats(
"element: expanded with fixed index");
847 if (index.vars_size() == 1 && target.vars_size() == 1 &&
848 index.vars(0) == target.vars(0)) {
849 ExpandElementWhenTargetShareVarWithIndex(ct, context);
854 bool all_constants =
true;
855 for (
const int64_t v : context->DomainOf(index.vars(0)).Values()) {
857 if (!context->IsFixed(element.exprs(index_value))) {
858 all_constants =
false;
864 ExpandConstantArrayElement(ct, context);
866 ExpandVariableElement(ct, context);
872void LinkLiteralsAndValues(absl::Span<const int> literals,
873 absl::Span<const int64_t> values,
874 const absl::flat_hash_map<int64_t, int>& encoding,
876 CHECK_EQ(literals.size(), values.size());
881 absl::btree_map<int, std::vector<int>> encoding_lit_to_support;
886 for (
int i = 0;
i < values.size(); ++
i) {
887 encoding_lit_to_support[encoding.at(values[
i])].push_back(literals[
i]);
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])) {
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);
912void AddImplyInReachableValues(
int literal,
913 std::vector<int64_t>& reachable_values,
914 const absl::flat_hash_map<int64_t, int> encoding,
917 if (reachable_values.size() == encoding.size())
return;
918 if (reachable_values.size() <= encoding.size() / 2) {
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));
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)) {
942 AutomatonConstraintProto& proto = *ct->mutable_automaton();
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");
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.");
960 std::vector<absl::flat_hash_set<int64_t>> reachable_states;
961 std::vector<absl::flat_hash_set<int64_t>> reachable_labels;
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;
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) {
981 std::vector<int64_t> in_states;
982 std::vector<int64_t> labels;
983 std::vector<int64_t> out_states;
984 absl::flat_hash_set<int64_t> still_reachable_after_domain_change;
985 for (
int i = 0;
i < proto.transition_label_size(); ++
i) {
986 const int64_t tail = proto.transition_tail(
i);
987 const int64_t label = proto.transition_label(
i);
988 const int64_t head = proto.transition_head(
i);
990 if (!reachable_states[time].contains(tail))
continue;
991 if (!reachable_states[time + 1].contains(head))
continue;
992 if (!context->DomainContains(proto.exprs(time), label))
continue;
994 still_reachable_after_domain_change.insert(head);
998 in_states.push_back(tail);
999 labels.push_back(label);
1003 out_states.push_back(time + 1 == n ? 0 : head);
1006 reachable_states[time + 1] = still_reachable_after_domain_change;
1009 const int num_tuples = in_states.size();
1010 if (num_tuples == 1) {
1011 if (!context->IntersectDomainWith(proto.exprs(time),
1012 Domain(labels.front()))) {
1013 VLOG(1) <<
"Infeasible automaton.";
1020 std::vector<int> at_false;
1021 for (
const auto [value, literal] : in_encoding) {
1022 if (value != in_states[0]) {
1023 if (!context->SetLiteralToFalse(literal))
return;
1027 in_encoding.clear();
1033 std::vector<int64_t> transitions = labels;
1034 const LinearExpressionProto& expr = proto.exprs(time);
1040 VLOG(1) <<
"Infeasible automaton.";
1046 if (!context->IsFixed(expr)) {
1047 const int var = expr.vars(0);
1048 for (
const int64_t v : context->DomainOf(var).Values()) {
1050 context->GetOrCreateVarValueEncoding(var, v);
1057 absl::flat_hash_map<int64_t, int> in_count;
1058 absl::flat_hash_map<int64_t, int> transition_count;
1059 absl::flat_hash_map<int64_t, int> out_count;
1060 for (
int i = 0;
i < num_tuples; ++
i) {
1061 in_count[in_states[
i]]++;
1062 transition_count[labels[
i]]++;
1063 out_count[out_states[
i]]++;
1070 std::vector<int64_t> states = out_states;
1073 out_encoding.clear();
1074 if (states.size() == 2) {
1075 const int var = context->NewBoolVar(
"automaton expansion");
1076 new_state_vars.push_back({var, time + 1, states[0]});
1077 out_encoding[states[0]] = var;
1079 }
else if (states.size() > 2) {
1080 struct UniqueDetector {
1081 void Set(int64_t v) {
1082 if (!is_unique)
return;
1084 if (v != value) is_unique =
false;
1090 bool is_set =
false;
1091 bool is_unique =
true;
1097 absl::flat_hash_map<int64_t, UniqueDetector> out_to_in;
1098 absl::flat_hash_map<int64_t, UniqueDetector> out_to_transition;
1099 for (
int i = 0;
i < num_tuples; ++
i) {
1100 out_to_in[out_states[
i]].Set(in_states[
i]);
1101 out_to_transition[out_states[
i]].Set(labels[
i]);
1104 for (
const int64_t state : states) {
1107 if (!in_encoding.empty() && out_to_in[state].is_unique) {
1108 const int64_t unique_in = out_to_in[state].value;
1109 if (in_count[unique_in] == out_count[state]) {
1110 out_encoding[state] = in_encoding[unique_in];
1117 if (!encoding.empty() && out_to_transition[state].is_unique) {
1118 const int64_t unique_transition = out_to_transition[state].value;
1119 if (transition_count[unique_transition] == out_count[state]) {
1120 out_encoding[state] = encoding[unique_transition];
1125 out_encoding[state] = context->NewBoolVar(
"automaton expansion");
1126 new_state_vars.push_back({out_encoding[state], time + 1, state});
1144 const int num_involved_variables =
1145 in_encoding.size() + encoding.size() + out_encoding.size();
1146 const bool use_light_encoding = (num_tuples > num_involved_variables);
1147 if (use_light_encoding && !in_encoding.empty() && !encoding.empty() &&
1148 !out_encoding.empty()) {
1152 absl::flat_hash_map<int64_t, std::vector<int64_t>> in_to_label;
1153 absl::flat_hash_map<int64_t, std::vector<int64_t>> in_to_out;
1154 for (
int i = 0;
i < num_tuples; ++
i) {
1155 in_to_label[in_states[
i]].push_back(labels[
i]);
1156 in_to_out[in_states[
i]].push_back(out_states[
i]);
1159 std::vector<std::pair<int64_t, int>> in_to_label_pairs(
1160 in_encoding.begin(), in_encoding.end());
1161 absl::c_sort(in_to_label_pairs);
1162 for (
const auto [in_value, in_literal] : in_to_label_pairs) {
1163 AddImplyInReachableValues(in_literal, in_to_label[in_value], encoding,
1165 AddImplyInReachableValues(in_literal, in_to_out[in_value], out_encoding,
1170 for (
int i = 0;
i < num_tuples; ++
i) {
1172 context->working_model->add_constraints()->mutable_bool_or();
1173 bool_or->add_literals(
NegatedRef(in_encoding.at(in_states[
i])));
1174 bool_or->add_literals(
NegatedRef(encoding.at(labels[
i])));
1175 bool_or->add_literals(out_encoding.at(out_states[
i]));
1178 in_encoding.swap(out_encoding);
1179 out_encoding.clear();
1187 std::vector<int> tuple_literals;
1188 if (num_tuples == 2) {
1189 const int bool_var = context->NewBoolVar(
"automaton expansion");
1190 new_transition_vars.push_back({bool_var, time, in_states[0], labels[0]});
1191 tuple_literals.push_back(bool_var);
1192 tuple_literals.push_back(
NegatedRef(bool_var));
1197 BoolArgumentProto* exactly_one =
1198 context->working_model->add_constraints()->mutable_exactly_one();
1199 for (
int i = 0;
i < num_tuples; ++
i) {
1201 if (in_count[in_states[
i]] == 1 && !in_encoding.empty()) {
1202 tuple_literal = in_encoding[in_states[
i]];
1203 }
else if (transition_count[labels[
i]] == 1 && !encoding.empty()) {
1204 tuple_literal = encoding[labels[
i]];
1205 }
else if (out_count[out_states[
i]] == 1 && !out_encoding.empty()) {
1206 tuple_literal = out_encoding[out_states[
i]];
1208 tuple_literal = context->NewBoolVar(
"automaton expansion");
1209 new_transition_vars.push_back(
1210 {tuple_literal, time, in_states[
i], labels[
i]});
1213 tuple_literals.push_back(tuple_literal);
1214 exactly_one->add_literals(tuple_literal);
1218 if (!in_encoding.empty()) {
1219 LinkLiteralsAndValues(tuple_literals, in_states, in_encoding, context);
1221 if (!encoding.empty()) {
1222 LinkLiteralsAndValues(tuple_literals, labels, encoding, context);
1224 if (!out_encoding.empty()) {
1225 LinkLiteralsAndValues(tuple_literals, out_states, out_encoding, context);
1228 in_encoding.swap(out_encoding);
1229 out_encoding.clear();
1232 context->solution_crush().SetAutomatonExpandedVars(proto, new_state_vars,
1233 new_transition_vars);
1234 if (removed_values) {
1235 context->UpdateRuleStats(
"automaton: reduced variable domains");
1237 context->UpdateRuleStats(
"automaton: expanded");
1241bool TableIsInCanonicalForm(ConstraintProto* ct) {
1242 TableConstraintProto& table = *ct->mutable_table();
1243 if (!table.vars().empty()) {
1244 LOG(ERROR) <<
"Table is in the legacy format.";
1247 if (table.values().empty()) {
1248 if (table.exprs().empty()) {
1251 if (table.exprs_size() != 1) {
1252 LOG(ERROR) <<
"Table is empty but has more than one expression.";
1255 if (table.exprs(0).offset() != 0) {
1256 LOG(ERROR) <<
"Table is empty but has an expression with a non-zero "
1260 if (!table.exprs(0).vars().empty()) {
1261 LOG(ERROR) <<
"Table is empty but has an expression with a non-constant "
1267 for (
const LinearExpressionProto& expr : table.exprs()) {
1268 if (expr.offset() != 0) {
1269 LOG(ERROR) <<
"Expression contains an non-zero offset.";
1272 if (expr.coeffs().size() == 1 && expr.coeffs(0) != 1) {
1273 LOG(ERROR) <<
"Expression contains a single variable with a coefficient "
1274 "different from 1.";
1277 if (expr.vars().empty()) {
1278 LOG(ERROR) <<
"Constant expression.";
1285void ExpandNegativeTable(ConstraintProto* ct,
PresolveContext* context) {
1286 DCHECK(TableIsInCanonicalForm(ct));
1287 TableConstraintProto& table = *ct->mutable_table();
1288 if (table.values().empty()) {
1289 context->UpdateRuleStats(
"table: empty negated constraint");
1294 const int num_exprs = table.exprs_size();
1295 DCHECK_GT(num_exprs, 0);
1296 const int num_original_tuples = table.values_size() / num_exprs;
1297 std::vector<std::vector<int64_t>> tuples(num_original_tuples);
1299 for (
int i = 0;
i < num_original_tuples; ++
i) {
1300 for (
int j = 0; j < num_exprs; ++j) {
1301 tuples[
i].push_back(table.values(count++));
1306 std::vector<int64_t> domain_sizes;
1307 for (
int i = 0;
i < num_exprs; ++
i) {
1308 domain_sizes.push_back(context->DomainOf(table.exprs(
i).vars(0)).Size());
1313 std::vector<int> clause;
1314 for (
const std::vector<int64_t>& tuple : tuples) {
1316 for (
int i = 0;
i < num_exprs; ++
i) {
1317 const int64_t value = tuple[
i];
1321 context->GetOrCreateVarValueEncoding(table.exprs(
i).vars(0), value);
1326 ConstraintProto* tuple_ct = context->working_model->add_constraints();
1327 *tuple_ct->mutable_enforcement_literal() = ct->enforcement_literal();
1328 BoolArgumentProto* bool_or = tuple_ct->mutable_bool_or();
1329 for (
const int lit : clause) {
1330 bool_or->add_literals(lit);
1333 context->UpdateRuleStats(
"table: expanded negated constraint");
1342void ProcessOneCompressedColumn(
1343 int variable, absl::Span<const int> tuple_literals,
1344 absl::Span<
const absl::InlinedVector<int64_t, 2>> values,
1345 std::optional<int> table_is_active_literal,
PresolveContext* context) {
1346 DCHECK_EQ(tuple_literals.size(), values.size());
1353 std::vector<std::pair<int64_t, int>> pairs;
1354 std::vector<int> any_values_literals;
1355 for (
int i = 0;
i < values.size(); ++
i) {
1356 if (values[
i].empty()) {
1357 any_values_literals.push_back(tuple_literals[
i]);
1361 ConstraintProto* ct = context->working_model->add_constraints();
1362 ct->add_enforcement_literal(tuple_literals[
i]);
1367 values[
i].size() == 1 ? ct->mutable_bool_and() : ct->mutable_bool_or();
1368 for (
const int64_t v : values[
i]) {
1369 DCHECK(context->DomainContains(variable, v));
1370 literals->add_literals(context->GetOrCreateVarValueEncoding(variable, v));
1371 pairs.emplace_back(v, tuple_literals[
i]);
1377 std::vector<int> selected;
1378 std::sort(pairs.begin(), pairs.end());
1379 for (
int i = 0;
i < pairs.size();) {
1381 const int64_t value = pairs[
i].first;
1382 for (;
i < pairs.size() && pairs[
i].first == value; ++
i) {
1383 selected.push_back(pairs[
i].second);
1388 BoolArgumentProto* no_support =
1389 context->working_model->add_constraints()->mutable_bool_or();
1390 for (
const int lit : selected) {
1391 no_support->add_literals(lit);
1393 for (
const int lit : any_values_literals) {
1394 no_support->add_literals(lit);
1396 if (table_is_active_literal.has_value()) {
1397 no_support->add_literals(
NegatedRef(table_is_active_literal.value()));
1401 const int value_literal =
1402 context->GetOrCreateVarValueEncoding(variable, value);
1403 no_support->add_literals(
NegatedRef(value_literal));
1408void AddSizeTwoTable(
1409 const std::vector<int>& vars,
1410 const std::vector<std::vector<int64_t>>& tuples,
1411 const std::vector<absl::flat_hash_set<int64_t>>& values_per_var,
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()) {
1423 absl::btree_map<int, std::vector<int>> left_to_right;
1424 absl::btree_map<int, std::vector<int>> right_to_left;
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));
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);
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());
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);
1459 if (support_literals.size() > max_support_size / 2) {
1460 num_large_clause_added++;
1465 for (
const auto& it : left_to_right) {
1466 add_support_constraint(it.first, it.second, values_per_var[1].size());
1468 for (
const auto& it : right_to_left) {
1469 add_support_constraint(it.first, it.second, values_per_var[0].size());
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
1481bool ReduceTableInPresenceOfUniqueVariableWithCosts(
1482 std::vector<int>* vars, std::vector<std::vector<int64_t>>* tuples,
1484 const int num_vars = vars->size();
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];
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] =
1502 context->RemoveVariableFromObjective(var);
1503 context->MarkVariableAsRemoved(var);
1504 deleted_vars.push_back(var);
1505 }
else if (context->VarToConstraints(var).size() == 1) {
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);
1514 new_vars.push_back(var);
1517 if (new_vars.size() == num_vars)
return false;
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) {
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;
1534 (*tuples)[
i][new_size++] = value;
1537 (*tuples)[
i].resize(new_size);
1538 (*tuples)[
i].push_back(cost);
1539 min_cost = std::min(min_cost, cost);
1543 (*tuples)[
i].insert((*tuples)[
i].end(), temp.begin(), temp.end());
1551 const int old_size = tuples->size();
1552 std::sort(tuples->begin(), tuples->end());
1553 for (
int i = 0;
i < tuples->size(); ++
i) {
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]) {
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]));
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]);
1582 (*tuples)[
i].resize(new_vars.size() + 1);
1583 (*tuples)[new_size++] = (*tuples)[
i];
1585 tuples->resize(new_size);
1586 if (new_size < old_size) {
1587 context->UpdateRuleStats(
1588 "table: removed duplicate tuples with different costs");
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;
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);
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);
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);
1636 context->UpdateRuleStats(absl::StrCat(
1637 "table: expansion with column(s) only in objective. Arity = ",
1646void CompressAndExpandPositiveTable(ConstraintProto* ct,
1647 bool last_column_is_cost,
1648 absl::Span<const int> vars,
1649 std::vector<std::vector<int64_t>>* tuples,
1651 const int num_tuples_before_compression = tuples->size();
1655 std::vector<int64_t> domain_sizes;
1656 for (
const int var : vars) {
1657 domain_sizes.push_back(context->DomainOf(var).Size());
1659 if (last_column_is_cost) {
1660 domain_sizes.push_back(std::numeric_limits<int64_t>::max());
1664 const int compression_level = context->params().table_compression_level();
1665 if (compression_level > 0) {
1668 const int num_tuples_after_first_compression = tuples->size();
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)) {
1685 if (compressed_table.size() < num_tuples_before_compression) {
1686 context->UpdateRuleStats(
"table: fully compress tuples");
1690 for (
int i = 0;
i < tuples->size(); ++
i) {
1691 compressed_table.push_back({});
1692 for (
const int64_t v : (*tuples)[
i]) {
1694 compressed_table.back().push_back({});
1696 compressed_table.back().push_back({v});
1700 if (compressed_table.size() < num_tuples_before_compression) {
1701 context->UpdateRuleStats(
"table: compress tuples");
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();
1713 std::sort(compressed_table.begin(), compressed_table.end());
1715 const int num_vars = vars.size();
1716 if (compressed_table.size() == 1 && ct->enforcement_literal().empty()) {
1718 context->UpdateRuleStats(
"table: one tuple");
1719 if (last_column_is_cost) {
1722 context->AddToObjectiveOffset(compressed_table[0].back()[0]);
1730 std::vector<bool> has_any(num_vars,
false);
1731 std::vector<absl::flat_hash_map<int64_t, int>> var_index_to_value_count(
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;
1739 for (
const int64_t v : compressed_table[
i][var_index]) {
1741 DCHECK(context->DomainContains(vars[var_index], v));
1742 var_index_to_value_count[var_index][v]++;
1749 BoolArgumentProto* exactly_one =
1750 context->working_model->add_constraints()->mutable_exactly_one();
1752 std::optional<int> table_is_active_literal = std::nullopt;
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());
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);
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);
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()) {
1788 const int64_t v = compressed_table[
i][var_index][0];
1789 if (var_index_to_value_count[var_index][v] != 1)
continue;
1791 ++num_reused_variables;
1792 create_new_var =
false;
1794 context->GetOrCreateVarValueEncoding(vars[var_index], v);
1795 existing_row_literals.push_back(tuple_literals[
i]);
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]});
1802 exactly_one->add_literals(tuple_literals[
i]);
1804 if (num_reused_variables > 0) {
1805 context->UpdateRuleStats(
"table: reused literals");
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]);
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;
1822 for (
int i = 0;
i < tuple_literals.size(); ++
i) {
1823 column.push_back(compressed_table[
i][var_index]);
1825 ProcessOneCompressedColumn(vars[var_index], tuple_literals, column,
1826 table_is_active_literal, context);
1829 context->solution_crush().SetTableExpandedVars(vars, existing_row_literals,
1831 context->UpdateRuleStats(
"table: expanded positive constraint");
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");
1850 const int num_exprs = table.exprs_size();
1851 const int num_original_tuples = table.values_size() / num_exprs;
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());
1859 for (
const LinearExpressionProto& expr : table.exprs()) {
1860 vars.push_back(expr.vars(0));
1863 std::vector<std::vector<int64_t>> tuples(num_original_tuples);
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++));
1873 std::vector<absl::flat_hash_set<int64_t>> values_per_var(num_exprs);
1875 for (
int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
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)) {
1885 for (
int var_index = 0; var_index < num_exprs; ++var_index) {
1886 values_per_var[var_index].insert(tuples[tuple_index][var_index]);
1888 std::swap(tuples[tuple_index], tuples[new_size]);
1892 tuples.resize(new_size);
1894 if (tuples.empty()) {
1895 if (ct->enforcement_literal().empty()) {
1896 context->UpdateRuleStats(
"table: empty");
1897 return (
void)context->NotifyThatModelIsUnsat();
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()) {
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(
1919 values_per_var[var_index].end()})));
1920 if (context->DomainOf(vars[var_index]).IsFixed()) {
1921 num_fixed_variables++;
1925 if (num_fixed_variables == num_exprs - 1) {
1926 context->UpdateRuleStats(
"table: one variable not fixed");
1929 }
else if (num_fixed_variables == num_exprs) {
1930 context->UpdateRuleStats(
"table: all variables fixed");
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");
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);
1957 CompressAndExpandPositiveTable(ct, last_column_is_cost, vars, &tuples,
1962bool AllDiffShouldBeExpanded(
const Domain& union_of_domains,
1964 const AllDifferentConstraintProto& proto = *ct->mutable_all_diff();
1965 const int num_exprs = proto.exprs_size();
1966 int num_fully_encoded = 0;
1967 for (
int i = 0;
i < num_exprs; ++
i) {
1968 if (context->IsFullyEncoded(proto.exprs(
i))) {
1969 num_fully_encoded++;
1973 if ((union_of_domains.Size() <= 2 * proto.exprs_size()) ||
1974 (union_of_domains.Size() <= 32)) {
1979 if (num_fully_encoded == num_exprs && union_of_domains.Size() < 256) {
1992void ExpandSomeLinearOfSizeTwo(ConstraintProto* ct,
PresolveContext* context) {
1993 const LinearConstraintProto& arg = ct->linear();
1994 if (arg.vars_size() != 2)
return;
1996 const int var1 = arg.vars(0);
1997 const int var2 = arg.vars(1);
1998 if (context->IsFixed(var1) || context->IsFixed(var2))
return;
2000 const int64_t coeff1 = arg.coeffs(0);
2001 const int64_t coeff2 = arg.coeffs(1);
2002 const Domain reachable_rhs_superset =
2003 context->DomainOf(var1)
2004 .MultiplicationBy(coeff1)
2005 .RelaxIfTooComplex()
2006 .AdditionWith(context->DomainOf(var2)
2007 .MultiplicationBy(coeff2)
2008 .RelaxIfTooComplex());
2009 const Domain infeasible_reachable_values =
2010 reachable_rhs_superset.IntersectionWith(
2014 if (infeasible_reachable_values.Size() != 1)
return;
2019 int64_t cte = infeasible_reachable_values.FixedValue();
2024 context->UpdateRuleStats(
"linear: expand always feasible ax + by != cte");
2028 const Domain reduced_domain =
2029 context->DomainOf(var1)
2030 .AdditionWith(Domain(-x0))
2031 .InverseMultiplicationBy(
b)
2032 .IntersectionWith(context->DomainOf(var2)
2033 .AdditionWith(Domain(-y0))
2034 .InverseMultiplicationBy(-a));
2036 if (reduced_domain.Size() > 16)
return;
2041 const int64_t size1 = context->DomainOf(var1).Size();
2042 const int64_t size2 = context->DomainOf(var2).Size();
2043 for (
const int64_t z : reduced_domain.Values()) {
2044 const int64_t value1 = x0 +
b * z;
2045 const int64_t value2 = y0 - a * z;
2046 DCHECK(context->DomainContains(var1, value1)) <<
"value1 = " << value1;
2047 DCHECK(context->DomainContains(var2, value2)) <<
"value2 = " << value2;
2048 DCHECK_EQ(coeff1 * value1 + coeff2 * value2,
2049 infeasible_reachable_values.FixedValue());
2051 if (!context->HasVarValueEncoding(var1, value1,
nullptr) || size1 == 2) {
2054 if (!context->HasVarValueEncoding(var2, value2,
nullptr) || size2 == 2) {
2061 for (
const int64_t z : reduced_domain.Values()) {
2062 const int64_t value1 = x0 +
b * z;
2063 const int64_t value2 = y0 - a * z;
2065 const int lit1 = context->GetOrCreateVarValueEncoding(var1, value1);
2066 const int lit2 = context->GetOrCreateVarValueEncoding(var2, value2);
2068 context->working_model->add_constraints()->mutable_bool_or();
2071 for (
const int lit : ct->enforcement_literal()) {
2076 context->UpdateRuleStats(
"linear: expand small ax + by != cte");
2088void ExpandComplexLinearConstraint(
int c, ConstraintProto* ct,
2094 if (ct->linear().domain().size() <= 2)
return;
2095 if (ct->linear().vars().size() == 1)
return;
2097 const SatParameters& params = context->params();
2098 if (params.encode_complex_linear_constraint_with_integer()) {
2104 const int slack = context->NewIntVar(rhs);
2105 context->solution_crush().SetVarToLinearExpression(
2106 slack, ct->linear().vars(), ct->linear().coeffs());
2107 ct->mutable_linear()->add_vars(slack);
2108 ct->mutable_linear()->add_coeffs(-1);
2109 ct->mutable_linear()->clear_domain();
2110 ct->mutable_linear()->add_domain(0);
2111 ct->mutable_linear()->add_domain(0);
2115 BoolArgumentProto* clause =
nullptr;
2116 if (ct->enforcement_literal().empty() && ct->linear().domain_size() == 4) {
2119 single_bool = context->NewBoolVar(
"complex linear expansion");
2121 clause = context->working_model->add_constraints()->mutable_bool_or();
2122 for (
const int ref : ct->enforcement_literal()) {
2128 const std::vector<int> enforcement_literals(
2129 ct->enforcement_literal().begin(), ct->enforcement_literal().end());
2130 ct->mutable_enforcement_literal()->Clear();
2131 std::vector<int> domain_literals;
2132 for (
int i = 0;
i < ct->linear().domain_size();
i += 2) {
2133 const int64_t lb = ct->linear().domain(
i);
2134 const int64_t ub = ct->linear().domain(
i + 1);
2136 int subdomain_literal;
2137 if (clause !=
nullptr) {
2138 subdomain_literal = context->NewBoolVar(
"complex linear expansion");
2139 clause->add_literals(subdomain_literal);
2140 domain_literals.push_back(subdomain_literal);
2142 if (
i == 0) domain_literals.push_back(single_bool);
2143 subdomain_literal =
i == 0 ? single_bool :
NegatedRef(single_bool);
2148 ConstraintProto* new_ct = context->working_model->add_constraints();
2150 new_ct->add_enforcement_literal(subdomain_literal);
2153 context->solution_crush().SetLinearWithComplexDomainExpandedVars(
2154 ct->linear(), domain_literals);
2157 if (context->params().enumerate_all_solutions() &&
2158 !enforcement_literals.empty()) {
2159 int linear_is_enforced;
2160 if (enforcement_literals.size() == 1) {
2161 linear_is_enforced = enforcement_literals[0];
2163 linear_is_enforced = context->NewBoolVar(
"complex linear expansion");
2164 BoolArgumentProto* maintain_linear_is_enforced =
2165 context->working_model->add_constraints()->mutable_bool_or();
2166 for (
const int e_lit : enforcement_literals) {
2169 maintain_linear_is_enforced->add_literals(
NegatedRef(e_lit));
2171 maintain_linear_is_enforced->add_literals(linear_is_enforced);
2172 context->solution_crush().SetVarToConjunction(linear_is_enforced,
2173 enforcement_literals);
2176 for (
const int lit : domain_literals) {
2177 context->AddImplication(
NegatedRef(linear_is_enforced),
2184 context->UpdateRuleStats(
"linear: expanded complex rhs");
2185 context->InitializeNewDomains();
2186 context->UpdateNewConstraintsVariableUsage();
2187 context->UpdateConstraintVariableUsage(c);
2191 const LinearConstraintProto& lin) {
2192 if (lin.vars_size() != 1)
return false;
2196 if (rhs.IsFixed())
return true;
2199 const Domain not_implied =
2200 rhs.InverseMultiplicationBy(lin.coeffs(0))
2202 .IntersectionWith(context->DomainOf(lin.vars(0)));
2203 if (not_implied.IsEmpty())
return false;
2204 return not_implied.IsFixed();
2220void ScanModelAndDecideAllDiffExpansion(
2222 absl::flat_hash_set<int>& domain_of_var_is_used,
2223 absl::flat_hash_set<int>& bounds_of_var_are_used,
2224 absl::flat_hash_set<int>& processed_variables,
bool& expand,
bool& keep) {
2225 CHECK_EQ(all_diff_ct->constraint_case(), ConstraintProto::kAllDiff);
2227 bool at_least_one_var_domain_is_used =
false;
2228 bool at_least_one_var_bound_is_used =
false;
2231 for (
const LinearExpressionProto& expr : all_diff_ct->all_diff().exprs()) {
2233 if (expr.vars().empty())
continue;
2234 DCHECK_EQ(1, expr.vars_size());
2235 const int var = expr.vars(0);
2237 if (context->IsFixed(var))
continue;
2239 bool at_least_one_var_domain_is_used =
false;
2240 bool at_least_one_var_bound_is_used =
false;
2243 if (!processed_variables.insert(var).second) {
2244 at_least_one_var_domain_is_used = bounds_of_var_are_used.contains(var);
2245 at_least_one_var_bound_is_used = domain_of_var_is_used.contains(var);
2247 bool domain_is_used =
false;
2248 bool bounds_are_used =
false;
2251 for (
const int ct_index : context->VarToConstraints(var)) {
2253 if (ct_index < 0)
continue;
2255 const ConstraintProto& other_ct =
2256 context->working_model->constraints(ct_index);
2257 switch (other_ct.constraint_case()) {
2258 case ConstraintProto::ConstraintCase::kBoolOr:
2260 case ConstraintProto::ConstraintCase::kBoolAnd:
2262 case ConstraintProto::ConstraintCase::kAtMostOne:
2264 case ConstraintProto::ConstraintCase::kExactlyOne:
2266 case ConstraintProto::ConstraintCase::kBoolXor:
2268 case ConstraintProto::ConstraintCase::kIntDiv:
2270 case ConstraintProto::ConstraintCase::kIntMod:
2272 case ConstraintProto::ConstraintCase::kLinMax:
2273 bounds_are_used =
true;
2275 case ConstraintProto::ConstraintCase::kIntProd:
2277 case ConstraintProto::ConstraintCase::kLinear:
2278 if (IsVarEqOrNeqValue(context, other_ct.linear()) &&
2279 var == other_ct.linear().vars(0)) {
2281 domain_is_used =
true;
2282 }
else if (other_ct.linear().vars_size() > 2 &&
2283 other_ct.linear().domain_size() == 2 &&
2284 other_ct.linear().domain(0) ==
2285 other_ct.linear().domain(1)) {
2288 bounds_are_used =
true;
2291 case ConstraintProto::ConstraintCase::kAllDiff:
2295 case ConstraintProto::ConstraintCase::kDummyConstraint:
2297 case ConstraintProto::ConstraintCase::kElement:
2299 if (other_ct.element().index() == var) {
2300 domain_is_used =
true;
2303 case ConstraintProto::ConstraintCase::kCircuit:
2305 case ConstraintProto::ConstraintCase::kRoutes:
2307 case ConstraintProto::ConstraintCase::kInverse:
2308 domain_is_used =
true;
2310 case ConstraintProto::ConstraintCase::kReservoir:
2312 case ConstraintProto::ConstraintCase::kTable:
2313 domain_is_used =
true;
2315 case ConstraintProto::ConstraintCase::kAutomaton:
2316 domain_is_used =
true;
2318 case ConstraintProto::ConstraintCase::kInterval:
2319 bounds_are_used =
true;
2321 case ConstraintProto::ConstraintCase::kNoOverlap:
2324 case ConstraintProto::ConstraintCase::kNoOverlap2D:
2327 case ConstraintProto::ConstraintCase::kCumulative:
2330 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
2335 if (domain_is_used && bounds_are_used)
break;
2339 if (domain_is_used) domain_of_var_is_used.insert(var);
2340 if (bounds_are_used) bounds_of_var_are_used.insert(var);
2343 at_least_one_var_domain_is_used |= domain_is_used;
2344 at_least_one_var_bound_is_used |= bounds_are_used;
2347 if (at_least_one_var_domain_is_used && at_least_one_var_bound_is_used) {
2352 expand = at_least_one_var_domain_is_used;
2353 keep = at_least_one_var_bound_is_used;
2357 absl::flat_hash_set<int>& domain_of_var_is_used,
2358 absl::flat_hash_set<int>& bounds_of_var_are_used,
2359 absl::flat_hash_set<int>& processed_variable) {
2360 const bool expand_all_diff_from_parameters =
2361 context->params().expand_alldiff_constraints();
2362 AllDifferentConstraintProto& proto = *ct->mutable_all_diff();
2363 if (proto.exprs_size() <= 1)
return;
2364 if (context->ModelIsUnsat())
return;
2366 bool keep_after_expansion =
false;
2367 bool expand_all_diff_from_usage =
false;
2368 ScanModelAndDecideAllDiffExpansion(
2369 ct, context, domain_of_var_is_used, bounds_of_var_are_used,
2370 processed_variable, expand_all_diff_from_usage, keep_after_expansion);
2372 const int num_exprs = proto.exprs_size();
2373 Domain union_of_domains = context->DomainSuperSetOf(proto.exprs(0));
2374 for (
int i = 1;
i < num_exprs; ++
i) {
2376 union_of_domains.UnionWith(context->DomainSuperSetOf(proto.exprs(
i)));
2379 const bool expand_all_diff_from_size =
2380 AllDiffShouldBeExpanded(union_of_domains, ct, context);
2387 const bool should_expand =
2388 expand_all_diff_from_parameters ||
2389 (expand_all_diff_from_size &&
2390 (expand_all_diff_from_usage || !keep_after_expansion));
2391 if (!should_expand)
return;
2393 const bool is_a_permutation = num_exprs == union_of_domains.Size();
2398 for (
const int64_t v : union_of_domains.Values()) {
2400 std::vector<LinearExpressionProto> possible_exprs;
2401 int fixed_expression_count = 0;
2402 for (
const LinearExpressionProto& expr : proto.exprs()) {
2403 if (!context->DomainContains(expr, v))
continue;
2404 possible_exprs.push_back(expr);
2405 if (context->IsFixed(expr)) {
2406 fixed_expression_count++;
2410 if (fixed_expression_count > 1) {
2412 return (
void)context->NotifyThatModelIsUnsat();
2413 }
else if (fixed_expression_count == 1) {
2415 for (
const LinearExpressionProto& expr : possible_exprs) {
2416 if (context->IsFixed(expr))
continue;
2417 if (!context->IntersectDomainWith(expr, Domain(v).Complement())) {
2418 VLOG(1) <<
"Empty domain for a variable in MaybeExpandAllDiff()";
2424 BoolArgumentProto* at_most_or_equal_one =
2426 ? context->working_model->add_constraints()->mutable_exactly_one()
2427 : context->working_model->add_constraints()->mutable_at_most_one();
2428 for (
const LinearExpressionProto& expr : possible_exprs) {
2431 if (!context->DomainContains(expr, v))
continue;
2436 const int encoding = context->GetOrCreateAffineValueEncoding(expr, v);
2437 at_most_or_equal_one->add_literals(encoding);
2441 context->UpdateRuleStats(
2442 absl::StrCat(
"all_diff:", is_a_permutation ?
" permutation" :
"",
2443 " expanded", keep_after_expansion ?
" and kept" :
""));
2444 if (!keep_after_expansion) ct->Clear();
2450 if (context->
params().disable_constraint_expansion())
return;
2464 bool has_all_diffs =
false;
2467 for (
int c = 0; c < context->
working_model->constraints_size(); ++c) {
2468 ConstraintProto*
const ct = context->
working_model->mutable_constraints(c);
2470 switch (ct->constraint_case()) {
2471 case ConstraintProto::kLinear:
2474 if (ct->linear().domain().size() > 2 &&
2475 !context->
params().cp_model_presolve()) {
2476 ExpandComplexLinearConstraint(c, ct, context);
2479 case ConstraintProto::kReservoir:
2480 if (context->
params().expand_reservoir_constraints()) {
2481 ExpandReservoir(ct, context);
2484 case ConstraintProto::kCumulative:
2485 if (context->
params().encode_cumulative_as_reservoir()) {
2486 EncodeCumulativeAsReservoir(ct, context);
2489 case ConstraintProto::kIntMod:
2490 ExpandIntMod(ct, context);
2492 case ConstraintProto::kIntProd:
2493 ExpandIntProd(ct, context);
2495 case ConstraintProto::kElement:
2496 ExpandElement(ct, context);
2498 case ConstraintProto::kInverse:
2499 ExpandInverse(ct, context);
2501 case ConstraintProto::kAutomaton:
2502 ExpandAutomaton(ct, context);
2504 case ConstraintProto::kTable:
2505 if (!context->
params().cp_model_presolve()) {
2508 if (ct->table().negated()) {
2509 ExpandNegativeTable(ct, context);
2511 ExpandPositiveTable(ct, context);
2514 case ConstraintProto::kLinMax:
2515 if (ct->lin_max().exprs().size() <=
2516 context->
params().max_lin_max_size_for_expansion()) {
2517 ExpandLinMax(ct, context);
2520 case ConstraintProto::kAllDiff:
2521 has_all_diffs =
true;
2532 if (ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
2548 absl::flat_hash_set<int> domain_of_var_is_used;
2549 absl::flat_hash_set<int> bounds_of_var_are_used;
2550 absl::flat_hash_set<int> processed_variables;
2552 ConstraintProto*
const ct = context->
working_model->mutable_constraints(
i);
2554 switch (ct->constraint_case()) {
2555 case ConstraintProto::kAllDiff:
2556 MaybeExpandAllDiff(ct, context, domain_of_var_is_used,
2557 bounds_of_var_are_used, processed_variables);
2559 case ConstraintProto::kLinear:
2560 ExpandSomeLinearOfSizeTwo(ct, context);
2571 if (ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
2601 if (context->
params().disable_constraint_expansion())
return;
2603 for (
int c = 0; c < context->
working_model->constraints_size(); ++c) {
2604 ConstraintProto*
const ct = context->
working_model->mutable_constraints(c);
2605 switch (ct->constraint_case()) {
2606 case ConstraintProto::kLinear:
2607 if (ct->linear().domain().size() > 2) {
2608 ExpandComplexLinearConstraint(c, ct, context);
static Domain FromValues(std::vector< int64_t > values)
Domain Complement() const
Domain DomainOf(int ref) const
const SatParameters & params() const
CpModelProto * working_model
void ClearPrecedenceCache()
Clear the precedence cache.
void NotifyThatModelIsExpanded()
bool ModelIsExpanded() const
void InitializeNewDomains()
Creates the internal structure for any new variables in working_model.
void UpdateConstraintVariableUsage(int c)
SolverLogger * logger() const
void UpdateNewConstraintsVariableUsage()
Calls UpdateConstraintVariableUsage() on all newly created constraints.
bool ModelIsUnsat() const
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
constexpr int64_t kTableAnyValue
void CompressTuples(absl::Span< const int64_t > domain_sizes, std::vector< std::vector< int64_t > > *tuples)
bool RefIsPositive(int ref)
void ExpandCpModel(PresolveContext *context)
bool SolveDiophantineEquationOfSizeTwo(int64_t &a, int64_t &b, int64_t &cte, int64_t &x0, int64_t &y0)
std::vector< std::vector< absl::InlinedVector< int64_t, 2 > > > FullyCompressTuples(absl::Span< const int64_t > domain_sizes, std::vector< std::vector< int64_t > > *tuples)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset)
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.
std::string ProtobufShortDebugString(const P &message)
#define SOLVER_LOG(logger,...)