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"
55void ExpandReservoirUsingCircuit(int64_t sum_of_positive_demand,
56 int64_t sum_of_negative_demand,
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);
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);
147 lin->add_domain(std::numeric_limits<int64_t>::max());
150 context->CanonicalizeLinearConstraint(new_ct);
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,
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();
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;
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");
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();
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;
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();
302 for (
int i = 0;
i < num_events; ++
i) {
303 const int active = reservoir.active_literals().empty()
305 : reservoir.active_literals(
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);
331 context->working_model->add_constraints();
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,
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");
380 if (!context->IsFixed(ct->cumulative().capacity())) {
381 context->UpdateRuleStats(
382 "cumulative -> reservoir: expansion is not supported with variable "
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();
404 *reservoir->add_level_changes() = demand;
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);
431 if (context->IsFixed(mod_expr))
return;
437 if (!context->IntersectDomainWith(
438 target_expr, context->DomainSuperSetOf(expr).PositiveModuloBySuperset(
439 context->DomainSuperSetOf(mod_expr)))) {
444 auto new_enforced_constraint = [&]() {
451 const int div_var = context->NewIntVar(
452 context->DomainSuperSetOf(expr).PositiveDivisionBySuperset(
453 context->DomainSuperSetOf(mod_expr)));
456 div_expr.add_coeffs(1);
459 new_enforced_constraint()->mutable_int_div();
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);
473 prod_expr.add_coeffs(1);
476 new_enforced_constraint()->mutable_int_prod();
478 *int_prod->add_exprs() = div_expr;
479 *int_prod->add_exprs() = mod_expr;
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) {
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);
511 context->working_model->add_constraints()->mutable_int_prod();
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();
521 context->working_model->add_constraints()->mutable_int_prod();
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;
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) {
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");
702 DCHECK_EQ(index.vars_size(), 1);
703 const int index_var = index.vars(0);
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()) {
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");
730 DCHECK_EQ(index.vars_size(), 1);
731 const int index_var = index.vars(0);
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);
760 context->working_model->add_constraints()->mutable_bool_or();
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");
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);
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();
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");
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)) {
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])) {
900 context->working_model->add_constraints()->mutable_bool_or();
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) {
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());
933 for (
const auto [value, literal] : encoding) {
934 if (!set.contains(value)) {
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) {
978 if (context->time_limit()->LimitReached())
return;
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);
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;
995 still_reachable_after_domain_change.insert(head);
999 in_states.push_back(tail);
1000 labels.push_back(label);
1004 out_states.push_back(time + 1 == n ? 0 : head);
1007 reachable_states[time + 1] = still_reachable_after_domain_change;
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.";
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;
1028 in_encoding.clear();
1034 std::vector<int64_t> transitions = labels;
1041 VLOG(1) <<
"Infeasible automaton.";
1047 if (!context->IsFixed(expr)) {
1048 const int var = expr.vars(0);
1049 for (
const int64_t v : context->DomainOf(var).Values()) {
1051 context->GetOrCreateVarValueEncoding(var, v);
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]]++;
1071 std::vector<int64_t> states = out_states;
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;
1080 }
else if (states.size() > 2) {
1081 struct UniqueDetector {
1082 void Set(int64_t v) {
1083 if (!is_unique)
return;
1085 if (v != value) is_unique =
false;
1091 bool is_set =
false;
1092 bool is_unique =
true;
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]);
1105 for (
const int64_t state : states) {
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];
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];
1126 out_encoding[state] = context->NewBoolVar(
"automaton expansion");
1127 new_state_vars.push_back({out_encoding[state], time + 1, state});
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()) {
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]);
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,
1166 AddImplyInReachableValues(in_literal, in_to_out[in_value], out_encoding,
1171 for (
int i = 0;
i < num_tuples; ++
i) {
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]));
1179 in_encoding.swap(out_encoding);
1180 out_encoding.clear();
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));
1199 context->working_model->add_constraints()->mutable_exactly_one();
1200 for (
int i = 0;
i < num_tuples; ++
i) {
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]];
1209 tuple_literal = context->NewBoolVar(
"automaton expansion");
1210 new_transition_vars.push_back(
1211 {tuple_literal, time, in_states[
i], labels[
i]});
1214 tuple_literals.push_back(tuple_literal);
1215 exactly_one->add_literals(tuple_literal);
1219 if (!in_encoding.empty()) {
1220 LinkLiteralsAndValues(tuple_literals, in_states, in_encoding, context);
1222 if (!encoding.empty()) {
1223 LinkLiteralsAndValues(tuple_literals, labels, encoding, context);
1225 if (!out_encoding.empty()) {
1226 LinkLiteralsAndValues(tuple_literals, out_states, out_encoding, context);
1229 in_encoding.swap(out_encoding);
1230 out_encoding.clear();
1233 context->solution_crush().SetAutomatonExpandedVars(proto, new_state_vars,
1234 new_transition_vars);
1235 if (removed_values) {
1236 context->UpdateRuleStats(
"automaton: reduced variable domains");
1238 context->UpdateRuleStats(
"automaton: expanded");
1244 if (!table.vars().empty()) {
1245 LOG(ERROR) <<
"Table is in the legacy format.";
1248 if (table.values().empty()) {
1249 if (table.exprs().empty()) {
1252 if (table.exprs_size() != 1) {
1253 LOG(ERROR) <<
"Table is empty but has more than one expression.";
1256 if (table.exprs(0).offset() != 0) {
1257 LOG(ERROR) <<
"Table is empty but has an expression with a non-zero "
1261 if (!table.exprs(0).vars().empty()) {
1262 LOG(ERROR) <<
"Table is empty but has an expression with a non-constant "
1269 if (expr.offset() != 0) {
1270 LOG(ERROR) <<
"Expression contains an non-zero offset.";
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.";
1278 if (expr.vars().empty()) {
1279 LOG(ERROR) <<
"Constant expression.";
1287 DCHECK(TableIsInCanonicalForm(ct));
1289 if (table.values().empty()) {
1290 context->UpdateRuleStats(
"table: empty negated constraint");
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);
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++));
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());
1314 std::vector<int> clause;
1315 for (
const std::vector<int64_t>& tuple : tuples) {
1317 for (
int i = 0;
i < num_exprs; ++
i) {
1318 const int64_t value = tuple[
i];
1322 context->GetOrCreateVarValueEncoding(table.exprs(
i).vars(0), value);
1327 ConstraintProto* tuple_ct = context->working_model->add_constraints();
1330 for (
const int lit : clause) {
1331 bool_or->add_literals(lit);
1334 context->UpdateRuleStats(
"table: expanded negated constraint");
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());
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]);
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]);
1378 std::vector<int> selected;
1379 std::sort(pairs.begin(), pairs.end());
1380 for (
int i = 0;
i < pairs.size();) {
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);
1390 context->working_model->add_constraints()->mutable_bool_or();
1391 for (
const int lit : selected) {
1392 no_support->add_literals(lit);
1394 for (
const int lit : any_values_literals) {
1395 no_support->add_literals(lit);
1397 if (table_is_active_literal.has_value()) {
1398 no_support->add_literals(
NegatedRef(table_is_active_literal.value()));
1402 const int value_literal =
1403 context->GetOrCreateVarValueEncoding(variable, value);
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,
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());
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) {
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]));
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 = ",
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]++;
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());
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");
1842 DCHECK(TableIsInCanonicalForm(ct));
1844 if (table.exprs().empty()) {
1845 CHECK(table.values().empty());
1846 context->UpdateRuleStats(
"table: empty trivial");
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());
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");
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 if (union_of_domains.Size() > context->params().max_alldiff_domain_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++;
1977 if ((union_of_domains.Size() <= 2 * proto.exprs_size()) ||
1978 (union_of_domains.Size() <= 32)) {
1983 if (num_fully_encoded == num_exprs) {
1998 if (arg.vars_size() != 2)
return;
2000 const int var1 = arg.
vars(0);
2001 const int var2 = arg.vars(1);
2002 if (context->IsFixed(var1) || context->IsFixed(var2))
return;
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(
2018 if (infeasible_reachable_values.Size() != 1)
return;
2023 int64_t cte = infeasible_reachable_values.FixedValue();
2028 context->UpdateRuleStats(
"linear: expand always feasible ax + by != cte");
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));
2040 if (reduced_domain.Size() > 16)
return;
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());
2055 if (!context->HasVarValueEncoding(var1, value1,
nullptr) || size1 == 2) {
2058 if (!context->HasVarValueEncoding(var2, value2,
nullptr) || size2 == 2) {
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;
2069 const int lit1 = context->GetOrCreateVarValueEncoding(var1, value1);
2070 const int lit2 = context->GetOrCreateVarValueEncoding(var2, value2);
2072 context->working_model->add_constraints()->mutable_bool_or();
2075 for (
const int lit : ct->enforcement_literal()) {
2080 context->UpdateRuleStats(
"linear: expand small ax + by != cte");
2098 if (ct->linear().domain().size() <= 2)
return;
2099 if (ct->linear().vars().size() == 1)
return;
2102 if (params.encode_complex_linear_constraint_with_integer()) {
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);
2120 if (ct->enforcement_literal().empty() && ct->linear().domain_size() == 4) {
2123 single_bool = context->NewBoolVar(
"complex linear expansion");
2125 clause = context->working_model->add_constraints()->mutable_bool_or();
2126 for (
const int ref : ct->enforcement_literal()) {
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);
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);
2146 if (
i == 0) domain_literals.push_back(single_bool);
2147 subdomain_literal =
i == 0 ? single_bool :
NegatedRef(single_bool);
2157 context->solution_crush().SetLinearWithComplexDomainExpandedVars(
2158 ct->linear(), domain_literals);
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];
2167 linear_is_enforced = context->NewBoolVar(
"complex linear expansion");
2169 context->working_model->add_constraints()->mutable_bool_or();
2170 for (
const int e_lit : enforcement_literals) {
2173 maintain_linear_is_enforced->add_literals(
NegatedRef(e_lit));
2175 maintain_linear_is_enforced->
add_literals(linear_is_enforced);
2176 context->solution_crush().SetVarToConjunction(linear_is_enforced,
2177 enforcement_literals);
2180 for (
const int lit : domain_literals) {
2181 context->AddImplication(
NegatedRef(linear_is_enforced),
2188 context->UpdateRuleStats(
"linear: expanded complex rhs");
2189 context->InitializeNewDomains();
2190 context->UpdateNewConstraintsVariableUsage();
2191 context->UpdateConstraintVariableUsage(c);
2196 if (lin.vars_size() != 1)
return false;
2200 if (rhs.IsFixed())
return true;
2203 const Domain not_implied =
2204 rhs.InverseMultiplicationBy(lin.coeffs(0))
2206 .IntersectionWith(context->DomainOf(lin.vars(0)));
2207 if (not_implied.IsEmpty())
return false;
2208 return not_implied.IsFixed();
2224void ScanModelAndDecideAllDiffExpansion(
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) {
2231 bool at_least_one_var_domain_is_used =
false;
2232 bool at_least_one_var_bound_is_used =
false;
2237 if (expr.vars().empty())
continue;
2238 DCHECK_EQ(1, expr.vars_size());
2239 const int var = expr.vars(0);
2241 if (context->IsFixed(var))
continue;
2243 bool at_least_one_var_domain_is_used =
false;
2244 bool at_least_one_var_bound_is_used =
false;
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);
2251 bool domain_is_used =
false;
2252 bool bounds_are_used =
false;
2255 for (
const int ct_index : context->VarToConstraints(var)) {
2257 if (ct_index < 0)
continue;
2260 context->working_model->constraints(ct_index);
2261 switch (other_ct.constraint_case()) {
2277 bounds_are_used =
true;
2282 if (IsVarEqOrNeqValue(context, other_ct.linear()) &&
2283 var == other_ct.linear().vars(0)) {
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)) {
2292 bounds_are_used =
true;
2303 if (other_ct.element().index() == var) {
2304 domain_is_used =
true;
2312 domain_is_used =
true;
2317 domain_is_used =
true;
2320 domain_is_used =
true;
2323 bounds_are_used =
true;
2339 if (domain_is_used && bounds_are_used)
break;
2343 if (domain_is_used) domain_of_var_is_used.insert(var);
2344 if (bounds_are_used) bounds_of_var_are_used.insert(var);
2347 at_least_one_var_domain_is_used |= domain_is_used;
2348 at_least_one_var_bound_is_used |= bounds_are_used;
2351 if (at_least_one_var_domain_is_used && at_least_one_var_bound_is_used) {
2356 expand = at_least_one_var_domain_is_used;
2357 keep = at_least_one_var_bound_is_used;
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();
2367 if (proto.exprs_size() <= 1)
return;
2368 if (context->ModelIsUnsat())
return;
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);
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) {
2380 union_of_domains.UnionWith(context->DomainSuperSetOf(proto.exprs(
i)));
2383 const bool expand_all_diff_from_size =
2384 AllDiffShouldBeExpanded(union_of_domains, ct, context);
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;
2397 const bool is_a_permutation = num_exprs == union_of_domains.Size();
2402 for (
const int64_t v : union_of_domains.Values()) {
2404 std::vector<LinearExpressionProto> possible_exprs;
2405 int fixed_expression_count = 0;
2407 if (!context->DomainContains(expr, v))
continue;
2408 possible_exprs.push_back(expr);
2409 if (context->IsFixed(expr)) {
2410 fixed_expression_count++;
2414 if (fixed_expression_count > 1) {
2416 return (
void)context->NotifyThatModelIsUnsat();
2417 }
else if (fixed_expression_count == 1) {
2420 if (context->IsFixed(expr))
continue;
2421 if (!context->IntersectDomainWith(expr, Domain(v).Complement())) {
2422 VLOG(1) <<
"Empty domain for a variable in MaybeExpandAllDiff()";
2430 ? context->working_model->add_constraints()->mutable_exactly_one()
2431 : context->working_model->add_constraints()->mutable_at_most_one();
2435 if (!context->DomainContains(expr, v))
continue;
2440 const int encoding = context->GetOrCreateAffineValueEncoding(expr, v);
2441 at_most_or_equal_one->add_literals(encoding);
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();
2468 bool has_all_diffs =
false;
2480 ExpandComplexLinearConstraint(c, ct, context);
2485 ExpandReservoir(ct, context);
2490 EncodeCumulativeAsReservoir(ct, context);
2494 ExpandIntMod(ct, context);
2497 ExpandIntProd(ct, context);
2500 ExpandElement(ct, context);
2503 ExpandInverse(ct, context);
2506 ExpandAutomaton(ct, context);
2513 ExpandNegativeTable(ct, context);
2515 ExpandPositiveTable(ct, context);
2521 ExpandLinMax(ct, context);
2525 has_all_diffs =
true;
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;
2560 MaybeExpandAllDiff(ct, context, domain_of_var_is_used,
2561 bounds_of_var_are_used, processed_variables);
2564 ExpandSomeLinearOfSizeTwo(ct, context);
2612 ExpandComplexLinearConstraint(c, ct, context);
static Domain FromValues(std::vector< int64_t > values)
Domain Complement() const
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 1;
void add_literals(::int32_t value)
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
const ::operations_research::sat::TableConstraintProto & table() const
ConstraintCase constraint_case() const
const ::operations_research::sat::LinearConstraintProto & linear() const
::operations_research::sat::ReservoirConstraintProto *PROTOBUF_NONNULL mutable_reservoir()
const ::operations_research::sat::LinearArgumentProto & lin_max() const
void add_enforcement_literal(::int32_t value)
::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()
::int32_t vars(int index) const
void add_vars(::int32_t value)
void add_domain(::int64_t value)
::int64_t domain(int index) const
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
void set_offset(::int64_t value)
void add_vars(::int32_t value)
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
int time_exprs_size() const
repeated .operations_research.sat.LinearExpressionProto time_exprs = 3;
void set_min_level(::int64_t value)
bool expand_reservoir_constraints() const
bool encode_cumulative_as_reservoir() const
::int32_t max_lin_max_size_for_expansion() const
bool disable_constraint_expansion() const
bool cp_model_presolve() const
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 4;
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)
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)
#define SOLVER_LOG(logger,...)