29 #include "absl/container/flat_hash_map.h"
30 #include "absl/container/flat_hash_set.h"
31 #include "absl/random/random.h"
32 #include "absl/strings/str_join.h"
41 #include "ortools/sat/cp_model.pb.h"
51 #include "ortools/sat/sat_parameters.pb.h"
58 bool CpModelPresolver::RemoveConstraint(ConstraintProto*
ct) {
66 std::vector<int> interval_mapping(context_->
working_model->constraints_size(),
68 int new_num_constraints = 0;
69 const int old_num_non_empty_constraints =
71 for (
int c = 0; c < old_num_non_empty_constraints; ++c) {
72 const auto type = context_->
working_model->constraints(c).constraint_case();
73 if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET)
continue;
74 if (type == ConstraintProto::ConstraintCase::kInterval) {
75 interval_mapping[c] = new_num_constraints;
77 context_->
working_model->mutable_constraints(new_num_constraints++)
80 context_->
working_model->mutable_constraints()->DeleteSubrange(
81 new_num_constraints, old_num_non_empty_constraints - new_num_constraints);
82 for (ConstraintProto& ct_ref :
85 [&interval_mapping](
int* ref) {
86 *ref = interval_mapping[*ref];
93 bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto*
ct) {
98 const int old_size =
ct->enforcement_literal().size();
99 for (
const int literal :
ct->enforcement_literal()) {
108 return RemoveConstraint(
ct);
115 return RemoveConstraint(
ct);
122 const int64 obj_coeff =
126 context_->
UpdateRuleStats(
"enforcement literal with unique direction");
128 return RemoveConstraint(
ct);
132 ct->set_enforcement_literal(new_size++,
literal);
134 ct->mutable_enforcement_literal()->Truncate(new_size);
135 return new_size != old_size;
138 bool CpModelPresolver::PresolveBoolXor(ConstraintProto*
ct) {
143 bool changed =
false;
144 int num_true_literals = 0;
146 for (
const int literal :
ct->bool_xor().literals()) {
167 ct->mutable_bool_xor()->set_literals(new_size++,
literal);
171 }
else if (new_size == 2) {
174 if (num_true_literals % 2 == 1) {
176 ct->mutable_bool_xor()->set_literals(new_size++, true_literal);
178 if (num_true_literals > 1) {
179 context_->
UpdateRuleStats(
"bool_xor: remove even number of true literals");
182 ct->mutable_bool_xor()->mutable_literals()->Truncate(new_size);
186 bool CpModelPresolver::PresolveBoolOr(ConstraintProto*
ct) {
193 for (
const int literal :
ct->enforcement_literal()) {
196 ct->clear_enforcement_literal();
200 bool changed =
false;
203 for (
const int literal :
ct->bool_or().literals()) {
210 return RemoveConstraint(
ct);
218 return RemoveConstraint(
ct);
222 return RemoveConstraint(
ct);
241 return RemoveConstraint(
ct);
254 ct->mutable_bool_or()->mutable_literals()->Clear();
256 ct->mutable_bool_or()->add_literals(lit);
262 ABSL_MUST_USE_RESULT
bool CpModelPresolver::MarkConstraintAsFalse(
263 ConstraintProto*
ct) {
266 ct->mutable_bool_or()->clear_literals();
267 for (
const int lit :
ct->enforcement_literal()) {
270 ct->clear_enforcement_literal();
278 bool CpModelPresolver::PresolveBoolAnd(ConstraintProto*
ct) {
283 for (
const int literal :
ct->bool_and().literals()) {
286 return RemoveConstraint(
ct);
289 bool changed =
false;
291 for (
const int literal :
ct->bool_and().literals()) {
294 return MarkConstraintAsFalse(
ct);
314 ct->mutable_bool_and()->mutable_literals()->Clear();
316 ct->mutable_bool_and()->add_literals(lit);
325 if (
ct->enforcement_literal().size() == 1 &&
326 ct->bool_and().literals().size() == 1) {
327 const int enforcement =
ct->enforcement_literal(0);
337 ct->bool_and().literals(0));
345 bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto*
ct) {
346 bool is_at_most_one =
ct->constraint_case() == ConstraintProto::kAtMostOne;
347 const std::string
name = is_at_most_one ?
"at_most_one: " :
"exactly_one: ";
348 auto* literals = is_at_most_one
349 ?
ct->mutable_at_most_one()->mutable_literals()
350 :
ct->mutable_exactly_one()->mutable_literals();
354 for (
const int literal : *literals) {
360 int num_positive = 0;
361 int num_negative = 0;
362 for (
const int other : *literals) {
383 return RemoveConstraint(
ct);
389 bool changed =
false;
390 bool transform_to_at_most_one =
false;
392 for (
const int literal : *literals) {
395 for (
const int other : *literals) {
400 return RemoveConstraint(
ct);
413 if (is_at_most_one && !is_removable &&
417 const int64 coeff = it->second;
424 if (is_at_most_one) {
431 is_at_most_one =
true;
432 transform_to_at_most_one =
true;
442 if (transform_to_at_most_one) {
445 literals =
ct->mutable_at_most_one()->mutable_literals();
457 bool CpModelPresolver::PresolveAtMostOne(ConstraintProto*
ct) {
460 const bool changed = PresolveAtMostOrExactlyOne(
ct);
461 if (
ct->constraint_case() != ConstraintProto::kAtMostOne)
return changed;
464 const auto& literals =
ct->at_most_one().literals();
465 if (literals.empty()) {
467 return RemoveConstraint(
ct);
471 if (literals.size() == 1) {
473 return RemoveConstraint(
ct);
479 bool CpModelPresolver::PresolveExactlyOne(ConstraintProto*
ct) {
482 const bool changed = PresolveAtMostOrExactlyOne(
ct);
483 if (
ct->constraint_case() != ConstraintProto::kExactlyOne)
return changed;
486 const auto& literals =
ct->exactly_one().literals();
487 if (literals.empty()) {
492 if (literals.size() == 1) {
495 return RemoveConstraint(
ct);
499 if (literals.size() == 2) {
503 return RemoveConstraint(
ct);
509 bool CpModelPresolver::PresolveIntMax(ConstraintProto*
ct) {
511 if (
ct->int_max().vars().empty()) {
513 return MarkConstraintAsFalse(
ct);
515 const int target_ref =
ct->int_max().target();
520 bool contains_target_ref =
false;
521 std::set<int> used_ref;
523 for (
const int ref :
ct->int_max().vars()) {
524 if (ref == target_ref) contains_target_ref =
true;
530 used_ref.insert(ref);
531 ct->mutable_int_max()->set_vars(new_size++, ref);
535 if (new_size < ct->int_max().vars_size()) {
538 ct->mutable_int_max()->mutable_vars()->Truncate(new_size);
539 if (contains_target_ref) {
541 for (
const int ref :
ct->int_max().vars()) {
542 if (ref == target_ref)
continue;
543 ConstraintProto* new_ct = context_->
working_model->add_constraints();
544 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
545 auto* arg = new_ct->mutable_linear();
546 arg->add_vars(target_ref);
553 return RemoveConstraint(
ct);
557 Domain infered_domain;
558 for (
const int ref :
ct->int_max().vars()) {
559 infered_domain = infered_domain.UnionWith(
564 bool domain_reduced =
false;
576 const Domain& target_domain = context_->
DomainOf(target_ref);
577 if (infered_domain.IntersectionWith(Domain(
kint64min, target_domain.Max()))
578 .IsIncludedIn(target_domain)) {
579 if (infered_domain.Max() <= target_domain.Max()) {
582 }
else if (
ct->enforcement_literal().empty()) {
584 for (
const int ref :
ct->int_max().vars()) {
587 ref, Domain(
kint64min, target_domain.Max()))) {
595 for (
const int ref :
ct->int_max().vars()) {
596 ConstraintProto* new_ct = context_->
working_model->add_constraints();
597 *(new_ct->mutable_enforcement_literal()) =
ct->enforcement_literal();
598 ct->mutable_linear()->add_vars(ref);
599 ct->mutable_linear()->add_coeffs(1);
601 ct->mutable_linear()->add_domain(target_domain.Max());
608 return RemoveConstraint(
ct);
614 const int size =
ct->int_max().vars_size();
615 const int64 target_max = context_->
MaxOf(target_ref);
616 for (
const int ref :
ct->int_max().vars()) {
623 if (context_->
MaxOf(ref) >= infered_min) {
624 ct->mutable_int_max()->set_vars(new_size++, ref);
627 if (domain_reduced) {
631 bool modified =
false;
632 if (new_size < size) {
634 ct->mutable_int_max()->mutable_vars()->Truncate(new_size);
640 return MarkConstraintAsFalse(
ct);
646 ConstraintProto* new_ct = context_->
working_model->add_constraints();
648 auto* arg = new_ct->mutable_linear();
649 arg->add_vars(target_ref);
651 arg->add_vars(
ct->int_max().vars(0));
656 return RemoveConstraint(
ct);
661 bool CpModelPresolver::PresolveLinMin(ConstraintProto*
ct) {
664 const auto copy =
ct->lin_min();
666 ct->mutable_lin_max()->mutable_target());
667 for (
const LinearExpressionProto& expr : copy.exprs()) {
668 LinearExpressionProto*
const new_expr =
ct->mutable_lin_max()->add_exprs();
671 return PresolveLinMax(
ct);
674 bool CpModelPresolver::PresolveLinMax(ConstraintProto*
ct) {
676 if (
ct->lin_max().exprs().empty()) {
678 return MarkConstraintAsFalse(
ct);
685 bool changed = CanonicalizeLinearExpression(
686 *
ct,
ct->mutable_lin_max()->mutable_target());
687 for (LinearExpressionProto& exp : *(
ct->mutable_lin_max()->mutable_exprs())) {
688 changed |= CanonicalizeLinearExpression(*
ct, &exp);
694 int64 infered_min = context_->
MinOf(
ct->lin_max().target());
695 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
706 for (
int i = 0; i <
ct->lin_max().exprs_size(); ++i) {
707 const LinearExpressionProto& expr =
ct->lin_max().exprs(i);
708 if (context_->
MaxOf(expr) >= infered_min) {
709 *
ct->mutable_lin_max()->mutable_exprs(new_size) = expr;
714 if (new_size < ct->lin_max().exprs_size()) {
716 ct->mutable_lin_max()->mutable_exprs()->DeleteSubrange(
717 new_size,
ct->lin_max().exprs_size() - new_size);
724 bool CpModelPresolver::PresolveIntAbs(ConstraintProto*
ct) {
727 const int target_ref =
ct->int_max().target();
732 const Domain new_target_domain = var_domain.
UnionWith(var_domain.Negation())
742 const Domain target_domain = context_->
DomainOf(target_ref);
743 const Domain new_var_domain =
744 target_domain.
UnionWith(target_domain.Negation());
754 ConstraintProto* new_ct = context_->
working_model->add_constraints();
755 new_ct->set_name(
ct->name());
756 auto* arg = new_ct->mutable_linear();
757 arg->add_vars(target_ref);
764 return RemoveConstraint(
ct);
769 ConstraintProto* new_ct = context_->
working_model->add_constraints();
770 new_ct->set_name(
ct->name());
771 auto* arg = new_ct->mutable_linear();
772 arg->add_vars(target_ref);
779 return RemoveConstraint(
ct);
785 context_->
IsFixed(target_ref)) {
786 if (!context_->
IsFixed(target_ref)) {
791 return RemoveConstraint(
ct);
801 bool CpModelPresolver::PresolveIntMin(ConstraintProto*
ct) {
804 const auto copy =
ct->int_min();
805 ct->mutable_int_max()->set_target(
NegatedRef(copy.target()));
806 for (
const int ref : copy.vars()) {
809 return PresolveIntMax(
ct);
812 bool CpModelPresolver::PresolveIntProd(ConstraintProto*
ct) {
816 if (
ct->int_prod().vars().empty()) {
821 return RemoveConstraint(
ct);
823 bool changed =
false;
828 for (
int i = 0; i <
ct->int_prod().vars().size(); ++i) {
829 const int ref =
ct->int_prod().vars(i);
831 if (r.representative != ref && r.offset == 0) {
833 ct->mutable_int_prod()->set_vars(i, r.representative);
848 const int old_target =
ct->int_prod().target();
849 const int new_target = context_->
working_model->variables_size();
851 IntegerVariableProto* var_proto = context_->
working_model->add_variables();
858 ct->mutable_int_prod()->set_target(new_target);
859 if (context_->
IsFixed(new_target)) {
871 ConstraintProto* new_ct = context_->
working_model->add_constraints();
872 LinearConstraintProto* lin = new_ct->mutable_linear();
873 lin->add_vars(old_target);
875 lin->add_vars(new_target);
876 lin->add_coeffs(-constant);
886 for (
const int ref :
ct->int_prod().vars()) {
887 implied = implied.ContinuousMultiplicationBy(context_->
DomainOf(ref));
889 bool modified =
false;
898 if (
ct->int_prod().vars_size() == 2) {
899 int a =
ct->int_prod().vars(0);
900 int b =
ct->int_prod().vars(1);
901 const int product =
ct->int_prod().target();
911 return RemoveConstraint(
ct);
912 }
else if (
b != product) {
913 ConstraintProto*
const lin = context_->
working_model->add_constraints();
914 lin->mutable_linear()->add_vars(
b);
915 lin->mutable_linear()->add_coeffs(value_a);
916 lin->mutable_linear()->add_vars(product);
917 lin->mutable_linear()->add_coeffs(-1);
918 lin->mutable_linear()->add_domain(0);
919 lin->mutable_linear()->add_domain(0);
922 return RemoveConstraint(
ct);
923 }
else if (value_a != 1) {
928 return RemoveConstraint(
ct);
931 return RemoveConstraint(
ct);
933 }
else if (
a ==
b &&
a == product) {
938 return RemoveConstraint(
ct);
943 const int target_ref =
ct->int_prod().target();
945 for (
const int var :
ct->int_prod().vars()) {
947 if (context_->
MinOf(
var) < 0)
return changed;
948 if (context_->
MaxOf(
var) > 1)
return changed;
957 ConstraintProto* new_ct = context_->
working_model->add_constraints();
958 new_ct->add_enforcement_literal(target_ref);
959 auto* arg = new_ct->mutable_bool_and();
960 for (
const int var :
ct->int_prod().vars()) {
961 arg->add_literals(
var);
965 ConstraintProto* new_ct = context_->
working_model->add_constraints();
966 auto* arg = new_ct->mutable_bool_or();
967 arg->add_literals(target_ref);
968 for (
const int var :
ct->int_prod().vars()) {
973 return RemoveConstraint(
ct);
976 bool CpModelPresolver::PresolveIntDiv(ConstraintProto*
ct) {
980 const int target =
ct->int_div().target();
981 const int ref_x =
ct->int_div().vars(0);
982 const int ref_div =
ct->int_div().vars(1);
989 const int64 divisor = context_->
MinOf(ref_div);
991 LinearConstraintProto*
const lin =
992 context_->
working_model->add_constraints()->mutable_linear();
993 lin->add_vars(ref_x);
995 lin->add_vars(target);
1001 return RemoveConstraint(
ct);
1003 bool domain_modified =
false;
1006 &domain_modified)) {
1007 if (domain_modified) {
1009 "int_div: updated domain of target in target = X / cte");
1020 if (context_->
MinOf(target) >= 0 && context_->
MinOf(ref_x) >= 0 &&
1022 LinearConstraintProto*
const lin =
1023 context_->
working_model->add_constraints()->mutable_linear();
1024 lin->add_vars(ref_x);
1026 lin->add_vars(target);
1027 lin->add_coeffs(-divisor);
1029 lin->add_domain(divisor - 1);
1032 "int_div: linearize positive division with a constant divisor");
1033 return RemoveConstraint(
ct);
1041 bool CpModelPresolver::ExploitEquivalenceRelations(
int c, ConstraintProto*
ct) {
1042 bool changed =
false;
1047 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
1048 for (
int& ref : *
ct->mutable_enforcement_literal()) {
1060 bool work_to_do =
false;
1063 if (r.representative !=
var) {
1068 if (!work_to_do)
return false;
1072 [&changed,
this](
int* ref) {
1083 [&changed,
this](
int* ref) {
1094 void CpModelPresolver::DivideLinearByGcd(ConstraintProto*
ct) {
1099 const int num_vars =
ct->linear().vars().size();
1100 for (
int i = 0; i < num_vars; ++i) {
1101 const int64 magnitude = std::abs(
ct->linear().coeffs(i));
1103 if (gcd == 1)
break;
1107 for (
int i = 0; i < num_vars; ++i) {
1108 ct->mutable_linear()->set_coeffs(i,
ct->linear().coeffs(i) / gcd);
1112 if (
ct->linear().domain_size() == 0) {
1113 return (
void)MarkConstraintAsFalse(
ct);
1118 void CpModelPresolver::PresolveLinearEqualityModuloTwo(ConstraintProto*
ct) {
1119 if (!
ct->enforcement_literal().empty())
return;
1120 if (
ct->linear().domain().size() != 2)
return;
1121 if (
ct->linear().domain(0) !=
ct->linear().domain(1))
return;
1126 std::vector<int> literals;
1127 for (
int i = 0; i <
ct->linear().vars().size(); ++i) {
1128 const int64 coeff =
ct->linear().coeffs(i);
1129 const int ref =
ct->linear().vars(i);
1130 if (coeff % 2 == 0)
continue;
1133 if (literals.size() > 2)
return;
1135 if (literals.size() == 1) {
1136 const int64 rhs = std::abs(
ct->linear().domain(0));
1137 context_->
UpdateRuleStats(
"linear: only one odd Boolean in equality");
1139 }
else if (literals.size() == 2) {
1140 const int64 rhs = std::abs(
ct->linear().domain(0));
1141 context_->
UpdateRuleStats(
"linear: only two odd Booleans in equality");
1151 template <
typename ProtoWithVarsAndCoeffs>
1152 bool CpModelPresolver::CanonicalizeLinearExpressionInternal(
1153 const ConstraintProto&
ct, ProtoWithVarsAndCoeffs*
proto,
int64* offset) {
1159 int64 sum_of_fixed_terms = 0;
1160 bool remapped =
false;
1161 const int old_size =
proto->vars().size();
1163 for (
int i = 0; i < old_size; ++i) {
1164 const int ref =
proto->vars(i);
1168 if (coeff == 0)
continue;
1171 sum_of_fixed_terms += coeff * context_->
MinOf(
var);
1177 bool removed =
false;
1178 for (
const int enf :
ct.enforcement_literal()) {
1182 sum_of_fixed_terms += coeff;
1191 context_->
UpdateRuleStats(
"linear: enforcement literal in expression");
1196 if (r.representative !=
var) {
1198 sum_of_fixed_terms += coeff * r.
offset;
1200 tmp_terms_.push_back({r.representative, coeff * r.coeff});
1202 proto->clear_vars();
1203 proto->clear_coeffs();
1204 std::sort(tmp_terms_.begin(), tmp_terms_.end());
1205 int current_var = 0;
1206 int64 current_coeff = 0;
1207 for (
const auto entry : tmp_terms_) {
1209 if (entry.first == current_var) {
1210 current_coeff += entry.second;
1212 if (current_coeff != 0) {
1213 proto->add_vars(current_var);
1214 proto->add_coeffs(current_coeff);
1216 current_var = entry.first;
1217 current_coeff = entry.second;
1220 if (current_coeff != 0) {
1221 proto->add_vars(current_var);
1222 proto->add_coeffs(current_coeff);
1227 if (
proto->vars().size() < old_size) {
1230 *offset = sum_of_fixed_terms;
1231 return remapped ||
proto->vars().size() < old_size;
1234 bool CpModelPresolver::CanonicalizeLinearExpression(
1235 const ConstraintProto&
ct, LinearExpressionProto* exp) {
1237 const bool result = CanonicalizeLinearExpressionInternal(
ct, exp, &offset);
1238 exp->set_offset(exp->offset() + offset);
1242 bool CpModelPresolver::CanonicalizeLinear(ConstraintProto*
ct) {
1243 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1249 CanonicalizeLinearExpressionInternal(*
ct,
ct->mutable_linear(), &offset);
1253 ct->mutable_linear());
1255 DivideLinearByGcd(
ct);
1259 bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto*
ct) {
1260 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1265 std::set<int> index_to_erase;
1266 const int num_vars =
ct->linear().vars().size();
1272 for (
int i = 0; i < num_vars; ++i) {
1273 const int var =
ct->linear().vars(i);
1274 const int64 coeff =
ct->linear().coeffs(i);
1278 const auto term_domain =
1280 if (!exact)
continue;
1284 if (new_rhs.NumIntervals() > 100)
continue;
1291 index_to_erase.insert(i);
1298 if (index_to_erase.empty()) {
1300 if (context_->
params().presolve_substitution_level() <= 0)
return false;
1301 if (!
ct->enforcement_literal().empty())
return false;
1305 if (rhs.Min() != rhs.Max())
return false;
1307 for (
int i = 0; i < num_vars; ++i) {
1308 const int var =
ct->linear().vars(i);
1309 const int64 coeff =
ct->linear().coeffs(i);
1327 const int64 objective_coeff =
1330 if (objective_coeff % coeff != 0)
continue;
1334 const auto term_domain =
1336 if (!exact)
continue;
1338 if (new_rhs.NumIntervals() > 100)
continue;
1346 objective_coeff))) {
1363 LOG(
WARNING) <<
"This was not supposed to happen and the presolve "
1364 "could be improved.";
1367 context_->
UpdateRuleStats(
"linear: singleton column define objective.");
1371 return RemoveConstraint(
ct);
1380 "linear: singleton column in equality and in objective.");
1382 index_to_erase.insert(i);
1386 if (index_to_erase.empty())
return false;
1395 for (
int i = 0; i < num_vars; ++i) {
1396 if (index_to_erase.count(i)) {
1400 ct->mutable_linear()->set_coeffs(new_size,
ct->linear().coeffs(i));
1401 ct->mutable_linear()->set_vars(new_size,
ct->linear().vars(i));
1404 ct->mutable_linear()->mutable_vars()->Truncate(new_size);
1405 ct->mutable_linear()->mutable_coeffs()->Truncate(new_size);
1407 DivideLinearByGcd(
ct);
1411 bool CpModelPresolver::PresolveSmallLinear(ConstraintProto*
ct) {
1412 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1418 if (
ct->linear().vars().empty()) {
1421 if (rhs.Contains(0)) {
1422 return RemoveConstraint(
ct);
1424 return MarkConstraintAsFalse(
ct);
1431 if (
ct->linear().vars_size() == 1 &&
ct->enforcement_literal_size() > 0 &&
1432 ct->linear().coeffs(0) == 1 &&
1435 context_->
UpdateRuleStats(
"linear: remove abs from abs(x) in domain");
1436 const Domain implied_abs_target_domain =
1439 .IntersectionWith(context_->
DomainOf(
ct->linear().vars(0)));
1441 if (implied_abs_target_domain.IsEmpty()) {
1442 return MarkConstraintAsFalse(
ct);
1445 const Domain new_abs_var_domain =
1446 implied_abs_target_domain
1447 .UnionWith(implied_abs_target_domain.Negation())
1448 .IntersectionWith(context_->
DomainOf(abs_arg));
1450 if (new_abs_var_domain.IsEmpty()) {
1451 return MarkConstraintAsFalse(
ct);
1454 ConstraintProto* new_ct = context_->
working_model->add_constraints();
1455 new_ct->set_name(
ct->name());
1456 for (
const int literal :
ct->enforcement_literal()) {
1457 new_ct->add_enforcement_literal(
literal);
1459 auto* arg = new_ct->mutable_linear();
1460 arg->add_vars(abs_arg);
1464 return RemoveConstraint(
ct);
1468 if (
ct->enforcement_literal_size() != 1 ||
ct->linear().vars_size() != 1 ||
1469 (
ct->linear().coeffs(0) != 1 &&
ct->linear().coeffs(0) == -1)) {
1473 const int literal =
ct->enforcement_literal(0);
1474 const LinearConstraintProto& linear =
ct->linear();
1475 const int ref = linear.vars(0);
1480 if (linear.domain_size() == 2 && linear.domain(0) == linear.domain(1)) {
1482 : -linear.domain(0) * coeff;
1491 if (complement.Size() != 1)
return false;
1493 : -complement.Min() * coeff;
1508 if (
ct->linear().vars().size() == 1) {
1510 ?
ct->linear().coeffs(0)
1511 : -
ct->linear().coeffs(0);
1516 rhs.InverseMultiplicationBy(coeff))) {
1519 return RemoveConstraint(
ct);
1526 const LinearConstraintProto& arg =
ct->linear();
1527 if (arg.vars_size() == 2) {
1529 const int64 rhs_min = rhs.Min();
1530 const int64 rhs_max = rhs.Max();
1531 if (rhs_min == rhs_max) {
1532 const int v1 = arg.vars(0);
1533 const int v2 = arg.vars(1);
1534 const int64 coeff1 = arg.coeffs(0);
1535 const int64 coeff2 = arg.coeffs(1);
1539 }
else if (coeff2 == 1) {
1541 }
else if (coeff1 == -1) {
1543 }
else if (coeff2 == -1) {
1546 if (added)
return RemoveConstraint(
ct);
1556 bool IsLeConstraint(
const Domain& domain,
const Domain& all_values) {
1557 return all_values.IntersectionWith(Domain(
kint64min, domain.Max()))
1558 .IsIncludedIn(domain);
1562 bool IsGeConstraint(
const Domain& domain,
const Domain& all_values) {
1563 return all_values.IntersectionWith(Domain(domain.Min(),
kint64max))
1564 .IsIncludedIn(domain);
1570 bool RhsCanBeFixedToMin(
int64 coeff,
const Domain& var_domain,
1571 const Domain& terms,
const Domain& rhs) {
1572 if (var_domain.NumIntervals() != 1)
return false;
1573 if (std::abs(coeff) != 1)
return false;
1581 if (coeff == 1 && terms.Max() + var_domain.Min() <= rhs.Min()) {
1584 if (coeff == -1 && terms.Max() - var_domain.Max() <= rhs.Min()) {
1590 bool RhsCanBeFixedToMax(
int64 coeff,
const Domain& var_domain,
1591 const Domain& terms,
const Domain& rhs) {
1592 if (var_domain.NumIntervals() != 1)
return false;
1593 if (std::abs(coeff) != 1)
return false;
1595 if (coeff == 1 && terms.Min() + var_domain.Max() >= rhs.Max()) {
1598 if (coeff == -1 && terms.Min() - var_domain.Min() >= rhs.Max()) {
1605 void TakeIntersectionWith(
const absl::flat_hash_set<int>& current,
1606 absl::flat_hash_set<int>* to_clear) {
1607 std::vector<int> new_set;
1608 for (
const int c : *to_clear) {
1609 if (current.contains(c)) new_set.push_back(c);
1612 for (
const int c : new_set) to_clear->insert(c);
1617 bool CpModelPresolver::PropagateDomainsInLinear(
int c, ConstraintProto*
ct) {
1618 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1626 const int num_vars =
ct->linear().vars_size();
1627 term_domains.resize(num_vars + 1);
1628 left_domains.resize(num_vars + 1);
1629 left_domains[0] = Domain(0);
1630 for (
int i = 0; i < num_vars; ++i) {
1631 const int var =
ct->linear().vars(i);
1632 const int64 coeff =
ct->linear().coeffs(i);
1635 left_domains[i + 1] =
1638 const Domain& implied_rhs = left_domains[num_vars];
1642 if (implied_rhs.IsIncludedIn(old_rhs)) {
1644 return RemoveConstraint(
ct);
1648 Domain rhs = old_rhs.SimplifyUsingImpliedDomain(implied_rhs);
1649 if (rhs.IsEmpty()) {
1651 return MarkConstraintAsFalse(
ct);
1653 if (rhs != old_rhs) {
1661 bool is_le_constraint = IsLeConstraint(rhs, implied_rhs);
1662 bool is_ge_constraint = IsGeConstraint(rhs, implied_rhs);
1665 if (
ct->enforcement_literal().size() > 1)
return false;
1667 bool new_bounds =
false;
1668 bool recanonicalize =
false;
1669 Domain negated_rhs = rhs.Negation();
1670 Domain right_domain(0);
1672 Domain implied_term_domain;
1673 term_domains[num_vars] = Domain(0);
1674 for (
int i = num_vars - 1; i >= 0; --i) {
1675 const int var =
ct->linear().vars(i);
1676 const int64 var_coeff =
ct->linear().coeffs(i);
1678 right_domain.AdditionWith(term_domains[i + 1]).RelaxIfTooComplex();
1679 implied_term_domain = left_domains[i].AdditionWith(right_domain);
1680 new_domain = implied_term_domain.AdditionWith(negated_rhs)
1681 .InverseMultiplicationBy(-var_coeff);
1683 if (
ct->enforcement_literal().empty()) {
1688 }
else if (
ct->enforcement_literal().size() == 1) {
1699 recanonicalize =
true;
1703 if (is_le_constraint || is_ge_constraint) {
1704 CHECK_NE(is_le_constraint, is_ge_constraint);
1705 if ((var_coeff > 0) == is_ge_constraint) {
1720 const bool is_in_objective =
1724 const int64 obj_coeff =
1733 if (obj_coeff <= 0 &&
1743 recanonicalize =
true;
1747 if (obj_coeff >= 0 &&
1757 recanonicalize =
true;
1765 if (!
ct->enforcement_literal().empty())
continue;
1777 if (rhs.Min() != rhs.Max() &&
1780 const bool same_sign = (var_coeff > 0) == (obj_coeff > 0);
1782 if (same_sign && RhsCanBeFixedToMin(var_coeff, context_->
DomainOf(
var),
1783 implied_term_domain, rhs)) {
1784 rhs = Domain(rhs.Min());
1787 if (!same_sign && RhsCanBeFixedToMax(var_coeff, context_->
DomainOf(
var),
1788 implied_term_domain, rhs)) {
1789 rhs = Domain(rhs.Max());
1795 negated_rhs = rhs.Negation();
1799 right_domain = Domain(0);
1803 is_le_constraint =
false;
1804 is_ge_constraint =
false;
1805 for (
const int var :
ct->linear().vars()) {
1822 if (
ct->linear().vars().size() <= 2)
continue;
1827 if (rhs.Min() != rhs.Max())
continue;
1833 if (context_->
DomainOf(
var) != new_domain)
continue;
1834 if (std::abs(var_coeff) != 1)
continue;
1835 if (context_->
params().presolve_substitution_level() <= 0)
continue;
1841 bool is_in_objective =
false;
1843 is_in_objective =
true;
1849 if (is_in_objective) col_size--;
1850 const int row_size =
ct->linear().vars_size();
1854 const int num_entries_added = (row_size - 1) * (col_size - 1);
1855 const int num_entries_removed = col_size + row_size - 1;
1857 if (num_entries_added > num_entries_removed) {
1863 std::vector<int> others;
1872 if (context_->
working_model->constraints(c).constraint_case() !=
1873 ConstraintProto::ConstraintCase::kLinear) {
1877 for (
const int ref :
1878 context_->
working_model->constraints(c).enforcement_literal()) {
1884 others.push_back(c);
1886 if (abort)
continue;
1889 for (
const int c : others) {
1902 if (is_in_objective) {
1907 absl::StrCat(
"linear: variable substitution ", others.size()));
1918 const int ct_index = context_->
mapping_model->constraints().size();
1920 LinearConstraintProto* mapping_linear_ct =
1923 std::swap(mapping_linear_ct->mutable_vars()->at(0),
1924 mapping_linear_ct->mutable_vars()->at(i));
1925 std::swap(mapping_linear_ct->mutable_coeffs()->at(0),
1926 mapping_linear_ct->mutable_coeffs()->at(i));
1927 return RemoveConstraint(
ct);
1932 if (recanonicalize)
return CanonicalizeLinear(
ct);
1943 void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
1944 int ct_index, ConstraintProto*
ct) {
1945 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1950 const LinearConstraintProto& arg =
ct->linear();
1951 const int num_vars = arg.vars_size();
1955 if (num_vars <= 1)
return;
1959 int64 max_coeff_magnitude = 0;
1960 for (
int i = 0; i < num_vars; ++i) {
1961 const int ref = arg.vars(i);
1962 const int64 coeff = arg.coeffs(i);
1963 const int64 term_a = coeff * context_->
MinOf(ref);
1964 const int64 term_b = coeff * context_->
MaxOf(ref);
1965 max_coeff_magnitude =
std::max(max_coeff_magnitude, std::abs(coeff));
1966 min_sum +=
std::min(term_a, term_b);
1967 max_sum +=
std::max(term_a, term_b);
1976 const auto& domain =
ct->linear().domain();
1977 const int64 ub_threshold = domain[domain.size() - 2] - min_sum;
1978 const int64 lb_threshold = max_sum - domain[1];
1980 if (max_coeff_magnitude <
std::max(ub_threshold, lb_threshold))
return;
1999 const bool lower_bounded = min_sum < rhs_domain.Min();
2000 const bool upper_bounded = max_sum > rhs_domain.Max();
2001 if (!lower_bounded && !upper_bounded)
return;
2002 if (lower_bounded && upper_bounded) {
2004 ConstraintProto* new_ct1 = context_->
working_model->add_constraints();
2006 if (!
ct->name().empty()) {
2007 new_ct1->set_name(absl::StrCat(
ct->name(),
" (part 1)"));
2010 new_ct1->mutable_linear());
2012 ConstraintProto* new_ct2 = context_->
working_model->add_constraints();
2014 if (!
ct->name().empty()) {
2015 new_ct2->set_name(absl::StrCat(
ct->name(),
" (part 2)"));
2018 new_ct2->mutable_linear());
2021 return (
void)RemoveConstraint(
ct);
2027 const int64 threshold = lower_bounded ? ub_threshold : lb_threshold;
2030 const bool only_booleans =
2031 !context_->
params().presolve_extract_integer_enforcement();
2036 int64 rhs_offset = 0;
2037 bool some_integer_encoding_were_extracted =
false;
2038 LinearConstraintProto* mutable_arg =
ct->mutable_linear();
2039 for (
int i = 0; i < arg.vars_size(); ++i) {
2040 int ref = arg.vars(i);
2041 int64 coeff = arg.coeffs(i);
2048 if (context_->
IsFixed(ref) || coeff < threshold ||
2049 (only_booleans && !is_boolean)) {
2051 mutable_arg->set_vars(new_size, mutable_arg->vars(i));
2052 mutable_arg->set_coeffs(new_size, mutable_arg->coeffs(i));
2060 some_integer_encoding_were_extracted =
true;
2062 "linear: extracted integer enforcement literal");
2064 if (lower_bounded) {
2065 ct->add_enforcement_literal(is_boolean
2068 ref, context_->
MinOf(ref)));
2069 rhs_offset -= coeff * context_->
MinOf(ref);
2071 ct->add_enforcement_literal(is_boolean
2074 ref, context_->
MaxOf(ref)));
2075 rhs_offset -= coeff * context_->
MaxOf(ref);
2078 mutable_arg->mutable_vars()->Truncate(new_size);
2079 mutable_arg->mutable_coeffs()->Truncate(new_size);
2081 if (some_integer_encoding_were_extracted) {
2087 void CpModelPresolver::ExtractAtMostOneFromLinear(ConstraintProto*
ct) {
2092 const LinearConstraintProto& arg =
ct->linear();
2093 const int num_vars = arg.vars_size();
2096 for (
int i = 0; i < num_vars; ++i) {
2097 const int ref = arg.vars(i);
2098 const int64 coeff = arg.coeffs(i);
2099 const int64 term_a = coeff * context_->
MinOf(ref);
2100 const int64 term_b = coeff * context_->
MaxOf(ref);
2101 min_sum +=
std::min(term_a, term_b);
2102 max_sum +=
std::max(term_a, term_b);
2104 for (
const int type : {0, 1}) {
2105 std::vector<int> at_most_one;
2106 for (
int i = 0; i < num_vars; ++i) {
2107 const int ref = arg.vars(i);
2108 const int64 coeff = arg.coeffs(i);
2109 if (context_->
MinOf(ref) != 0)
continue;
2110 if (context_->
MaxOf(ref) != 1)
continue;
2115 if (min_sum + 2 * std::abs(coeff) > rhs.Max()) {
2116 at_most_one.push_back(coeff > 0 ? ref :
NegatedRef(ref));
2119 if (max_sum - 2 * std::abs(coeff) < rhs.Min()) {
2120 at_most_one.push_back(coeff > 0 ?
NegatedRef(ref) : ref);
2124 if (at_most_one.size() > 1) {
2130 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2131 new_ct->set_name(
ct->name());
2132 for (
const int ref : at_most_one) {
2133 new_ct->mutable_at_most_one()->add_literals(ref);
2142 bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto*
ct) {
2143 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
2148 const LinearConstraintProto& arg =
ct->linear();
2149 const int num_vars = arg.vars_size();
2151 int64 max_coeff = 0;
2154 for (
int i = 0; i < num_vars; ++i) {
2156 const int var = arg.vars(i);
2157 const int64 coeff = arg.coeffs(i);
2160 if (context_->
MinOf(
var) != 0)
return false;
2161 if (context_->
MaxOf(
var) != 1)
return false;
2165 min_coeff =
std::min(min_coeff, coeff);
2166 max_coeff =
std::max(max_coeff, coeff);
2170 min_coeff =
std::min(min_coeff, -coeff);
2171 max_coeff =
std::max(max_coeff, -coeff);
2183 if ((!rhs_domain.Contains(min_sum) &&
2184 min_sum + min_coeff > rhs_domain.Max()) ||
2185 (!rhs_domain.Contains(max_sum) &&
2186 max_sum - min_coeff < rhs_domain.Min())) {
2187 context_->
UpdateRuleStats(
"linear: all booleans and trivially false");
2188 return MarkConstraintAsFalse(
ct);
2190 if (Domain(min_sum, max_sum).IsIncludedIn(rhs_domain)) {
2192 return RemoveConstraint(
ct);
2199 DCHECK(!rhs_domain.IsEmpty());
2200 if (min_sum + min_coeff > rhs_domain.Max()) {
2203 const auto copy = arg;
2204 ct->mutable_bool_and()->clear_literals();
2205 for (
int i = 0; i < num_vars; ++i) {
2206 ct->mutable_bool_and()->add_literals(
2207 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
2209 return PresolveBoolAnd(
ct);
2210 }
else if (max_sum - min_coeff < rhs_domain.Min()) {
2213 const auto copy = arg;
2214 ct->mutable_bool_and()->clear_literals();
2215 for (
int i = 0; i < num_vars; ++i) {
2216 ct->mutable_bool_and()->add_literals(
2217 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
2219 return PresolveBoolAnd(
ct);
2220 }
else if (min_sum + min_coeff >= rhs_domain.Min() &&
2221 rhs_domain.front().end >= max_sum) {
2224 const auto copy = arg;
2225 ct->mutable_bool_or()->clear_literals();
2226 for (
int i = 0; i < num_vars; ++i) {
2227 ct->mutable_bool_or()->add_literals(
2228 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
2230 return PresolveBoolOr(
ct);
2231 }
else if (max_sum - min_coeff <= rhs_domain.Max() &&
2232 rhs_domain.back().start <= min_sum) {
2235 const auto copy = arg;
2236 ct->mutable_bool_or()->clear_literals();
2237 for (
int i = 0; i < num_vars; ++i) {
2238 ct->mutable_bool_or()->add_literals(
2239 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
2241 return PresolveBoolOr(
ct);
2243 min_sum + max_coeff <= rhs_domain.Max() &&
2244 min_sum + 2 * min_coeff > rhs_domain.Max() &&
2245 rhs_domain.back().start <= min_sum) {
2248 const auto copy = arg;
2249 ct->mutable_at_most_one()->clear_literals();
2250 for (
int i = 0; i < num_vars; ++i) {
2251 ct->mutable_at_most_one()->add_literals(
2252 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
2256 max_sum - max_coeff >= rhs_domain.Min() &&
2257 max_sum - 2 * min_coeff < rhs_domain.Min() &&
2258 rhs_domain.front().end >= max_sum) {
2261 const auto copy = arg;
2262 ct->mutable_at_most_one()->clear_literals();
2263 for (
int i = 0; i < num_vars; ++i) {
2264 ct->mutable_at_most_one()->add_literals(
2265 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
2269 min_sum < rhs_domain.Min() &&
2270 min_sum + min_coeff >= rhs_domain.Min() &&
2271 min_sum + 2 * min_coeff > rhs_domain.Max() &&
2272 min_sum + max_coeff <= rhs_domain.Max()) {
2274 ConstraintProto* exactly_one = context_->
working_model->add_constraints();
2275 exactly_one->set_name(
ct->name());
2276 for (
int i = 0; i < num_vars; ++i) {
2277 exactly_one->mutable_exactly_one()->add_literals(
2278 arg.coeffs(i) > 0 ? arg.vars(i) :
NegatedRef(arg.vars(i)));
2281 return RemoveConstraint(
ct);
2283 max_sum > rhs_domain.Max() &&
2284 max_sum - min_coeff <= rhs_domain.Max() &&
2285 max_sum - 2 * min_coeff < rhs_domain.Min() &&
2286 max_sum - max_coeff >= rhs_domain.Min()) {
2288 ConstraintProto* exactly_one = context_->
working_model->add_constraints();
2289 exactly_one->set_name(
ct->name());
2290 for (
int i = 0; i < num_vars; ++i) {
2291 exactly_one->mutable_exactly_one()->add_literals(
2292 arg.coeffs(i) > 0 ?
NegatedRef(arg.vars(i)) : arg.vars(i));
2295 return RemoveConstraint(
ct);
2302 if (num_vars > 3)
return false;
2307 const int max_mask = (1 << arg.vars_size());
2308 for (
int mask = 0; mask < max_mask; ++mask) {
2310 for (
int i = 0; i < num_vars; ++i) {
2311 if ((mask >> i) & 1)
value += arg.coeffs(i);
2313 if (rhs_domain.Contains(
value))
continue;
2316 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2317 auto* new_arg = new_ct->mutable_bool_or();
2319 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
2321 for (
int i = 0; i < num_vars; ++i) {
2322 new_arg->add_literals(((mask >> i) & 1) ?
NegatedRef(arg.vars(i))
2328 return RemoveConstraint(
ct);
2333 void AddLinearExpression(
int64 coeff,
const LinearExpressionProto& exp,
2334 LinearConstraintProto* linear_ct) {
2335 const int size = exp.vars().size();
2336 for (
int i = 0; i < size; ++i) {
2337 linear_ct->add_vars(exp.vars(i));
2338 linear_ct->add_coeffs(coeff * exp.coeffs(i));
2340 if (exp.offset() != 0) {
2342 .AdditionWith(Domain(-coeff * exp.offset())),
2349 bool CpModelPresolver::PresolveInterval(
int c, ConstraintProto*
ct) {
2352 if (
ct->enforcement_literal().empty() && !
ct->interval().has_start_view()) {
2353 bool changed =
false;
2354 const int start =
ct->interval().start();
2355 const int end =
ct->interval().end();
2356 const int size =
ct->interval().size();
2357 const Domain start_domain = context_->
DomainOf(start);
2358 const Domain end_domain = context_->
DomainOf(end);
2359 const Domain size_domain = context_->
DomainOf(size);
2366 end, start_domain.AdditionWith(size_domain), &changed)) {
2370 start, end_domain.AdditionWith(size_domain.Negation()), &changed)) {
2374 size, end_domain.AdditionWith(start_domain.Negation()), &changed)) {
2383 if (!
ct->interval().has_start_view()) {
2385 const int start =
ct->interval().start();
2386 const int end =
ct->interval().end();
2387 const int size =
ct->interval().size();
2388 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2389 *(new_ct->mutable_enforcement_literal()) =
ct->enforcement_literal();
2390 new_ct->mutable_linear()->add_domain(0);
2391 new_ct->mutable_linear()->add_domain(0);
2392 new_ct->mutable_linear()->add_vars(start);
2393 new_ct->mutable_linear()->add_coeffs(1);
2394 new_ct->mutable_linear()->add_vars(size);
2395 new_ct->mutable_linear()->add_coeffs(1);
2396 new_ct->mutable_linear()->add_vars(end);
2397 new_ct->mutable_linear()->add_coeffs(-1);
2401 return RemoveConstraint(
ct);
2409 if (context_->
params().convert_intervals()) {
2410 bool changed =
false;
2411 IntervalConstraintProto*
interval =
ct->mutable_interval();
2412 if (!
ct->interval().has_start_view()) {
2417 interval->mutable_start_view()->add_coeffs(1);
2418 interval->mutable_start_view()->set_offset(0);
2420 interval->mutable_size_view()->add_coeffs(1);
2421 interval->mutable_size_view()->set_offset(0);
2423 interval->mutable_end_view()->add_coeffs(1);
2424 interval->mutable_end_view()->set_offset(0);
2431 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2432 *(new_ct->mutable_enforcement_literal()) =
ct->enforcement_literal();
2433 new_ct->mutable_linear()->add_domain(0);
2434 new_ct->mutable_linear()->add_domain(0);
2435 AddLinearExpression(1,
interval->start_view(), new_ct->mutable_linear());
2436 AddLinearExpression(1,
interval->size_view(), new_ct->mutable_linear());
2437 AddLinearExpression(-1,
interval->end_view(), new_ct->mutable_linear());
2447 CanonicalizeLinearExpression(*
ct,
interval->mutable_start_view());
2448 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_size_view());
2449 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_end_view());
2458 if ( (
false) &&
ct->enforcement_literal().empty() &&
2459 context_->
IsFixed(
ct->interval().size())) {
2461 1, context_->
MinOf(
ct->interval().size()));
2468 bool CpModelPresolver::PresolveElement(ConstraintProto*
ct) {
2471 const int index_ref =
ct->element().index();
2472 const int target_ref =
ct->element().target();
2477 bool all_constants =
true;
2478 absl::flat_hash_set<int64> constant_set;
2479 bool all_included_in_target_domain =
true;
2482 bool reduced_index_domain =
false;
2484 Domain(0,
ct->element().vars_size() - 1),
2485 &reduced_index_domain)) {
2493 std::vector<int64> possible_indices;
2494 const Domain& index_domain = context_->
DomainOf(index_ref);
2495 for (
const ClosedInterval&
interval : index_domain) {
2498 const int ref =
ct->element().vars(index_value);
2499 const int64 target_value =
2500 target_ref == index_ref ? index_value : -index_value;
2502 possible_indices.push_back(target_value);
2506 if (possible_indices.size() < index_domain.Size()) {
2512 "element: reduced index domain when target equals index");
2518 Domain infered_domain;
2519 const Domain& initial_index_domain = context_->
DomainOf(index_ref);
2520 const Domain& target_domain = context_->
DomainOf(target_ref);
2521 std::vector<int64> possible_indices;
2522 for (
const ClosedInterval
interval : initial_index_domain) {
2526 const int ref =
ct->element().vars(
value);
2527 const Domain& domain = context_->
DomainOf(ref);
2528 if (domain.IntersectionWith(target_domain).IsEmpty())
continue;
2529 possible_indices.push_back(
value);
2530 if (domain.IsFixed()) {
2531 constant_set.insert(domain.Min());
2533 all_constants =
false;
2535 if (!domain.IsIncludedIn(target_domain)) {
2536 all_included_in_target_domain =
false;
2538 infered_domain = infered_domain.
UnionWith(domain);
2541 if (possible_indices.size() < initial_index_domain.Size()) {
2548 bool domain_modified =
false;
2550 &domain_modified)) {
2553 if (domain_modified) {
2559 if (context_->
IsFixed(index_ref)) {
2560 const int var =
ct->element().vars(context_->
MinOf(index_ref));
2561 if (
var != target_ref) {
2562 LinearConstraintProto*
const lin =
2563 context_->
working_model->add_constraints()->mutable_linear();
2565 lin->add_coeffs(-1);
2566 lin->add_vars(target_ref);
2573 return RemoveConstraint(
ct);
2579 if (all_constants && constant_set.size() == 1) {
2582 return RemoveConstraint(
ct);
2587 if (context_->
MinOf(index_ref) == 0 && context_->
MaxOf(index_ref) == 1 &&
2589 const int64 v0 = context_->
MinOf(
ct->element().vars(0));
2590 const int64 v1 = context_->
MinOf(
ct->element().vars(1));
2592 LinearConstraintProto*
const lin =
2593 context_->
working_model->add_constraints()->mutable_linear();
2594 lin->add_vars(target_ref);
2596 lin->add_vars(index_ref);
2597 lin->add_coeffs(v0 - v1);
2598 lin->add_domain(v0);
2599 lin->add_domain(v0);
2601 context_->
UpdateRuleStats(
"element: linearize constant element of size 2");
2602 return RemoveConstraint(
ct);
2606 const AffineRelation::Relation r_index =
2608 if (r_index.representative != index_ref) {
2610 if (context_->
DomainOf(r_index.representative).
Size() >
2618 const int array_size =
ct->element().vars_size();
2620 context_->
UpdateRuleStats(
"TODO element: representative has bad domain");
2621 }
else if (r_index.offset >= 0 && r_index.offset < array_size &&
2622 r_index.offset + r_max * r_index.coeff >= 0 &&
2623 r_index.offset + r_max * r_index.coeff < array_size) {
2625 ElementConstraintProto*
const element =
2626 context_->
working_model->add_constraints()->mutable_element();
2627 for (
int64 v = 0; v <= r_max; ++v) {
2628 const int64 scaled_index = v * r_index.coeff + r_index.offset;
2630 CHECK_LT(scaled_index, array_size);
2631 element->add_vars(
ct->element().vars(scaled_index));
2633 element->set_index(r_ref);
2634 element->set_target(target_ref);
2636 if (r_index.coeff == 1) {
2642 return RemoveConstraint(
ct);
2648 if (all_constants && unique_index) {
2652 context_->
UpdateRuleStats(
"element: trivial target domain reduction");
2655 return RemoveConstraint(
ct);
2658 const bool unique_target =
2660 context_->
IsFixed(target_ref);
2661 if (all_included_in_target_domain && unique_target) {
2665 return RemoveConstraint(
ct);
2668 if (unique_target && !context_->
IsFixed(target_ref)) {
2678 bool CpModelPresolver::PresolveTable(ConstraintProto*
ct) {
2681 if (
ct->table().vars().empty()) {
2683 return RemoveConstraint(
ct);
2689 const int num_vars =
ct->table().vars_size();
2690 const int num_tuples =
ct->table().values_size() / num_vars;
2691 std::vector<int64> tuple(num_vars);
2692 std::vector<std::vector<int64>> new_tuples;
2693 new_tuples.reserve(num_tuples);
2694 std::vector<absl::flat_hash_set<int64>> new_domains(num_vars);
2695 std::vector<AffineRelation::Relation> affine_relations;
2697 absl::flat_hash_set<int> visited;
2698 for (
const int ref :
ct->table().vars()) {
2706 bool modified_variables =
false;
2707 for (
int v = 0; v < num_vars; ++v) {
2708 const int ref =
ct->table().vars(v);
2710 affine_relations.push_back(r);
2711 if (r.representative != ref) {
2712 modified_variables =
true;
2716 for (
int i = 0; i < num_tuples; ++i) {
2717 bool delete_row =
false;
2719 for (
int j = 0; j < num_vars; ++j) {
2720 const int ref =
ct->table().vars(j);
2721 int64 v =
ct->table().values(i * num_vars + j);
2722 const AffineRelation::Relation& r = affine_relations[j];
2723 if (r.representative != ref) {
2724 const int64 inverse_value = (v - r.offset) / r.coeff;
2725 if (inverse_value * r.coeff + r.offset != v) {
2738 if (delete_row)
continue;
2739 new_tuples.push_back(tuple);
2740 for (
int j = 0; j < num_vars; ++j) {
2741 const int64 v = tuple[j];
2742 new_domains[j].insert(v);
2748 if (new_tuples.size() < num_tuples || modified_variables) {
2749 ct->mutable_table()->clear_values();
2750 for (
const std::vector<int64>& t : new_tuples) {
2751 for (
const int64 v : t) {
2752 ct->mutable_table()->add_values(v);
2755 if (new_tuples.size() < num_tuples) {
2760 if (modified_variables) {
2761 for (
int j = 0; j < num_vars; ++j) {
2762 const AffineRelation::Relation& r = affine_relations[j];
2763 if (r.representative !=
ct->table().vars(j)) {
2764 ct->mutable_table()->set_vars(j, r.representative);
2768 "table: replace variable by canonical affine one");
2772 if (
ct->table().negated())
return modified_variables;
2775 bool changed =
false;
2776 for (
int j = 0; j < num_vars; ++j) {
2777 const int ref =
ct->table().vars(j);
2781 new_domains[j].end())),
2789 if (num_vars == 1) {
2792 return RemoveConstraint(
ct);
2797 for (
int j = 0; j < num_vars; ++j) prod *= new_domains[j].size();
2798 if (prod == new_tuples.size()) {
2800 return RemoveConstraint(
ct);
2806 if (new_tuples.size() > 0.7 * prod) {
2808 std::vector<std::vector<int64>> var_to_values(num_vars);
2809 for (
int j = 0; j < num_vars; ++j) {
2810 var_to_values[j].assign(new_domains[j].begin(), new_domains[j].end());
2812 std::vector<std::vector<int64>> all_tuples(prod);
2813 for (
int i = 0; i < prod; ++i) {
2814 all_tuples[i].resize(num_vars);
2816 for (
int j = 0; j < num_vars; ++j) {
2817 all_tuples[i][j] = var_to_values[j][
index % var_to_values[j].size()];
2818 index /= var_to_values[j].size();
2824 std::vector<std::vector<int64>> diff(prod - new_tuples.size());
2825 std::set_difference(all_tuples.begin(), all_tuples.end(),
2826 new_tuples.begin(), new_tuples.end(), diff.begin());
2829 ct->mutable_table()->set_negated(!
ct->table().negated());
2830 ct->mutable_table()->clear_values();
2831 for (
const std::vector<int64>& t : diff) {
2832 for (
const int64 v : t)
ct->mutable_table()->add_values(v);
2836 return modified_variables;
2839 bool CpModelPresolver::PresolveAllDiff(ConstraintProto*
ct) {
2843 AllDifferentConstraintProto& all_diff = *
ct->mutable_all_diff();
2845 bool constraint_has_changed =
false;
2847 const int size = all_diff.vars_size();
2850 return RemoveConstraint(
ct);
2854 return RemoveConstraint(
ct);
2857 bool something_was_propagated =
false;
2858 std::vector<int> new_variables;
2859 for (
int i = 0; i < size; ++i) {
2860 if (!context_->
IsFixed(all_diff.vars(i))) {
2861 new_variables.push_back(all_diff.vars(i));
2866 bool propagated =
false;
2867 for (
int j = 0; j < size; ++j) {
2868 if (i == j)
continue;
2871 Domain(
value).Complement())) {
2879 something_was_propagated =
true;
2883 std::sort(new_variables.begin(), new_variables.end());
2884 for (
int i = 1; i < new_variables.size(); ++i) {
2885 if (new_variables[i] == new_variables[i - 1]) {
2887 "Duplicate variable in all_diff");
2891 if (new_variables.size() < all_diff.vars_size()) {
2892 all_diff.mutable_vars()->Clear();
2893 for (
const int var : new_variables) {
2894 all_diff.add_vars(
var);
2897 something_was_propagated =
true;
2898 constraint_has_changed =
true;
2899 if (new_variables.size() <= 1)
continue;
2904 Domain domain = context_->
DomainOf(all_diff.vars(0));
2905 for (
int i = 1; i < all_diff.vars_size(); ++i) {
2908 if (all_diff.vars_size() == domain.Size()) {
2909 absl::flat_hash_map<int64, std::vector<int>> value_to_refs;
2910 for (
const int ref : all_diff.vars()) {
2913 value_to_refs[v].push_back(ref);
2917 bool propagated =
false;
2918 for (
const auto& it : value_to_refs) {
2919 if (it.second.size() == 1 &&
2921 const int ref = it.second.
front();
2930 "all_diff: propagated mandatory values in permutation");
2931 something_was_propagated =
true;
2934 if (!something_was_propagated)
break;
2937 return constraint_has_changed;
2944 std::vector<int> GetLiteralsFromSetPPCConstraint(
const ConstraintProto&
ct) {
2945 std::vector<int> sorted_literals;
2946 if (
ct.constraint_case() == ConstraintProto::kAtMostOne) {
2947 for (
const int literal :
ct.at_most_one().literals()) {
2948 sorted_literals.push_back(
literal);
2950 }
else if (
ct.constraint_case() == ConstraintProto::kBoolOr) {
2951 for (
const int literal :
ct.bool_or().literals()) {
2952 sorted_literals.push_back(
literal);
2954 }
else if (
ct.constraint_case() == ConstraintProto::kExactlyOne) {
2955 for (
const int literal :
ct.exactly_one().literals()) {
2956 sorted_literals.push_back(
literal);
2959 std::sort(sorted_literals.begin(), sorted_literals.end());
2960 return sorted_literals;
2965 void AddImplication(
int lhs,
int rhs, CpModelProto*
proto,
2966 absl::flat_hash_map<int, int>* ref_to_bool_and) {
2967 if (ref_to_bool_and->contains(lhs)) {
2968 const int ct_index = (*ref_to_bool_and)[lhs];
2969 proto->mutable_constraints(ct_index)->mutable_bool_and()->add_literals(rhs);
2970 }
else if (ref_to_bool_and->contains(
NegatedRef(rhs))) {
2971 const int ct_index = (*ref_to_bool_and)[
NegatedRef(rhs)];
2972 proto->mutable_constraints(ct_index)->mutable_bool_and()->add_literals(
2975 (*ref_to_bool_and)[lhs] =
proto->constraints_size();
2976 ConstraintProto*
ct =
proto->add_constraints();
2977 ct->add_enforcement_literal(lhs);
2978 ct->mutable_bool_and()->add_literals(rhs);
2982 template <
typename ClauseContainer>
2983 void ExtractClauses(
bool use_bool_and,
const ClauseContainer& container,
2984 CpModelProto*
proto) {
2991 absl::flat_hash_map<int, int> ref_to_bool_and;
2992 for (
int i = 0; i < container.NumClauses(); ++i) {
2993 const std::vector<Literal>& clause = container.Clause(i);
2994 if (clause.empty())
continue;
2997 if (use_bool_and && clause.size() == 2) {
2998 const int a = clause[0].IsPositive()
2999 ? clause[0].Variable().value()
3001 const int b = clause[1].IsPositive()
3002 ? clause[1].Variable().value()
3009 ConstraintProto*
ct =
proto->add_constraints();
3010 for (
const Literal l : clause) {
3011 if (l.IsPositive()) {
3012 ct->mutable_bool_or()->add_literals(l.Variable().value());
3014 ct->mutable_bool_or()->add_literals(
NegatedRef(l.Variable().value()));
3022 int64 CpModelPresolver::StartMin(
3023 const IntervalConstraintProto&
interval)
const {
3028 int64 CpModelPresolver::EndMax(
const IntervalConstraintProto&
interval)
const {
3033 int64 CpModelPresolver::SizeMin(
const IntervalConstraintProto&
interval)
const {
3038 int64 CpModelPresolver::SizeMax(
const IntervalConstraintProto&
interval)
const {
3043 bool CpModelPresolver::PresolveNoOverlap(ConstraintProto*
ct) {
3045 const NoOverlapConstraintProto&
proto =
ct->no_overlap();
3046 const int initial_num_intervals =
proto.intervals_size();
3050 for (
int i = 0; i <
proto.intervals_size(); ++i) {
3051 const int interval_index =
proto.intervals(i);
3053 .constraint_case() ==
3054 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
3057 ct->mutable_no_overlap()->set_intervals(new_size++, interval_index);
3059 ct->mutable_no_overlap()->mutable_intervals()->Truncate(new_size);
3063 ct->mutable_no_overlap()->mutable_intervals()->begin(),
3064 ct->mutable_no_overlap()->mutable_intervals()->end(),
3065 [
this](
int i1,
int i2) {
3066 return StartMin(context_->working_model->constraints(i1).interval()) <
3067 StartMin(context_->working_model->constraints(i2).interval());
3076 for (
int i = 0; i <
proto.intervals_size(); ++i) {
3077 const int interval_index =
proto.intervals(i);
3078 const IntervalConstraintProto&
interval =
3079 context_->
working_model->constraints(interval_index).interval();
3080 const int64 end_max_of_previous_intervals = end_max_so_far;
3082 if (StartMin(
interval) >= end_max_of_previous_intervals &&
3083 (i + 1 ==
proto.intervals_size() ||
3085 ->constraints(
proto.intervals(i + 1))
3090 ct->mutable_no_overlap()->set_intervals(new_size++, interval_index);
3092 ct->mutable_no_overlap()->mutable_intervals()->Truncate(new_size);
3094 if (
proto.intervals_size() == 1) {
3096 return RemoveConstraint(
ct);
3098 if (
proto.intervals().empty()) {
3100 return RemoveConstraint(
ct);
3103 return new_size < initial_num_intervals;
3106 bool CpModelPresolver::PresolveCumulative(ConstraintProto*
ct) {
3109 const CumulativeConstraintProto&
proto =
ct->cumulative();
3113 bool changed =
false;
3114 int num_zero_demand_removed = 0;
3115 int64 sum_of_max_demands = 0;
3116 for (
int i = 0; i <
proto.intervals_size(); ++i) {
3118 .constraint_case() ==
3119 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
3123 const int demand_ref =
proto.demands(i);
3124 const int64 demand_max = context_->
MaxOf(demand_ref);
3125 if (demand_max == 0) {
3126 num_zero_demand_removed++;
3129 sum_of_max_demands += demand_max;
3131 ct->mutable_cumulative()->set_intervals(new_size,
proto.intervals(i));
3132 ct->mutable_cumulative()->set_demands(new_size,
proto.demands(i));
3139 if (sum_of_max_demands <= capacity_min) {
3140 context_->
UpdateRuleStats(
"cumulative: capacity exceeds sum of demands");
3141 return RemoveConstraint(
ct);
3144 if (new_size <
proto.intervals_size()) {
3146 ct->mutable_cumulative()->mutable_intervals()->Truncate(new_size);
3147 ct->mutable_cumulative()->mutable_demands()->Truncate(new_size);
3150 if (num_zero_demand_removed > 0) {
3151 context_->
UpdateRuleStats(
"cumulative: removed intervals with no demands");
3154 if (new_size == 0) {
3156 return RemoveConstraint(
ct);
3161 const int num_intervals =
proto.intervals_size();
3162 bool with_start_view =
false;
3163 std::vector<int> start_refs(num_intervals, -1);
3165 int num_duration_one = 0;
3166 int num_greater_half_capacity = 0;
3168 bool has_optional_interval =
false;
3169 for (
int i = 0; i < num_intervals; ++i) {
3171 const ConstraintProto&
ct =
3173 if (!
ct.enforcement_literal().empty()) has_optional_interval =
true;
3174 const IntervalConstraintProto&
interval =
ct.interval();
3175 if (
interval.has_start_view()) with_start_view =
true;
3177 const int demand_ref =
proto.demands(i);
3187 const int64 demand_min = context_->
MinOf(demand_ref);
3188 const int64 demand_max = context_->
MaxOf(demand_ref);
3189 if (demand_min > capacity_max / 2) {
3190 num_greater_half_capacity++;
3192 if (demand_min > capacity_max) {
3193 context_->
UpdateRuleStats(
"cumulative: demand_min exceeds capacity max");
3194 if (
ct.enforcement_literal().empty()) {
3197 CHECK_EQ(
ct.enforcement_literal().size(), 1);
3203 }
else if (demand_max > capacity_max) {
3204 if (
ct.enforcement_literal().empty()) {
3206 "cumulative: demand_max exceeds capacity max.");
3215 "cumulative: demand_max of optional interval exceeds capacity.");
3221 if (num_greater_half_capacity == num_intervals) {
3222 if (num_duration_one == num_intervals && !has_optional_interval &&
3225 ConstraintProto* new_ct = context_->
working_model->add_constraints();
3226 auto* arg = new_ct->mutable_all_diff();
3227 for (
const int var : start_refs) arg->add_vars(
var);
3229 return RemoveConstraint(
ct);
3232 ConstraintProto* new_ct = context_->
working_model->add_constraints();
3233 auto* arg = new_ct->mutable_no_overlap();
3238 return RemoveConstraint(
ct);
3245 bool CpModelPresolver::PresolveRoutes(ConstraintProto*
ct) {
3248 RoutesConstraintProto&
proto = *
ct->mutable_routes();
3251 const int num_arcs =
proto.literals_size();
3252 for (
int i = 0; i < num_arcs; ++i) {
3253 const int ref =
proto.literals(i);
3260 proto.set_literals(new_size, ref);
3265 if (new_size < num_arcs) {
3266 proto.mutable_literals()->Truncate(new_size);
3267 proto.mutable_tails()->Truncate(new_size);
3268 proto.mutable_heads()->Truncate(new_size);
3274 bool CpModelPresolver::PresolveCircuit(ConstraintProto*
ct) {
3277 CircuitConstraintProto&
proto = *
ct->mutable_circuit();
3281 ct->mutable_circuit()->mutable_heads());
3285 std::vector<std::vector<int>> incoming_arcs;
3286 std::vector<std::vector<int>> outgoing_arcs;
3288 const int num_arcs =
proto.literals_size();
3289 for (
int i = 0; i < num_arcs; ++i) {
3290 const int ref =
proto.literals(i);
3298 incoming_arcs[
head].push_back(ref);
3299 outgoing_arcs[
tail].push_back(ref);
3307 bool loop_again =
true;
3308 int num_fixed_at_true = 0;
3309 while (loop_again) {
3311 for (
const auto* node_to_refs : {&incoming_arcs, &outgoing_arcs}) {
3312 for (
const std::vector<int>& refs : *node_to_refs) {
3313 if (refs.size() == 1) {
3315 ++num_fixed_at_true;
3324 for (
const int ref : refs) {
3334 if (num_true == 1) {
3335 for (
const int ref : refs) {
3336 if (ref != true_ref) {
3337 if (!context_->
IsFixed(ref)) {
3348 if (num_fixed_at_true > 0) {
3355 int circuit_start = -1;
3356 std::vector<int>
next(num_nodes, -1);
3357 std::vector<int> new_in_degree(num_nodes, 0);
3358 std::vector<int> new_out_degree(num_nodes, 0);
3359 for (
int i = 0; i < num_arcs; ++i) {
3360 const int ref =
proto.literals(i);
3368 circuit_start =
proto.tails(i);
3372 ++new_out_degree[
proto.tails(i)];
3373 ++new_in_degree[
proto.heads(i)];
3376 proto.set_literals(new_size,
proto.literals(i));
3386 for (
int i = 0; i < num_nodes; ++i) {
3388 if (incoming_arcs[i].empty() && outgoing_arcs[i].empty())
continue;
3390 if (new_in_degree[i] == 0 || new_out_degree[i] == 0) {
3396 if (circuit_start != -1) {
3397 std::vector<bool> visited(num_nodes,
false);
3398 int current = circuit_start;
3399 while (current != -1 && !visited[current]) {
3400 visited[current] =
true;
3401 current =
next[current];
3403 if (current == circuit_start) {
3406 for (
int i = 0; i < num_arcs; ++i) {
3407 if (visited[
proto.tails(i)])
continue;
3415 return RemoveConstraint(
ct);
3419 if (num_true == new_size) {
3421 return RemoveConstraint(
ct);
3427 for (
int i = 0; i < num_nodes; ++i) {
3428 for (
const std::vector<int>* arc_literals :
3429 {&incoming_arcs[i], &outgoing_arcs[i]}) {
3430 std::vector<int> literals;
3431 for (
const int ref : *arc_literals) {
3437 literals.push_back(ref);
3439 if (literals.size() == 2 && literals[0] !=
NegatedRef(literals[1])) {
3448 if (new_size < num_arcs) {
3449 proto.mutable_tails()->Truncate(new_size);
3450 proto.mutable_heads()->Truncate(new_size);
3451 proto.mutable_literals()->Truncate(new_size);
3458 bool CpModelPresolver::PresolveAutomaton(ConstraintProto*
ct) {
3461 AutomatonConstraintProto&
proto = *
ct->mutable_automaton();
3462 if (
proto.vars_size() == 0 ||
proto.transition_label_size() == 0) {
3466 bool all_affine =
true;
3467 std::vector<AffineRelation::Relation> affine_relations;
3468 for (
int v = 0; v <
proto.vars_size(); ++v) {
3469 const int var =
ct->automaton().vars(v);
3471 affine_relations.push_back(r);
3472 if (r.representative ==
var) {
3476 if (v > 0 && (r.coeff != affine_relations[v - 1].coeff ||
3477 r.offset != affine_relations[v - 1].offset)) {
3484 for (
int v = 0; v <
proto.vars_size(); ++v) {
3487 const AffineRelation::Relation rep = affine_relations.front();
3489 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
3490 const int64 label =
proto.transition_label(t);
3491 int64 inverse_label = (label - rep.offset) / rep.coeff;
3492 if (inverse_label * rep.coeff + rep.offset == label) {
3493 if (new_size != t) {
3494 proto.set_transition_tail(new_size,
proto.transition_tail(t));
3495 proto.set_transition_head(new_size,
proto.transition_head(t));
3497 proto.set_transition_label(new_size, inverse_label);
3501 if (new_size <
proto.transition_tail_size()) {
3502 proto.mutable_transition_tail()->Truncate(new_size);
3503 proto.mutable_transition_label()->Truncate(new_size);
3504 proto.mutable_transition_head()->Truncate(new_size);
3512 for (
int v = 1; v <
proto.vars_size(); ++v) {
3517 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
3518 const int64 label =
proto.transition_label(t);
3519 if (hull.Contains(label)) {
3520 if (new_size != t) {
3521 proto.set_transition_tail(new_size,
proto.transition_tail(t));
3522 proto.set_transition_label(new_size, label);
3523 proto.set_transition_head(new_size,
proto.transition_head(t));
3528 if (new_size <
proto.transition_tail_size()) {
3529 proto.mutable_transition_tail()->Truncate(new_size);
3530 proto.mutable_transition_label()->Truncate(new_size);
3531 proto.mutable_transition_head()->Truncate(new_size);
3536 const int n =
proto.vars_size();
3537 const std::vector<int> vars = {
proto.vars().begin(),
proto.vars().end()};
3540 std::vector<std::set<int64>> reachable_states(n + 1);
3541 reachable_states[0].insert(
proto.starting_state());
3542 reachable_states[n] = {
proto.final_states().begin(),
3543 proto.final_states().end()};
3550 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
3552 const int64 label =
proto.transition_label(t);
3556 reachable_states[
time + 1].insert(
head);
3560 std::vector<std::set<int64>> reached_values(n);
3564 std::set<int64> new_set;
3565 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
3567 const int64 label =
proto.transition_label(t);
3573 new_set.insert(
tail);
3574 reached_values[
time].insert(label);
3576 reachable_states[
time].swap(new_set);
3579 bool removed_values =
false;
3584 {reached_values[time].begin(), reached_values[time].end()}),
3589 if (removed_values) {
3595 bool CpModelPresolver::PresolveReservoir(ConstraintProto*
ct) {
3599 bool changed =
false;
3601 ReservoirConstraintProto& mutable_reservoir = *
ct->mutable_reservoir();
3602 if (mutable_reservoir.actives().empty()) {
3604 for (
int i = 0; i < mutable_reservoir.times_size(); ++i) {
3605 mutable_reservoir.add_actives(true_literal);
3610 const auto& demand_is_null = [&](
int i) {
3611 return mutable_reservoir.demands(i) == 0 ||
3617 for (
int i = 0; i < mutable_reservoir.demands_size(); ++i) {
3618 if (demand_is_null(i)) num_zeros++;
3621 if (num_zeros > 0) {
3624 for (
int i = 0; i < mutable_reservoir.demands_size(); ++i) {
3625 if (demand_is_null(i))
continue;
3626 mutable_reservoir.set_demands(new_size, mutable_reservoir.demands(i));
3627 mutable_reservoir.set_times(new_size, mutable_reservoir.times(i));
3628 mutable_reservoir.set_actives(new_size, mutable_reservoir.actives(i));
3632 mutable_reservoir.mutable_demands()->Truncate(new_size);
3633 mutable_reservoir.mutable_times()->Truncate(new_size);
3634 mutable_reservoir.mutable_actives()->Truncate(new_size);
3637 "reservoir: remove zero demands or inactive events.");
3640 const int num_events = mutable_reservoir.demands_size();
3641 int64 gcd = mutable_reservoir.demands().empty()
3643 : std::abs(mutable_reservoir.demands(0));
3644 int num_positives = 0;
3645 int num_negatives = 0;
3646 int64 sum_of_demands = 0;
3647 int64 max_sum_of_positive_demands = 0;
3648 int64 min_sum_of_negative_demands = 0;
3649 for (
int i = 0; i < num_events; ++i) {
3650 const int64 demand = mutable_reservoir.demands(i);
3651 sum_of_demands +=
demand;
3655 max_sum_of_positive_demands +=
demand;
3659 min_sum_of_negative_demands +=
demand;
3663 if (min_sum_of_negative_demands >= mutable_reservoir.min_level() &&
3664 max_sum_of_positive_demands <= mutable_reservoir.max_level()) {
3666 return RemoveConstraint(
ct);
3669 if (min_sum_of_negative_demands > mutable_reservoir.max_level() ||
3670 max_sum_of_positive_demands < mutable_reservoir.min_level()) {
3675 if (min_sum_of_negative_demands > mutable_reservoir.min_level()) {
3676 mutable_reservoir.set_min_level(min_sum_of_negative_demands);
3678 "reservoir: increase min_level to reachable value");
3681 if (max_sum_of_positive_demands < mutable_reservoir.max_level()) {
3682 mutable_reservoir.set_max_level(max_sum_of_positive_demands);
3683 context_->
UpdateRuleStats(
"reservoir: reduce max_level to reachable value");
3686 if (mutable_reservoir.min_level() <= 0 &&
3687 mutable_reservoir.max_level() >= 0 &&
3688 (num_positives == 0 || num_negatives == 0)) {
3692 context_->
working_model->add_constraints()->mutable_linear();
3693 int64 fixed_contrib = 0;
3694 for (
int i = 0; i < mutable_reservoir.demands_size(); ++i) {
3695 const int64 demand = mutable_reservoir.demands(i);
3698 const int active = mutable_reservoir.actives(i);
3700 sum->add_vars(active);
3704 sum->add_coeffs(-
demand);
3708 sum->add_domain(mutable_reservoir.min_level() - fixed_contrib);
3709 sum->add_domain(mutable_reservoir.max_level() - fixed_contrib);
3711 return RemoveConstraint(
ct);
3715 for (
int i = 0; i < mutable_reservoir.demands_size(); ++i) {
3716 mutable_reservoir.set_demands(i, mutable_reservoir.demands(i) / gcd);
3722 const Domain reduced_domain =
3723 Domain({mutable_reservoir.min_level(), mutable_reservoir.max_level()})
3724 .InverseMultiplicationBy(gcd);
3725 mutable_reservoir.set_min_level(reduced_domain.Min());
3726 mutable_reservoir.set_max_level(reduced_domain.Max());
3727 context_->
UpdateRuleStats(
"reservoir: simplify demands and levels by gcd.");
3730 if (num_positives == 1 && num_negatives > 0) {
3732 "TODO reservoir: one producer, multiple consumers.");
3735 absl::flat_hash_set<std::pair<int, int>> time_active_set;
3736 for (
int i = 0; i < mutable_reservoir.demands_size(); ++i) {
3737 const std::pair<int, int> key = std::make_pair(
3738 mutable_reservoir.times(i), mutable_reservoir.actives(i));
3739 if (time_active_set.contains(key)) {
3740 context_->
UpdateRuleStats(
"TODO reservoir: merge synchronized events.");
3743 time_active_set.insert(key);
3753 void CpModelPresolver::ExtractBoolAnd() {
3754 absl::flat_hash_map<int, int> ref_to_bool_and;
3755 const int num_constraints = context_->
working_model->constraints_size();
3756 std::vector<int> to_remove;
3757 for (
int c = 0; c < num_constraints; ++c) {
3761 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr &&
3762 ct.bool_or().literals().size() == 2) {
3766 to_remove.push_back(c);
3770 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne &&
3771 ct.at_most_one().literals().size() == 2) {
3772 AddImplication(
ct.at_most_one().literals(0),
3775 to_remove.push_back(c);
3781 for (
const int c : to_remove) {
3782 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
3788 void CpModelPresolver::Probe() {
3792 for (
int i = 0; i < context_->
working_model->variables_size(); ++i) {
3812 auto* local_param =
model.GetOrCreate<SatParameters>();
3813 *local_param = context_->
params();
3814 local_param->set_use_implied_bounds(
false);
3816 model.GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(
3818 model.Register<ModelRandomGenerator>(context_->
random());
3819 auto* encoder =
model.GetOrCreate<IntegerEncoder>();
3820 encoder->DisableImplicationBetweenLiteral();
3821 auto* mapping =
model.GetOrCreate<CpModelMapping>();
3825 auto* sat_solver =
model.GetOrCreate<SatSolver>();
3826 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
3827 if (mapping->ConstraintIsAlreadyLoaded(&
ct))
continue;
3829 if (sat_solver->IsModelUnsat()) {
3833 encoder->AddAllImplicationsBetweenAssociatedLiterals();
3834 if (!sat_solver->Propagate()) {
3842 auto* implication_graph =
model.GetOrCreate<BinaryImplicationGraph>();
3843 auto* prober =
model.GetOrCreate<Prober>();
3844 prober->ProbeBooleanVariables(1.0);
3846 model.GetOrCreate<TimeLimit>()->GetElapsedDeterministicTime());
3847 if (sat_solver->IsModelUnsat() || !implication_graph->DetectEquivalences()) {
3852 CHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
3853 for (
int i = 0; i < sat_solver->LiteralTrail().
Index(); ++i) {
3854 const Literal l = sat_solver->LiteralTrail()[i];
3855 const int var = mapping->GetProtoVariableFromBooleanVariable(l.Variable());
3862 const int num_variables = context_->
working_model->variables().size();
3863 auto* integer_trail =
model.GetOrCreate<IntegerTrail>();
3864 for (
int var = 0;
var < num_variables; ++
var) {
3867 if (!mapping->IsBoolean(
var)) {
3870 integer_trail->InitialVariableDomain(mapping->Integer(
var)))) {
3877 const Literal l = mapping->Literal(
var);
3878 const Literal r = implication_graph->RepresentativeOf(l);
3881 mapping->GetProtoVariableFromBooleanVariable(r.Variable());
3891 void CpModelPresolver::PresolvePureSatPart() {
3896 const int num_variables = context_->
working_model->variables_size();
3897 SatPostsolver sat_postsolver(num_variables);
3898 SatPresolver sat_presolver(&sat_postsolver);
3899 sat_presolver.SetNumVariables(num_variables);
3900 sat_presolver.SetTimeLimit(context_->
time_limit());
3902 SatParameters params = context_->
params();
3909 if (params.cp_model_postsolve_with_full_solver()) {
3910 params.set_presolve_blocked_clause(
false);
3916 params.set_presolve_use_bva(
false);
3917 sat_presolver.SetParameters(params);
3920 absl::flat_hash_set<int> used_variables;
3921 auto convert = [&used_variables](
int ref) {
3923 if (
RefIsPositive(ref))
return Literal(BooleanVariable(ref),
true);
3924 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
3932 for (
int c = 0; c < context_->
working_model->constraints_size(); ++c) {
3934 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr ||
3935 ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
3954 std::vector<Literal> clause;
3955 int num_removed_constraints = 0;
3956 for (
int i = 0; i < context_->
working_model->constraints_size(); ++i) {
3959 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
3960 ++num_removed_constraints;
3962 for (
const int ref :
ct.bool_or().literals()) {
3963 clause.push_back(convert(ref));
3965 for (
const int ref :
ct.enforcement_literal()) {
3966 clause.push_back(convert(ref).Negated());
3968 sat_presolver.AddClause(clause);
3975 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
3976 ++num_removed_constraints;
3977 std::vector<Literal> clause;
3978 for (
const int ref :
ct.enforcement_literal()) {
3979 clause.push_back(convert(ref).Negated());
3982 for (
const int ref :
ct.bool_and().literals()) {
3983 clause.back() = convert(ref);
3984 sat_presolver.AddClause(clause);
3994 if (num_removed_constraints == 0)
return;
4004 std::vector<bool> can_be_removed(num_variables,
false);
4005 for (
int i = 0; i < num_variables; ++i) {
4007 can_be_removed[i] =
true;
4013 if (used_variables.contains(i) && context_->
IsFixed(i)) {
4015 sat_presolver.AddClause({convert(i)});
4017 sat_presolver.AddClause({convert(
NegatedRef(i))});
4025 const int num_passes = params.presolve_use_bva() ? 4 : 1;
4026 for (
int i = 0; i < num_passes; ++i) {
4027 const int old_num_clause = sat_postsolver.NumClauses();
4028 if (!sat_presolver.Presolve(can_be_removed, context_->
log_info())) {
4029 VLOG(1) <<
"UNSAT during SAT presolve.";
4032 if (old_num_clause == sat_postsolver.NumClauses())
break;
4036 const int new_num_variables = sat_presolver.NumVariables();
4037 if (new_num_variables > context_->
working_model->variables_size()) {
4038 VLOG(1) <<
"New variables added by the SAT presolver.";
4040 i < new_num_variables; ++i) {
4041 IntegerVariableProto* var_proto =
4043 var_proto->add_domain(0);
4044 var_proto->add_domain(1);
4050 ExtractClauses(
true, sat_presolver, context_->
working_model);
4058 ExtractClauses(
false, sat_postsolver,
4066 void CpModelPresolver::ExpandObjective() {
4085 int unique_expanded_constraint = -1;
4086 const bool objective_was_a_single_variable =
4091 const int num_variables = context_->
working_model->variables_size();
4092 const int num_constraints = context_->
working_model->constraints_size();
4093 absl::flat_hash_set<int> relevant_constraints;
4094 std::vector<int> var_to_num_relevant_constraints(num_variables, 0);
4095 for (
int ct_index = 0; ct_index < num_constraints; ++ct_index) {
4096 const ConstraintProto&
ct = context_->
working_model->constraints(ct_index);
4098 if (!
ct.enforcement_literal().empty() ||
4099 ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
4100 ct.linear().domain().size() != 2 ||
4101 ct.linear().domain(0) !=
ct.linear().domain(1)) {
4105 relevant_constraints.insert(ct_index);
4106 const int num_terms =
ct.linear().vars_size();
4107 for (
int i = 0; i < num_terms; ++i) {
4108 var_to_num_relevant_constraints[
PositiveRef(
ct.linear().vars(i))]++;
4112 std::set<int> var_to_process;
4114 const int var = entry.first;
4116 if (var_to_num_relevant_constraints[
var] != 0) {
4117 var_to_process.insert(
var);
4122 int num_expansions = 0;
4123 absl::flat_hash_set<int> processed_vars;
4124 std::vector<int> new_vars_in_objective;
4125 while (!relevant_constraints.empty()) {
4127 int objective_var = -1;
4128 while (!var_to_process.empty()) {
4129 const int var = *var_to_process.begin();
4130 CHECK(!processed_vars.contains(
var));
4131 if (var_to_num_relevant_constraints[
var] == 0) {
4132 processed_vars.insert(
var);
4133 var_to_process.erase(
var);
4138 var_to_process.erase(
var);
4141 objective_var =
var;
4145 if (objective_var == -1)
break;
4147 processed_vars.insert(objective_var);
4148 var_to_process.erase(objective_var);
4150 int expanded_linear_index = -1;
4151 int64 objective_coeff_in_expanded_constraint;
4152 int64 size_of_expanded_constraint = 0;
4153 const auto& non_deterministic_list =
4155 std::vector<int> constraints_with_objective(non_deterministic_list.begin(),
4156 non_deterministic_list.end());
4157 std::sort(constraints_with_objective.begin(),
4158 constraints_with_objective.end());
4159 for (
const int ct_index : constraints_with_objective) {
4160 if (relevant_constraints.count(ct_index) == 0)
continue;
4161 const ConstraintProto&
ct =
4166 relevant_constraints.erase(ct_index);
4167 const int num_terms =
ct.linear().vars_size();
4168 for (
int i = 0; i < num_terms; ++i) {
4169 var_to_num_relevant_constraints[
PositiveRef(
ct.linear().vars(i))]--;
4181 bool is_present =
false;
4182 int64 objective_coeff;
4183 for (
int i = 0; i < num_terms; ++i) {
4184 const int ref =
ct.linear().vars(i);
4185 const int64 coeff =
ct.linear().coeffs(i);
4187 CHECK(!is_present) <<
"Duplicate variables not supported.";
4189 objective_coeff = (ref == objective_var) ? coeff : -coeff;
4202 if (std::abs(objective_coeff) == 1 &&
4203 num_terms > size_of_expanded_constraint) {
4204 expanded_linear_index = ct_index;
4205 size_of_expanded_constraint = num_terms;
4206 objective_coeff_in_expanded_constraint = objective_coeff;
4210 if (expanded_linear_index != -1) {
4211 context_->
UpdateRuleStats(
"objective: expanded objective constraint.");
4215 CHECK_EQ(std::abs(objective_coeff_in_expanded_constraint), 1);
4216 const ConstraintProto&
ct =
4217 context_->
working_model->constraints(expanded_linear_index);
4219 objective_var, objective_coeff_in_expanded_constraint,
ct,
4220 &new_vars_in_objective);
4223 for (
const int var : new_vars_in_objective) {
4224 if (!processed_vars.contains(
var)) var_to_process.insert(
var);
4237 for (
int i = 0; i < size_of_expanded_constraint; ++i) {
4238 const int ref =
ct.linear().vars(i);
4243 -
ct.linear().coeffs(i)))
4244 .RelaxIfTooComplex();
4246 implied_domain = implied_domain.InverseMultiplicationBy(
4247 objective_coeff_in_expanded_constraint);
4251 if (implied_domain.IsIncludedIn(context_->
DomainOf(objective_var))) {
4252 context_->
UpdateRuleStats(
"objective: removed objective constraint.");
4254 context_->
working_model->mutable_constraints(expanded_linear_index)
4258 unique_expanded_constraint = expanded_linear_index;
4268 if (num_expansions == 1 && objective_was_a_single_variable &&
4269 unique_expanded_constraint != -1) {
4271 "objective: removed unique objective constraint.");
4272 ConstraintProto* mutable_ct = context_->
working_model->mutable_constraints(
4273 unique_expanded_constraint);
4274 *(context_->
mapping_model->add_constraints()) = *mutable_ct;
4275 mutable_ct->Clear();
4287 void CpModelPresolver::MergeNoOverlapConstraints() {
4290 const int num_constraints = context_->
working_model->constraints_size();
4291 int old_num_no_overlaps = 0;
4292 int old_num_intervals = 0;
4295 std::vector<int> disjunctive_index;
4296 std::vector<std::vector<Literal>> cliques;
4297 for (
int c = 0; c < num_constraints; ++c) {
4299 if (
ct.constraint_case() != ConstraintProto::ConstraintCase::kNoOverlap) {
4302 std::vector<Literal> clique;
4303 for (
const int i :
ct.no_overlap().intervals()) {
4304 clique.push_back(Literal(BooleanVariable(i),
true));
4306 cliques.push_back(clique);
4307 disjunctive_index.push_back(c);
4309 old_num_no_overlaps++;
4310 old_num_intervals += clique.size();
4312 if (old_num_no_overlaps == 0)
return;
4316 local_model.GetOrCreate<Trail>()->Resize(num_constraints);
4317 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
4318 graph->Resize(num_constraints);
4319 for (
const std::vector<Literal>& clique : cliques) {
4322 CHECK(graph->AddAtMostOne(clique));
4324 CHECK(graph->DetectEquivalences());
4325 graph->TransformIntoMaxCliques(
4326 &cliques, context_->
params().merge_no_overlap_work_limit());
4329 int new_num_no_overlaps = 0;
4330 int new_num_intervals = 0;
4331 for (
int i = 0; i < cliques.size(); ++i) {
4332 const int ct_index = disjunctive_index[i];
4333 ConstraintProto*
ct =
4336 if (cliques[i].empty())
continue;
4337 for (
const Literal l : cliques[i]) {
4338 CHECK(l.IsPositive());
4339 ct->mutable_no_overlap()->add_intervals(l.Variable().value());
4341 new_num_no_overlaps++;
4342 new_num_intervals += cliques[i].size();
4344 if (old_num_intervals != new_num_intervals ||
4345 old_num_no_overlaps != new_num_no_overlaps) {
4346 VLOG(1) << absl::StrCat(
"Merged ", old_num_no_overlaps,
" no-overlaps (",
4347 old_num_intervals,
" intervals) into ",
4348 new_num_no_overlaps,
" no-overlaps (",
4349 new_num_intervals,
" intervals).");
4358 void CpModelPresolver::TransformIntoMaxCliques() {
4361 auto convert = [](
int ref) {
4362 if (
RefIsPositive(ref))
return Literal(BooleanVariable(ref),
true);
4363 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
4365 const int num_constraints = context_->
working_model->constraints_size();
4368 std::vector<std::vector<Literal>> cliques;
4370 for (
int c = 0; c < num_constraints; ++c) {
4371 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
4372 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne) {
4373 std::vector<Literal> clique;
4374 for (
const int ref :
ct->at_most_one().literals()) {
4375 clique.push_back(convert(ref));
4377 cliques.push_back(clique);
4378 if (RemoveConstraint(
ct)) {
4381 }
else if (
ct->constraint_case() ==
4382 ConstraintProto::ConstraintCase::kBoolAnd) {
4383 if (
ct->enforcement_literal().size() != 1)
continue;
4384 const Literal enforcement = convert(
ct->enforcement_literal(0));
4385 for (
const int ref :
ct->bool_and().literals()) {
4386 if (ref ==
ct->enforcement_literal(0))
continue;
4387 cliques.push_back({enforcement, convert(ref).Negated()});
4389 if (RemoveConstraint(
ct)) {
4395 const int num_old_cliques = cliques.size();
4399 const int num_variables = context_->
working_model->variables().size();
4400 local_model.GetOrCreate<Trail>()->Resize(num_variables);
4401 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
4402 graph->Resize(num_variables);
4403 for (
const std::vector<Literal>& clique : cliques) {
4404 if (!graph->AddAtMostOne(clique)) {
4408 if (!graph->DetectEquivalences()) {
4411 graph->TransformIntoMaxCliques(
4412 &cliques, context_->
params().merge_at_most_one_work_limit());
4417 for (
int var = 0;
var < num_variables; ++
var) {
4418 const Literal l = Literal(BooleanVariable(
var),
true);
4419 if (graph->RepresentativeOf(l) != l) {
4420 const Literal r = graph->RepresentativeOf(l);
4422 var, r.IsPositive() ? r.Variable().value()
4427 int num_new_cliques = 0;
4428 for (
const std::vector<Literal>& clique : cliques) {
4429 if (clique.empty())
continue;
4432 for (
const Literal
literal : clique) {
4434 ct->mutable_at_most_one()->add_literals(
literal.Variable().value());
4436 ct->mutable_at_most_one()->add_literals(
4442 PresolveAtMostOne(
ct);
4445 if (num_new_cliques != num_old_cliques) {
4446 context_->
UpdateRuleStats(
"at_most_one: transformed into max clique.");
4450 LOG(
INFO) <<
"Merged " << num_old_cliques <<
" into " << num_new_cliques
4457 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
4460 if (ExploitEquivalenceRelations(c,
ct)) {
4465 if (PresolveEnforcementLiteral(
ct)) {
4470 switch (
ct->constraint_case()) {
4471 case ConstraintProto::ConstraintCase::kBoolOr:
4472 return PresolveBoolOr(
ct);
4473 case ConstraintProto::ConstraintCase::kBoolAnd:
4474 return PresolveBoolAnd(
ct);
4475 case ConstraintProto::ConstraintCase::kAtMostOne:
4476 return PresolveAtMostOne(
ct);
4477 case ConstraintProto::ConstraintCase::kExactlyOne:
4478 return PresolveExactlyOne(
ct);
4479 case ConstraintProto::ConstraintCase::kBoolXor:
4480 return PresolveBoolXor(
ct);
4481 case ConstraintProto::ConstraintCase::kIntMax:
4482 if (
ct->int_max().vars_size() == 2 &&
4484 return PresolveIntAbs(
ct);
4486 return PresolveIntMax(
ct);
4488 case ConstraintProto::ConstraintCase::kIntMin:
4489 return PresolveIntMin(
ct);
4490 case ConstraintProto::ConstraintCase::kLinMax:
4491 return PresolveLinMax(
ct);
4492 case ConstraintProto::ConstraintCase::kLinMin:
4493 return PresolveLinMin(
ct);
4494 case ConstraintProto::ConstraintCase::kIntProd:
4495 return PresolveIntProd(
ct);
4496 case ConstraintProto::ConstraintCase::kIntDiv:
4497 return PresolveIntDiv(
ct);
4498 case ConstraintProto::ConstraintCase::kLinear: {
4499 if (CanonicalizeLinear(
ct)) {
4502 if (PresolveSmallLinear(
ct)) {
4505 if (PropagateDomainsInLinear(c,
ct)) {
4508 if (PresolveSmallLinear(
ct)) {
4512 if (RemoveSingletonInLinear(
ct)) {
4517 if (PresolveSmallLinear(
ct)) {
4521 if (PresolveLinearOnBooleans(
ct)) {
4524 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
4525 const int old_num_enforcement_literals =
ct->enforcement_literal_size();
4526 ExtractEnforcementLiteralFromLinearConstraint(c,
ct);
4527 if (
ct->constraint_case() ==
4528 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
4532 if (
ct->enforcement_literal_size() > old_num_enforcement_literals &&
4533 PresolveSmallLinear(
ct)) {
4536 PresolveLinearEqualityModuloTwo(
ct);
4540 case ConstraintProto::ConstraintCase::kInterval:
4541 return PresolveInterval(c,
ct);
4542 case ConstraintProto::ConstraintCase::kElement:
4543 return PresolveElement(
ct);
4544 case ConstraintProto::ConstraintCase::kTable:
4545 return PresolveTable(
ct);
4546 case ConstraintProto::ConstraintCase::kAllDiff:
4547 return PresolveAllDiff(
ct);
4548 case ConstraintProto::ConstraintCase::kNoOverlap:
4549 return PresolveNoOverlap(
ct);
4550 case ConstraintProto::ConstraintCase::kCumulative:
4551 return PresolveCumulative(
ct);
4552 case ConstraintProto::ConstraintCase::kCircuit:
4553 return PresolveCircuit(
ct);
4554 case ConstraintProto::ConstraintCase::kRoutes:
4555 return PresolveRoutes(
ct);
4556 case ConstraintProto::ConstraintCase::kAutomaton:
4557 return PresolveAutomaton(
ct);
4558 case ConstraintProto::ConstraintCase::kReservoir:
4559 return PresolveReservoir(
ct);
4568 bool CpModelPresolver::ProcessSetPPCSubset(
4569 int c1,
int c2,
const std::vector<int>& c2_minus_c1,
4570 const std::vector<int>& original_constraint_index,
4571 std::vector<bool>* removed) {
4574 CHECK(!(*removed)[c1]);
4575 CHECK(!(*removed)[c2]);
4577 ConstraintProto* ct1 = context_->
working_model->mutable_constraints(
4578 original_constraint_index[c1]);
4579 ConstraintProto* ct2 = context_->
working_model->mutable_constraints(
4580 original_constraint_index[c2]);
4582 if ((ct1->constraint_case() == ConstraintProto::kBoolOr ||
4583 ct1->constraint_case() == ConstraintProto::kExactlyOne) &&
4584 (ct2->constraint_case() == ConstraintProto::kAtMostOne ||
4585 ct2->constraint_case() == ConstraintProto::kExactlyOne)) {
4590 for (
const int literal : c2_minus_c1) {
4596 if (ct2->constraint_case() != ConstraintProto::kExactlyOne) {
4597 ConstraintProto copy = *ct2;
4598 (*ct2->mutable_exactly_one()->mutable_literals()) =
4599 copy.at_most_one().literals();
4603 (*removed)[c1] =
true;
4609 if ((ct1->constraint_case() == ConstraintProto::kBoolOr ||
4610 ct1->constraint_case() == ConstraintProto::kExactlyOne) &&
4611 ct2->constraint_case() == ConstraintProto::kBoolOr) {
4614 (*removed)[c2] =
true;
4620 if (ct1->constraint_case() == ConstraintProto::kAtMostOne &&
4621 (ct2->constraint_case() == ConstraintProto::kAtMostOne ||
4622 ct2->constraint_case() == ConstraintProto::kExactlyOne)) {
4624 (*removed)[c1] =
true;
4640 bool CpModelPresolver::ProcessSetPPC() {
4641 const int num_constraints = context_->
working_model->constraints_size();
4645 std::vector<uint64> signatures;
4649 std::vector<std::vector<int>> constraint_literals;
4653 std::vector<std::vector<int>> literals_to_constraints;
4656 std::vector<bool> removed;
4660 std::vector<int> original_constraint_index;
4664 int num_setppc_constraints = 0;
4665 for (
int c = 0; c < num_constraints; ++c) {
4666 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
4667 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kBoolOr ||
4668 ct->constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne ||
4669 ct->constraint_case() == ConstraintProto::ConstraintCase::kExactlyOne) {
4678 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kBoolOr ||
4679 ct->constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne ||
4680 ct->constraint_case() == ConstraintProto::ConstraintCase::kExactlyOne) {
4681 constraint_literals.push_back(GetLiteralsFromSetPPCConstraint(*
ct));
4684 for (
const int literal : constraint_literals.back()) {
4686 signature |= (
int64{1} << (positive_literal % 64));
4688 if (positive_literal >= literals_to_constraints.size()) {
4689 literals_to_constraints.resize(positive_literal + 1);
4691 literals_to_constraints[positive_literal].push_back(
4692 num_setppc_constraints);
4694 signatures.push_back(signature);
4695 removed.push_back(
false);
4696 original_constraint_index.push_back(c);
4697 num_setppc_constraints++;
4700 VLOG(1) <<
"#setppc constraints: " << num_setppc_constraints;
4703 absl::flat_hash_set<std::pair<int, int>> compared_constraints;
4704 for (
const std::vector<int>& literal_to_constraints :
4705 literals_to_constraints) {
4706 for (
int index1 = 0; index1 < literal_to_constraints.size(); ++index1) {
4709 const int c1 = literal_to_constraints[index1];
4710 if (removed[c1])
continue;
4711 const std::vector<int>& c1_literals = constraint_literals[c1];
4713 for (
int index2 = index1 + 1; index2 < literal_to_constraints.size();
4715 const int c2 = literal_to_constraints[index2];
4716 if (removed[c2])
continue;
4717 if (removed[c1])
break;
4720 if (c1 == c2)
continue;
4724 std::pair<int, int>(c1, c2))) {
4727 compared_constraints.insert({c1, c2});
4731 if (compared_constraints.size() >= 50000)
return true;
4733 const bool smaller = (signatures[c1] & ~signatures[c2]) == 0;
4734 const bool larger = (signatures[c2] & ~signatures[c1]) == 0;
4735 if (!(smaller || larger))
continue;
4738 const std::vector<int>& c2_literals = constraint_literals[c2];
4742 std::vector<int> c1_minus_c2;
4744 std::vector<int> c2_minus_c1;
4747 if (c1_minus_c2.empty()) {
4748 if (!ProcessSetPPCSubset(c1, c2, c2_minus_c1,
4749 original_constraint_index, &removed)) {
4752 }
else if (c2_minus_c1.empty()) {
4753 if (!ProcessSetPPCSubset(c2, c1, c1_minus_c2,
4754 original_constraint_index, &removed)) {
4765 void CpModelPresolver::TryToSimplifyDomain(
int var) {
4773 if (r.representative !=
var)
return;
4788 if (domain.Size() == 2 && (domain.Min() != 0 || domain.Max() != 1)) {
4793 if (domain.NumIntervals() != domain.Size())
return;
4795 const int64 var_min = domain.Min();
4796 int64 gcd = domain[1].start - var_min;
4798 const ClosedInterval& i = domain[
index];
4800 const int64 shifted_value = i.start - var_min;
4804 if (gcd == 1)
break;
4806 if (gcd == 1)
return;
4810 std::vector<int64> scaled_values;
4812 const ClosedInterval& i = domain[
index];
4814 const int64 shifted_value = i.start - var_min;
4815 scaled_values.push_back(shifted_value / gcd);
4827 void CpModelPresolver::EncodeAllAffineRelations() {
4828 int64 num_added = 0;
4833 if (r.representative ==
var)
continue;
4840 if (!PresolveAffineRelationIfAny(
var))
break;
4847 auto* arg =
ct->mutable_linear();
4850 arg->add_vars(r.representative);
4851 arg->add_coeffs(-r.coeff);
4852 arg->add_domain(r.offset);
4853 arg->add_domain(r.offset);
4861 if (context_->
log_info() && num_added > 0) {
4862 LOG(
INFO) << num_added <<
" affine relations still in the model.";
4867 bool CpModelPresolver::PresolveAffineRelationIfAny(
int var) {
4871 if (r.representative ==
var)
return true;
4890 auto* arg =
ct->mutable_linear();
4893 arg->add_vars(r.representative);
4894 arg->add_coeffs(-r.coeff);
4895 arg->add_domain(r.offset);
4896 arg->add_domain(r.offset);
4902 void CpModelPresolver::PresolveToFixPoint() {
4906 const int64 max_num_operations =
4907 context_->
params().cp_model_max_num_presolve_operations() > 0
4908 ? context_->
params().cp_model_max_num_presolve_operations()
4914 absl::flat_hash_set<std::pair<int, int>> var_constraint_pair_already_called;
4919 std::vector<bool> in_queue(context_->
working_model->constraints_size(),
4921 std::deque<int> queue;
4922 for (
int c = 0; c < in_queue.size(); ++c) {
4923 if (context_->
working_model->constraints(c).constraint_case() !=
4924 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
4934 if (context_->
params().permute_presolve_constraint_order()) {
4935 std::shuffle(queue.begin(), queue.end(), *context_->
random());
4937 std::sort(queue.begin(), queue.end(), [
this](
int a,
int b) {
4938 const int score_a = context_->ConstraintToVars(a).size();
4939 const int score_b = context_->ConstraintToVars(b).size();
4940 return score_a < score_b || (score_a == score_b && a < b);
4950 const int c = queue.front();
4951 in_queue[c] =
false;
4954 const int old_num_constraint =
4958 LOG(
INFO) <<
"Unsat after presolving constraint #" << c
4959 <<
" (warning, dump might be inconsistent): "
4960 << context_->
working_model->constraints(c).ShortDebugString();
4964 const int new_num_constraints =
4966 if (new_num_constraints > old_num_constraint) {
4968 in_queue.resize(new_num_constraints,
true);
4969 for (
int c = old_num_constraint; c < new_num_constraints; ++c) {
4986 const int current_num_variables = context_->
working_model->variables_size();
4987 for (
int v = 0; v < current_num_variables; ++v) {
4989 if (!PresolveAffineRelationIfAny(v))
return;
4994 TryToSimplifyDomain(v);
5003 in_queue.resize(context_->
working_model->constraints_size(),
false);
5008 if (c >= 0 && !in_queue[c]) {
5018 const int num_vars = context_->
working_model->variables_size();
5019 for (
int v = 0; v < num_vars; ++v) {
5021 if (constraints.size() != 1)
continue;
5022 const int c = *constraints.begin();
5023 if (c < 0)
continue;
5029 std::pair<int, int>(v, c))) {
5032 var_constraint_pair_already_called.insert({v, c});
5042 std::sort(queue.begin(), queue.end());
5056 VarDomination var_dom;
5057 DualBoundStrengthening dual_bound_strengthening;
5059 if (!dual_bound_strengthening.Strengthen(context_))
return;
5076 const int num_constraints = context_->
working_model->constraints_size();
5077 for (
int c = 0; c < num_constraints; ++c) {
5078 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
5079 switch (
ct->constraint_case()) {
5080 case ConstraintProto::ConstraintCase::kNoOverlap:
5082 if (PresolveNoOverlap(
ct)) {
5086 case ConstraintProto::ConstraintCase::kNoOverlap2D:
5090 case ConstraintProto::ConstraintCase::kCumulative:
5092 if (PresolveCumulative(
ct)) {
5096 case ConstraintProto::ConstraintCase::kBoolOr: {
5099 for (
const auto& pair :
5101 bool modified =
false;
5122 <<
" affine relations were detected.";
5124 <<
" variable equivalence relations were detected.";
5125 std::map<std::string, int> sorted_rules(
context->stats_by_rule_name.begin(),
5126 context->stats_by_rule_name.end());
5127 for (
const auto& entry : sorted_rules) {
5128 if (entry.second == 1) {
5129 LOG(
INFO) <<
"- rule '" << entry.first <<
"' was applied 1 time.";
5131 LOG(
INFO) <<
"- rule '" << entry.first <<
"' was applied " << entry.second
5142 std::vector<int>* postsolve_mapping) {
5148 std::vector<int>* postsolve_mapping)
5149 : postsolve_mapping_(postsolve_mapping), context_(
context) {
5152 context_->
params().keep_all_feasible_solutions_in_presolve() ||
5153 context_->
params().enumerate_all_solutions() ||
5154 context_->
params().fill_tightened_domains_in_response() ||
5155 !context_->
params().cp_model_presolve();
5158 for (
const auto& decision_strategy :
5160 *(context_->
mapping_model->add_search_strategy()) = decision_strategy;
5195 if (!context_->
params().cp_model_presolve()) {
5207 for (
int c = 0; c < context_->
working_model->constraints_size(); ++c) {
5208 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
5209 PresolveEnforcementLiteral(
ct);
5210 switch (
ct->constraint_case()) {
5211 case ConstraintProto::ConstraintCase::kBoolOr:
5214 case ConstraintProto::ConstraintCase::kBoolAnd:
5215 PresolveBoolAnd(
ct);
5217 case ConstraintProto::ConstraintCase::kAtMostOne:
5218 PresolveAtMostOne(
ct);
5220 case ConstraintProto::ConstraintCase::kExactlyOne:
5221 PresolveExactlyOne(
ct);
5223 case ConstraintProto::ConstraintCase::kLinear:
5224 CanonicalizeLinear(
ct);
5236 for (
int iter = 0; iter < context_->
params().max_presolve_iterations();
5241 int old_num_non_empty_constraints = 0;
5242 for (
int c = 0; c < context_->
working_model->constraints_size(); ++c) {
5245 if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET)
continue;
5246 old_num_non_empty_constraints++;
5253 PresolveToFixPoint();
5260 if (context_->
params().cp_model_probing_level() > 0) {
5263 PresolveToFixPoint();
5270 if (context_->
params().cp_model_use_sat_presolve()) {
5272 PresolvePureSatPart();
5285 const int old_size = context_->
working_model->constraints_size();
5286 for (
int c = 0; c < old_size; ++c) {
5287 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
5288 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
5291 ExtractAtMostOneFromLinear(
ct);
5296 if (iter == 0) TransformIntoMaxCliques();
5313 PresolveToFixPoint();
5319 old_num_non_empty_constraints)) {
5326 MergeNoOverlapConstraints();
5336 EncodeAllAffineRelations();
5343 const std::vector<int> duplicates =
5345 if (!duplicates.empty()) {
5346 for (
const int c : duplicates) {
5349 if (type == ConstraintProto::ConstraintCase::kInterval) {
5366 context_->
working_model->add_constraints()->mutable_bool_or();
5378 absl::flat_hash_set<int> used_variables;
5379 for (DecisionStrategyProto& strategy :
5381 DecisionStrategyProto copy = strategy;
5382 strategy.clear_variables();
5383 for (
const int ref : copy.variables()) {
5392 used_variables.insert(
var);
5400 strategy.add_variables(rep);
5401 if (strategy.variable_selection_strategy() !=
5402 DecisionStrategyProto::CHOOSE_FIRST) {
5403 DecisionStrategyProto::AffineTransformation* t =
5404 strategy.add_transformations();
5407 t->set_positive_coeff(std::abs(r.
coeff));
5415 strategy.add_variables(ref);
5421 for (
int i = 0; i < context_->
working_model->variables_size(); ++i) {
5432 postsolve_mapping_->clear();
5433 std::vector<int> mapping(context_->
working_model->variables_size(), -1);
5434 for (
int i = 0; i < context_->
working_model->variables_size(); ++i) {
5439 mapping[i] = postsolve_mapping_->size();
5440 postsolve_mapping_->push_back(i);
5443 if (context_->
params().permute_variable_randomly()) {
5444 std::shuffle(postsolve_mapping_->begin(), postsolve_mapping_->end(),
5446 for (
int i = 0; i < postsolve_mapping_->size(); ++i) {
5447 mapping[(*postsolve_mapping_)[i]] = i;
5472 if (!error.empty()) {
5474 LOG(
INFO) <<
"Error while validating postsolved model: " << error;
5481 if (!error.empty()) {
5483 LOG(
INFO) <<
"Error while validating mapping_model model: " << error;
5497 auto mapping_function = [&mapping](
int* ref) {
5502 for (ConstraintProto& ct_ref : *
proto->mutable_constraints()) {
5508 if (
proto->has_objective()) {
5509 for (
int& mutable_ref : *
proto->mutable_objective()->mutable_vars()) {
5510 mapping_function(&mutable_ref);
5515 for (
int& mutable_ref : *
proto->mutable_assumptions()) {
5516 mapping_function(&mutable_ref);
5521 for (DecisionStrategyProto& strategy : *
proto->mutable_search_strategy()) {
5522 DecisionStrategyProto copy = strategy;
5523 strategy.clear_variables();
5524 for (
const int ref : copy.variables()) {
5530 strategy.clear_transformations();
5531 for (
const auto& transform : copy.transformations()) {
5532 const int ref = transform.var();
5535 auto* new_transform = strategy.add_transformations();
5536 *new_transform = transform;
5543 if (
proto->has_solution_hint()) {
5544 auto* mutable_hint =
proto->mutable_solution_hint();
5546 for (
int i = 0; i < mutable_hint->vars_size(); ++i) {
5547 const int old_ref = mutable_hint->vars(i);
5548 const int64 old_value = mutable_hint->values(i);
5556 const int image = mapping[
var];
5558 mutable_hint->set_vars(new_size, image);
5559 mutable_hint->set_values(new_size,
value);
5564 mutable_hint->mutable_vars()->Truncate(new_size);
5565 mutable_hint->mutable_values()->Truncate(new_size);
5567 proto->clear_solution_hint();
5572 std::vector<IntegerVariableProto> new_variables;
5573 for (
int i = 0; i < mapping.size(); ++i) {
5574 const int image = mapping[i];
5575 if (image < 0)
continue;
5576 if (image >= new_variables.size()) {
5577 new_variables.resize(image + 1, IntegerVariableProto());
5579 new_variables[image].Swap(
proto->mutable_variables(i));
5581 proto->clear_variables();
5582 for (IntegerVariableProto& proto_ref : new_variables) {
5583 proto->add_variables()->Swap(&proto_ref);
5587 for (
const IntegerVariableProto& v :
proto->variables()) {
5593 std::vector<int> result;
5596 ConstraintProto copy;
5597 absl::flat_hash_map<int64, int> equiv_constraints;
5600 const int num_constraints =
model_proto.constraints().size();
5601 for (
int c = 0; c < num_constraints; ++c) {
5602 if (
model_proto.constraints(c).constraint_case() ==
5603 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
5612 s = copy.SerializeAsString();
5614 const int64 hash = std::hash<std::string>()(s);
5615 const auto insert = equiv_constraints.insert({
hash, c});
5616 if (!insert.second) {
5618 const int other_c_with_same_hash = insert.first->second;
5619 copy =
model_proto.constraints(other_c_with_same_hash);
5621 if (s == copy.SerializeAsString()) {
5622 result.push_back(c);
#define DCHECK_NE(val1, val2)
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define CHECK_GT(val1, val2)
#define DCHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define CHECK_LE(val1, val2)
#define DCHECK_EQ(val1, val2)
#define VLOG(verboselevel)
bool IsIncludedIn(const Domain &domain) const
Returns true iff D is included in the given domain.
Domain MultiplicationBy(int64 coeff, bool *exact=nullptr) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e * coeff}.
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
int64 Size() const
Returns the number of elements in the domain.
Domain InverseMultiplicationBy(const int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
Domain AdditionWith(const Domain &domain) const
Returns {x ∈ Int64, ∃ a ∈ D, ∃ b ∈ domain, x = a + b}.
ClosedInterval front() const
Domain UnionWith(const Domain &domain) const
Returns the union of D and domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
Domain RelaxIfTooComplex() const
If NumIntervals() is too large, this return a superset of the domain.
Domain DivisionBy(int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e / coeff}.
static int64 GCD64(int64 x, int64 y)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
void Set(IntegerType index)
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
void RemoveEmptyConstraints()
CpModelPresolver(PresolveContext *context, std::vector< int > *postsolve_mapping)
bool PresolveOneConstraint(int c)
std::vector< std::pair< int, Domain > > ProcessClause(absl::Span< const int > clause)
void MarkProcessingAsDoneForNow()
int NumDeductions() const
void AddDeduction(int literal_ref, int var, Domain domain)
bool StoreAbsRelation(int target_ref, int ref)
SparseBitset< int64 > modified_domains
bool ConstraintVariableUsageIsConsistent()
int64 num_presolve_operations
bool ModelIsUnsat() const
bool VariableIsOnlyUsedInEncoding(int ref) const
ABSL_MUST_USE_RESULT bool IntersectDomainWith(int ref, const Domain &domain, bool *domain_modified=nullptr)
std::vector< absl::flat_hash_set< int > > var_to_lb_only_constraints
bool ConstraintVariableGraphIsUpToDate() const
int GetOrCreateVarValueEncoding(int ref, int64 value)
bool DomainContains(int ref, int64 value) const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value)
const Domain & ObjectiveDomain() const
bool DomainOfVarIsIncludedIn(int var, const Domain &domain)
bool VariableWithCostIsUniqueAndRemovable(int ref) const
void WriteObjectiveToProto() const
int GetLiteralRepresentative(int ref) const
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value)
std::vector< int > tmp_literals
int64 MaxOf(int ref) const
std::vector< absl::flat_hash_set< int > > var_to_ub_only_constraints
bool ObjectiveDomainIsConstraining() const
CpModelProto * mapping_model
const std::vector< int > & ConstraintToVars(int c) const
void UpdateNewConstraintsVariableUsage()
bool VariableIsUniqueAndRemovable(int ref) const
void RemoveVariableFromAffineRelation(int var)
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(const std::string &message="")
bool PropagateAffineRelation(int ref)
Domain DomainOf(int ref) const
void InitializeNewDomains()
int GetVariableRepresentative(int ref) const
int NewIntVar(const Domain &domain)
void MarkVariableAsRemoved(int ref)
DomainDeductions deductions
std::vector< Domain > tmp_left_domains
bool DomainIsEmpty(int ref) const
void CanonicalizeDomainOfSizeTwo(int var)
bool LiteralIsTrue(int lit) const
void StoreBooleanEqualityRelation(int ref_a, int ref_b)
int IntervalUsage(int c) const
CpModelProto * working_model
bool SubstituteVariableInObjective(int var_in_equality, int64 coeff_in_equality, const ConstraintProto &equality, std::vector< int > *new_vars_in_objective=nullptr)
int GetOrCreateConstantVar(int64 cst)
bool LiteralIsFalse(int lit) const
const absl::flat_hash_map< int, int64 > & ObjectiveMap() const
void UpdateRuleStats(const std::string &name, int num_times=1)
ABSL_MUST_USE_RESULT bool CanonicalizeObjective()
const SatParameters & params() const
void RemoveAllVariablesFromAffineRelationConstraint()
AffineRelation::Relation GetAffineRelation(int ref) const
bool VariableIsNotUsedAnymore(int ref) const
void UpdateConstraintVariableUsage(int c)
bool keep_all_feasible_solutions
bool IsFixed(int ref) const
std::vector< Domain > tmp_term_domains
const absl::flat_hash_set< int > & VarToConstraints(int var) const
ModelRandomGenerator * random()
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
int64 MinOf(int ref) const
absl::flat_hash_set< int > tmp_literal_set
void ReadObjectiveFromProto()
bool CanBeUsedAsLiteral(int ref) const
void RegisterVariablesUsedInAssumptions()
void ExploitFixedDomain(int var)
bool GetAbsRelation(int target_ref, int *ref)
bool StoreAffineRelation(int ref_x, int ref_y, int64 coeff, int64 offset)
CpModelProto const * model_proto
SharedTimeLimit * time_limit
GurobiMPCallbackContext * context
static const int64 kint64max
static const int32 kint32min
static const int64 kint64min
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
void STLSetDifference(const In1 &a, const In2 &b, Out *out, Compare compare)
bool ContainsKey(const Collection &collection, const Key &key)
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
bool DetectAndExploitSymmetriesInPresolve(PresolveContext *context)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
bool RefIsPositive(int ref)
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
const LiteralIndex kNoLiteralIndex(-1)
bool HasEnforcementLiteral(const ConstraintProto &ct)
void ExpandCpModel(PresolveContext *context)
constexpr int kAffineRelationConstraint
bool PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void SubstituteVariable(int var, int64 var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
void DetectDominanceRelations(const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
int ReindexArcs(IntContainer *tails, IntContainer *heads)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
std::vector< int > FindDuplicateConstraints(const CpModelProto &model_proto)
void LogInfoFromContext(const PresolveContext *context)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
constexpr int kObjectiveConstraint
bool ExploitDominanceRelations(const VarDomination &var_domination, PresolveContext *context)
void ApplyVariableMapping(const std::vector< int > &mapping, const PresolveContext &context)
std::string ValidateCpModel(const CpModelProto &model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...