18 #include "absl/container/flat_hash_map.h"
23 #include "ortools/sat/cp_model.pb.h"
34 void ExpandReservoir(ConstraintProto*
ct, PresolveContext*
context) {
35 if (
ct->reservoir().min_level() >
ct->reservoir().max_level()) {
36 VLOG(1) <<
"Empty level domain in reservoir constraint.";
37 return (
void)
context->NotifyThatModelIsUnsat();
40 const ReservoirConstraintProto& reservoir =
ct->reservoir();
41 const int num_events = reservoir.times_size();
43 const int true_literal =
context->GetOrCreateConstantVar(1);
45 const auto is_active_literal = [&reservoir, true_literal](
int index) {
46 if (reservoir.actives_size() == 0)
return true_literal;
47 return reservoir.actives(
index);
50 int num_positives = 0;
51 int num_negatives = 0;
60 if (num_positives > 0 && num_negatives > 0) {
62 for (
int i = 0; i < num_events - 1; ++i) {
63 const int active_i = is_active_literal(i);
64 if (
context->LiteralIsFalse(active_i))
continue;
65 const int time_i = reservoir.times(i);
67 for (
int j = i + 1; j < num_events; ++j) {
68 const int active_j = is_active_literal(j);
69 if (
context->LiteralIsFalse(active_j))
continue;
70 const int time_j = reservoir.times(j);
72 const int i_lesseq_j =
context->GetOrCreateReifiedPrecedenceLiteral(
73 time_i, time_j, active_i, active_j);
74 context->working_model->mutable_variables(i_lesseq_j)
75 ->set_name(absl::StrCat(i,
" before ", j));
76 const int j_lesseq_i =
context->GetOrCreateReifiedPrecedenceLiteral(
77 time_j, time_i, active_j, active_i);
78 context->working_model->mutable_variables(j_lesseq_i)
79 ->set_name(absl::StrCat(j,
" before ", i));
87 for (
int i = 0; i < num_events; ++i) {
88 const int active_i = is_active_literal(i);
89 if (
context->LiteralIsFalse(active_i))
continue;
90 const int time_i = reservoir.times(i);
93 ConstraintProto*
const level =
context->working_model->add_constraints();
94 level->add_enforcement_literal(active_i);
97 for (
int j = 0; j < num_events; ++j) {
99 const int active_j = is_active_literal(j);
100 if (
context->LiteralIsFalse(active_j))
continue;
102 const int time_j = reservoir.times(j);
103 level->mutable_linear()->add_vars(
104 context->GetOrCreateReifiedPrecedenceLiteral(time_j, time_i,
105 active_j, active_i));
106 level->mutable_linear()->add_coeffs(reservoir.demands(j));
110 const int64 demand_i = reservoir.demands(i);
111 level->mutable_linear()->add_domain(
112 CapSub(reservoir.min_level(), demand_i));
113 level->mutable_linear()->add_domain(
114 CapSub(reservoir.max_level(), demand_i));
120 context->working_model->add_constraints()->mutable_linear();
121 for (
int i = 0; i < num_events; ++i) {
122 sum->add_vars(is_active_literal(i));
123 sum->add_coeffs(reservoir.demands(i));
125 sum->add_domain(reservoir.min_level());
126 sum->add_domain(reservoir.max_level());
130 context->UpdateRuleStats(
"reservoir: expanded");
135 void ExpandIntDiv(ConstraintProto*
ct, PresolveContext*
context) {
136 const int divisor =
ct->int_div().vars(1);
137 if (!
context->IntersectDomainWith(divisor, Domain(0).Complement())) {
138 return (
void)
context->NotifyThatModelIsUnsat();
142 void ExpandIntMod(ConstraintProto*
ct, PresolveContext*
context) {
143 const IntegerArgumentProto& int_mod =
ct->int_mod();
144 const int var = int_mod.vars(0);
145 const int mod_var = int_mod.vars(1);
146 const int target_var = int_mod.target();
157 context->NewIntVar(Domain(var_lb / mod_ub, var_ub / mod_lb));
159 auto add_enforcement_literal_if_needed = [&]() {
160 if (
ct->enforcement_literal_size() == 0)
return;
161 const int literal =
ct->enforcement_literal(0);
162 ConstraintProto*
const last =
context->working_model->mutable_constraints(
163 context->working_model->constraints_size() - 1);
164 last->add_enforcement_literal(
literal);
168 IntegerArgumentProto*
const div_proto =
169 context->working_model->add_constraints()->mutable_int_div();
170 div_proto->set_target(div_var);
171 div_proto->add_vars(
var);
172 div_proto->add_vars(mod_var);
173 add_enforcement_literal_if_needed();
176 if (mod_lb == mod_ub) {
178 LinearConstraintProto*
const lin =
179 context->working_model->add_constraints()->mutable_linear();
180 lin->add_vars(int_mod.vars(0));
182 lin->add_vars(div_var);
183 lin->add_coeffs(-mod_lb);
184 lin->add_vars(target_var);
188 add_enforcement_literal_if_needed();
191 const int prod_var =
context->NewIntVar(
192 Domain(var_lb * mod_lb / mod_ub, var_ub * mod_ub / mod_lb));
193 IntegerArgumentProto*
const int_prod =
194 context->working_model->add_constraints()->mutable_int_prod();
195 int_prod->set_target(prod_var);
196 int_prod->add_vars(div_var);
197 int_prod->add_vars(mod_var);
198 add_enforcement_literal_if_needed();
201 LinearConstraintProto*
const lin =
202 context->working_model->add_constraints()->mutable_linear();
205 lin->add_vars(prod_var);
207 lin->add_vars(target_var);
211 add_enforcement_literal_if_needed();
215 context->UpdateRuleStats(
"int_mod: expanded");
218 void ExpandIntProdWithBoolean(
int bool_ref,
int int_ref,
int product_ref,
220 ConstraintProto*
const one =
context->working_model->add_constraints();
221 one->add_enforcement_literal(bool_ref);
222 one->mutable_linear()->add_vars(int_ref);
223 one->mutable_linear()->add_coeffs(1);
224 one->mutable_linear()->add_vars(product_ref);
225 one->mutable_linear()->add_coeffs(-1);
226 one->mutable_linear()->add_domain(0);
227 one->mutable_linear()->add_domain(0);
229 ConstraintProto*
const zero =
context->working_model->add_constraints();
230 zero->add_enforcement_literal(
NegatedRef(bool_ref));
231 zero->mutable_linear()->add_vars(product_ref);
232 zero->mutable_linear()->add_coeffs(1);
233 zero->mutable_linear()->add_domain(0);
234 zero->mutable_linear()->add_domain(0);
237 void AddXEqualYOrXEqualZero(
int x_eq_y,
int x,
int y,
239 ConstraintProto* equality =
context->working_model->add_constraints();
240 equality->add_enforcement_literal(x_eq_y);
241 equality->mutable_linear()->add_vars(x);
242 equality->mutable_linear()->add_coeffs(1);
243 equality->mutable_linear()->add_vars(y);
244 equality->mutable_linear()->add_coeffs(-1);
245 equality->mutable_linear()->add_domain(0);
246 equality->mutable_linear()->add_domain(0);
251 void ExpandIntProdWithOneAcrossZero(
int a_ref,
int b_ref,
int product_ref,
258 const int a_is_positive =
context->NewBoolVar();
261 const int pos_a_ref =
context->NewIntVar({0,
context->MaxOf(a_ref)});
262 AddXEqualYOrXEqualZero(a_is_positive, pos_a_ref, a_ref,
context);
264 const int neg_a_ref =
context->NewIntVar({
context->MinOf(a_ref), 0});
268 const bool b_is_positive =
context->MinOf(b_ref) >= 0;
269 const Domain pos_a_product_domain =
270 b_is_positive ? Domain({0,
context->MaxOf(product_ref)})
271 : Domain({
context->MinOf(product_ref), 0});
272 const int pos_a_product =
context->NewIntVar(pos_a_product_domain);
273 IntegerArgumentProto* pos_product =
274 context->working_model->add_constraints()->mutable_int_prod();
275 pos_product->set_target(pos_a_product);
276 pos_product->add_vars(pos_a_ref);
277 pos_product->add_vars(b_ref);
280 const Domain neg_a_product_domain =
281 b_is_positive ? Domain({
context->MinOf(product_ref), 0})
282 : Domain({0,
context->MaxOf(product_ref)});
283 const int neg_a_product =
context->NewIntVar(neg_a_product_domain);
284 IntegerArgumentProto* neg_product =
285 context->working_model->add_constraints()->mutable_int_prod();
286 neg_product->set_target(neg_a_product);
287 neg_product->add_vars(neg_a_ref);
288 neg_product->add_vars(b_ref);
291 LinearConstraintProto* lin =
292 context->working_model->add_constraints()->mutable_linear();
293 lin->add_vars(product_ref);
295 lin->add_vars(pos_a_product);
297 lin->add_vars(neg_a_product);
303 void ExpandIntProdWithTwoAcrossZero(
int a_ref,
int b_ref,
int product_ref,
306 const int a_is_positive =
context->NewBoolVar();
312 const int pos_a_ref =
context->NewIntVar({0, max_of_a});
313 AddXEqualYOrXEqualZero(a_is_positive, pos_a_ref, a_ref,
context);
315 const int neg_a_ref =
context->NewIntVar({min_of_a, 0});
319 const int pos_product_ref =
321 ExpandIntProdWithOneAcrossZero(b_ref, pos_a_ref, pos_product_ref,
context);
322 const int neg_product_ref =
324 ExpandIntProdWithOneAcrossZero(b_ref, neg_a_ref, neg_product_ref,
context);
327 LinearConstraintProto* lin =
328 context->working_model->add_constraints()->mutable_linear();
329 lin->add_vars(product_ref);
331 lin->add_vars(pos_product_ref);
333 lin->add_vars(neg_product_ref);
339 void ExpandIntProd(ConstraintProto*
ct, PresolveContext*
context) {
340 const IntegerArgumentProto& int_prod =
ct->int_prod();
341 if (int_prod.vars_size() != 2)
return;
342 const int a = int_prod.vars(0);
343 const int b = int_prod.vars(1);
344 const int p = int_prod.target();
345 const bool a_is_boolean =
347 const bool b_is_boolean =
352 if (a_is_boolean && !b_is_boolean) {
353 ExpandIntProdWithBoolean(
a,
b, p,
context);
355 context->UpdateRuleStats(
"int_prod: expanded product with Boolean var");
358 if (b_is_boolean && !a_is_boolean) {
359 ExpandIntProdWithBoolean(
b,
a, p,
context);
361 context->UpdateRuleStats(
"int_prod: expanded product with Boolean var");
365 const bool a_span_across_zero =
367 const bool b_span_across_zero =
369 if (a_span_across_zero && !b_span_across_zero) {
370 ExpandIntProdWithOneAcrossZero(
a,
b, p,
context);
373 "int_prod: expanded product with general integer variables");
376 if (!a_span_across_zero && b_span_across_zero) {
377 ExpandIntProdWithOneAcrossZero(
b,
a, p,
context);
380 "int_prod: expanded product with general integer variables");
383 if (a_span_across_zero && b_span_across_zero) {
384 ExpandIntProdWithTwoAcrossZero(
a,
b, p,
context);
387 "int_prod: expanded product with general integer variables");
392 void ExpandInverse(ConstraintProto*
ct, PresolveContext*
context) {
393 const int size =
ct->inverse().f_direct().size();
394 CHECK_EQ(size,
ct->inverse().f_inverse().size());
400 for (
const int ref :
ct->inverse().f_direct()) {
401 if (!
context->IntersectDomainWith(ref, Domain(0, size - 1))) {
402 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
406 for (
const int ref :
ct->inverse().f_inverse()) {
407 if (!
context->IntersectDomainWith(ref, Domain(0, size - 1))) {
408 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
415 std::vector<int64> possible_values;
419 const auto filter_inverse_domain = [
context, size, &possible_values](
421 const auto& inverse) {
423 for (
int i = 0; i < size; ++i) {
424 possible_values.clear();
425 const Domain domain =
context->DomainOf(direct[i]);
426 bool removed_value =
false;
427 for (
const ClosedInterval&
interval : domain) {
429 if (
context->DomainOf(inverse[j]).Contains(i)) {
430 possible_values.push_back(j);
432 removed_value =
true;
437 if (!
context->IntersectDomainWith(
439 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
447 if (!filter_inverse_domain(
ct->inverse().f_direct(),
448 ct->inverse().f_inverse())) {
452 if (!filter_inverse_domain(
ct->inverse().f_inverse(),
453 ct->inverse().f_direct())) {
459 for (
int i = 0; i < size; ++i) {
460 const int f_i =
ct->inverse().f_direct(i);
461 const Domain domain =
context->DomainOf(f_i);
462 for (
const ClosedInterval&
interval : domain) {
465 const int r_j =
ct->inverse().f_inverse(j);
467 if (
context->HasVarValueEncoding(r_j, i, &r_j_i)) {
468 context->InsertVarValueEncoding(r_j_i, f_i, j);
470 const int f_i_j =
context->GetOrCreateVarValueEncoding(f_i, j);
471 context->InsertVarValueEncoding(f_i_j, r_j, i);
478 context->UpdateRuleStats(
"inverse: expanded");
481 void ExpandElement(ConstraintProto*
ct, PresolveContext*
context) {
482 const ElementConstraintProto& element =
ct->element();
483 const int index_ref = element.index();
484 const int target_ref = element.target();
485 const int size = element.vars_size();
487 if (!
context->IntersectDomainWith(index_ref, Domain(0, size - 1))) {
488 VLOG(1) <<
"Empty domain for the index variable in ExpandElement()";
489 return (
void)
context->NotifyThatModelIsUnsat();
492 bool all_constants =
true;
493 absl::flat_hash_map<int64, int> constant_var_values_usage;
494 std::vector<int64> constant_var_values;
495 std::vector<int64> invalid_indices;
496 Domain index_domain =
context->DomainOf(index_ref);
497 Domain target_domain =
context->DomainOf(target_ref);
498 for (
const ClosedInterval&
interval : index_domain) {
500 const int var = element.vars(v);
501 const Domain var_domain =
context->DomainOf(
var);
502 if (var_domain.IntersectionWith(target_domain).IsEmpty()) {
503 invalid_indices.push_back(v);
506 if (var_domain.Min() != var_domain.Max()) {
507 all_constants =
false;
512 if (constant_var_values_usage[
value]++ == 0) {
513 constant_var_values.push_back(
value);
518 if (!invalid_indices.empty() && target_ref != index_ref) {
519 if (!
context->IntersectDomainWith(
521 VLOG(1) <<
"No compatible variable domains in ExpandElement()";
522 return (
void)
context->NotifyThatModelIsUnsat();
526 index_domain =
context->DomainOf(index_ref);
534 absl::flat_hash_map<int64, BoolArgumentProto*> supports;
535 if (all_constants && target_ref != index_ref) {
536 if (!
context->IntersectDomainWith(
538 VLOG(1) <<
"Empty domain for the target variable in ExpandElement()";
542 target_domain =
context->DomainOf(target_ref);
543 if (target_domain.Size() == 1) {
544 context->UpdateRuleStats(
"element: one value array");
549 for (
const ClosedInterval&
interval : target_domain) {
553 const int lit =
context->GetOrCreateVarValueEncoding(target_ref, v);
554 BoolArgumentProto*
const support =
555 context->working_model->add_constraints()->mutable_bool_or();
556 supports[v] = support;
565 auto* bool_or =
context->working_model->add_constraints()->mutable_bool_or();
567 for (
const ClosedInterval&
interval : index_domain) {
569 const int var = element.vars(v);
570 const int index_lit =
context->GetOrCreateVarValueEncoding(index_ref, v);
571 const Domain var_domain =
context->DomainOf(
var);
573 bool_or->add_literals(index_lit);
575 if (target_ref == index_ref) {
578 context->AddImplyInDomain(index_lit,
var, Domain(v));
579 }
else if (target_domain.Size() == 1) {
582 context->AddImplyInDomain(index_lit,
var, target_domain);
583 }
else if (var_domain.Size() == 1) {
586 if (constant_var_values_usage[
value] > 1) {
589 const int target_lit =
590 context->GetOrCreateVarValueEncoding(target_ref,
value);
591 context->AddImplication(index_lit, target_lit);
595 context->InsertVarValueEncoding(index_lit, target_ref,
value);
598 context->AddImplyInDomain(index_lit, target_ref, var_domain);
601 ConstraintProto*
const ct =
context->working_model->add_constraints();
602 ct->add_enforcement_literal(index_lit);
603 ct->mutable_linear()->add_vars(
var);
604 ct->mutable_linear()->add_coeffs(1);
605 ct->mutable_linear()->add_vars(target_ref);
606 ct->mutable_linear()->add_coeffs(-1);
607 ct->mutable_linear()->add_domain(0);
608 ct->mutable_linear()->add_domain(0);
614 const int64 var_min = target_domain.Min();
619 for (
const auto it : constant_var_values_usage) {
620 if (it.second > usage ||
621 (it.second == usage && it.first < most_frequent_value)) {
623 most_frequent_value = it.first;
635 usage > 2 && usage > size / 10 ? most_frequent_value : var_min;
636 if (base != var_min) {
637 VLOG(3) <<
"expand element: choose " << base <<
" with usage " << usage
638 <<
" over " << var_min <<
" among " << size <<
" values.";
641 LinearConstraintProto*
const linear =
642 context->working_model->add_constraints()->mutable_linear();
644 linear->add_vars(target_ref);
645 linear->add_coeffs(-1);
646 for (
const ClosedInterval&
interval : index_domain) {
648 const int ref = element.vars(v);
649 const int index_lit =
650 context->GetOrCreateVarValueEncoding(index_ref, v);
653 linear->add_vars(index_lit);
654 linear->add_coeffs(
delta);
657 linear->add_coeffs(-
delta);
662 linear->add_domain(rhs);
663 linear->add_domain(rhs);
665 context->UpdateRuleStats(
"element: expanded value element");
667 context->UpdateRuleStats(
"element: expanded");
674 void LinkLiteralsAndValues(
675 const std::vector<int>& value_literals,
const std::vector<int64>& values,
676 const absl::flat_hash_map<int64, int>& target_encoding,
678 CHECK_EQ(value_literals.size(), values.size());
682 std::map<int, std::vector<int>> value_literals_per_target_literal;
687 for (
int i = 0; i < values.size(); ++i) {
688 const int64 v = values[i];
689 CHECK(target_encoding.contains(v));
691 value_literals_per_target_literal[lit].push_back(value_literals[i]);
696 for (
const auto& it : value_literals_per_target_literal) {
697 const int target_literal = it.first;
698 switch (it.second.size()) {
700 if (!
context->SetLiteralToFalse(target_literal)) {
706 context->StoreBooleanEqualityRelation(target_literal,
711 BoolArgumentProto*
const bool_or =
712 context->working_model->add_constraints()->mutable_bool_or();
713 bool_or->add_literals(
NegatedRef(target_literal));
714 for (
const int value_literal : it.second) {
715 bool_or->add_literals(value_literal);
716 context->AddImplication(value_literal, target_literal);
723 void ExpandAutomaton(ConstraintProto*
ct, PresolveContext*
context) {
724 AutomatonConstraintProto&
proto = *
ct->mutable_automaton();
726 if (
proto.vars_size() == 0) {
727 const int64 initial_state =
proto.starting_state();
728 for (
const int64 final_state :
proto.final_states()) {
729 if (initial_state == final_state) {
730 context->UpdateRuleStats(
"automaton: empty constraint");
736 return (
void)
context->NotifyThatModelIsUnsat();
737 }
else if (
proto.transition_label_size() == 0) {
739 return (
void)
context->NotifyThatModelIsUnsat();
742 const int n =
proto.vars_size();
743 const std::vector<int> vars = {
proto.vars().begin(),
proto.vars().end()};
746 const absl::flat_hash_set<int64> final_states(
747 {
proto.final_states().begin(),
proto.final_states().end()});
748 std::vector<absl::flat_hash_set<int64>> reachable_states(n + 1);
749 reachable_states[0].insert(
proto.starting_state());
753 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
755 const int64 label =
proto.transition_label(t);
757 if (!reachable_states[
time].contains(
tail))
continue;
758 if (!
context->DomainContains(vars[
time], label))
continue;
759 if (
time == n - 1 && !final_states.contains(
head))
continue;
760 reachable_states[
time + 1].insert(
head);
766 absl::flat_hash_set<int64> new_set;
767 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
769 const int64 label =
proto.transition_label(t);
772 if (!reachable_states[
time].contains(
tail))
continue;
773 if (!
context->DomainContains(vars[
time], label))
continue;
774 if (!reachable_states[
time + 1].contains(
head))
continue;
775 new_set.insert(
tail);
777 reachable_states[
time].swap(new_set);
785 absl::flat_hash_map<int64, int> encoding;
786 absl::flat_hash_map<int64, int> in_encoding;
787 absl::flat_hash_map<int64, int> out_encoding;
788 bool removed_values =
false;
794 std::vector<int64> in_states;
795 std::vector<int64> transition_values;
796 std::vector<int64> out_states;
797 for (
int i = 0; i <
proto.transition_label_size(); ++i) {
799 const int64 label =
proto.transition_label(i);
802 if (!reachable_states[
time].contains(
tail))
continue;
803 if (!reachable_states[
time + 1].contains(
head))
continue;
804 if (!
context->DomainContains(vars[
time], label))
continue;
809 in_states.push_back(
tail);
810 transition_values.push_back(label);
814 out_states.push_back(
time + 1 == n ? 0 :
head);
817 std::vector<int> tuple_literals;
818 if (transition_values.size() == 1) {
819 bool tmp_removed_values =
false;
820 tuple_literals.push_back(
context->GetOrCreateConstantVar(1));
823 Domain(transition_values.front()),
824 &tmp_removed_values)) {
825 return (
void)
context->NotifyThatModelIsUnsat();
829 }
else if (transition_values.size() == 2) {
830 const int bool_var =
context->NewBoolVar();
831 tuple_literals.push_back(bool_var);
832 tuple_literals.push_back(
NegatedRef(bool_var));
837 LinearConstraintProto*
const exactly_one =
838 context->working_model->add_constraints()->mutable_linear();
839 exactly_one->add_domain(1);
840 exactly_one->add_domain(1);
841 for (
int i = 0; i < transition_values.size(); ++i) {
842 const int tuple_literal =
context->NewBoolVar();
843 tuple_literals.push_back(tuple_literal);
844 exactly_one->add_vars(tuple_literal);
845 exactly_one->add_coeffs(1);
851 std::vector<int64> s = transition_values;
857 return (
void)
context->NotifyThatModelIsUnsat();
863 encoding[v] =
context->GetOrCreateVarValueEncoding(vars[
time], v);
870 std::vector<int64> s = out_states;
873 out_encoding.clear();
876 out_encoding[s.front()] =
var;
878 }
else if (s.size() > 2) {
879 for (
const int64 state : s) {
880 out_encoding[state] =
context->NewBoolVar();
885 if (!in_encoding.empty()) {
886 LinkLiteralsAndValues(tuple_literals, in_states, in_encoding,
context);
888 if (!encoding.empty()) {
889 LinkLiteralsAndValues(tuple_literals, transition_values, encoding,
892 if (!out_encoding.empty()) {
893 LinkLiteralsAndValues(tuple_literals, out_states, out_encoding,
context);
895 in_encoding.swap(out_encoding);
896 out_encoding.clear();
899 if (removed_values) {
900 context->UpdateRuleStats(
"automaton: reduced variable domains");
902 context->UpdateRuleStats(
"automaton: expanded");
906 void ExpandNegativeTable(ConstraintProto*
ct, PresolveContext*
context) {
907 TableConstraintProto& table = *
ct->mutable_table();
908 const int num_vars = table.vars_size();
909 const int num_original_tuples = table.values_size() / num_vars;
910 std::vector<std::vector<int64>> tuples(num_original_tuples);
912 for (
int i = 0; i < num_original_tuples; ++i) {
913 for (
int j = 0; j < num_vars; ++j) {
914 tuples[i].push_back(table.values(count++));
918 if (tuples.empty()) {
919 context->UpdateRuleStats(
"table: empty negated constraint");
926 std::vector<int64> domain_sizes;
927 for (
int i = 0; i < num_vars; ++i) {
928 domain_sizes.push_back(
context->DomainOf(table.vars(i)).Size());
933 std::vector<int> clause;
934 for (
const std::vector<int64>& tuple : tuples) {
936 for (
int i = 0; i < num_vars; ++i) {
938 if (
value == any_value)
continue;
941 context->GetOrCreateVarValueEncoding(table.vars(i),
value);
944 if (!clause.empty()) {
945 BoolArgumentProto* bool_or =
946 context->working_model->add_constraints()->mutable_bool_or();
947 for (
const int lit : clause) {
948 bool_or->add_literals(lit);
952 context->UpdateRuleStats(
"table: expanded negated constraint");
956 void ExpandLinMin(ConstraintProto*
ct, PresolveContext*
context) {
957 ConstraintProto*
const lin_max =
context->working_model->add_constraints();
958 for (
int i = 0; i <
ct->enforcement_literal_size(); ++i) {
959 lin_max->add_enforcement_literal(
ct->enforcement_literal(i));
964 lin_max->mutable_lin_max()->mutable_target());
966 for (
int i = 0; i <
ct->lin_min().exprs_size(); ++i) {
967 LinearExpressionProto*
const expr = lin_max->mutable_lin_max()->add_exprs();
978 void ProcessOneVariable(
const std::vector<int>& tuple_literals,
979 const std::vector<int64>& values,
int variable,
980 const std::vector<int>& tuples_with_any,
982 VLOG(2) <<
"Process var(" << variable <<
") with domain "
983 <<
context->DomainOf(variable) <<
" and " << values.size()
984 <<
" active tuples, and " << tuples_with_any.size() <<
" any tuples";
985 CHECK_EQ(tuple_literals.size(), values.size());
986 std::vector<std::pair<int64, int>> pairs;
989 for (
int i = 0; i < values.size(); ++i) {
992 pairs.emplace_back(
value, tuple_literals[i]);
997 std::vector<int> selected;
998 std::sort(pairs.begin(), pairs.end());
999 for (
int i = 0; i < pairs.size();) {
1002 for (; i < pairs.size() && pairs[i].first ==
value; ++i) {
1003 selected.push_back(pairs[i].second);
1006 CHECK(!selected.empty() || !tuples_with_any.empty());
1007 if (selected.size() == 1 && tuples_with_any.empty()) {
1008 context->InsertVarValueEncoding(selected.front(), variable,
value);
1010 const int value_literal =
1012 BoolArgumentProto* no_support =
1013 context->working_model->add_constraints()->mutable_bool_or();
1014 for (
const int lit : selected) {
1015 no_support->add_literals(lit);
1016 context->AddImplication(lit, value_literal);
1018 for (
const int lit : tuples_with_any) {
1019 no_support->add_literals(lit);
1023 no_support->add_literals(
NegatedRef(value_literal));
1029 void AddSizeTwoTable(
1030 const std::vector<int>& vars,
const std::vector<std::vector<int64>>& tuples,
1031 const std::vector<absl::flat_hash_set<int64>>& values_per_var,
1034 const int left_var = vars[0];
1035 const int right_var = vars[1];
1036 if (
context->DomainOf(left_var).Size() == 1 ||
1037 context->DomainOf(right_var).Size() == 1) {
1043 std::map<int, std::vector<int>> left_to_right;
1044 std::map<int, std::vector<int>> right_to_left;
1046 for (
const auto& tuple : tuples) {
1047 const int64 left_value(tuple[0]);
1048 const int64 right_value(tuple[1]);
1050 CHECK(
context->DomainContains(right_var, right_value));
1052 const int left_literal =
1053 context->GetOrCreateVarValueEncoding(left_var, left_value);
1054 const int right_literal =
1055 context->GetOrCreateVarValueEncoding(right_var, right_value);
1056 left_to_right[left_literal].push_back(right_literal);
1057 right_to_left[right_literal].push_back(left_literal);
1060 int num_implications = 0;
1061 int num_clause_added = 0;
1062 int num_large_clause_added = 0;
1063 auto add_support_constraint =
1064 [
context, &num_clause_added, &num_large_clause_added, &num_implications](
1065 int lit,
const std::vector<int>& support_literals,
1066 int max_support_size) {
1067 if (support_literals.size() == max_support_size)
return;
1068 if (support_literals.size() == 1) {
1069 context->AddImplication(lit, support_literals.front());
1072 BoolArgumentProto* bool_or =
1073 context->working_model->add_constraints()->mutable_bool_or();
1074 for (
const int support_literal : support_literals) {
1075 bool_or->add_literals(support_literal);
1079 if (support_literals.size() > max_support_size / 2) {
1080 num_large_clause_added++;
1085 for (
const auto& it : left_to_right) {
1086 add_support_constraint(it.first, it.second, values_per_var[1].size());
1088 for (
const auto& it : right_to_left) {
1089 add_support_constraint(it.first, it.second, values_per_var[0].size());
1091 VLOG(2) <<
"Table: 2 variables, " << tuples.size() <<
" tuples encoded using "
1092 << num_clause_added <<
" clauses, including "
1093 << num_large_clause_added <<
" large clauses, " << num_implications
1097 void ExpandPositiveTable(ConstraintProto*
ct, PresolveContext*
context) {
1098 const TableConstraintProto& table =
ct->table();
1099 const std::vector<int> vars(table.vars().begin(), table.vars().end());
1100 const int num_vars = table.vars_size();
1101 const int num_original_tuples = table.values_size() / num_vars;
1104 std::vector<std::vector<int64>> tuples(num_original_tuples);
1106 for (
int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
1107 for (
int var_index = 0; var_index < num_vars; ++var_index) {
1108 tuples[tuple_index].push_back(table.values(count++));
1114 std::vector<absl::flat_hash_set<int64>> values_per_var(num_vars);
1116 for (
int tuple_index = 0; tuple_index < num_original_tuples; ++tuple_index) {
1118 for (
int var_index = 0; var_index < num_vars; ++var_index) {
1119 const int64 value = tuples[tuple_index][var_index];
1120 if (!
context->DomainContains(vars[var_index],
value)) {
1126 for (
int var_index = 0; var_index < num_vars; ++var_index) {
1127 values_per_var[var_index].insert(tuples[tuple_index][var_index]);
1129 std::swap(tuples[tuple_index], tuples[new_size]);
1133 tuples.resize(new_size);
1134 const int num_valid_tuples = tuples.size();
1136 if (tuples.empty()) {
1137 context->UpdateRuleStats(
"table: empty");
1138 return (
void)
context->NotifyThatModelIsUnsat();
1144 int num_fixed_variables = 0;
1145 for (
int var_index = 0; var_index < num_vars; ++var_index) {
1149 values_per_var[var_index].end()})));
1150 if (
context->DomainOf(vars[var_index]).Size() == 1) {
1151 num_fixed_variables++;
1155 if (num_fixed_variables == num_vars - 1) {
1156 context->UpdateRuleStats(
"table: one variable not fixed");
1159 }
else if (num_fixed_variables == num_vars) {
1160 context->UpdateRuleStats(
"table: all variables fixed");
1166 if (num_vars == 2) {
1167 AddSizeTwoTable(vars, tuples, values_per_var,
context);
1169 "table: expanded positive constraint with two variables");
1176 int num_prefix_tuples = 0;
1178 absl::flat_hash_set<absl::Span<const int64>> prefixes;
1179 for (
const std::vector<int64>& tuple : tuples) {
1180 prefixes.insert(absl::MakeSpan(tuple.data(), num_vars - 1));
1182 num_prefix_tuples = prefixes.size();
1189 std::vector<int64> domain_sizes;
1190 for (
int i = 0; i < num_vars; ++i) {
1191 domain_sizes.push_back(values_per_var[i].size());
1194 const int num_compressed_tuples = tuples.size();
1196 if (num_compressed_tuples == 1) {
1198 context->UpdateRuleStats(
"table: one tuple");
1204 const bool prefixes_are_all_different = num_prefix_tuples == num_valid_tuples;
1205 if (prefixes_are_all_different) {
1207 "TODO table: last value implied by previous values");
1217 int64 max_num_prefix_tuples = 1;
1218 for (
int var_index = 0; var_index + 1 < num_vars; ++var_index) {
1219 max_num_prefix_tuples =
1220 CapProd(max_num_prefix_tuples, values_per_var[var_index].size());
1224 absl::StrCat(
"Table: ", num_vars,
1225 " variables, original tuples = ", num_original_tuples);
1226 if (num_valid_tuples != num_original_tuples) {
1227 absl::StrAppend(&
message,
", valid tuples = ", num_valid_tuples);
1229 if (prefixes_are_all_different) {
1230 if (num_prefix_tuples < max_num_prefix_tuples) {
1231 absl::StrAppend(&
message,
", partial prefix = ", num_prefix_tuples,
"/",
1232 max_num_prefix_tuples);
1234 absl::StrAppend(&
message,
", full prefix = true");
1237 absl::StrAppend(&
message,
", num prefix tuples = ", num_prefix_tuples);
1239 if (num_compressed_tuples != num_valid_tuples) {
1241 ", compressed tuples = ", num_compressed_tuples);
1247 if (num_compressed_tuples == 2) {
1248 context->UpdateRuleStats(
"TODO table: two tuples");
1260 std::vector<int> tuple_literals(num_compressed_tuples);
1261 BoolArgumentProto* at_least_one_tuple =
1262 context->working_model->add_constraints()->mutable_bool_or();
1275 BoolArgumentProto* at_most_one_tuple =
nullptr;
1276 if (
context->keep_all_feasible_solutions) {
1278 context->working_model->add_constraints()->mutable_at_most_one();
1281 for (
int var_index = 0; var_index < num_compressed_tuples; ++var_index) {
1282 tuple_literals[var_index] =
context->NewBoolVar();
1283 at_least_one_tuple->add_literals(tuple_literals[var_index]);
1284 if (at_most_one_tuple !=
nullptr) {
1285 at_most_one_tuple->add_literals(tuple_literals[var_index]);
1289 std::vector<int> active_tuple_literals;
1290 std::vector<int64> active_values;
1291 std::vector<int> any_tuple_literals;
1292 for (
int var_index = 0; var_index < num_vars; ++var_index) {
1293 if (values_per_var[var_index].size() == 1)
continue;
1295 active_tuple_literals.clear();
1296 active_values.clear();
1297 any_tuple_literals.clear();
1298 for (
int tuple_index = 0; tuple_index < tuple_literals.size();
1300 const int64 value = tuples[tuple_index][var_index];
1301 const int tuple_literal = tuple_literals[tuple_index];
1303 if (
value == any_value) {
1304 any_tuple_literals.push_back(tuple_literal);
1306 active_tuple_literals.push_back(tuple_literal);
1307 active_values.push_back(
value);
1311 if (!active_tuple_literals.empty()) {
1312 ProcessOneVariable(active_tuple_literals, active_values, vars[var_index],
1317 context->UpdateRuleStats(
"table: expanded positive constraint");
1321 void ExpandAllDiff(
bool expand_non_permutations, ConstraintProto*
ct,
1323 AllDifferentConstraintProto&
proto = *
ct->mutable_all_diff();
1324 if (
proto.vars_size() <= 2)
return;
1326 const int num_vars =
proto.vars_size();
1328 Domain union_of_domains =
context->DomainOf(
proto.vars(0));
1329 for (
int i = 1; i < num_vars; ++i) {
1331 union_of_domains.UnionWith(
context->DomainOf(
proto.vars(i)));
1334 const bool is_permutation =
proto.vars_size() == union_of_domains.Size();
1336 if (!is_permutation && !expand_non_permutations)
return;
1341 for (
const ClosedInterval&
interval : union_of_domains) {
1344 std::vector<int> possible_refs;
1345 int fixed_variable_count = 0;
1346 for (
const int ref :
proto.vars()) {
1347 if (!
context->DomainContains(ref, v))
continue;
1348 possible_refs.push_back(ref);
1349 if (
context->DomainOf(ref).Size() == 1) {
1350 fixed_variable_count++;
1354 if (fixed_variable_count > 1) {
1356 return (
void)
context->NotifyThatModelIsUnsat();
1357 }
else if (fixed_variable_count == 1) {
1359 for (
const int ref : possible_refs) {
1360 if (
context->DomainOf(ref).Size() == 1)
continue;
1361 if (!
context->IntersectDomainWith(ref, Domain(v).Complement())) {
1362 VLOG(1) <<
"Empty domain for a variable in ExpandAllDiff()";
1368 LinearConstraintProto* at_most_or_equal_one =
1369 context->working_model->add_constraints()->mutable_linear();
1370 int lb = is_permutation ? 1 : 0;
1372 for (
const int ref : possible_refs) {
1375 const int encoding =
context->GetOrCreateVarValueEncoding(ref, v);
1377 at_most_or_equal_one->add_vars(encoding);
1378 at_most_or_equal_one->add_coeffs(1);
1380 at_most_or_equal_one->add_vars(
PositiveRef(encoding));
1381 at_most_or_equal_one->add_coeffs(-1);
1386 at_most_or_equal_one->add_domain(lb);
1387 at_most_or_equal_one->add_domain(ub);
1390 if (is_permutation) {
1391 context->UpdateRuleStats(
"alldiff: permutation expanded");
1393 context->UpdateRuleStats(
"alldiff: expanded");
1401 if (
context->params().disable_constraint_expansion())
return;
1403 if (
context->ModelIsUnsat())
return;
1406 context->InitializeNewDomains();
1409 context->ClearPrecedenceCache();
1411 const int num_constraints =
context->working_model->constraints_size();
1412 for (
int i = 0; i < num_constraints; ++i) {
1413 ConstraintProto*
const ct =
context->working_model->mutable_constraints(i);
1415 switch (
ct->constraint_case()) {
1416 case ConstraintProto::ConstraintCase::kReservoir:
1417 if (
context->params().expand_reservoir_constraints()) {
1421 case ConstraintProto::ConstraintCase::kIntMod:
1424 case ConstraintProto::ConstraintCase::kIntDiv:
1427 case ConstraintProto::ConstraintCase::kIntProd:
1430 case ConstraintProto::ConstraintCase::kLinMin:
1433 case ConstraintProto::ConstraintCase::kElement:
1434 if (
context->params().expand_element_constraints()) {
1438 case ConstraintProto::ConstraintCase::kInverse:
1441 case ConstraintProto::ConstraintCase::kAutomaton:
1442 if (
context->params().expand_automaton_constraints()) {
1446 case ConstraintProto::ConstraintCase::kTable:
1447 if (
ct->table().negated()) {
1449 }
else if (
context->params().expand_table_constraints()) {
1453 case ConstraintProto::ConstraintCase::kAllDiff:
1454 ExpandAllDiff(
context->params().expand_alldiff_constraints(),
ct,
1464 context->UpdateNewConstraintsVariableUsage();
1465 if (
ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
1466 context->UpdateConstraintVariableUsage(i);
1470 if (
context->ModelIsUnsat()) {
1472 LOG(
INFO) <<
"UNSAT after expansion of "
1482 context->ClearPrecedenceCache();
1485 context->InitializeNewDomains();
1488 for (
int i = 0; i <
context->working_model->variables_size(); ++i) {
1490 context->working_model->mutable_variables(i));
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define VLOG(verboselevel)
Domain Complement() const
Returns the set Int64 ∖ D.
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
GurobiMPCallbackContext * context
static const int64 kint64max
static const int64 kint64min
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
bool RefIsPositive(int ref)
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
void ExpandCpModel(PresolveContext *context)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
void CompressTuples(absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 >> *tuples)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapSub(int64 x, int64 y)
std::string ProtobufShortDebugString(const P &message)
int64 CapProd(int64 x, int64 y)
#define VLOG_IS_ON(verboselevel)