31#include "absl/base/attributes.h"
32#include "absl/container/flat_hash_map.h"
33#include "absl/container/flat_hash_set.h"
34#include "absl/hash/hash.h"
35#include "absl/random/random.h"
36#include "absl/strings/str_join.h"
63bool CpModelPresolver::RemoveConstraint(ConstraintProto*
ct) {
76 int new_num_constraints = 0;
77 const int old_num_non_empty_constraints =
79 for (
int c = 0; c < old_num_non_empty_constraints; ++c) {
81 if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET)
continue;
82 if (type == ConstraintProto::ConstraintCase::kDummyConstraint)
continue;
83 if (type == ConstraintProto::ConstraintCase::kInterval) {
84 interval_mapping[c] = new_num_constraints;
90 new_num_constraints, old_num_non_empty_constraints - new_num_constraints);
94 [&interval_mapping](
int* ref) {
95 *ref = interval_mapping[*ref];
107 const int old_size =
ct->enforcement_literal().size();
108 for (
const int literal :
ct->enforcement_literal()) {
117 return RemoveConstraint(
ct);
124 return RemoveConstraint(
ct);
131 const int64_t obj_coeff =
135 context_->
UpdateRuleStats(
"enforcement literal with unique direction");
137 return RemoveConstraint(
ct);
141 ct->set_enforcement_literal(new_size++,
literal);
143 ct->mutable_enforcement_literal()->Truncate(new_size);
144 return new_size != old_size;
147bool CpModelPresolver::PresolveBoolXor(ConstraintProto*
ct) {
152 bool changed =
false;
153 int num_true_literals = 0;
155 for (
const int literal :
ct->bool_xor().literals()) {
176 ct->mutable_bool_xor()->set_literals(new_size++,
literal);
180 if (num_true_literals % 2 == 0) {
184 return RemoveConstraint(
ct);
186 }
else if (new_size == 1) {
187 if (num_true_literals % 2 == 0) {
190 "bool_xor: cannot fix last literal");
195 "bool_xor: cannot fix last literal");
199 return RemoveConstraint(
ct);
200 }
else if (new_size == 2) {
201 const int a =
ct->bool_xor().literals(0);
202 const int b =
ct->bool_xor().literals(1);
204 if (num_true_literals % 2 == 0) {
208 return RemoveConstraint(
ct);
212 if (num_true_literals % 2 == 1) {
216 return RemoveConstraint(
ct);
219 if (num_true_literals % 2 == 0) {
226 return RemoveConstraint(
ct);
229 if (num_true_literals % 2 == 1) {
231 ct->mutable_bool_xor()->set_literals(new_size++, true_literal);
233 if (num_true_literals > 1) {
234 context_->
UpdateRuleStats(
"bool_xor: remove even number of true literals");
237 ct->mutable_bool_xor()->mutable_literals()->Truncate(new_size);
241bool CpModelPresolver::PresolveBoolOr(ConstraintProto*
ct) {
248 for (
const int literal :
ct->enforcement_literal()) {
251 ct->clear_enforcement_literal();
255 bool changed =
false;
258 for (
const int literal :
ct->bool_or().literals()) {
265 return RemoveConstraint(
ct);
273 return RemoveConstraint(
ct);
277 return RemoveConstraint(
ct);
296 return RemoveConstraint(
ct);
309 ct->mutable_bool_or()->mutable_literals()->Clear();
311 ct->mutable_bool_or()->add_literals(lit);
320ABSL_MUST_USE_RESULT
bool CpModelPresolver::MarkConstraintAsFalse(
321 ConstraintProto*
ct) {
324 ct->mutable_bool_or()->clear_literals();
325 for (
const int lit :
ct->enforcement_literal()) {
328 ct->clear_enforcement_literal();
336bool CpModelPresolver::PresolveBoolAnd(ConstraintProto*
ct) {
341 for (
const int literal :
ct->bool_and().literals()) {
344 return RemoveConstraint(
ct);
347 bool changed =
false;
349 for (
const int literal :
ct->bool_and().literals()) {
352 return MarkConstraintAsFalse(
ct);
372 ct->mutable_bool_and()->mutable_literals()->Clear();
374 ct->mutable_bool_and()->add_literals(lit);
383 if (
ct->enforcement_literal().size() == 1 &&
384 ct->bool_and().literals().size() == 1) {
385 const int enforcement =
ct->enforcement_literal(0);
395 ct->bool_and().literals(0));
403bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto*
ct) {
405 const std::string
name = is_at_most_one ?
"at_most_one: " :
"exactly_one: ";
406 auto* literals = is_at_most_one
407 ?
ct->mutable_at_most_one()->mutable_literals()
408 :
ct->mutable_exactly_one()->mutable_literals();
412 for (
const int literal : *literals) {
419 int num_positive = 0;
420 int num_negative = 0;
421 for (
const int other : *literals) {
442 return RemoveConstraint(
ct);
447 bool changed =
false;
448 bool transform_to_at_most_one =
false;
450 for (
const int literal : *literals) {
453 for (
const int other : *literals) {
458 return RemoveConstraint(
ct);
471 if (is_at_most_one && !is_removable &&
475 const int64_t
coeff = it->second;
482 if (is_at_most_one) {
489 is_at_most_one =
true;
490 transform_to_at_most_one =
true;
501 if (!is_at_most_one && !transform_to_at_most_one &&
506 if (transform_to_at_most_one) {
509 literals =
ct->mutable_at_most_one()->mutable_literals();
521bool CpModelPresolver::PresolveAtMostOne(ConstraintProto*
ct) {
525 const bool changed = PresolveAtMostOrExactlyOne(
ct);
529 const auto& literals =
ct->at_most_one().literals();
530 if (literals.empty()) {
532 return RemoveConstraint(
ct);
536 if (literals.size() == 1) {
538 return RemoveConstraint(
ct);
544bool CpModelPresolver::PresolveExactlyOne(ConstraintProto*
ct) {
547 const bool changed = PresolveAtMostOrExactlyOne(
ct);
551 const auto& literals =
ct->exactly_one().literals();
552 if (literals.empty()) {
557 if (literals.size() == 1) {
560 return RemoveConstraint(
ct);
564 if (literals.size() == 2) {
568 return RemoveConstraint(
ct);
574bool CpModelPresolver::CanonicalizeLinearArgument(
const ConstraintProto&
ct,
575 LinearArgumentProto*
proto) {
579 bool changed = CanonicalizeLinearExpression(
ct,
proto->mutable_target());
580 for (LinearExpressionProto& exp : *(
proto->mutable_exprs())) {
581 changed |= CanonicalizeLinearExpression(
ct, &exp);
586bool CpModelPresolver::PresolveLinMax(ConstraintProto*
ct) {
592 const LinearExpressionProto& target =
ct->lin_max().target();
594 int64_t infered_min = context_->
MinOf(target);
596 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
601 if (target.vars().empty()) {
602 if (!Domain(infered_min, infered_max).Contains(target.offset())) {
604 return MarkConstraintAsFalse(
ct);
607 if (target.vars().size() <= 1) {
609 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
610 rhs_domain = rhs_domain.UnionWith(
612 {infered_min, infered_max}));
614 bool reduced =
false;
625 const int64_t target_min = context_->
MinOf(target);
626 const int64_t target_max = context_->
MaxOf(target);
627 bool changed =
false;
634 bool has_greater_or_equal_to_target_min =
false;
636 int index_to_keep = -1;
637 for (
int i = 0; i <
ct->lin_max().exprs_size(); ++i) {
638 const LinearExpressionProto& expr =
ct->lin_max().exprs(i);
639 if (context_->
MinOf(expr) >= target_min) {
640 const int64_t expr_max = context_->
MaxOf(expr);
641 if (expr_max > max_at_index_to_keep) {
642 max_at_index_to_keep = expr_max;
645 has_greater_or_equal_to_target_min =
true;
650 for (
int i = 0; i <
ct->lin_max().exprs_size(); ++i) {
651 const LinearExpressionProto& expr =
ct->lin_max().exprs(i);
652 const int64_t expr_max = context_->
MaxOf(expr);
655 if (expr_max < target_min)
continue;
656 if (expr_max == target_min && has_greater_or_equal_to_target_min &&
657 i != index_to_keep) {
660 *
ct->mutable_lin_max()->mutable_exprs(new_size) = expr;
663 if (new_size < ct->lin_max().exprs_size()) {
665 ct->mutable_lin_max()->mutable_exprs()->DeleteSubrange(
666 new_size,
ct->lin_max().exprs_size() - new_size);
671 if (
ct->lin_max().exprs().empty()) {
673 return MarkConstraintAsFalse(
ct);
678 if (
ct->lin_max().exprs().size() == 1) {
682 auto* arg = new_ct->mutable_linear();
683 const LinearExpressionProto&
a =
ct->lin_max().target();
684 const LinearExpressionProto&
b =
ct->lin_max().exprs(0);
685 for (
int i = 0; i <
a.vars().size(); ++i) {
686 arg->add_vars(
a.vars(i));
687 arg->add_coeffs(
a.coeffs(i));
689 for (
int i = 0; i <
b.vars().size(); ++i) {
690 arg->add_vars(
b.vars(i));
691 arg->add_coeffs(-
b.coeffs(i));
693 arg->add_domain(
b.offset() -
a.offset());
694 arg->add_domain(
b.offset() -
a.offset());
696 return RemoveConstraint(
ct);
704 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
705 const int64_t value_min = context_->
MinOf(expr);
706 bool modified =
false;
714 const int64_t value_max = context_->
MaxOf(expr);
715 if (value_max > target_max) {
716 context_->
UpdateRuleStats(
"TODO lin_max: linear expression above max.");
720 if (abort)
return changed;
724 if (target_min == target_max) {
725 bool all_booleans =
true;
726 std::vector<int> literals;
727 const int64_t fixed_target = target_min;
728 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
729 const int64_t value_min = context_->
MinOf(expr);
730 const int64_t value_max = context_->
MaxOf(expr);
731 CHECK_LE(value_max, fixed_target) <<
"Presolved above";
732 if (value_max < fixed_target)
continue;
734 if (value_min == value_max && value_max == fixed_target) {
736 return RemoveConstraint(
ct);
742 all_booleans =
false;
746 if (literals.empty()) {
747 return MarkConstraintAsFalse(
ct);
752 for (
const int lit : literals) {
753 ct->mutable_bool_or()->add_literals(lit);
766 bool min_is_reachable =
false;
767 std::vector<int> min_literals;
768 std::vector<int> literals_above_min;
769 std::vector<int> max_literals;
771 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
772 const int64_t value_min = context_->
MinOf(expr);
773 const int64_t value_max = context_->
MaxOf(expr);
776 if (value_min > target_min) {
784 if (value_min == value_max) {
785 if (value_min == target_min) min_is_reachable =
true;
796 if (value_min == target_min) {
801 if (value_max == target_max) {
802 max_literals.push_back(ref);
803 literals_above_min.push_back(ref);
804 }
else if (value_max > target_min) {
805 literals_above_min.push_back(ref);
806 }
else if (value_max == target_min) {
807 min_literals.push_back(ref);
816 clause->mutable_bool_or();
817 for (
const int lit : max_literals) {
818 clause->mutable_bool_or()->add_literals(lit);
822 for (
const int lit : literals_above_min) {
826 if (!min_is_reachable) {
830 clause->mutable_bool_or();
831 for (
const int lit : min_literals) {
832 clause->mutable_bool_or()->add_literals(lit);
837 return RemoveConstraint(
ct);
845bool CpModelPresolver::PresolveIntAbs(ConstraintProto*
ct) {
848 const LinearExpressionProto& target_expr =
ct->lin_max().target();
849 const LinearExpressionProto& expr =
ct->lin_max().exprs(0);
855 const Domain new_target_domain =
856 expr_domain.
UnionWith(expr_domain.Negation())
858 bool target_domain_modified =
false;
860 &target_domain_modified)) {
863 if (expr_domain.IsFixed()) {
865 return RemoveConstraint(
ct);
867 if (target_domain_modified) {
868 context_->
UpdateRuleStats(
"int_abs: propagate domain from x to abs(x)");
874 const Domain target_domain =
877 const Domain new_expr_domain =
878 target_domain.
UnionWith(target_domain.Negation());
879 bool expr_domain_modified =
false;
881 &expr_domain_modified)) {
886 if (context_->
IsFixed(target_expr)) {
888 return RemoveConstraint(
ct);
890 if (expr_domain_modified) {
891 context_->
UpdateRuleStats(
"int_abs: propagate domain from abs(x) to x");
896 if (context_->
MinOf(expr) >= 0) {
900 auto* arg = new_ct->mutable_linear();
905 if (!CanonicalizeLinear(new_ct))
return false;
907 return RemoveConstraint(
ct);
910 if (context_->
MaxOf(expr) <= 0) {
914 auto* arg = new_ct->mutable_linear();
919 if (!CanonicalizeLinear(new_ct))
return false;
921 return RemoveConstraint(
ct);
933 return RemoveConstraint(
ct);
954bool CpModelPresolver::PresolveIntProd(ConstraintProto*
ct) {
959 int64_t constant_factor = 1;
961 bool changed =
false;
962 LinearArgumentProto*
proto =
ct->mutable_int_prod();
963 for (
int i = 0; i <
ct->int_prod().exprs().size(); ++i) {
964 LinearExpressionProto expr =
ct->int_prod().exprs(i);
971 const int64_t
coeff = expr.coeffs(0);
972 const int64_t offset = expr.offset();
975 static_cast<uint64_t
>(std::abs(offset)));
977 constant_factor =
CapProd(constant_factor, gcd);
978 expr.set_coeffs(0,
coeff / gcd);
979 expr.set_offset(offset / gcd);
982 *
proto->mutable_exprs(new_size++) = expr;
984 proto->mutable_exprs()->erase(
proto->mutable_exprs()->begin() + new_size,
985 proto->mutable_exprs()->end());
987 if (
ct->int_prod().exprs().empty()) {
989 Domain(constant_factor))) {
993 return RemoveConstraint(
ct);
996 if (constant_factor == 0) {
1001 return RemoveConstraint(
ct);
1012 constant_factor = 1;
1016 if (
ct->int_prod().exprs().size() == 1) {
1017 LinearConstraintProto*
const lin =
1023 -constant_factor, lin);
1025 context_->
UpdateRuleStats(
"int_prod: linearize product by constant.");
1026 return RemoveConstraint(
ct);
1029 if (constant_factor != 1) {
1034 const LinearExpressionProto old_target =
ct->int_prod().target();
1035 if (!context_->
IsFixed(old_target)) {
1036 const int ref = old_target.vars(0);
1037 const int64_t
coeff = old_target.coeffs(0);
1038 const int64_t offset = old_target.offset();
1049 if (context_->
IsFixed(old_target)) {
1050 const int64_t target_value = context_->
FixedValue(old_target);
1051 if (target_value % constant_factor != 0) {
1053 "int_prod: constant factor does not divide constant target");
1055 proto->clear_target();
1056 proto->mutable_target()->set_offset(target_value / constant_factor);
1058 "int_prod: divide product and fixed target by constant factor");
1061 const AffineRelation::Relation r =
1063 const absl::int128 temp_coeff =
1064 absl::int128(old_target.coeffs(0)) * absl::int128(r.coeff);
1065 CHECK_EQ(temp_coeff % absl::int128(constant_factor), 0);
1066 const absl::int128 temp_offset =
1067 absl::int128(old_target.coeffs(0)) * absl::int128(r.offset) +
1068 absl::int128(old_target.offset());
1069 CHECK_EQ(temp_offset % absl::int128(constant_factor), 0);
1070 const absl::int128 new_coeff = temp_coeff / absl::int128(constant_factor);
1071 const absl::int128 new_offset =
1072 temp_offset / absl::int128(constant_factor);
1085 "int_prod: overflow during simplification.");
1089 proto->mutable_target()->set_coeffs(0,
static_cast<int64_t
>(new_coeff));
1090 proto->mutable_target()->set_vars(0, r.representative);
1091 proto->mutable_target()->set_offset(
static_cast<int64_t
>(new_offset));
1092 context_->
UpdateRuleStats(
"int_prod: divide product by constant factor");
1099 bool is_square =
false;
1100 if (
ct->int_prod().exprs_size() == 2 &&
1102 ct->int_prod().exprs(1))) {
1107 for (
const LinearExpressionProto& expr :
ct->int_prod().exprs()) {
1112 bool domain_modified =
false;
1114 &domain_modified)) {
1117 if (domain_modified) {
1119 is_square ?
"int_square" :
"int_prod",
": reduced target domain."));
1124 const int64_t target_max = context_->
MaxOf(
ct->int_prod().target());
1127 bool expr_reduced =
false;
1129 {-sqrt_max, sqrt_max}, &expr_reduced)) {
1137 if (
ct->int_prod().exprs_size() == 2) {
1138 LinearExpressionProto
a =
ct->int_prod().exprs(0);
1139 LinearExpressionProto
b =
ct->int_prod().exprs(1);
1140 const LinearExpressionProto product =
ct->int_prod().target();
1147 context_->
UpdateRuleStats(
"int_square: fix variable to zero or one.");
1148 return RemoveConstraint(
ct);
1153 const LinearExpressionProto target_expr =
ct->int_prod().target();
1158 std::vector<int> literals;
1159 for (
const LinearExpressionProto& expr :
ct->int_prod().exprs()) {
1164 literals.push_back(lit);
1172 auto* arg = new_ct->mutable_bool_and();
1173 for (
const int lit : literals) {
1174 arg->add_literals(lit);
1181 for (
const int lit : literals) {
1186 return RemoveConstraint(
ct);
1189bool CpModelPresolver::PresolveIntDiv(ConstraintProto*
ct) {
1192 const LinearExpressionProto target =
ct->int_div().target();
1193 const LinearExpressionProto expr =
ct->int_div().exprs(0);
1194 const LinearExpressionProto div =
ct->int_div().exprs(1);
1201 return RemoveConstraint(
ct);
1207 return RemoveConstraint(
ct);
1211 if (!context_->
IsFixed(div))
return false;
1213 const int64_t divisor = context_->
FixedValue(div);
1215 LinearConstraintProto*
const lin =
1223 return RemoveConstraint(
ct);
1225 bool domain_modified =
false;
1228 &domain_modified)) {
1231 if (domain_modified) {
1233 "int_div: updated domain of target in target = X / cte");
1239 if (context_->
MinOf(target) >= 0 && context_->
MinOf(expr) >= 0 &&
1241 LinearConstraintProto*
const lin =
1244 lin->add_domain(divisor - 1);
1249 "int_div: linearize positive division with a constant divisor");
1250 return RemoveConstraint(
ct);
1258bool CpModelPresolver::PresolveIntMod(ConstraintProto*
ct) {
1261 const LinearExpressionProto target =
ct->int_mod().target();
1262 const LinearExpressionProto expr =
ct->int_mod().exprs(0);
1263 const LinearExpressionProto mod =
ct->int_mod().exprs(1);
1265 bool domain_changed =
false;
1274 if (domain_changed) {
1281bool CpModelPresolver::ExploitEquivalenceRelations(
int c, ConstraintProto*
ct) {
1282 bool changed =
false;
1287 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
1288 for (
int& ref : *
ct->mutable_enforcement_literal()) {
1300 bool work_to_do =
false;
1303 if (r.representative !=
var) {
1308 if (!work_to_do)
return false;
1312 [&changed,
this](
int* ref) {
1323 [&changed,
this](
int* ref) {
1334bool CpModelPresolver::DivideLinearByGcd(ConstraintProto*
ct) {
1339 const int num_vars =
ct->linear().vars().size();
1340 for (
int i = 0; i < num_vars; ++i) {
1341 const int64_t magnitude = std::abs(
ct->linear().coeffs(i));
1343 if (gcd == 1)
break;
1347 for (
int i = 0; i < num_vars; ++i) {
1348 ct->mutable_linear()->set_coeffs(i,
ct->linear().coeffs(i) / gcd);
1352 if (
ct->linear().domain_size() == 0) {
1353 return MarkConstraintAsFalse(
ct);
1359template <
typename ProtoWithVarsAndCoeffs>
1360bool CpModelPresolver::CanonicalizeLinearExpressionInternal(
1361 const ConstraintProto&
ct, ProtoWithVarsAndCoeffs*
proto, int64_t* offset) {
1367 int64_t sum_of_fixed_terms = 0;
1368 bool remapped =
false;
1369 const int old_size =
proto->vars().size();
1371 for (
int i = 0; i < old_size; ++i) {
1379 const int ref =
proto->vars(i);
1381 const int64_t
coeff =
1383 if (
coeff == 0)
continue;
1391 if (r.representative !=
var) {
1393 sum_of_fixed_terms +=
coeff * r.offset;
1396 new_var = r.representative;
1397 new_coeff =
coeff * r.coeff;
1402 bool removed =
false;
1403 for (
const int enf :
ct.enforcement_literal()) {
1407 sum_of_fixed_terms += new_coeff;
1416 context_->
UpdateRuleStats(
"linear: enforcement literal in expression");
1420 tmp_terms_.push_back({new_var, new_coeff});
1422 proto->clear_vars();
1423 proto->clear_coeffs();
1424 std::sort(tmp_terms_.begin(), tmp_terms_.end());
1425 int current_var = 0;
1426 int64_t current_coeff = 0;
1427 for (
const auto entry : tmp_terms_) {
1429 if (entry.first == current_var) {
1430 current_coeff += entry.second;
1432 if (current_coeff != 0) {
1433 proto->add_vars(current_var);
1434 proto->add_coeffs(current_coeff);
1436 current_var = entry.first;
1437 current_coeff = entry.second;
1440 if (current_coeff != 0) {
1441 proto->add_vars(current_var);
1442 proto->add_coeffs(current_coeff);
1447 if (
proto->vars().size() < old_size) {
1450 *offset = sum_of_fixed_terms;
1451 return remapped ||
proto->vars().size() < old_size;
1454bool CpModelPresolver::CanonicalizeLinearExpression(
1455 const ConstraintProto&
ct, LinearExpressionProto* exp) {
1457 const bool result = CanonicalizeLinearExpressionInternal(
ct, exp, &offset);
1458 exp->set_offset(exp->offset() + offset);
1462bool CpModelPresolver::CanonicalizeLinear(ConstraintProto*
ct) {
1463 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1468 if (
ct->linear().domain().empty()) {
1470 return MarkConstraintAsFalse(
ct);
1475 CanonicalizeLinearExpressionInternal(*
ct,
ct->mutable_linear(), &offset);
1479 ct->mutable_linear());
1481 changed |= DivideLinearByGcd(
ct);
1485bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto*
ct) {
1486 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
1491 std::set<int> index_to_erase;
1492 const int num_vars =
ct->linear().vars().size();
1498 for (
int i = 0; i < num_vars; ++i) {
1499 const int var =
ct->linear().vars(i);
1500 const int64_t
coeff =
ct->linear().coeffs(i);
1504 const auto term_domain =
1506 if (!exact)
continue;
1510 if (new_rhs.NumIntervals() > 100)
continue;
1517 index_to_erase.insert(i);
1524 if (index_to_erase.empty()) {
1527 if (!
ct->enforcement_literal().empty())
return false;
1531 if (rhs.Min() != rhs.Max())
return false;
1533 for (
int i = 0; i < num_vars; ++i) {
1534 const int var =
ct->linear().vars(i);
1535 const int64_t
coeff =
ct->linear().coeffs(i);
1556 if (objective_coeff %
coeff != 0)
continue;
1560 const auto term_domain =
1562 if (!exact)
continue;
1564 if (new_rhs.NumIntervals() > 100)
continue;
1572 objective_coeff))) {
1596 LOG(
WARNING) <<
"This was not supposed to happen and the presolve "
1597 "could be improved.";
1605 context_->
UpdateRuleStats(
"linear: singleton column define objective.");
1608 return RemoveConstraint(
ct);
1620 "linear: singleton column in equality and in objective.");
1622 index_to_erase.insert(i);
1626 if (index_to_erase.empty())
return false;
1637 if (!
ct->enforcement_literal().empty()) {
1638 for (
const int i : index_to_erase) {
1639 const int var =
ct->linear().vars(i);
1654 for (
int i = 0; i < num_vars; ++i) {
1655 if (index_to_erase.count(i)) {
1659 ct->mutable_linear()->set_coeffs(new_size,
ct->linear().coeffs(i));
1660 ct->mutable_linear()->set_vars(new_size,
ct->linear().vars(i));
1663 ct->mutable_linear()->mutable_vars()->Truncate(new_size);
1664 ct->mutable_linear()->mutable_coeffs()->Truncate(new_size);
1666 DivideLinearByGcd(
ct);
1672bool CpModelPresolver::AddVarAffineRepresentativeFromLinearEquality(
1673 int target_index, ConstraintProto*
ct) {
1675 const int num_variables =
ct->linear().vars().size();
1676 for (
int i = 0; i < num_variables; ++i) {
1677 if (i == target_index)
continue;
1678 const int64_t magnitude = std::abs(
ct->linear().coeffs(i));
1680 if (gcd == 1)
return false;
1686 const int ref =
ct->linear().vars(target_index);
1687 const int64_t
coeff =
ct->linear().coeffs(target_index);
1688 const int64_t rhs =
ct->linear().domain(0);
1692 if (
coeff % gcd == 0)
return false;
1700 return CanonicalizeLinear(
ct);
1710bool CpModelPresolver::PresolveLinearEqualityWithModulo(ConstraintProto*
ct) {
1713 if (
ct->linear().domain().size() != 2)
return false;
1714 if (
ct->linear().domain(0) !=
ct->linear().domain(1))
return false;
1715 if (!
ct->enforcement_literal().empty())
return false;
1717 const int num_variables =
ct->linear().vars().size();
1718 if (num_variables < 2)
return false;
1720 std::vector<int> mod2_indices;
1721 std::vector<int> mod3_indices;
1722 std::vector<int> mod5_indices;
1724 int64_t min_magnitude;
1725 int num_smallest = 0;
1727 for (
int i = 0; i < num_variables; ++i) {
1728 const int64_t magnitude = std::abs(
ct->linear().coeffs(i));
1729 if (num_smallest == 0 || magnitude < min_magnitude) {
1730 min_magnitude = magnitude;
1733 }
else if (magnitude == min_magnitude) {
1737 if (magnitude % 2 != 0) mod2_indices.push_back(i);
1738 if (magnitude % 3 != 0) mod3_indices.push_back(i);
1739 if (magnitude % 5 != 0) mod5_indices.push_back(i);
1742 if (mod2_indices.size() == 2) {
1744 std::vector<int> literals;
1745 for (
const int i : mod2_indices) {
1746 const int ref =
ct->linear().vars(i);
1751 literals.push_back(ref);
1754 const int64_t rhs = std::abs(
ct->linear().domain(0));
1755 context_->
UpdateRuleStats(
"linear: only two odd Booleans in equality");
1767 if (mod2_indices.size() == 1) {
1768 return AddVarAffineRepresentativeFromLinearEquality(mod2_indices[0],
ct);
1770 if (mod3_indices.size() == 1) {
1771 return AddVarAffineRepresentativeFromLinearEquality(mod3_indices[0],
ct);
1773 if (mod5_indices.size() == 1) {
1774 return AddVarAffineRepresentativeFromLinearEquality(mod5_indices[0],
ct);
1776 if (num_smallest == 1) {
1777 return AddVarAffineRepresentativeFromLinearEquality(smallest_index,
ct);
1783bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto*
ct) {
1789 ?
ct->linear().coeffs(0)
1790 : -
ct->linear().coeffs(0);
1795 rhs.InverseMultiplicationBy(
coeff))) {
1798 return RemoveConstraint(
ct);
1804 const bool zero_ok = rhs.Contains(0);
1805 const bool one_ok = rhs.Contains(
ct->linear().coeffs(0));
1807 if (!zero_ok && !one_ok) {
1808 return MarkConstraintAsFalse(
ct);
1810 if (zero_ok && one_ok) {
1811 return RemoveConstraint(
ct);
1813 const int ref =
ct->linear().vars(0);
1817 ct->mutable_bool_and()->add_literals(ref);
1828 if (
ct->linear().coeffs(0) == 1 &&
1832 context_->
UpdateRuleStats(
"linear1: remove abs from abs(x) in domain");
1833 const Domain implied_abs_target_domain =
1836 .IntersectionWith(context_->
DomainOf(
ct->linear().vars(0)));
1838 if (implied_abs_target_domain.IsEmpty()) {
1839 return MarkConstraintAsFalse(
ct);
1842 const Domain new_abs_var_domain =
1843 implied_abs_target_domain
1844 .UnionWith(implied_abs_target_domain.Negation())
1845 .IntersectionWith(context_->
DomainOf(abs_arg));
1847 if (new_abs_var_domain.IsEmpty()) {
1848 return MarkConstraintAsFalse(
ct);
1854 ct->mutable_linear()->add_coeffs(1);
1860 if (
ct->enforcement_literal_size() != 1 ||
1861 (
ct->linear().coeffs(0) != 1 &&
ct->linear().coeffs(0) == -1)) {
1869 const int literal =
ct->enforcement_literal(0);
1870 const LinearConstraintProto& linear =
ct->linear();
1871 const int ref = linear.vars(0);
1873 const int64_t
coeff =
1876 if (linear.domain_size() == 2 && linear.domain(0) == linear.domain(1)) {
1878 : -linear.domain(0) *
coeff;
1889 if (complement.Size() != 1)
return false;
1891 : -complement.Min() *
coeff;
1905bool CpModelPresolver::PresolveLinearOfSizeTwo(ConstraintProto*
ct) {
1908 const LinearConstraintProto& arg =
ct->linear();
1909 const int var1 = arg.vars(0);
1910 const int var2 = arg.vars(1);
1911 const int64_t coeff1 = arg.coeffs(0);
1912 const int64_t coeff2 = arg.coeffs(1);
1923 const bool is_equality =
1924 arg.domain_size() == 2 && arg.domain(0) == arg.domain(1);
1927 int64_t value_on_true,
coeff;
1930 value_on_true = coeff1;
1935 value_on_true = coeff2;
1943 const Domain rhs_if_true =
1944 rhs.AdditionWith(Domain(-value_on_true)).InverseMultiplicationBy(
coeff);
1945 const Domain rhs_if_false = rhs.InverseMultiplicationBy(
coeff);
1946 const bool implied_false =
1948 const bool implied_true =
1950 if (implied_true && implied_false) {
1952 return MarkConstraintAsFalse(
ct);
1953 }
else if (implied_true) {
1954 context_->
UpdateRuleStats(
"linear2: Boolean with one feasible value.");
1959 new_ct->mutable_bool_and()->add_literals(lit);
1963 ct->mutable_linear()->Clear();
1964 ct->mutable_linear()->add_vars(
var);
1965 ct->mutable_linear()->add_coeffs(1);
1967 return PresolveLinearOfSizeOne(
ct) ||
true;
1968 }
else if (implied_false) {
1969 context_->
UpdateRuleStats(
"linear2: Boolean with one feasible value.");
1974 new_ct->mutable_bool_and()->add_literals(
NegatedRef(lit));
1978 ct->mutable_linear()->Clear();
1979 ct->mutable_linear()->add_vars(
var);
1980 ct->mutable_linear()->add_coeffs(1);
1982 return PresolveLinearOfSizeOne(
ct) ||
true;
1994 const int64_t rhs = arg.domain(0);
1995 if (
ct->enforcement_literal().empty()) {
2003 }
else if (coeff2 == 1) {
2005 }
else if (coeff1 == -1) {
2007 }
else if (coeff2 == -1) {
2020 if (added)
return RemoveConstraint(
ct);
2030 "linear2: implied ax + by = cte has no solutions");
2031 return MarkConstraintAsFalse(
ct);
2033 const Domain reduced_domain =
2039 .InverseMultiplicationBy(-
a));
2041 if (reduced_domain.IsEmpty()) {
2043 "linear2: implied ax + by = cte has no solutions");
2044 return MarkConstraintAsFalse(
ct);
2047 if (reduced_domain.Size() == 1) {
2048 const int64_t z = reduced_domain.FixedValue();
2049 const int64_t value1 = x0 +
b * z;
2050 const int64_t value2 = y0 -
a * z;
2054 DCHECK_EQ(coeff1 * value1 + coeff2 * value2, rhs);
2058 imply1->mutable_linear()->add_vars(var1);
2059 imply1->mutable_linear()->add_coeffs(1);
2060 imply1->mutable_linear()->add_domain(value1);
2061 imply1->mutable_linear()->add_domain(value1);
2065 imply2->mutable_linear()->add_vars(var2);
2066 imply2->mutable_linear()->add_coeffs(1);
2067 imply2->mutable_linear()->add_domain(value2);
2068 imply2->mutable_linear()->add_domain(value2);
2070 "linear2: implied ax + by = cte has only one solution");
2072 return RemoveConstraint(
ct);
2079bool CpModelPresolver::PresolveSmallLinear(ConstraintProto*
ct) {
2083 if (
ct->linear().vars().empty()) {
2086 if (rhs.Contains(0)) {
2087 return RemoveConstraint(
ct);
2089 return MarkConstraintAsFalse(
ct);
2091 }
else if (
ct->linear().vars().size() == 1) {
2092 return PresolveLinearOfSizeOne(
ct);
2093 }
else if (
ct->linear().vars().size() == 2) {
2094 return PresolveLinearOfSizeTwo(
ct);
2103bool IsLeConstraint(
const Domain& domain,
const Domain& all_values) {
2107 .IsIncludedIn(domain);
2111bool IsGeConstraint(
const Domain& domain,
const Domain& all_values) {
2115 .IsIncludedIn(domain);
2121bool RhsCanBeFixedToMin(int64_t
coeff,
const Domain& var_domain,
2122 const Domain& terms,
const Domain& rhs) {
2123 if (var_domain.NumIntervals() != 1)
return false;
2124 if (std::abs(
coeff) != 1)
return false;
2132 if (
coeff == 1 && terms.Max() + var_domain.Min() <= rhs.Min()) {
2135 if (
coeff == -1 && terms.Max() - var_domain.Max() <= rhs.Min()) {
2141bool RhsCanBeFixedToMax(int64_t
coeff,
const Domain& var_domain,
2142 const Domain& terms,
const Domain& rhs) {
2143 if (var_domain.NumIntervals() != 1)
return false;
2144 if (std::abs(
coeff) != 1)
return false;
2146 if (
coeff == 1 && terms.Min() + var_domain.Max() >= rhs.Max()) {
2149 if (
coeff == -1 && terms.Min() - var_domain.Min() >= rhs.Max()) {
2156void TakeIntersectionWith(
const absl::flat_hash_set<int>& current,
2157 absl::flat_hash_set<int>* to_clear) {
2158 std::vector<int> new_set;
2159 for (
const int c : *to_clear) {
2160 if (current.contains(c)) new_set.push_back(c);
2163 for (
const int c : new_set) to_clear->insert(c);
2168bool CpModelPresolver::DetectAndProcessOneSidedLinearConstraint(
2169 int c, ConstraintProto*
ct) {
2170 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
2178 Domain implied_rhs(0);
2179 const int num_vars =
ct->linear().vars().size();
2180 for (
int i = 0; i < num_vars; ++i) {
2181 const int ref =
ct->linear().vars(i);
2182 const int64_t
coeff =
ct->linear().coeffs(i);
2186 .RelaxIfTooComplex();
2191 if (implied_rhs.IsIncludedIn(old_rhs)) {
2193 return RemoveConstraint(
ct);
2197 const Domain rhs = old_rhs.SimplifyUsingImpliedDomain(implied_rhs);
2198 if (rhs.IsEmpty()) {
2200 return MarkConstraintAsFalse(
ct);
2202 if (rhs != old_rhs) {
2210 const bool is_le_constraint = IsLeConstraint(rhs, implied_rhs);
2211 const bool is_ge_constraint = IsGeConstraint(rhs, implied_rhs);
2212 if (!is_le_constraint && !is_ge_constraint)
return false;
2213 CHECK_NE(is_le_constraint, is_ge_constraint);
2220 absl::flat_hash_set<int> enforcement_set;
2222 for (
const int ref :
ct->enforcement_literal()) {
2223 enforcement_set.insert(ref);
2227 bool recanonicalize =
false;
2228 for (
int i = 0; i < num_vars; ++i) {
2229 const int var =
ct->linear().vars(i);
2230 const int64_t var_coeff =
ct->linear().coeffs(i);
2233 if ((var_coeff > 0) == is_ge_constraint) {
2247 const int64_t obj_coeff =
2256 if (obj_coeff <= 0 &&
2265 recanonicalize =
true;
2270 if (obj_coeff >= 0 &&
2279 recanonicalize =
true;
2285 if (recanonicalize)
return CanonicalizeLinear(
ct);
2289bool CpModelPresolver::PropagateDomainsInLinear(
int ct_index,
2290 ConstraintProto*
ct) {
2291 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
2299 const int num_vars =
ct->linear().vars_size();
2300 term_domains.resize(num_vars + 1);
2301 left_domains.resize(num_vars + 1);
2302 left_domains[0] = Domain(0);
2303 for (
int i = 0; i < num_vars; ++i) {
2304 const int var =
ct->linear().vars(i);
2305 const int64_t
coeff =
ct->linear().coeffs(i);
2308 left_domains[i + 1] =
2311 const Domain& implied_rhs = left_domains[num_vars];
2315 if (implied_rhs.IsIncludedIn(old_rhs)) {
2317 return RemoveConstraint(
ct);
2321 Domain rhs = old_rhs.SimplifyUsingImpliedDomain(implied_rhs);
2322 if (rhs.IsEmpty()) {
2324 return MarkConstraintAsFalse(
ct);
2326 if (rhs != old_rhs) {
2332 if (
ct->enforcement_literal().size() > 1)
return false;
2334 bool new_bounds =
false;
2335 bool recanonicalize =
false;
2336 Domain negated_rhs = rhs.Negation();
2337 Domain right_domain(0);
2339 Domain implied_term_domain;
2340 term_domains[num_vars] = Domain(0);
2341 for (
int i = num_vars - 1; i >= 0; --i) {
2342 const int var =
ct->linear().vars(i);
2343 const int64_t var_coeff =
ct->linear().coeffs(i);
2345 right_domain.AdditionWith(term_domains[i + 1]).RelaxIfTooComplex();
2346 implied_term_domain = left_domains[i].AdditionWith(right_domain);
2347 new_domain = implied_term_domain.AdditionWith(negated_rhs)
2348 .InverseMultiplicationBy(-var_coeff);
2350 if (
ct->enforcement_literal().empty()) {
2355 }
else if (
ct->enforcement_literal().size() == 1) {
2366 recanonicalize =
true;
2371 if (!
ct->enforcement_literal().empty())
continue;
2383 if (rhs.Min() != rhs.Max() &&
2386 const bool same_sign = (var_coeff > 0) == (obj_coeff > 0);
2388 if (same_sign && RhsCanBeFixedToMin(var_coeff, context_->
DomainOf(
var),
2389 implied_term_domain, rhs)) {
2390 rhs = Domain(rhs.Min());
2393 if (!same_sign && RhsCanBeFixedToMax(var_coeff, context_->
DomainOf(
var),
2394 implied_term_domain, rhs)) {
2395 rhs = Domain(rhs.Max());
2401 negated_rhs = rhs.Negation();
2405 right_domain = Domain(0);
2419 if (
ct->linear().vars().size() <= 2)
continue;
2424 if (rhs.Min() != rhs.Max())
continue;
2430 if (context_->
DomainOf(
var) != new_domain)
continue;
2431 if (std::abs(var_coeff) != 1)
continue;
2438 bool is_in_objective =
false;
2440 is_in_objective =
true;
2446 if (is_in_objective) col_size--;
2447 const int row_size =
ct->linear().vars_size();
2451 const int num_entries_added = (row_size - 1) * (col_size - 1);
2452 const int num_entries_removed = col_size + row_size - 1;
2454 if (num_entries_added > num_entries_removed) {
2460 std::vector<int> others;
2468 if (c == ct_index)
continue;
2470 ConstraintProto::ConstraintCase::kLinear) {
2474 for (
const int ref :
2481 others.push_back(c);
2483 if (abort)
continue;
2486 for (
const int c : others) {
2505 if (is_in_objective &&
2511 absl::StrCat(
"linear: variable substitution ", others.size()));
2524 LinearConstraintProto* mapping_linear_ct =
2527 std::swap(mapping_linear_ct->mutable_vars()->at(0),
2528 mapping_linear_ct->mutable_vars()->at(i));
2529 std::swap(mapping_linear_ct->mutable_coeffs()->at(0),
2530 mapping_linear_ct->mutable_coeffs()->at(i));
2531 return RemoveConstraint(
ct);
2536 if (recanonicalize)
return CanonicalizeLinear(
ct);
2547void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
2548 int ct_index, ConstraintProto*
ct) {
2549 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
2554 const LinearConstraintProto& arg =
ct->linear();
2555 const int num_vars = arg.vars_size();
2559 if (num_vars <= 1)
return;
2561 int64_t min_sum = 0;
2562 int64_t max_sum = 0;
2563 int64_t max_coeff_magnitude = 0;
2564 for (
int i = 0; i < num_vars; ++i) {
2565 const int ref = arg.vars(i);
2566 const int64_t
coeff = arg.coeffs(i);
2567 const int64_t term_a =
coeff * context_->
MinOf(ref);
2568 const int64_t term_b =
coeff * context_->
MaxOf(ref);
2569 max_coeff_magnitude =
std::max(max_coeff_magnitude, std::abs(
coeff));
2570 min_sum +=
std::min(term_a, term_b);
2571 max_sum +=
std::max(term_a, term_b);
2580 const auto& domain =
ct->linear().domain();
2581 const int64_t ub_threshold = domain[domain.size() - 2] - min_sum;
2582 const int64_t lb_threshold = max_sum - domain[1];
2584 if (max_coeff_magnitude <
std::max(ub_threshold, lb_threshold))
return;
2603 const bool lower_bounded = min_sum < rhs_domain.Min();
2604 const bool upper_bounded = max_sum > rhs_domain.Max();
2605 if (!lower_bounded && !upper_bounded)
return;
2606 if (lower_bounded && upper_bounded) {
2610 if (!
ct->name().empty()) {
2611 new_ct1->set_name(absl::StrCat(
ct->name(),
" (part 1)"));
2614 new_ct1->mutable_linear());
2618 if (!
ct->name().empty()) {
2619 new_ct2->set_name(absl::StrCat(
ct->name(),
" (part 2)"));
2622 new_ct2->mutable_linear());
2625 return (
void)RemoveConstraint(
ct);
2631 const int64_t threshold = lower_bounded ? ub_threshold : lb_threshold;
2638 const bool only_booleans =
2645 int64_t rhs_offset = 0;
2646 bool some_integer_encoding_were_extracted =
false;
2647 LinearConstraintProto* mutable_arg =
ct->mutable_linear();
2648 for (
int i = 0; i < arg.vars_size(); ++i) {
2649 int ref = arg.vars(i);
2650 int64_t
coeff = arg.coeffs(i);
2658 (only_booleans && !is_boolean)) {
2660 mutable_arg->set_vars(new_size, mutable_arg->vars(i));
2661 mutable_arg->set_coeffs(new_size, mutable_arg->coeffs(i));
2669 some_integer_encoding_were_extracted =
true;
2671 "linear: extracted integer enforcement literal");
2673 if (lower_bounded) {
2674 ct->add_enforcement_literal(is_boolean
2677 ref, context_->
MinOf(ref)));
2680 ct->add_enforcement_literal(is_boolean
2683 ref, context_->
MaxOf(ref)));
2687 mutable_arg->mutable_vars()->Truncate(new_size);
2688 mutable_arg->mutable_coeffs()->Truncate(new_size);
2690 if (some_integer_encoding_were_extracted) {
2696void CpModelPresolver::ExtractAtMostOneFromLinear(ConstraintProto*
ct) {
2701 const LinearConstraintProto& arg =
ct->linear();
2702 const int num_vars = arg.vars_size();
2703 int64_t min_sum = 0;
2704 int64_t max_sum = 0;
2705 for (
int i = 0; i < num_vars; ++i) {
2706 const int ref = arg.vars(i);
2707 const int64_t
coeff = arg.coeffs(i);
2708 const int64_t term_a =
coeff * context_->
MinOf(ref);
2709 const int64_t term_b =
coeff * context_->
MaxOf(ref);
2710 min_sum +=
std::min(term_a, term_b);
2711 max_sum +=
std::max(term_a, term_b);
2713 for (
const int type : {0, 1}) {
2714 std::vector<int> at_most_one;
2715 for (
int i = 0; i < num_vars; ++i) {
2716 const int ref = arg.vars(i);
2717 const int64_t
coeff = arg.coeffs(i);
2718 if (context_->
MinOf(ref) != 0)
continue;
2719 if (context_->
MaxOf(ref) != 1)
continue;
2724 if (min_sum + 2 * std::abs(
coeff) > rhs.Max()) {
2728 if (max_sum - 2 * std::abs(
coeff) < rhs.Min()) {
2733 if (at_most_one.size() > 1) {
2741 for (
const int ref : at_most_one) {
2742 new_ct->mutable_at_most_one()->add_literals(ref);
2751bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto*
ct) {
2752 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
2757 const LinearConstraintProto& arg =
ct->linear();
2758 const int num_vars = arg.vars_size();
2760 int64_t max_coeff = 0;
2761 int64_t min_sum = 0;
2762 int64_t max_sum = 0;
2763 for (
int i = 0; i < num_vars; ++i) {
2765 const int var = arg.vars(i);
2766 const int64_t
coeff = arg.coeffs(i);
2769 if (context_->
MinOf(
var) != 0)
return false;
2770 if (context_->
MaxOf(
var) != 1)
return false;
2792 if ((!rhs_domain.Contains(min_sum) &&
2793 min_sum + min_coeff > rhs_domain.Max()) ||
2794 (!rhs_domain.Contains(max_sum) &&
2795 max_sum - min_coeff < rhs_domain.Min())) {
2796 context_->
UpdateRuleStats(
"linear: all booleans and trivially false");
2797 return MarkConstraintAsFalse(
ct);
2799 if (Domain(min_sum, max_sum).IsIncludedIn(rhs_domain)) {
2801 return RemoveConstraint(
ct);
2808 DCHECK(!rhs_domain.IsEmpty());
2809 if (min_sum + min_coeff > rhs_domain.Max()) {
2812 const auto copy = arg;
2813 ct->mutable_bool_and()->clear_literals();
2814 for (
int i = 0; i < num_vars; ++i) {
2815 ct->mutable_bool_and()->add_literals(
2816 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
2818 PresolveBoolAnd(
ct);
2820 }
else if (max_sum - min_coeff < rhs_domain.Min()) {
2823 const auto copy = arg;
2824 ct->mutable_bool_and()->clear_literals();
2825 for (
int i = 0; i < num_vars; ++i) {
2826 ct->mutable_bool_and()->add_literals(
2827 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
2829 PresolveBoolAnd(
ct);
2831 }
else if (min_sum + min_coeff >= rhs_domain.Min() &&
2832 rhs_domain.front().end >= max_sum) {
2835 const auto copy = arg;
2836 ct->mutable_bool_or()->clear_literals();
2837 for (
int i = 0; i < num_vars; ++i) {
2838 ct->mutable_bool_or()->add_literals(
2839 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
2843 }
else if (max_sum - min_coeff <= rhs_domain.Max() &&
2844 rhs_domain.back().start <= min_sum) {
2847 const auto copy = arg;
2848 ct->mutable_bool_or()->clear_literals();
2849 for (
int i = 0; i < num_vars; ++i) {
2850 ct->mutable_bool_or()->add_literals(
2851 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
2856 min_sum + max_coeff <= rhs_domain.Max() &&
2857 min_sum + 2 * min_coeff > rhs_domain.Max() &&
2858 rhs_domain.back().start <= min_sum) {
2861 const auto copy = arg;
2862 ct->mutable_at_most_one()->clear_literals();
2863 for (
int i = 0; i < num_vars; ++i) {
2864 ct->mutable_at_most_one()->add_literals(
2865 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
2869 max_sum - max_coeff >= rhs_domain.Min() &&
2870 max_sum - 2 * min_coeff < rhs_domain.Min() &&
2871 rhs_domain.front().end >= max_sum) {
2874 const auto copy = arg;
2875 ct->mutable_at_most_one()->clear_literals();
2876 for (
int i = 0; i < num_vars; ++i) {
2877 ct->mutable_at_most_one()->add_literals(
2878 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
2882 min_sum < rhs_domain.Min() &&
2883 min_sum + min_coeff >= rhs_domain.Min() &&
2884 min_sum + 2 * min_coeff > rhs_domain.Max() &&
2885 min_sum + max_coeff <= rhs_domain.Max()) {
2889 for (
int i = 0; i < num_vars; ++i) {
2890 exactly_one->mutable_exactly_one()->add_literals(
2891 arg.coeffs(i) > 0 ? arg.vars(i) :
NegatedRef(arg.vars(i)));
2894 return RemoveConstraint(
ct);
2896 max_sum > rhs_domain.Max() &&
2897 max_sum - min_coeff <= rhs_domain.Max() &&
2898 max_sum - 2 * min_coeff < rhs_domain.Min() &&
2899 max_sum - max_coeff >= rhs_domain.Min()) {
2903 for (
int i = 0; i < num_vars; ++i) {
2904 exactly_one->mutable_exactly_one()->add_literals(
2905 arg.coeffs(i) > 0 ?
NegatedRef(arg.vars(i)) : arg.vars(i));
2908 return RemoveConstraint(
ct);
2915 if (num_vars > 3)
return false;
2920 const int max_mask = (1 << arg.vars_size());
2921 for (
int mask = 0; mask < max_mask; ++mask) {
2923 for (
int i = 0; i < num_vars; ++i) {
2924 if ((mask >> i) & 1)
value += arg.coeffs(i);
2926 if (rhs_domain.Contains(
value))
continue;
2932 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
2934 for (
int i = 0; i < num_vars; ++i) {
2935 new_arg->add_literals(((mask >> i) & 1) ?
NegatedRef(arg.vars(i))
2941 return RemoveConstraint(
ct);
2944bool CpModelPresolver::PresolveInterval(
int c, ConstraintProto*
ct) {
2946 IntervalConstraintProto*
interval =
ct->mutable_interval();
2949 if (!
ct->enforcement_literal().empty() && context_->
SizeMax(c) < 0) {
2950 context_->
UpdateRuleStats(
"interval: negative size implies unperformed");
2951 return MarkConstraintAsFalse(
ct);
2954 bool changed =
false;
2955 if (
ct->enforcement_literal().empty()) {
2963 "interval: performed intervals must have a positive size");
2966 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_start());
2967 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_size());
2968 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_end());
2973bool CpModelPresolver::PresolveInverse(ConstraintProto*
ct) {
2974 const int size =
ct->inverse().f_direct().size();
2975 bool changed =
false;
2978 for (
const int ref :
ct->inverse().f_direct()) {
2980 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
2984 for (
const int ref :
ct->inverse().f_inverse()) {
2986 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
2996 absl::flat_hash_set<int> direct_vars;
2997 for (
const int ref :
ct->inverse().f_direct()) {
2998 const auto [it, inserted] = direct_vars.insert(
PositiveRef(ref));
3004 absl::flat_hash_set<int> inverse_vars;
3005 for (
const int ref :
ct->inverse().f_inverse()) {
3006 const auto [it, inserted] = inverse_vars.insert(
PositiveRef(ref));
3016 const auto filter_inverse_domain =
3017 [
this, size, &changed](
const auto& direct,
const auto& inverse) {
3019 std::vector<absl::flat_hash_set<int64_t>> inverse_values(size);
3020 for (
int i = 0; i < size; ++i) {
3021 const Domain domain = context_->
DomainOf(inverse[i]);
3022 for (
const int64_t j : domain.Values()) {
3023 inverse_values[i].insert(j);
3030 std::vector<int64_t> possible_values;
3031 for (
int i = 0; i < size; ++i) {
3032 possible_values.clear();
3033 const Domain domain = context_->
DomainOf(direct[i]);
3034 bool removed_value =
false;
3035 for (
const int64_t j : domain.Values()) {
3036 if (inverse_values[j].contains(i)) {
3037 possible_values.push_back(j);
3039 removed_value =
true;
3042 if (removed_value) {
3046 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
3054 if (!filter_inverse_domain(
ct->inverse().f_direct(),
3055 ct->inverse().f_inverse())) {
3059 if (!filter_inverse_domain(
ct->inverse().f_inverse(),
3060 ct->inverse().f_direct())) {
3071bool CpModelPresolver::PresolveElement(ConstraintProto*
ct) {
3074 if (
ct->element().vars().empty()) {
3079 const int index_ref =
ct->element().index();
3080 const int target_ref =
ct->element().target();
3085 bool all_constants =
true;
3086 absl::flat_hash_set<int64_t> constant_set;
3087 bool all_included_in_target_domain =
true;
3090 bool reduced_index_domain =
false;
3092 Domain(0,
ct->element().vars_size() - 1),
3093 &reduced_index_domain)) {
3101 std::vector<int64_t> possible_indices;
3102 const Domain& index_domain = context_->
DomainOf(index_ref);
3103 for (
const int64_t index_value : index_domain.Values()) {
3104 const int ref =
ct->element().vars(index_value);
3105 const int64_t target_value =
3106 target_ref == index_ref ? index_value : -index_value;
3108 possible_indices.push_back(target_value);
3111 if (possible_indices.size() < index_domain.Size()) {
3117 "element: reduced index domain when target equals index");
3123 Domain infered_domain;
3124 const Domain& initial_index_domain = context_->
DomainOf(index_ref);
3125 const Domain& target_domain = context_->
DomainOf(target_ref);
3126 std::vector<int64_t> possible_indices;
3127 for (
const int64_t
value : initial_index_domain.Values()) {
3130 const int ref =
ct->element().vars(
value);
3131 const Domain& domain = context_->
DomainOf(ref);
3132 if (domain.IntersectionWith(target_domain).IsEmpty())
continue;
3133 possible_indices.push_back(
value);
3134 if (domain.IsFixed()) {
3135 constant_set.insert(domain.Min());
3137 all_constants =
false;
3139 if (!domain.IsIncludedIn(target_domain)) {
3140 all_included_in_target_domain =
false;
3142 infered_domain = infered_domain.
UnionWith(domain);
3144 if (possible_indices.size() < initial_index_domain.Size()) {
3151 bool domain_modified =
false;
3153 &domain_modified)) {
3156 if (domain_modified) {
3162 if (context_->
IsFixed(index_ref)) {
3163 const int var =
ct->element().vars(context_->
MinOf(index_ref));
3164 if (
var != target_ref) {
3165 LinearConstraintProto*
const lin =
3168 lin->add_coeffs(-1);
3169 lin->add_vars(target_ref);
3176 return RemoveConstraint(
ct);
3182 if (all_constants && constant_set.size() == 1) {
3185 return RemoveConstraint(
ct);
3190 if (context_->
MinOf(index_ref) == 0 && context_->
MaxOf(index_ref) == 1 &&
3192 const int64_t v0 = context_->
MinOf(
ct->element().vars(0));
3193 const int64_t v1 = context_->
MinOf(
ct->element().vars(1));
3195 LinearConstraintProto*
const lin =
3199 lin->add_vars(index_ref);
3200 lin->add_coeffs(v0 - v1);
3201 lin->add_domain(v0);
3202 lin->add_domain(v0);
3204 context_->
UpdateRuleStats(
"element: linearize constant element of size 2");
3205 return RemoveConstraint(
ct);
3209 const AffineRelation::Relation r_index =
3211 if (r_index.representative != index_ref) {
3213 if (context_->
DomainOf(r_index.representative).
Size() >
3219 const int64_t r_min = context_->
MinOf(r_ref);
3220 const int64_t r_max = context_->
MaxOf(r_ref);
3221 const int array_size =
ct->element().vars_size();
3223 context_->
UpdateRuleStats(
"TODO element: representative has bad domain");
3224 }
else if (r_index.offset >= 0 && r_index.offset < array_size &&
3225 r_index.offset + r_max * r_index.coeff >= 0 &&
3226 r_index.offset + r_max * r_index.coeff < array_size) {
3228 ElementConstraintProto*
const element =
3230 for (int64_t v = 0; v <= r_max; ++v) {
3231 const int64_t scaled_index = v * r_index.coeff + r_index.offset;
3233 CHECK_LT(scaled_index, array_size);
3234 element->add_vars(
ct->element().vars(scaled_index));
3236 element->set_index(r_ref);
3237 element->set_target(target_ref);
3239 if (r_index.coeff == 1) {
3245 return RemoveConstraint(
ct);
3256 absl::flat_hash_map<int, int> local_var_occurrence_counter;
3257 local_var_occurrence_counter[
PositiveRef(index_ref)]++;
3258 local_var_occurrence_counter[
PositiveRef(target_ref)]++;
3264 const int ref =
ct->element().vars(
value);
3270 local_var_occurrence_counter.at(
PositiveRef(index_ref)) == 1) {
3271 if (all_constants) {
3275 context_->
UpdateRuleStats(
"element: trivial target domain reduction");
3278 return RemoveConstraint(
ct);
3284 if (!context_->
IsFixed(target_ref) &&
3286 local_var_occurrence_counter.at(
PositiveRef(target_ref)) == 1) {
3287 if (all_included_in_target_domain) {
3291 return RemoveConstraint(
ct);
3300bool CpModelPresolver::PresolveTable(ConstraintProto*
ct) {
3303 if (
ct->table().vars().empty()) {
3305 return RemoveConstraint(
ct);
3308 const int initial_num_vars =
ct->table().vars_size();
3309 bool changed =
true;
3312 std::vector<AffineRelation::Relation> affine_relations;
3313 std::vector<int64_t> old_var_lb;
3314 std::vector<int64_t> old_var_ub;
3316 for (
int v = 0; v < initial_num_vars; ++v) {
3317 const int ref =
ct->table().vars(v);
3319 affine_relations.push_back(r);
3320 old_var_lb.push_back(context_->
MinOf(ref));
3321 old_var_ub.push_back(context_->
MaxOf(ref));
3322 if (r.representative != ref) {
3324 ct->mutable_table()->set_vars(v, r.representative);
3326 "table: replace variable by canonical affine one");
3335 std::vector<int> old_index_of_duplicate_to_new_index_of_first_occurrence(
3336 initial_num_vars, -1);
3338 std::vector<int> old_index_to_new_index(initial_num_vars, -1);
3341 absl::flat_hash_map<int, int> first_visit;
3342 for (
int p = 0; p < initial_num_vars; ++p) {
3343 const int ref =
ct->table().vars(p);
3345 const auto& it = first_visit.find(
var);
3346 if (it != first_visit.end()) {
3347 const int previous = it->second;
3348 old_index_of_duplicate_to_new_index_of_first_occurrence[p] = previous;
3352 ct->mutable_table()->set_vars(num_vars, ref);
3353 first_visit[
var] = num_vars;
3354 old_index_to_new_index[p] = num_vars;
3359 if (num_vars < initial_num_vars) {
3360 ct->mutable_table()->mutable_vars()->Truncate(num_vars);
3367 std::vector<std::vector<int64_t>> new_tuples;
3368 const int initial_num_tuples =
ct->table().values_size() / initial_num_vars;
3369 std::vector<absl::flat_hash_set<int64_t>> new_domains(num_vars);
3372 std::vector<int64_t> tuple(num_vars);
3373 new_tuples.reserve(initial_num_tuples);
3374 for (
int i = 0; i < initial_num_tuples; ++i) {
3375 bool delete_row =
false;
3377 for (
int j = 0; j < initial_num_vars; ++j) {
3378 const int64_t old_value =
ct->table().values(i * initial_num_vars + j);
3382 if (old_value < old_var_lb[j] || old_value > old_var_ub[j]) {
3388 const AffineRelation::Relation& r = affine_relations[j];
3389 const int64_t
value = (old_value - r.offset) / r.coeff;
3390 if (
value * r.coeff + r.offset != old_value) {
3395 const int mapped_position = old_index_to_new_index[j];
3396 if (mapped_position == -1) {
3397 const int new_index_of_first_occurrence =
3398 old_index_of_duplicate_to_new_index_of_first_occurrence[j];
3399 if (
value != tuple[new_index_of_first_occurrence]) {
3404 const int ref =
ct->table().vars(mapped_position);
3409 tuple[mapped_position] =
value;
3416 new_tuples.push_back(tuple);
3417 for (
int j = 0; j < num_vars; ++j) {
3418 new_domains[j].insert(tuple[j]);
3422 if (new_tuples.size() < initial_num_tuples) {
3429 ct->mutable_table()->clear_values();
3430 for (
const std::vector<int64_t>& t : new_tuples) {
3431 for (
const int64_t v : t) {
3432 ct->mutable_table()->add_values(v);
3438 if (
ct->table().negated())
return changed;
3441 for (
int j = 0; j < num_vars; ++j) {
3442 const int ref =
ct->table().vars(j);
3446 new_domains[j].
end())),
3454 if (num_vars == 1) {
3457 return RemoveConstraint(
ct);
3462 for (
int j = 0; j < num_vars; ++j) prod *= new_domains[j].size();
3463 if (prod == new_tuples.size()) {
3465 return RemoveConstraint(
ct);
3471 if (new_tuples.size() > 0.7 * prod) {
3473 std::vector<std::vector<int64_t>> var_to_values(num_vars);
3474 for (
int j = 0; j < num_vars; ++j) {
3475 var_to_values[j].assign(new_domains[j].begin(), new_domains[j].
end());
3477 std::vector<std::vector<int64_t>> all_tuples(prod);
3478 for (
int i = 0; i < prod; ++i) {
3479 all_tuples[i].resize(num_vars);
3481 for (
int j = 0; j < num_vars; ++j) {
3482 all_tuples[i][j] = var_to_values[j][
index % var_to_values[j].size()];
3483 index /= var_to_values[j].size();
3489 std::vector<std::vector<int64_t>> diff(prod - new_tuples.size());
3490 std::set_difference(all_tuples.begin(), all_tuples.end(),
3491 new_tuples.begin(), new_tuples.end(), diff.begin());
3494 ct->mutable_table()->set_negated(!
ct->table().negated());
3495 ct->mutable_table()->clear_values();
3496 for (
const std::vector<int64_t>& t : diff) {
3497 for (
const int64_t v : t)
ct->mutable_table()->add_values(v);
3504bool CpModelPresolver::PresolveAllDiff(ConstraintProto*
ct) {
3508 AllDifferentConstraintProto& all_diff = *
ct->mutable_all_diff();
3510 bool constraint_has_changed =
false;
3511 for (LinearExpressionProto& exp :
3512 *(
ct->mutable_all_diff()->mutable_exprs())) {
3513 constraint_has_changed |= CanonicalizeLinearExpression(*
ct, &exp);
3517 const int size = all_diff.exprs_size();
3520 return RemoveConstraint(
ct);
3524 return RemoveConstraint(
ct);
3527 bool something_was_propagated =
false;
3528 std::vector<LinearExpressionProto> kept_expressions;
3529 for (
int i = 0; i < size; ++i) {
3530 if (!context_->
IsFixed(all_diff.exprs(i))) {
3531 kept_expressions.push_back(all_diff.exprs(i));
3535 const int64_t
value = context_->
MinOf(all_diff.exprs(i));
3536 bool propagated =
false;
3537 for (
int j = 0; j < size; ++j) {
3538 if (i == j)
continue;
3541 Domain(
value).Complement())) {
3549 something_was_propagated =
true;
3556 kept_expressions.begin(), kept_expressions.end(),
3557 [](
const LinearExpressionProto& expr_a,
3558 const LinearExpressionProto& expr_b) {
3559 DCHECK_EQ(expr_a.vars_size(), 1);
3560 DCHECK_EQ(expr_b.vars_size(), 1);
3561 const int ref_a = expr_a.vars(0);
3562 const int ref_b = expr_b.vars(0);
3563 const int64_t coeff_a = expr_a.coeffs(0);
3564 const int64_t coeff_b = expr_b.coeffs(0);
3565 const int64_t abs_coeff_a = std::abs(coeff_a);
3566 const int64_t abs_coeff_b = std::abs(coeff_b);
3567 const int64_t offset_a = expr_a.offset();
3568 const int64_t offset_b = expr_b.offset();
3569 const int64_t abs_offset_a = std::abs(offset_a);
3570 const int64_t abs_offset_b = std::abs(offset_b);
3571 return std::tie(ref_a, abs_coeff_a, coeff_a, abs_offset_a, offset_a) <
3572 std::tie(ref_b, abs_coeff_b, coeff_b, abs_offset_b, offset_b);
3578 for (
int i = 1; i < kept_expressions.size(); ++i) {
3580 kept_expressions[i - 1], 1)) {
3582 "Duplicate variable in all_diff");
3585 kept_expressions[i - 1], -1)) {
3586 bool domain_modified =
false;
3588 Domain(0).Complement(),
3589 &domain_modified)) {
3592 if (domain_modified) {
3594 "all_diff: remove 0 from expression appearing with its "
3600 if (kept_expressions.size() < all_diff.exprs_size()) {
3601 all_diff.clear_exprs();
3602 for (
const LinearExpressionProto& expr : kept_expressions) {
3603 *all_diff.add_exprs() = expr;
3606 something_was_propagated =
true;
3607 constraint_has_changed =
true;
3608 if (kept_expressions.size() <= 1)
continue;
3612 CHECK_GE(all_diff.exprs_size(), 2);
3614 for (
int i = 1; i < all_diff.exprs_size(); ++i) {
3617 if (all_diff.exprs_size() == domain.Size()) {
3618 absl::flat_hash_map<int64_t, std::vector<LinearExpressionProto>>
3620 for (
const LinearExpressionProto& expr : all_diff.exprs()) {
3621 for (
const int64_t v : context_->
DomainOf(expr.vars(0)).
Values()) {
3622 value_to_exprs[expr.coeffs(0) * v + expr.offset()].push_back(expr);
3625 bool propagated =
false;
3626 for (
const auto& it : value_to_exprs) {
3627 if (it.second.size() == 1 && !context_->
IsFixed(it.second.front())) {
3628 const LinearExpressionProto& expr = it.second.
front();
3637 "all_diff: propagated mandatory values in permutation");
3638 something_was_propagated =
true;
3641 if (!something_was_propagated)
break;
3644 return constraint_has_changed;
3651std::vector<int> GetLiteralsFromSetPPCConstraint(
const ConstraintProto&
ct) {
3652 std::vector<int> sorted_literals;
3654 for (
const int literal :
ct.at_most_one().literals()) {
3655 sorted_literals.push_back(
literal);
3658 for (
const int literal :
ct.bool_or().literals()) {
3659 sorted_literals.push_back(
literal);
3662 for (
const int literal :
ct.exactly_one().literals()) {
3663 sorted_literals.push_back(
literal);
3666 std::sort(sorted_literals.begin(), sorted_literals.end());
3667 return sorted_literals;
3672void AddImplication(
int lhs,
int rhs, CpModelProto*
proto,
3673 absl::flat_hash_map<int, int>* ref_to_bool_and) {
3674 if (ref_to_bool_and->contains(lhs)) {
3675 const int ct_index = (*ref_to_bool_and)[lhs];
3677 }
else if (ref_to_bool_and->contains(
NegatedRef(rhs))) {
3678 const int ct_index = (*ref_to_bool_and)[
NegatedRef(rhs)];
3684 ct->add_enforcement_literal(lhs);
3685 ct->mutable_bool_and()->add_literals(rhs);
3689template <
typename ClauseContainer>
3690void ExtractClauses(
bool use_bool_and,
const ClauseContainer& container,
3691 CpModelProto*
proto) {
3698 absl::flat_hash_map<int, int> ref_to_bool_and;
3699 for (
int i = 0; i < container.NumClauses(); ++i) {
3700 const std::vector<Literal>& clause = container.Clause(i);
3701 if (clause.empty())
continue;
3704 if (use_bool_and && clause.size() == 2) {
3705 const int a = clause[0].IsPositive()
3706 ? clause[0].Variable().value()
3708 const int b = clause[1].IsPositive()
3709 ? clause[1].Variable().value()
3717 for (
const Literal l : clause) {
3718 if (l.IsPositive()) {
3719 ct->mutable_bool_or()->add_literals(l.Variable().value());
3721 ct->mutable_bool_or()->add_literals(
NegatedRef(l.Variable().value()));
3729bool CpModelPresolver::PresolveNoOverlap(ConstraintProto*
ct) {
3731 NoOverlapConstraintProto*
proto =
ct->mutable_no_overlap();
3732 bool changed =
false;
3736 const int initial_num_intervals =
proto->intervals_size();
3739 for (
int i = 0; i < initial_num_intervals; ++i) {
3740 const int interval_index =
proto->intervals(i);
3743 proto->set_intervals(new_size++, interval_index);
3746 if (new_size < initial_num_intervals) {
3747 proto->mutable_intervals()->Truncate(new_size);
3754 if (
proto->intervals_size() > 1) {
3755 std::vector<IndexedInterval> indexed_intervals;
3756 for (
int i = 0; i <
proto->intervals().size(); ++i) {
3758 indexed_intervals.push_back({
index,
3762 std::vector<std::vector<int>> components;
3765 if (components.size() > 1) {
3766 for (
const std::vector<int>& intervals : components) {
3767 if (intervals.size() <= 1)
continue;
3769 NoOverlapConstraintProto* new_no_overlap =
3773 for (
const int i : intervals) {
3778 context_->
UpdateRuleStats(
"no_overlap: split into disjoint components");
3779 return RemoveConstraint(
ct);
3783 std::vector<int> constant_intervals;
3784 int64_t size_min_of_non_constant_intervals =
3786 for (
int i = 0; i <
proto->intervals_size(); ++i) {
3787 const int interval_index =
proto->intervals(i);
3789 constant_intervals.push_back(interval_index);
3791 size_min_of_non_constant_intervals =
3792 std::min(size_min_of_non_constant_intervals,
3793 context_->
SizeMin(interval_index));
3797 bool move_constraint_last =
false;
3798 if (!constant_intervals.empty()) {
3800 std::sort(constant_intervals.begin(), constant_intervals.end(),
3801 [
this](
int i1,
int i2) {
3802 const int64_t s1 = context_->StartMin(i1);
3803 const int64_t e1 = context_->EndMax(i1);
3804 const int64_t s2 = context_->StartMin(i2);
3805 const int64_t e2 = context_->EndMax(i2);
3806 return std::tie(s1, e1) < std::tie(s2, e2);
3812 for (
int i = 0; i + 1 < constant_intervals.size(); ++i) {
3813 if (context_->
EndMax(constant_intervals[i]) >
3814 context_->
StartMin(constant_intervals[i + 1])) {
3820 if (constant_intervals.size() ==
proto->intervals_size()) {
3822 return RemoveConstraint(
ct);
3825 absl::flat_hash_set<int> intervals_to_remove;
3829 for (
int i = 0; i + 1 < constant_intervals.size(); ++i) {
3830 const int start = i;
3831 while (i + 1 < constant_intervals.size() &&
3832 context_->
StartMin(constant_intervals[i + 1]) -
3833 context_->
EndMax(constant_intervals[i]) <
3834 size_min_of_non_constant_intervals) {
3837 if (i ==
start)
continue;
3838 for (
int j =
start; j <= i; ++j) {
3839 intervals_to_remove.insert(constant_intervals[j]);
3841 const int64_t new_start = context_->
StartMin(constant_intervals[
start]);
3842 const int64_t new_end = context_->
EndMax(constant_intervals[i]);
3844 IntervalConstraintProto* new_interval =
3847 new_interval->mutable_size()->set_offset(new_end - new_start);
3848 new_interval->mutable_end()->set_offset(new_end);
3849 move_constraint_last =
true;
3853 if (!intervals_to_remove.empty()) {
3855 const int old_size =
proto->intervals_size();
3856 for (
int i = 0; i < old_size; ++i) {
3857 const int interval_index =
proto->intervals(i);
3858 if (intervals_to_remove.contains(interval_index)) {
3861 proto->set_intervals(new_size++, interval_index);
3864 proto->mutable_intervals()->Truncate(new_size);
3866 "no_overlap: merge constant contiguous intervals");
3867 intervals_to_remove.clear();
3868 constant_intervals.clear();
3874 if (
proto->intervals_size() == 1) {
3876 return RemoveConstraint(
ct);
3878 if (
proto->intervals().empty()) {
3880 return RemoveConstraint(
ct);
3886 if (move_constraint_last) {
3890 return RemoveConstraint(
ct);
3896bool CpModelPresolver::PresolveNoOverlap2D(
int c, ConstraintProto*
ct) {
3901 const NoOverlap2DConstraintProto&
proto =
ct->no_overlap_2d();
3902 const int initial_num_boxes =
proto.x_intervals_size();
3904 bool has_zero_sizes =
false;
3905 bool x_constant =
true;
3906 bool y_constant =
true;
3910 std::vector<Rectangle> bounding_boxes;
3911 std::vector<int> active_boxes;
3912 for (
int i = 0; i <
proto.x_intervals_size(); ++i) {
3913 const int x_interval_index =
proto.x_intervals(i);
3914 const int y_interval_index =
proto.y_intervals(i);
3921 if (
proto.boxes_with_null_area_can_overlap() &&
3922 (context_->
SizeMax(x_interval_index) == 0 ||
3923 context_->
SizeMax(y_interval_index) == 0)) {
3924 if (
proto.boxes_with_null_area_can_overlap())
continue;
3925 has_zero_sizes =
true;
3927 ct->mutable_no_overlap_2d()->set_x_intervals(new_size, x_interval_index);
3928 ct->mutable_no_overlap_2d()->set_y_intervals(new_size, y_interval_index);
3929 bounding_boxes.push_back(
3930 {IntegerValue(context_->
StartMin(x_interval_index)),
3931 IntegerValue(context_->
EndMax(x_interval_index)),
3932 IntegerValue(context_->
StartMin(y_interval_index)),
3933 IntegerValue(context_->
EndMax(y_interval_index))});
3934 active_boxes.push_back(new_size);
3946 bounding_boxes, absl::MakeSpan(active_boxes));
3947 if (components.size() > 1) {
3948 for (
const absl::Span<int> boxes : components) {
3949 if (boxes.size() <= 1)
continue;
3951 NoOverlap2DConstraintProto* new_no_overlap_2d =
3953 for (
const int b : boxes) {
3955 new_no_overlap_2d->add_y_intervals(
proto.y_intervals(
b));
3959 context_->
UpdateRuleStats(
"no_overlap_2d: split into disjoint components");
3960 return RemoveConstraint(
ct);
3963 if (!has_zero_sizes && (x_constant || y_constant)) {
3965 "no_overlap_2d: a dimension is constant, splitting into many no "
3967 std::vector<IndexedInterval> indexed_intervals;
3968 for (
int i = 0; i < new_size; ++i) {
3969 int x =
proto.x_intervals(i);
3970 int y =
proto.y_intervals(i);
3972 indexed_intervals.push_back({x, IntegerValue(context_->
StartMin(y)),
3973 IntegerValue(context_->
EndMax(y))});
3975 std::vector<std::vector<int>> no_overlaps;
3978 for (
const std::vector<int>& no_overlap : no_overlaps) {
3982 for (
const int i : no_overlap) {
3987 return RemoveConstraint(
ct);
3990 if (new_size < initial_num_boxes) {
3992 ct->mutable_no_overlap_2d()->mutable_x_intervals()->Truncate(new_size);
3993 ct->mutable_no_overlap_2d()->mutable_y_intervals()->Truncate(new_size);
3996 if (new_size == 0) {
3998 return RemoveConstraint(
ct);
4001 if (new_size == 1) {
4003 return RemoveConstraint(
ct);
4006 return new_size < initial_num_boxes;
4010LinearExpressionProto ConstantExpressionProto(int64_t
value) {
4011 LinearExpressionProto expr;
4012 expr.set_offset(
value);
4017bool CpModelPresolver::PresolveCumulative(ConstraintProto*
ct) {
4020 CumulativeConstraintProto*
proto =
ct->mutable_cumulative();
4022 bool changed = CanonicalizeLinearExpression(*
ct,
proto->mutable_capacity());
4023 for (LinearExpressionProto& exp :
4024 *(
ct->mutable_cumulative()->mutable_demands())) {
4025 changed |= CanonicalizeLinearExpression(*
ct, &exp);
4028 const int64_t capacity_max = context_->
MaxOf(
proto->capacity());
4032 bool domain_changed =
false;
4034 proto->capacity(), Domain(0, capacity_max), &domain_changed)) {
4037 if (domain_changed) {
4046 int num_zero_demand_removed = 0;
4047 int num_zero_size_removed = 0;
4048 int num_incompatible_demands = 0;
4049 for (
int i = 0; i <
proto->intervals_size(); ++i) {
4052 const LinearExpressionProto& demand_expr =
proto->demands(i);
4053 const int64_t demand_max = context_->
MaxOf(demand_expr);
4054 if (demand_max == 0) {
4055 num_zero_demand_removed++;
4061 num_zero_size_removed++;
4065 if (context_->
MinOf(demand_expr) > capacity_max) {
4067 ConstraintProto* interval_ct =
4069 DCHECK_EQ(interval_ct->enforcement_literal_size(), 1);
4070 const int literal = interval_ct->enforcement_literal(0);
4074 num_incompatible_demands++;
4078 "cumulative: performed demand exceeds capacity.");
4082 proto->set_intervals(new_size,
proto->intervals(i));
4083 *
proto->mutable_demands(new_size) =
proto->demands(i);
4087 if (new_size < proto->intervals_size()) {
4089 proto->mutable_intervals()->Truncate(new_size);
4090 proto->mutable_demands()->erase(
4091 proto->mutable_demands()->begin() + new_size,
4092 proto->mutable_demands()->end());
4095 if (num_zero_demand_removed > 0) {
4097 "cumulative: removed intervals with no demands");
4099 if (num_zero_size_removed > 0) {
4101 "cumulative: removed intervals with a size of zero");
4103 if (num_incompatible_demands > 0) {
4105 "cumulative: removed intervals demands greater than the capacity");
4111 for (
int i = 0; i <
proto->demands_size(); ++i) {
4113 const LinearExpressionProto& demand_expr =
proto->demands(i);
4115 bool domain_changed =
false;
4120 if (domain_changed) {
4122 "cumulative: fit demand in [0..capacity_max]");
4134 if (
proto->intervals_size() > 1) {
4135 std::vector<IndexedInterval> indexed_intervals;
4136 for (
int i = 0; i <
proto->intervals().size(); ++i) {
4138 indexed_intervals.push_back({i, IntegerValue(context_->
StartMin(
index)),
4141 std::vector<std::vector<int>> components;
4144 if (components.size() > 1) {
4145 for (
const std::vector<int>& component : components) {
4146 CumulativeConstraintProto* new_cumulative =
4148 for (
const int i : component) {
4150 *new_cumulative->add_demands() =
proto->demands(i);
4152 *new_cumulative->mutable_capacity() =
proto->capacity();
4155 context_->
UpdateRuleStats(
"cumulative: split into disjoint components");
4156 return RemoveConstraint(
ct);
4164 std::map<int64_t, int64_t> time_to_demand_deltas;
4165 const int64_t capacity_min = context_->
MinOf(
proto->capacity());
4166 for (
int i = 0; i <
proto->intervals_size(); ++i) {
4167 const int interval_index =
proto->intervals(i);
4168 const int64_t demand_max = context_->
MaxOf(
proto->demands(i));
4169 time_to_demand_deltas[context_->
StartMin(interval_index)] += demand_max;
4170 time_to_demand_deltas[context_->
EndMax(interval_index)] -= demand_max;
4179 int num_possible_overloads = 0;
4180 int64_t current_load = 0;
4181 absl::flat_hash_map<int64_t, int64_t> num_possible_overloads_before;
4182 for (
const auto& it : time_to_demand_deltas) {
4183 num_possible_overloads_before[it.first] = num_possible_overloads;
4184 current_load += it.second;
4185 if (current_load > capacity_min) {
4186 ++num_possible_overloads;
4192 if (num_possible_overloads == 0) {
4194 "cumulative: max profile is always under the min capacity");
4195 return RemoveConstraint(
ct);
4205 for (
int i = 0; i <
proto->intervals_size(); ++i) {
4223 const int num_diff = num_possible_overloads_before.at(
end_max) -
4224 num_possible_overloads_before.at(
start_min);
4225 if (num_diff == 0)
continue;
4227 proto->set_intervals(new_size,
proto->intervals(i));
4228 *
proto->mutable_demands(new_size) =
proto->demands(i);
4232 if (new_size < proto->intervals_size()) {
4234 proto->mutable_intervals()->Truncate(new_size);
4235 proto->mutable_demands()->erase(
4236 proto->mutable_demands()->begin() + new_size,
4237 proto->mutable_demands()->end());
4239 "cumulative: remove never conflicting intervals.");
4243 if (
proto->intervals().empty()) {
4245 return RemoveConstraint(
ct);
4249 int64_t max_of_performed_demand_mins = 0;
4250 int64_t sum_of_max_demands = 0;
4251 for (
int i = 0; i <
proto->intervals_size(); ++i) {
4252 const ConstraintProto& interval_ct =
4255 const LinearExpressionProto& demand_expr =
proto->demands(i);
4256 sum_of_max_demands += context_->
MaxOf(demand_expr);
4258 if (interval_ct.enforcement_literal().empty()) {
4259 max_of_performed_demand_mins =
std::max(max_of_performed_demand_mins,
4260 context_->
MinOf(demand_expr));
4264 const LinearExpressionProto& capacity_expr =
proto->capacity();
4265 if (max_of_performed_demand_mins > context_->
MinOf(capacity_expr)) {
4268 capacity_expr, Domain(max_of_performed_demand_mins,
4274 if (max_of_performed_demand_mins > context_->
MaxOf(capacity_expr)) {
4275 context_->
UpdateRuleStats(
"cumulative: cannot fit performed demands");
4279 if (sum_of_max_demands <= context_->MinOf(capacity_expr)) {
4280 context_->
UpdateRuleStats(
"cumulative: capacity exceeds sum of demands");
4281 return RemoveConstraint(
ct);
4287 for (
int i = 0; i <
ct->cumulative().demands_size(); ++i) {
4288 const LinearExpressionProto& demand_expr =
ct->cumulative().demands(i);
4289 if (!context_->
IsFixed(demand_expr)) {
4295 if (gcd == 1)
break;
4299 for (
int i = 0; i <
ct->cumulative().demands_size(); ++i) {
4300 const int64_t
demand = context_->
MinOf(
ct->cumulative().demands(i));
4301 *
proto->mutable_demands(i) = ConstantExpressionProto(
demand / gcd);
4304 const int64_t old_capacity = context_->
MinOf(
proto->capacity());
4305 *
proto->mutable_capacity() = ConstantExpressionProto(old_capacity / gcd);
4307 "cumulative: divide demands and capacity by gcd");
4311 const int num_intervals =
proto->intervals_size();
4312 const LinearExpressionProto& capacity_expr =
proto->capacity();
4314 std::vector<LinearExpressionProto> start_exprs(num_intervals);
4316 int num_duration_one = 0;
4317 int num_greater_half_capacity = 0;
4319 bool has_optional_interval =
false;
4320 bool all_starts_are_variables =
true;
4321 for (
int i = 0; i < num_intervals; ++i) {
4325 const ConstraintProto&
ct =
4327 const IntervalConstraintProto&
interval =
ct.interval();
4330 const LinearExpressionProto& demand_expr =
proto->demands(i);
4339 const int64_t demand_min = context_->
MinOf(demand_expr);
4340 const int64_t demand_max = context_->
MaxOf(demand_expr);
4341 if (demand_min > capacity_max / 2) {
4342 num_greater_half_capacity++;
4344 if (demand_min > capacity_max) {
4345 context_->
UpdateRuleStats(
"cumulative: demand_min exceeds capacity max");
4349 CHECK_EQ(
ct.enforcement_literal().size(), 1);
4355 }
else if (demand_max > capacity_max) {
4356 if (
ct.enforcement_literal().empty()) {
4358 "cumulative: demand_max exceeds capacity max.");
4368 "cumulative: demand_max of optional interval exceeds capacity.");
4373 if (num_greater_half_capacity == num_intervals) {
4374 if (num_duration_one == num_intervals && !has_optional_interval &&
4375 all_starts_are_variables) {
4379 for (
const LinearExpressionProto& expr : start_exprs) {
4383 return RemoveConstraint(
ct);
4388 for (
int i = 0; i <
proto->demands_size(); ++i) {
4389 const LinearExpressionProto& demand_expr =
proto->demands(i);
4390 const int64_t demand_max = context_->
MaxOf(demand_expr);
4391 if (demand_max > context_->
MinOf(capacity_expr)) {
4392 ConstraintProto* capacity_gt =
4397 capacity_gt->mutable_linear()->add_domain(0);
4398 capacity_gt->mutable_linear()->add_domain(
4401 capacity_gt->mutable_linear());
4403 capacity_gt->mutable_linear());
4413 return RemoveConstraint(
ct);
4420bool CpModelPresolver::PresolveRoutes(ConstraintProto*
ct) {
4423 RoutesConstraintProto&
proto = *
ct->mutable_routes();
4425 const int old_size =
proto.literals_size();
4427 std::vector<bool> has_incoming_or_outgoing_arcs;
4428 const int num_arcs =
proto.literals_size();
4429 for (
int i = 0; i < num_arcs; ++i) {
4430 const int ref =
proto.literals(i);
4437 proto.set_literals(new_size, ref);
4441 if (
tail >= has_incoming_or_outgoing_arcs.size()) {
4442 has_incoming_or_outgoing_arcs.resize(
tail + 1,
false);
4444 if (
head >= has_incoming_or_outgoing_arcs.size()) {
4445 has_incoming_or_outgoing_arcs.resize(
head + 1,
false);
4447 has_incoming_or_outgoing_arcs[
tail] =
true;
4448 has_incoming_or_outgoing_arcs[
head] =
true;
4451 if (old_size > 0 && new_size == 0) {
4456 "routes: graph with nodes and no arcs");
4459 if (new_size < num_arcs) {
4460 proto.mutable_literals()->Truncate(new_size);
4461 proto.mutable_tails()->Truncate(new_size);
4462 proto.mutable_heads()->Truncate(new_size);
4468 for (
int n = 0; n < has_incoming_or_outgoing_arcs.size(); ++n) {
4469 if (!has_incoming_or_outgoing_arcs[n]) {
4471 "routes: node ", n,
" misses incoming or outgoing arcs"));
4478bool CpModelPresolver::PresolveCircuit(ConstraintProto*
ct) {
4481 CircuitConstraintProto&
proto = *
ct->mutable_circuit();
4485 ct->mutable_circuit()->mutable_heads());
4489 std::vector<std::vector<int>> incoming_arcs;
4490 std::vector<std::vector<int>> outgoing_arcs;
4492 const int num_arcs =
proto.literals_size();
4493 for (
int i = 0; i < num_arcs; ++i) {
4494 const int ref =
proto.literals(i);
4502 incoming_arcs[
head].push_back(ref);
4503 outgoing_arcs[
tail].push_back(ref);
4507 for (
int i = 0; i < num_nodes; ++i) {
4508 if (incoming_arcs[i].empty() || outgoing_arcs[i].empty()) {
4509 return MarkConstraintAsFalse(
ct);
4518 bool loop_again =
true;
4519 int num_fixed_at_true = 0;
4520 while (loop_again) {
4522 for (
const auto* node_to_refs : {&incoming_arcs, &outgoing_arcs}) {
4523 for (
const std::vector<int>& refs : *node_to_refs) {
4524 if (refs.size() == 1) {
4526 ++num_fixed_at_true;
4535 for (
const int ref : refs) {
4545 if (num_true == 1) {
4546 for (
const int ref : refs) {
4547 if (ref != true_ref) {
4548 if (!context_->
IsFixed(ref)) {
4559 if (num_fixed_at_true > 0) {
4566 int circuit_start = -1;
4567 std::vector<int>
next(num_nodes, -1);
4568 std::vector<int> new_in_degree(num_nodes, 0);
4569 std::vector<int> new_out_degree(num_nodes, 0);
4570 for (
int i = 0; i < num_arcs; ++i) {
4571 const int ref =
proto.literals(i);
4579 circuit_start =
proto.tails(i);
4583 ++new_out_degree[
proto.tails(i)];
4584 ++new_in_degree[
proto.heads(i)];
4587 proto.set_literals(new_size,
proto.literals(i));
4597 for (
int i = 0; i < num_nodes; ++i) {
4598 if (new_in_degree[i] == 0 || new_out_degree[i] == 0) {
4604 if (circuit_start != -1) {
4605 std::vector<bool> visited(num_nodes,
false);
4606 int current = circuit_start;
4607 while (current != -1 && !visited[current]) {
4608 visited[current] =
true;
4609 current =
next[current];
4611 if (current == circuit_start) {
4614 std::vector<bool> has_self_arc(num_nodes,
false);
4615 for (
int i = 0; i < num_arcs; ++i) {
4616 if (visited[
proto.tails(i)])
continue;
4618 has_self_arc[
proto.tails(i)] =
true;
4624 for (
int n = 0; n < num_nodes; ++n) {
4625 if (!visited[n] && !has_self_arc[n]) {
4627 return MarkConstraintAsFalse(
ct);
4631 return RemoveConstraint(
ct);
4635 if (num_true == new_size) {
4637 return RemoveConstraint(
ct);
4643 for (
int i = 0; i < num_nodes; ++i) {
4644 for (
const std::vector<int>* arc_literals :
4645 {&incoming_arcs[i], &outgoing_arcs[i]}) {
4646 std::vector<int> literals;
4647 for (
const int ref : *arc_literals) {
4653 literals.push_back(ref);
4655 if (literals.size() == 2 && literals[0] !=
NegatedRef(literals[1])) {
4664 if (new_size < num_arcs) {
4665 proto.mutable_tails()->Truncate(new_size);
4666 proto.mutable_heads()->Truncate(new_size);
4667 proto.mutable_literals()->Truncate(new_size);
4674bool CpModelPresolver::PresolveAutomaton(ConstraintProto*
ct) {
4677 AutomatonConstraintProto&
proto = *
ct->mutable_automaton();
4678 if (
proto.vars_size() == 0 ||
proto.transition_label_size() == 0) {
4682 bool all_have_same_affine_relation =
true;
4683 std::vector<AffineRelation::Relation> affine_relations;
4684 for (
int v = 0; v <
proto.vars_size(); ++v) {
4685 const int var =
ct->automaton().vars(v);
4687 affine_relations.push_back(r);
4688 if (r.representative ==
var) {
4689 all_have_same_affine_relation =
false;
4692 if (v > 0 && (r.coeff != affine_relations[v - 1].coeff ||
4693 r.offset != affine_relations[v - 1].offset)) {
4694 all_have_same_affine_relation =
false;
4699 if (all_have_same_affine_relation) {
4700 for (
int v = 0; v <
proto.vars_size(); ++v) {
4703 const AffineRelation::Relation rep = affine_relations.front();
4705 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
4706 const int64_t label =
proto.transition_label(t);
4707 int64_t inverse_label = (label - rep.offset) / rep.coeff;
4708 if (inverse_label * rep.coeff + rep.offset == label) {
4709 if (new_size != t) {
4710 proto.set_transition_tail(new_size,
proto.transition_tail(t));
4711 proto.set_transition_head(new_size,
proto.transition_head(t));
4713 proto.set_transition_label(new_size, inverse_label);
4717 if (new_size <
proto.transition_tail_size()) {
4718 proto.mutable_transition_tail()->Truncate(new_size);
4719 proto.mutable_transition_label()->Truncate(new_size);
4720 proto.mutable_transition_head()->Truncate(new_size);
4728 for (
int v = 1; v <
proto.vars_size(); ++v) {
4733 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
4734 const int64_t label =
proto.transition_label(t);
4735 if (hull.Contains(label)) {
4736 if (new_size != t) {
4737 proto.set_transition_tail(new_size,
proto.transition_tail(t));
4738 proto.set_transition_label(new_size, label);
4739 proto.set_transition_head(new_size,
proto.transition_head(t));
4744 if (new_size <
proto.transition_tail_size()) {
4745 proto.mutable_transition_tail()->Truncate(new_size);
4746 proto.mutable_transition_label()->Truncate(new_size);
4747 proto.mutable_transition_head()->Truncate(new_size);
4752 const int n =
proto.vars_size();
4753 const std::vector<int> vars = {
proto.vars().begin(),
proto.vars().end()};
4756 std::vector<std::set<int64_t>> reachable_states(n + 1);
4757 reachable_states[0].insert(
proto.starting_state());
4758 reachable_states[n] = {
proto.final_states().begin(),
4759 proto.final_states().end()};
4763 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
4764 const int64_t
tail =
proto.transition_tail(t);
4765 const int64_t label =
proto.transition_label(t);
4766 const int64_t
head =
proto.transition_head(t);
4769 reachable_states[
time + 1].insert(
head);
4773 std::vector<std::set<int64_t>> reached_values(n);
4777 std::set<int64_t> new_set;
4778 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
4779 const int64_t
tail =
proto.transition_tail(t);
4780 const int64_t label =
proto.transition_label(t);
4781 const int64_t
head =
proto.transition_head(t);
4786 new_set.insert(
tail);
4787 reached_values[
time].insert(label);
4789 reachable_states[
time].swap(new_set);
4792 bool removed_values =
false;
4797 {reached_values[time].begin(), reached_values[time].end()}),
4802 if (removed_values) {
4808bool CpModelPresolver::PresolveReservoir(ConstraintProto*
ct) {
4812 ReservoirConstraintProto&
proto = *
ct->mutable_reservoir();
4813 bool changed =
false;
4814 for (LinearExpressionProto& exp : *(
proto.mutable_time_exprs())) {
4815 changed |= CanonicalizeLinearExpression(*
ct, &exp);
4818 if (
proto.active_literals().empty()) {
4820 for (
int i = 0; i <
proto.time_exprs_size(); ++i) {
4821 proto.add_active_literals(true_literal);
4826 const auto& demand_is_null = [&](
int i) {
4827 return proto.level_changes(i) == 0 ||
4833 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
4834 if (demand_is_null(i)) num_zeros++;
4837 if (num_zeros > 0) {
4840 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
4841 if (demand_is_null(i))
continue;
4842 proto.set_level_changes(new_size,
proto.level_changes(i));
4843 *
proto.mutable_time_exprs(new_size) =
proto.time_exprs(i);
4844 proto.set_active_literals(new_size,
proto.active_literals(i));
4848 proto.mutable_level_changes()->Truncate(new_size);
4849 proto.mutable_time_exprs()->erase(
4850 proto.mutable_time_exprs()->begin() + new_size,
4851 proto.mutable_time_exprs()->end());
4852 proto.mutable_active_literals()->Truncate(new_size);
4855 "reservoir: remove zero level_changes or inactive events.");
4858 const int num_events =
proto.level_changes_size();
4860 proto.level_changes().empty() ? 0 : std::abs(
proto.level_changes(0));
4861 int num_positives = 0;
4862 int num_negatives = 0;
4863 int64_t max_sum_of_positive_level_changes = 0;
4864 int64_t min_sum_of_negative_level_changes = 0;
4865 for (
int i = 0; i < num_events; ++i) {
4870 max_sum_of_positive_level_changes +=
demand;
4874 min_sum_of_negative_level_changes +=
demand;
4878 if (min_sum_of_negative_level_changes >=
proto.min_level() &&
4879 max_sum_of_positive_level_changes <=
proto.max_level()) {
4881 return RemoveConstraint(
ct);
4884 if (min_sum_of_negative_level_changes >
proto.max_level() ||
4885 max_sum_of_positive_level_changes <
proto.min_level()) {
4890 if (min_sum_of_negative_level_changes >
proto.min_level()) {
4891 proto.set_min_level(min_sum_of_negative_level_changes);
4893 "reservoir: increase min_level to reachable value");
4896 if (max_sum_of_positive_level_changes <
proto.max_level()) {
4897 proto.set_max_level(max_sum_of_positive_level_changes);
4898 context_->
UpdateRuleStats(
"reservoir: reduce max_level to reachable value");
4901 if (
proto.min_level() <= 0 &&
proto.max_level() >= 0 &&
4902 (num_positives == 0 || num_negatives == 0)) {
4907 int64_t fixed_contrib = 0;
4908 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
4912 const int active =
proto.active_literals(i);
4914 sum->add_vars(active);
4918 sum->add_coeffs(-
demand);
4922 sum->add_domain(
proto.min_level() - fixed_contrib);
4923 sum->add_domain(
proto.max_level() - fixed_contrib);
4925 return RemoveConstraint(
ct);
4929 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
4930 proto.set_level_changes(i,
proto.level_changes(i) / gcd);
4936 const Domain reduced_domain = Domain({
proto.min_level(),
proto.max_level()})
4937 .InverseMultiplicationBy(gcd);
4938 proto.set_min_level(reduced_domain.Min());
4939 proto.set_max_level(reduced_domain.Max());
4941 "reservoir: simplify level_changes and levels by gcd.");
4944 if (num_positives == 1 && num_negatives > 0) {
4946 "TODO reservoir: one producer, multiple consumers.");
4949 absl::flat_hash_set<std::tuple<int, int64_t, int64_t, int>> time_active_set;
4950 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
4951 const LinearExpressionProto&
time =
proto.time_exprs(i);
4955 const std::tuple<int, int64_t, int64_t, int> key = std::make_tuple(
4958 proto.active_literals(i));
4959 if (time_active_set.contains(key)) {
4960 context_->
UpdateRuleStats(
"TODO reservoir: merge synchronized events.");
4963 time_active_set.insert(key);
4973void CpModelPresolver::ExtractBoolAnd() {
4974 absl::flat_hash_map<int, int> ref_to_bool_and;
4976 std::vector<int> to_remove;
4977 for (
int c = 0; c < num_constraints; ++c) {
4981 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr &&
4982 ct.bool_or().literals().size() == 2) {
4986 to_remove.push_back(c);
4990 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne &&
4991 ct.at_most_one().literals().size() == 2) {
4992 AddImplication(
ct.at_most_one().literals(0),
4995 to_remove.push_back(c);
5001 for (
const int c : to_remove) {
5010void CpModelPresolver::Probe() {
5018 auto* implication_graph =
model.GetOrCreate<BinaryImplicationGraph>();
5019 auto* sat_solver =
model.GetOrCreate<SatSolver>();
5020 auto* mapping =
model.GetOrCreate<CpModelMapping>();
5021 auto* prober =
model.GetOrCreate<Prober>();
5022 prober->ProbeBooleanVariables(1.0);
5024 model.GetOrCreate<TimeLimit>()->GetElapsedDeterministicTime());
5025 if (sat_solver->IsModelUnsat() || !implication_graph->DetectEquivalences()) {
5030 CHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
5031 for (
int i = 0; i < sat_solver->LiteralTrail().
Index(); ++i) {
5032 const Literal l = sat_solver->LiteralTrail()[i];
5033 const int var = mapping->GetProtoVariableFromBooleanVariable(l.Variable());
5041 auto* integer_trail =
model.GetOrCreate<IntegerTrail>();
5042 for (
int var = 0;
var < num_variables; ++
var) {
5045 if (!mapping->IsBoolean(
var)) {
5048 integer_trail->InitialVariableDomain(mapping->Integer(
var)))) {
5055 const Literal l = mapping->Literal(
var);
5056 const Literal r = implication_graph->RepresentativeOf(l);
5059 mapping->GetProtoVariableFromBooleanVariable(r.Variable());
5069void CpModelPresolver::PresolvePureSatPart() {
5075 SatPostsolver sat_postsolver(num_variables);
5076 SatPresolver sat_presolver(&sat_postsolver, logger_);
5077 sat_presolver.SetNumVariables(num_variables);
5078 sat_presolver.SetTimeLimit(context_->
time_limit());
5080 SatParameters params = context_->
params();
5087 if (params.debug_postsolve_with_full_solver()) {
5094 params.set_presolve_use_bva(
false);
5095 sat_presolver.SetParameters(params);
5098 absl::flat_hash_set<int> used_variables;
5099 auto convert = [&used_variables](
int ref) {
5101 if (
RefIsPositive(ref))
return Literal(BooleanVariable(ref),
true);
5102 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
5112 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr ||
5113 ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
5132 std::vector<Literal> clause;
5133 int num_removed_constraints = 0;
5137 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
5138 ++num_removed_constraints;
5140 for (
const int ref :
ct.bool_or().literals()) {
5141 clause.push_back(convert(ref));
5143 for (
const int ref :
ct.enforcement_literal()) {
5144 clause.push_back(convert(ref).Negated());
5146 sat_presolver.AddClause(clause);
5153 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
5154 ++num_removed_constraints;
5155 std::vector<Literal> clause;
5156 for (
const int ref :
ct.enforcement_literal()) {
5157 clause.push_back(convert(ref).Negated());
5160 for (
const int ref :
ct.bool_and().literals()) {
5161 clause.back() = convert(ref);
5162 sat_presolver.AddClause(clause);
5172 if (num_removed_constraints == 0)
return;
5182 std::vector<bool> can_be_removed(num_variables,
false);
5183 for (
int i = 0; i < num_variables; ++i) {
5185 can_be_removed[i] =
true;
5191 if (used_variables.contains(i) && context_->
IsFixed(i)) {
5193 sat_presolver.AddClause({convert(i)});
5195 sat_presolver.AddClause({convert(
NegatedRef(i))});
5203 const int num_passes = params.presolve_use_bva() ? 4 : 1;
5204 for (
int i = 0; i < num_passes; ++i) {
5205 const int old_num_clause = sat_postsolver.NumClauses();
5206 if (!sat_presolver.Presolve(can_be_removed)) {
5207 VLOG(1) <<
"UNSAT during SAT presolve.";
5210 if (old_num_clause == sat_postsolver.NumClauses())
break;
5214 const int new_num_variables = sat_presolver.NumVariables();
5216 VLOG(1) <<
"New variables added by the SAT presolver.";
5218 i < new_num_variables; ++i) {
5219 IntegerVariableProto* var_proto =
5222 var_proto->add_domain(1);
5228 ExtractClauses(
true, sat_presolver, context_->
working_model);
5236 ExtractClauses(
false, sat_postsolver,
5244void CpModelPresolver::ExpandObjective() {
5263 int unique_expanded_constraint = -1;
5264 const bool objective_was_a_single_variable =
5271 absl::flat_hash_set<int> relevant_constraints;
5272 std::vector<int> var_to_num_relevant_constraints(num_variables, 0);
5273 for (
int ct_index = 0; ct_index < num_constraints; ++ct_index) {
5276 if (!
ct.enforcement_literal().empty() ||
5277 ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
5278 ct.linear().domain().size() != 2 ||
5279 ct.linear().domain(0) !=
ct.linear().domain(1)) {
5283 relevant_constraints.insert(ct_index);
5284 const int num_terms =
ct.linear().vars_size();
5285 for (
int i = 0; i < num_terms; ++i) {
5286 var_to_num_relevant_constraints[
PositiveRef(
ct.linear().vars(i))]++;
5290 std::set<int> var_to_process;
5292 const int var = entry.first;
5294 if (var_to_num_relevant_constraints[
var] != 0) {
5295 var_to_process.insert(
var);
5300 int num_expansions = 0;
5301 int last_expanded_objective_var;
5302 absl::flat_hash_set<int> processed_vars;
5303 std::vector<int> new_vars_in_objective;
5304 while (!relevant_constraints.empty()) {
5306 int objective_var = -1;
5307 while (!var_to_process.empty()) {
5308 const int var = *var_to_process.begin();
5309 CHECK(!processed_vars.contains(
var));
5310 if (var_to_num_relevant_constraints[
var] == 0) {
5311 processed_vars.insert(
var);
5312 var_to_process.erase(
var);
5317 var_to_process.erase(
var);
5320 objective_var =
var;
5324 if (objective_var == -1)
break;
5326 processed_vars.insert(objective_var);
5327 var_to_process.erase(objective_var);
5329 int expanded_linear_index = -1;
5330 int64_t objective_coeff_in_expanded_constraint;
5331 int64_t size_of_expanded_constraint = 0;
5332 const auto& non_deterministic_list =
5334 std::vector<int> constraints_with_objective(non_deterministic_list.begin(),
5335 non_deterministic_list.end());
5336 std::sort(constraints_with_objective.begin(),
5337 constraints_with_objective.end());
5338 for (
const int ct_index : constraints_with_objective) {
5339 if (relevant_constraints.count(ct_index) == 0)
continue;
5340 const ConstraintProto&
ct =
5345 relevant_constraints.erase(ct_index);
5346 const int num_terms =
ct.linear().vars_size();
5347 for (
int i = 0; i < num_terms; ++i) {
5348 var_to_num_relevant_constraints[
PositiveRef(
ct.linear().vars(i))]--;
5360 bool is_present =
false;
5361 int64_t objective_coeff;
5362 for (
int i = 0; i < num_terms; ++i) {
5363 const int ref =
ct.linear().vars(i);
5364 const int64_t
coeff =
ct.linear().coeffs(i);
5366 CHECK(!is_present) <<
"Duplicate variables not supported.";
5368 objective_coeff = (ref == objective_var) ?
coeff : -
coeff;
5381 if (std::abs(objective_coeff) == 1 &&
5382 num_terms > size_of_expanded_constraint) {
5383 expanded_linear_index = ct_index;
5384 size_of_expanded_constraint = num_terms;
5385 objective_coeff_in_expanded_constraint = objective_coeff;
5389 if (expanded_linear_index != -1) {
5392 CHECK_EQ(std::abs(objective_coeff_in_expanded_constraint), 1);
5393 const ConstraintProto&
ct =
5396 objective_var, objective_coeff_in_expanded_constraint,
ct,
5397 &new_vars_in_objective)) {
5402 context_->
UpdateRuleStats(
"objective: expanded objective constraint.");
5405 for (
const int var : new_vars_in_objective) {
5406 if (!processed_vars.contains(
var)) var_to_process.insert(
var);
5419 for (
int i = 0; i < size_of_expanded_constraint; ++i) {
5420 const int ref =
ct.linear().vars(i);
5425 -
ct.linear().coeffs(i)))
5426 .RelaxIfTooComplex();
5428 implied_domain = implied_domain.InverseMultiplicationBy(
5429 objective_coeff_in_expanded_constraint);
5433 if (implied_domain.IsIncludedIn(context_->
DomainOf(objective_var))) {
5435 context_->
UpdateRuleStats(
"objective: removed objective constraint.");
5441 unique_expanded_constraint = expanded_linear_index;
5446 last_expanded_objective_var = objective_var;
5452 if (num_expansions == 1 && objective_was_a_single_variable &&
5453 unique_expanded_constraint != -1) {
5455 "objective: removed unique objective constraint.");
5457 unique_expanded_constraint);
5459 mutable_ct->
Clear();
5472void CpModelPresolver::MergeNoOverlapConstraints() {
5476 int old_num_no_overlaps = 0;
5477 int old_num_intervals = 0;
5480 std::vector<int> disjunctive_index;
5481 std::vector<std::vector<Literal>> cliques;
5482 for (
int c = 0; c < num_constraints; ++c) {
5484 if (
ct.constraint_case() != ConstraintProto::ConstraintCase::kNoOverlap) {
5487 std::vector<Literal> clique;
5488 for (
const int i :
ct.no_overlap().intervals()) {
5489 clique.push_back(Literal(BooleanVariable(i),
true));
5491 cliques.push_back(clique);
5492 disjunctive_index.push_back(c);
5494 old_num_no_overlaps++;
5495 old_num_intervals += clique.size();
5497 if (old_num_no_overlaps == 0)
return;
5501 local_model.GetOrCreate<Trail>()->Resize(num_constraints);
5502 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
5503 graph->Resize(num_constraints);
5504 for (
const std::vector<Literal>& clique : cliques) {
5507 CHECK(graph->AddAtMostOne(clique));
5509 CHECK(graph->DetectEquivalences());
5510 graph->TransformIntoMaxCliques(
5514 int new_num_no_overlaps = 0;
5515 int new_num_intervals = 0;
5516 for (
int i = 0; i < cliques.size(); ++i) {
5517 const int ct_index = disjunctive_index[i];
5518 ConstraintProto*
ct =
5521 if (cliques[i].empty())
continue;
5522 for (
const Literal l : cliques[i]) {
5523 CHECK(l.IsPositive());
5524 ct->mutable_no_overlap()->add_intervals(l.Variable().value());
5526 new_num_no_overlaps++;
5527 new_num_intervals += cliques[i].size();
5529 if (old_num_intervals != new_num_intervals ||
5530 old_num_no_overlaps != new_num_no_overlaps) {
5531 VLOG(1) << absl::StrCat(
"Merged ", old_num_no_overlaps,
" no-overlaps (",
5532 old_num_intervals,
" intervals) into ",
5533 new_num_no_overlaps,
" no-overlaps (",
5534 new_num_intervals,
" intervals).");
5543void CpModelPresolver::TransformIntoMaxCliques() {
5546 auto convert = [](
int ref) {
5547 if (
RefIsPositive(ref))
return Literal(BooleanVariable(ref),
true);
5548 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
5553 std::vector<std::vector<Literal>> cliques;
5555 for (
int c = 0; c < num_constraints; ++c) {
5557 if (
ct->constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne) {
5558 std::vector<Literal> clique;
5559 for (
const int ref :
ct->at_most_one().literals()) {
5560 clique.push_back(convert(ref));
5562 cliques.push_back(clique);
5563 if (RemoveConstraint(
ct)) {
5566 }
else if (
ct->constraint_case() ==
5567 ConstraintProto::ConstraintCase::kBoolAnd) {
5568 if (
ct->enforcement_literal().size() != 1)
continue;
5569 const Literal enforcement = convert(
ct->enforcement_literal(0));
5570 for (
const int ref :
ct->bool_and().literals()) {
5571 if (ref ==
ct->enforcement_literal(0))
continue;
5572 cliques.push_back({enforcement, convert(ref).Negated()});
5574 if (RemoveConstraint(
ct)) {
5580 int64_t num_literals_before = 0;
5581 const int num_old_cliques = cliques.size();
5586 local_model.GetOrCreate<Trail>()->Resize(num_variables);
5587 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
5588 graph->Resize(num_variables);
5589 for (
const std::vector<Literal>& clique : cliques) {
5590 num_literals_before += clique.size();
5591 if (!graph->AddAtMostOne(clique)) {
5595 if (!graph->DetectEquivalences()) {
5598 graph->TransformIntoMaxCliques(
5604 for (
int var = 0;
var < num_variables; ++
var) {
5605 const Literal l = Literal(BooleanVariable(
var),
true);
5606 if (graph->RepresentativeOf(l) != l) {
5607 const Literal r = graph->RepresentativeOf(l);
5609 var, r.IsPositive() ? r.Variable().value()
5614 int num_new_cliques = 0;
5615 int64_t num_literals_after = 0;
5616 for (
const std::vector<Literal>& clique : cliques) {
5617 if (clique.empty())
continue;
5619 num_literals_after += clique.size();
5621 for (
const Literal
literal : clique) {
5623 ct->mutable_at_most_one()->add_literals(
literal.Variable().value());
5625 ct->mutable_at_most_one()->add_literals(
5631 PresolveAtMostOne(
ct);
5634 if (num_new_cliques != num_old_cliques) {
5635 context_->
UpdateRuleStats(
"at_most_one: transformed into max clique.");
5638 if (num_old_cliques != num_new_cliques ||
5639 num_literals_before != num_literals_after) {
5640 SOLVER_LOG(logger_,
"[MaxClique] Merged ", num_old_cliques,
"(",
5641 num_literals_before,
" literals) into ", num_new_cliques,
"(",
5642 num_literals_after,
" literals) at_most_ones.");
5648bool IsAffineIntAbs(ConstraintProto*
ct) {
5650 ct->lin_max().exprs_size() != 2 ||
5651 ct->lin_max().target().vars_size() > 1 ||
5652 ct->lin_max().exprs(0).vars_size() != 1 ||
5653 ct->lin_max().exprs(1).vars_size() != 1) {
5657 const LinearArgumentProto& lin_max =
ct->lin_max();
5658 if (lin_max.exprs(0).offset() != -lin_max.exprs(1).offset())
return false;
5664 const int64_t left_coeff =
RefIsPositive(lin_max.exprs(0).vars(0))
5665 ? lin_max.exprs(0).coeffs(0)
5666 : -lin_max.exprs(0).coeffs(0);
5667 const int64_t right_coeff =
RefIsPositive(lin_max.exprs(1).vars(0))
5668 ? lin_max.exprs(1).coeffs(0)
5669 : -lin_max.exprs(1).coeffs(0);
5670 return left_coeff == -right_coeff;
5680 if (ExploitEquivalenceRelations(c,
ct)) {
5685 if (PresolveEnforcementLiteral(
ct)) {
5690 switch (
ct->constraint_case()) {
5691 case ConstraintProto::ConstraintCase::kBoolOr:
5692 return PresolveBoolOr(
ct);
5693 case ConstraintProto::ConstraintCase::kBoolAnd:
5694 return PresolveBoolAnd(
ct);
5695 case ConstraintProto::ConstraintCase::kAtMostOne:
5696 return PresolveAtMostOne(
ct);
5697 case ConstraintProto::ConstraintCase::kExactlyOne:
5698 return PresolveExactlyOne(
ct);
5699 case ConstraintProto::ConstraintCase::kBoolXor:
5700 return PresolveBoolXor(
ct);
5701 case ConstraintProto::ConstraintCase::kLinMax:
5702 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_lin_max())) {
5705 if (IsAffineIntAbs(
ct)) {
5706 return PresolveIntAbs(
ct);
5708 return PresolveLinMax(
ct);
5710 case ConstraintProto::ConstraintCase::kIntProd:
5711 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_int_prod())) {
5714 return PresolveIntProd(
ct);
5715 case ConstraintProto::ConstraintCase::kIntDiv:
5716 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_int_div())) {
5719 return PresolveIntDiv(
ct);
5720 case ConstraintProto::ConstraintCase::kIntMod:
5721 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_int_mod())) {
5724 return PresolveIntMod(
ct);
5725 case ConstraintProto::ConstraintCase::kLinear: {
5734 for (
const int ref :
ct->linear().vars()) {
5740 if (CanonicalizeLinear(
ct)) {
5743 if (PropagateDomainsInLinear(c,
ct)) {
5746 if (PresolveSmallLinear(
ct)) {
5749 if (PresolveLinearEqualityWithModulo(
ct)) {
5753 if (RemoveSingletonInLinear(
ct)) {
5758 if (PresolveSmallLinear(
ct)) {
5762 if (PresolveSmallLinear(
ct)) {
5765 if (PresolveLinearOnBooleans(
ct)) {
5769 const int old_num_enforcement_literals =
ct->enforcement_literal_size();
5770 ExtractEnforcementLiteralFromLinearConstraint(c,
ct);
5771 if (
ct->constraint_case() ==
5772 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
5776 if (
ct->enforcement_literal_size() > old_num_enforcement_literals &&
5777 PresolveSmallLinear(
ct)) {
5786 DetectAndProcessOneSidedLinearConstraint(c,
ct)) {
5791 case ConstraintProto::ConstraintCase::kInterval:
5792 return PresolveInterval(c,
ct);
5793 case ConstraintProto::ConstraintCase::kInverse:
5794 return PresolveInverse(
ct);
5795 case ConstraintProto::ConstraintCase::kElement:
5796 return PresolveElement(
ct);
5797 case ConstraintProto::ConstraintCase::kTable:
5798 return PresolveTable(
ct);
5799 case ConstraintProto::ConstraintCase::kAllDiff:
5800 return PresolveAllDiff(
ct);
5801 case ConstraintProto::ConstraintCase::kNoOverlap:
5802 return PresolveNoOverlap(
ct);
5803 case ConstraintProto::ConstraintCase::kNoOverlap2D:
5804 return PresolveNoOverlap2D(c,
ct);
5805 case ConstraintProto::ConstraintCase::kCumulative:
5806 return PresolveCumulative(
ct);
5807 case ConstraintProto::ConstraintCase::kCircuit:
5808 return PresolveCircuit(
ct);
5809 case ConstraintProto::ConstraintCase::kRoutes:
5810 return PresolveRoutes(
ct);
5811 case ConstraintProto::ConstraintCase::kAutomaton:
5812 return PresolveAutomaton(
ct);
5813 case ConstraintProto::ConstraintCase::kReservoir:
5814 return PresolveReservoir(
ct);
5824bool CpModelPresolver::ProcessSetPPCSubset(
5825 int c1,
int c2,
const std::vector<int>& c2_minus_c1,
5826 const std::vector<int>& original_constraint_index,
5827 std::vector<bool>* marked_for_removal) {
5830 CHECK(!(*marked_for_removal)[c1]);
5831 CHECK(!(*marked_for_removal)[c2]);
5834 original_constraint_index[c1]);
5836 original_constraint_index[c2]);
5846 for (
const int literal : c2_minus_c1) {
5853 ConstraintProto copy = *ct2;
5859 (*marked_for_removal)[c1] =
true;
5870 (*marked_for_removal)[c2] =
true;
5880 (*marked_for_removal)[c1] =
true;
5897 int num_matches = 0;
5898 for (
int i = 0; i < ct2->
linear().vars().size(); ++i) {
5900 if (literals.contains(
var)) {
5908 if (num_matches != literals.size())
return true;
5914 for (
int i = 0; i < ct2->
linear().vars().size(); ++i) {
5917 if (literals.contains(
var)) {
5919 if (
coeff == min_coeff)
continue;
5946bool CpModelPresolver::ProcessSetPPC() {
5951 std::vector<uint64_t> signatures;
5955 std::vector<std::vector<int>> constraint_literals;
5959 std::vector<std::vector<int>> literals_to_constraints;
5962 std::vector<bool> removed;
5966 std::vector<int> original_constraint_index;
5970 int num_setppc_constraints = 0;
5971 std::vector<int> temp_literals;
5973 for (
int c = 0; c < num_constraints; ++c) {
5985 constraint_literals.push_back(GetLiteralsFromSetPPCConstraint(*
ct));
5996 const int size =
ct->linear().vars().size();
5997 if (size <= 2)
continue;
6002 temp_literals.clear();
6003 for (
int i = 0; i < size; ++i) {
6004 const int var =
ct->linear().vars(i);
6005 const int64_t
coeff =
ct->linear().coeffs(i);
6008 if (
coeff < 0)
continue;
6009 temp_literals.push_back(
var);
6011 if (temp_literals.size() <= 2)
continue;
6012 constraint_literals.push_back(temp_literals);
6017 uint64_t signature = 0;
6018 for (
const int literal : constraint_literals.back()) {
6020 signature |= (int64_t{1} << (positive_literal % 64));
6022 if (positive_literal >= literals_to_constraints.size()) {
6023 literals_to_constraints.resize(positive_literal + 1);
6025 literals_to_constraints[positive_literal].push_back(
6026 num_setppc_constraints);
6028 signatures.push_back(signature);
6029 removed.push_back(
false);
6030 original_constraint_index.push_back(c);
6031 num_setppc_constraints++;
6033 VLOG(1) <<
"#setppc constraints: " << num_setppc_constraints;
6036 absl::flat_hash_set<std::pair<int, int>> compared_constraints;
6037 for (
const std::vector<int>& literal_to_constraints :
6038 literals_to_constraints) {
6039 for (
int index1 = 0; index1 < literal_to_constraints.size(); ++index1) {
6042 const int c1 = literal_to_constraints[index1];
6043 if (removed[c1])
continue;
6044 const std::vector<int>& c1_literals = constraint_literals[c1];
6046 for (
int index2 = index1 + 1; index2 < literal_to_constraints.size();
6048 const int c2 = literal_to_constraints[index2];
6049 if (removed[c2])
continue;
6050 if (removed[c1])
break;
6053 if (c1 == c2)
continue;
6056 const auto [_, inserted] = compared_constraints.insert({c1, c2});
6057 if (!inserted)
continue;
6061 if (compared_constraints.size() >= 50000)
return true;
6063 const bool smaller = (signatures[c1] & ~signatures[c2]) == 0;
6064 const bool larger = (signatures[c2] & ~signatures[c1]) == 0;
6065 if (!(smaller || larger))
continue;
6068 const std::vector<int>& c2_literals = constraint_literals[c2];
6072 std::vector<int> c1_minus_c2;
6074 std::vector<int> c2_minus_c1;
6077 if (c1_minus_c2.empty()) {
6078 if (!ProcessSetPPCSubset(c1, c2, c2_minus_c1,
6079 original_constraint_index, &removed)) {
6082 }
else if (c2_minus_c1.empty()) {
6083 if (!ProcessSetPPCSubset(c2, c1, c1_minus_c2,
6084 original_constraint_index, &removed)) {
6103bool CpModelPresolver::ProcessEncodingFromLinear(
6104 const int linear_encoding_ct_index,
6105 const ConstraintProto& at_most_or_exactly_one, int64_t* num_unique_terms,
6106 int64_t* num_multiple_terms) {
6108 bool in_exactly_one =
false;
6109 absl::flat_hash_map<int, int> var_to_ref;
6111 for (
const int ref : at_most_or_exactly_one.at_most_one().literals()) {
6116 in_exactly_one =
true;
6117 for (
const int ref : at_most_or_exactly_one.exactly_one().literals()) {
6124 const ConstraintProto& linear_encoding =
6128 std::vector<std::pair<int, int64_t>> ref_to_coeffs;
6129 const int num_terms = linear_encoding.linear().vars().size();
6130 for (
int i = 0; i < num_terms; ++i) {
6131 const int ref = linear_encoding.linear().vars(i);
6132 const int64_t
coeff = linear_encoding.linear().coeffs(i);
6133 const auto it = var_to_ref.find(
PositiveRef(ref));
6135 if (it == var_to_ref.end()) {
6144 if (it->second == ref) {
6146 ref_to_coeffs.push_back({ref,
coeff});
6158 context_->
UpdateRuleStats(
"encoding: candidate linear is all Boolean now.");
6163 std::vector<int64_t> all_values;
6164 std::map<int64_t, std::vector<int>> value_to_refs;
6165 for (
const auto& [ref,
coeff] : ref_to_coeffs) {
6167 all_values.push_back(
value);
6168 value_to_refs[
value].push_back(ref);
6172 for (
const auto& [
var, ref] : var_to_ref) {
6173 all_values.push_back(rhs);
6174 value_to_refs[rhs].push_back(ref);
6176 if (!in_exactly_one) {
6179 all_values.push_back(rhs);
6184 bool domain_reduced =
false;
6188 if (domain_reduced) {
6194 context_->
UpdateRuleStats(
"encoding: candidate linear is all Boolean now.");
6199 absl::flat_hash_set<int64_t> value_set;
6200 for (
const int64_t v : context_->
DomainOf(target_ref).
Values()) {
6201 value_set.insert(v);
6203 for (
const auto& [
value, literals] : value_to_refs) {
6205 if (!value_set.contains(
value)) {
6206 for (
const int lit : literals) {
6212 if (literals.size() == 1 && (in_exactly_one ||
value != rhs)) {
6215 ++*num_unique_terms;
6220 ++*num_multiple_terms;
6221 const int associated_lit =
6223 for (
const int lit : literals) {
6229 if (in_exactly_one ||
value != rhs) {
6236 for (
const int lit : literals) bool_or->
add_literals(lit);
6237 bool_or->add_literals(
NegatedRef(associated_lit));
6253uint64_t ComputeSignature(
const std::vector<int>& integers) {
6254 uint64_t signature = 0;
6255 for (
const int i : integers) signature |= (int64_t{1} << (i & 63));
6261void CpModelPresolver::ExtractEncodingFromLinear() {
6270 std::vector<int> vars;
6271 bool is_exactly_one;
6273 std::vector<Superset> potential_supersets;
6277 std::vector<int> vars;
6279 std::vector<Subset> potential_subsets;
6283 for (
int c = 0; c < num_constraints; ++c) {
6285 switch (
ct.constraint_case()) {
6287 std::vector<int> vars;
6288 for (
const int ref :
ct.at_most_one().literals()) {
6291 potential_supersets.push_back({c, std::move(vars),
false});
6295 std::vector<int> vars;
6296 for (
const int ref :
ct.exactly_one().literals()) {
6299 potential_supersets.push_back({c, std::move(vars),
true});
6304 if (!
ct.enforcement_literal().empty())
continue;
6305 if (
ct.linear().domain().size() != 2)
continue;
6306 if (
ct.linear().domain(0) !=
ct.linear().domain(1))
continue;
6310 std::vector<int> vars;
6311 bool is_candidate =
true;
6312 int num_integers = 0;
6313 const int num_terms =
ct.linear().vars().size();
6314 for (
int i = 0; i < num_terms; ++i) {
6315 const int ref =
ct.linear().vars(i);
6320 if (std::abs(
ct.linear().coeffs(i)) != 1) {
6321 is_candidate =
false;
6324 if (num_integers == 2) {
6325 is_candidate =
false;
6333 if (is_candidate && num_integers == 1 && vars.size() > 1) {
6334 potential_subsets.push_back({c, std::move(vars)});
6343 if (potential_supersets.empty())
return;
6344 if (potential_subsets.empty())
return;
6348 std::sort(potential_supersets.begin(), potential_supersets.end(),
6349 [](
const Superset&
a,
const Superset&
b) {
6350 const int size_a = a.vars.size();
6351 const int size_b = b.vars.size();
6352 return std::tie(size_a, a.is_exactly_one) <
6353 std::tie(size_b, b.is_exactly_one);
6355 std::sort(potential_subsets.begin(), potential_subsets.end(),
6356 [](
const Subset&
a,
const Subset&
b) {
6357 return a.vars.size() < b.vars.size();
6361 int64_t num_exactly_one_encodings = 0;
6362 int64_t num_at_most_one_encodings = 0;
6363 int64_t num_literals = 0;
6364 int64_t num_unique_terms = 0;
6365 int64_t num_multiple_terms = 0;
6371 int subset_index = 0;
6372 std::vector<uint64_t> signatures;
6373 std::vector<std::vector<int>> one_watcher;
6374 std::vector<bool> is_in_superset;
6375 for (
const Superset& superset : potential_supersets) {
6377 const int superset_size = superset.vars.size();
6378 for (; subset_index < potential_subsets.size(); ++subset_index) {
6379 const std::vector<int>& vars = potential_subsets[subset_index].vars;
6380 if (vars.size() > superset_size)
break;
6383 int best_choice = -1;
6384 for (
const int var : vars) {
6385 if (one_watcher.size() <=
var) one_watcher.resize(
var + 1);
6386 if (best_choice == -1 ||
6387 one_watcher[
var].size() < one_watcher[best_choice].size()) {
6391 one_watcher[best_choice].push_back(subset_index);
6392 CHECK_EQ(signatures.size(), subset_index);
6393 signatures.push_back(ComputeSignature(vars));
6397 DCHECK(absl::c_all_of(is_in_superset, [](
bool b) {
return !
b; }));
6398 for (
const int var : superset.vars) {
6399 if (
var >= is_in_superset.size()) {
6400 is_in_superset.resize(
var + 1,
false);
6402 is_in_superset[
var] =
true;
6405 const int max_size =
std::max(one_watcher.size(), is_in_superset.size());
6406 one_watcher.resize(max_size);
6407 is_in_superset.resize(max_size,
false);
6410 const uint64_t superset_signature = ComputeSignature(superset.vars);
6411 for (
const int superset_var : superset.vars) {
6412 for (
int i = 0; i < one_watcher[superset_var].size(); ++i) {
6413 const int subset_index = one_watcher[superset_var][i];
6414 const Subset& subset = potential_subsets[subset_index];
6415 CHECK_LE(subset.vars.size(), superset_size);
6418 if ((signatures[subset_index] & ~superset_signature) != 0)
continue;
6421 bool is_included =
true;
6422 for (
const int subset_var : subset.vars) {
6423 if (!is_in_superset[subset_var]) {
6424 is_included =
false;
6428 if (!is_included)
continue;
6430 if (!superset.is_exactly_one) {
6431 ++num_at_most_one_encodings;
6433 ++num_exactly_one_encodings;
6435 num_literals += subset.vars.size();
6438 if (!ProcessEncodingFromLinear(
6440 &num_unique_terms, &num_multiple_terms)) {
6447 one_watcher[superset_var].back());
6448 one_watcher[superset_var].pop_back();
6454 for (
const int var : superset.vars) {
6455 is_in_superset[
var] =
false;
6459 SOLVER_LOG(logger_,
"[ExtractEncodingFromLinear]",
6460 " #potential_supersets=", potential_supersets.size(),
6461 " #potential_subsets=", potential_subsets.size(),
6462 " #at_most_one_encodings=", num_at_most_one_encodings,
6463 " #exactly_one_encodings=", num_exactly_one_encodings,
6464 " #unique_terms=", num_unique_terms,
6465 " #multiple_terms=", num_multiple_terms,
6466 " #literals=", num_literals,
" time=",
wall_timer.
Get(),
"s");
6469void CpModelPresolver::TryToSimplifyDomain(
int var) {
6478 if (r.representative !=
var)
return;
6498 absl::flat_hash_set<int64_t> values_set;
6499 absl::flat_hash_map<int64_t, std::vector<int>> value_to_equal_literals;
6500 absl::flat_hash_map<int64_t, std::vector<int>> value_to_not_equal_literals;
6503 if (c < 0)
continue;
6507 int64_t
coeff =
ct.linear().coeffs(0);
6508 if (std::abs(
coeff) != 1 ||
ct.enforcement_literal().size() != 1) {
6516 if (rhs.IsFixed()) {
6522 values_set.insert(rhs.FixedValue());
6523 value_to_equal_literals[rhs.FixedValue()].push_back(
6524 ct.enforcement_literal(0));
6527 const Domain complement =
6529 if (complement.IsEmpty()) {
6534 if (complement.IsFixed()) {
6536 values_set.insert(complement.FixedValue());
6537 value_to_not_equal_literals[complement.FixedValue()].push_back(
6538 ct.enforcement_literal(0));
6548 }
else if (value_to_not_equal_literals.empty() &&
6549 value_to_equal_literals.empty()) {
6554 std::vector<int64_t> encoded_values(values_set.begin(), values_set.end());
6555 std::sort(encoded_values.begin(), encoded_values.end());
6556 CHECK(!encoded_values.empty());
6557 const bool is_fully_encoded =
6563 for (
const int64_t v : encoded_values) {
6565 const auto eq_it = value_to_equal_literals.find(v);
6566 if (eq_it != value_to_equal_literals.end()) {
6567 for (
const int lit : eq_it->second) {
6571 const auto neq_it = value_to_not_equal_literals.find(v);
6572 if (neq_it != value_to_not_equal_literals.end()) {
6573 for (
const int lit : neq_it->second) {
6581 Domain other_values;
6582 if (!is_fully_encoded) {
6592 if (is_fully_encoded) {
6596 obj_coeff > 0 ? encoded_values.front() : encoded_values.back();
6605 Domain(obj_coeff > 0 ? other_values.Min() : other_values.Max());
6606 min_value = other_values.FixedValue();
6611 int64_t accumulated = std::abs(min_value);
6612 for (
const int64_t
value : encoded_values) {
6616 "TODO variables: only used in objective and in encoding");
6621 ConstraintProto encoding_ct;
6622 LinearConstraintProto* linear = encoding_ct.mutable_linear();
6623 const int64_t coeff_in_equality = -1;
6624 linear->add_vars(
var);
6625 linear->add_coeffs(coeff_in_equality);
6627 linear->add_domain(-min_value);
6628 linear->add_domain(-min_value);
6629 for (
const int64_t
value : encoded_values) {
6630 if (
value == min_value)
continue;
6634 linear->add_vars(enf);
6635 linear->add_coeffs(
coeff);
6638 linear->set_domain(0, encoding_ct.linear().domain(0) -
coeff);
6639 linear->set_domain(1, encoding_ct.linear().domain(1) -
coeff);
6641 linear->add_coeffs(-
coeff);
6647 "TODO variables: only used in objective and in encoding");
6651 "variables: only used in objective and in encoding");
6658 for (
const int c : copy) {
6659 if (c < 0)
continue;
6666 for (
const int64_t
value : encoded_values) {
6669 ct->add_enforcement_literal(enf);
6670 ct->mutable_linear()->add_vars(
var);
6671 ct->mutable_linear()->add_coeffs(1);
6672 ct->mutable_linear()->add_domain(
value);
6673 ct->mutable_linear()->add_domain(
value);
6678 if (is_fully_encoded) {
6680 for (
const int64_t
value : encoded_values) {
6684 PresolveExactlyOne(new_ct);
6687 ConstraintProto* mapping_ct =
6690 mapping_ct->mutable_linear()->add_coeffs(1);
6693 for (
const int64_t
value : encoded_values) {
6696 new_ct->mutable_at_most_one()->add_literals(
literal);
6698 PresolveAtMostOne(new_ct);
6723 Domain union_of_domain;
6724 int num_positive = 0;
6725 std::vector<int> constraint_indices_to_remove;
6731 constraint_indices_to_remove.push_back(c);
6733 if (
ct.enforcement_literal().size() != 1 ||
6736 ct.linear().vars().size() != 1) {
6740 if (
ct.enforcement_literal(0) ==
var) ++num_positive;
6741 if (ct_var != -1 &&
PositiveRef(
ct.linear().vars(0)) != ct_var) {
6746 union_of_domain = union_of_domain.UnionWith(
6749 ?
ct.linear().coeffs(0)
6750 : -
ct.linear().coeffs(0)));
6752 if (!abort && num_positive == 1) {
6756 context_->
UpdateRuleStats(
"variables: removable enforcement literal");
6757 for (
const int c : constraint_indices_to_remove) {
6776 if (domain.Size() == 2 && (domain.Min() != 0 || domain.Max() != 1)) {
6781 if (domain.NumIntervals() != domain.Size())
return;
6783 const int64_t var_min = domain.Min();
6784 int64_t gcd = domain[1].start - var_min;
6786 const ClosedInterval& i = domain[
index];
6788 const int64_t shifted_value = i.start - var_min;
6792 if (gcd == 1)
break;
6794 if (gcd == 1)
return;
6801void CpModelPresolver::EncodeAllAffineRelations() {
6802 int64_t num_added = 0;
6807 if (r.representative ==
var)
continue;
6814 if (!PresolveAffineRelationIfAny(
var))
break;
6821 auto* arg =
ct->mutable_linear();
6824 arg->add_vars(r.representative);
6825 arg->add_coeffs(-r.coeff);
6826 arg->add_domain(r.offset);
6827 arg->add_domain(r.offset);
6835 if (num_added > 0) {
6836 SOLVER_LOG(logger_, num_added,
" affine relations still in the model.");
6841bool CpModelPresolver::PresolveAffineRelationIfAny(
int var) {
6845 if (r.representative ==
var)
return true;
6864 auto* arg =
ct->mutable_linear();
6867 arg->add_vars(r.representative);
6868 arg->add_coeffs(-r.coeff);
6869 arg->add_domain(r.offset);
6870 arg->add_domain(r.offset);
6876void CpModelPresolver::PresolveToFixPoint() {
6880 const int64_t max_num_operations =
6888 absl::flat_hash_set<std::pair<int, int>> var_constraint_pair_already_called;
6895 std::deque<int> queue;
6896 for (
int c = 0; c < in_queue.size(); ++c) {
6898 ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
6909 std::shuffle(queue.begin(), queue.end(), *context_->
random());
6911 std::sort(queue.begin(), queue.end(), [
this](
int a,
int b) {
6912 const int score_a = context_->ConstraintToVars(a).size();
6913 const int score_b = context_->ConstraintToVars(b).size();
6914 return score_a < score_b || (score_a == score_b && a < b);
6924 const int c = queue.front();
6925 in_queue[c] =
false;
6928 const int old_num_constraint =
6932 SOLVER_LOG(logger_,
"Unsat after presolving constraint #", c,
6933 " (warning, dump might be inconsistent): ",
6938 const int new_num_constraints =
6940 if (new_num_constraints > old_num_constraint) {
6942 in_queue.resize(new_num_constraints,
true);
6943 for (
int c = old_num_constraint; c < new_num_constraints; ++c) {
6966 for (
int v = 0; v < current_num_variables; ++v) {
6968 if (!PresolveAffineRelationIfAny(v))
return;
6973 TryToSimplifyDomain(v);
6982 for (
int v = 0; v < num_vars; ++v) {
6984 if (constraints.size() != 1)
continue;
6985 const int c = *constraints.begin();
6986 if (c < 0)
continue;
6991 if (var_constraint_pair_already_called.contains(
6992 std::pair<int, int>(v, c))) {
6995 var_constraint_pair_already_called.insert({v, c});
7003 for (
int i = 0; i < 2; ++i) {
7014 if (c >= 0 && !in_queue[c]) {
7022 if (!queue.empty() || i == 1)
break;
7032 VarDomination var_dom;
7033 DualBoundStrengthening dual_bound_strengthening;
7035 &dual_bound_strengthening);
7036 if (!dual_bound_strengthening.Strengthen(context_))
return;
7048 std::sort(queue.begin(), queue.end());
7063 for (
int c = 0; c < num_constraints; ++c) {
7065 switch (
ct->constraint_case()) {
7066 case ConstraintProto::ConstraintCase::kNoOverlap:
7068 if (PresolveNoOverlap(
ct)) {
7072 case ConstraintProto::ConstraintCase::kNoOverlap2D:
7074 if (PresolveNoOverlap2D(c,
ct)) {
7078 case ConstraintProto::ConstraintCase::kCumulative:
7080 if (PresolveCumulative(
ct)) {
7084 case ConstraintProto::ConstraintCase::kBoolOr: {
7087 for (
const auto& pair :
7089 bool modified =
false;
7116 const CpModelProto& in_model,
const std::vector<int>& ignored_constraints,
7118 const absl::flat_hash_set<int> ignored_constraints_set(
7119 ignored_constraints.begin(), ignored_constraints.end());
7124 std::vector<int> constraints_using_intervals;
7128 if (ignored_constraints_set.contains(c))
continue;
7131 if (OneEnforcementLiteralIsFalse(
ct))
continue;
7133 switch (
ct.constraint_case()) {
7137 if (!CopyBoolOr(
ct))
return CreateUnsatModel();
7140 if (!CopyBoolAnd(
ct))
return CreateUnsatModel();
7143 if (!CopyLinear(
ct))
return CreateUnsatModel();
7146 if (!CopyAtMostOne(
ct))
return CreateUnsatModel();
7149 if (!CopyExactlyOne(
ct))
return CreateUnsatModel();
7152 if (!CopyInterval(
ct, c))
return CreateUnsatModel();
7156 constraints_using_intervals.push_back(c);
7158 CopyAndMapNoOverlap(
ct);
7163 constraints_using_intervals.push_back(c);
7165 CopyAndMapNoOverlap2D(
ct);
7170 constraints_using_intervals.push_back(c);
7172 CopyAndMapCumulative(
ct);
7181 DCHECK(first_copy || constraints_using_intervals.empty());
7182 for (
const int c : constraints_using_intervals) {
7184 switch (
ct.constraint_case()) {
7186 CopyAndMapNoOverlap(
ct);
7189 CopyAndMapNoOverlap2D(
ct);
7192 CopyAndMapCumulative(
ct);
7195 LOG(DFATAL) <<
"Shouldn't be here.";
7204 temp_enforcement_literals_.clear();
7207 skipped_non_zero_++;
7210 temp_enforcement_literals_.push_back(lit);
7213 temp_enforcement_literals_.end());
7216bool ModelCopy::OneEnforcementLiteralIsFalse(
const ConstraintProto&
ct)
const {
7217 for (
const int lit :
ct.enforcement_literal()) {
7225bool ModelCopy::CopyBoolOr(
const ConstraintProto&
ct) {
7226 temp_literals_.clear();
7227 for (
const int lit :
ct.enforcement_literal()) {
7231 for (
const int lit :
ct.bool_or().literals()) {
7236 skipped_non_zero_++;
7238 temp_literals_.push_back(lit);
7245 ->Add(temp_literals_.begin(), temp_literals_.end());
7246 return !temp_literals_.empty();
7249bool ModelCopy::CopyBoolAnd(
const ConstraintProto&
ct) {
7250 bool at_least_one_false =
false;
7251 int num_non_fixed_literals = 0;
7252 for (
const int lit :
ct.bool_and().literals()) {
7254 at_least_one_false =
true;
7258 num_non_fixed_literals++;
7262 if (at_least_one_false) {
7267 for (
const int lit :
ct.enforcement_literal()) {
7269 skipped_non_zero_++;
7274 return !bool_or->literals().empty();
7275 }
else if (num_non_fixed_literals > 0) {
7277 CopyEnforcementLiterals(
ct, new_ct);
7278 BoolArgumentProto* bool_and = new_ct->mutable_bool_and();
7279 bool_and->mutable_literals()->Reserve(num_non_fixed_literals);
7280 for (
const int lit :
ct.bool_and().literals()) {
7282 skipped_non_zero_++;
7285 bool_and->add_literals(lit);
7291bool ModelCopy::CopyLinear(
const ConstraintProto&
ct) {
7292 non_fixed_variables_.clear();
7293 non_fixed_coefficients_.clear();
7295 for (
int i = 0; i <
ct.linear().vars_size(); ++i) {
7296 const int ref =
ct.linear().vars(i);
7297 const int64_t
coeff =
ct.linear().coeffs(i);
7300 skipped_non_zero_++;
7302 non_fixed_variables_.push_back(ref);
7303 non_fixed_coefficients_.push_back(
coeff);
7307 const Domain new_domain =
7309 if (non_fixed_variables_.empty() && !new_domain.Contains(0)) {
7310 if (
ct.enforcement_literal().empty()) {
7313 temp_literals_.clear();
7314 for (
const int literal :
ct.enforcement_literal()) {
7316 skipped_non_zero_++;
7324 ->Add(temp_literals_.begin(), temp_literals_.end());
7325 return !temp_literals_.empty();
7331 CopyEnforcementLiterals(
ct, new_ct);
7332 LinearConstraintProto* linear = new_ct->mutable_linear();
7333 linear->mutable_vars()->Add(non_fixed_variables_.begin(),
7334 non_fixed_variables_.end());
7335 linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(),
7336 non_fixed_coefficients_.end());
7341bool ModelCopy::CopyAtMostOne(
const ConstraintProto&
ct) {
7343 temp_literals_.clear();
7344 for (
const int lit :
ct.at_most_one().literals()) {
7346 skipped_non_zero_++;
7349 temp_literals_.push_back(lit);
7353 if (temp_literals_.size() <= 1)
return true;
7354 if (num_true > 1)
return false;
7358 CopyEnforcementLiterals(
ct, new_ct);
7359 new_ct->mutable_at_most_one()->mutable_literals()->Add(temp_literals_.begin(),
7360 temp_literals_.end());
7364bool ModelCopy::CopyExactlyOne(
const ConstraintProto&
ct) {
7366 temp_literals_.clear();
7367 for (
const int lit :
ct.exactly_one().literals()) {
7369 skipped_non_zero_++;
7372 temp_literals_.push_back(lit);
7376 if (temp_literals_.empty() || num_true > 1)
return false;
7377 if (temp_literals_.size() == 1 && num_true == 1)
return true;
7381 CopyEnforcementLiterals(
ct, new_ct);
7382 new_ct->mutable_exactly_one()->mutable_literals()->Add(temp_literals_.begin(),
7383 temp_literals_.end());
7387bool ModelCopy::CopyInterval(
const ConstraintProto&
ct,
int c) {
7388 CHECK_EQ(starting_constraint_index_, 0)
7389 <<
"Adding new interval constraints to partially filled model is not "
7396void ModelCopy::CopyAndMapNoOverlap(
const ConstraintProto&
ct) {
7401 for (
const int index :
ct.no_overlap().intervals()) {
7402 const auto it = interval_mapping_.find(
index);
7403 if (it == interval_mapping_.end())
continue;
7404 new_ct->add_intervals(it->second);
7408void ModelCopy::CopyAndMapNoOverlap2D(
const ConstraintProto&
ct) {
7413 ct.no_overlap_2d().boxes_with_null_area_can_overlap());
7415 const int num_intervals =
ct.no_overlap_2d().x_intervals().size();
7416 new_ct->mutable_x_intervals()->Reserve(num_intervals);
7417 new_ct->mutable_y_intervals()->Reserve(num_intervals);
7418 for (
int i = 0; i < num_intervals; ++i) {
7419 const auto x_it = interval_mapping_.find(
ct.no_overlap_2d().x_intervals(i));
7420 if (x_it == interval_mapping_.end())
continue;
7421 const auto y_it = interval_mapping_.find(
ct.no_overlap_2d().y_intervals(i));
7422 if (y_it == interval_mapping_.end())
continue;
7423 new_ct->add_x_intervals(x_it->second);
7424 new_ct->add_y_intervals(y_it->second);
7428void ModelCopy::CopyAndMapCumulative(
const ConstraintProto&
ct) {
7434 const int num_intervals =
ct.cumulative().intervals().size();
7435 new_ct->mutable_intervals()->Reserve(num_intervals);
7436 new_ct->mutable_demands()->Reserve(num_intervals);
7437 for (
int i = 0; i < num_intervals; ++i) {
7438 const auto it = interval_mapping_.find(
ct.cumulative().intervals(i));
7439 if (it == interval_mapping_.end())
continue;
7440 new_ct->add_intervals(it->second);
7441 *new_ct->add_demands() =
ct.cumulative().demands(i);
7445bool ModelCopy::CreateUnsatModel() {
7459 return context->NotifyThatModelIsUnsat();
7464 if (!in_model.
name().empty()) {
7465 context->working_model->set_name(in_model.
name());
7471 *
context->working_model->mutable_floating_point_objective() =
7475 *
context->working_model->mutable_search_strategy() =
7494 std::vector<int>* postsolve_mapping) {
7500 std::vector<int>* postsolve_mapping)
7501 : postsolve_mapping_(postsolve_mapping),
7535 for (
const auto& decision_strategy :
7551 PresolveEnforcementLiteral(
ct);
7552 switch (
ct->constraint_case()) {
7553 case ConstraintProto::ConstraintCase::kBoolOr:
7556 case ConstraintProto::ConstraintCase::kBoolAnd:
7557 PresolveBoolAnd(
ct);
7559 case ConstraintProto::ConstraintCase::kAtMostOne:
7560 PresolveAtMostOne(
ct);
7562 case ConstraintProto::ConstraintCase::kExactlyOne:
7563 PresolveExactlyOne(
ct);
7565 case ConstraintProto::ConstraintCase::kLinear:
7566 CanonicalizeLinear(
ct);
7574 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7584 "The floating point objective cannot be scaled with enough "
7607 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7610 EncodeAllAffineRelations();
7616 for (
int iter = 0; iter < context_->
params().max_presolve_iterations();
7621 int old_num_non_empty_constraints = 0;
7625 if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET)
continue;
7626 old_num_non_empty_constraints++;
7633 PresolveToFixPoint();
7637 ExtractEncodingFromLinear();
7646 PresolveToFixPoint();
7655 PresolvePureSatPart();
7669 for (
int c = 0; c < old_size; ++c) {
7671 if (
ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
7674 ExtractAtMostOneFromLinear(
ct);
7679 if (iter == 0) TransformIntoMaxCliques();
7696 PresolveToFixPoint();
7705 old_num_non_empty_constraints)) {
7709 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7712 MergeNoOverlapConstraints();
7713 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7718 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7722 EncodeAllAffineRelations();
7723 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7730 const std::vector<std::pair<int, int>> duplicates =
7732 for (
const auto [dup, rep] : duplicates) {
7743 if (type == ConstraintProto::ConstraintCase::kInterval) {
7754 if (rep_domain != d) {
7755 context_->
UpdateRuleStats(
"duplicate: merged rhs of linear constraint");
7758 if (!MarkConstraintAsFalse(
7760 SOLVER_LOG(logger_,
"Unsat after merging two linear constraints");
7777 "duplicate: linear constraint parallel to objective");
7778 const Domain objective_domain =
7782 if (objective_domain != d) {
7787 "Constraint parallel to the objective makes the objective domain "
7789 return InfeasibleStatus();
7801 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
7811 absl::flat_hash_set<int> used_variables;
7816 strategy.clear_transformations();
7817 for (
const int ref : copy.
variables()) {
7825 if (used_variables.contains(
var))
continue;
7826 used_variables.insert(
var);
7834 if (strategy.variable_selection_strategy() !=
7837 strategy.add_transformations();
7838 t->
set_index(strategy.variables_size());
7842 strategy.add_variables(rep);
7849 strategy.add_variables(ref);
7866 postsolve_mapping_->clear();
7868 int num_free_variables = 0;
7870 if (mapping[i] != -1)
continue;
7879 mapping[r] = postsolve_mapping_->size();
7880 postsolve_mapping_->push_back(r);
7892 ++num_free_variables;
7898 mapping[i] = postsolve_mapping_->size();
7899 postsolve_mapping_->push_back(i);
7901 context_->
UpdateRuleStats(absl::StrCat(
"presolve: ", num_free_variables,
7902 " unused variables removed."));
7905 std::shuffle(postsolve_mapping_->begin(), postsolve_mapping_->end(),
7907 for (
int i = 0; i < postsolve_mapping_->size(); ++i) {
7908 mapping[(*postsolve_mapping_)[i]] = i;
7931 const std::string error =
7933 if (!error.empty()) {
7934 SOLVER_LOG(logger_,
"Error while validating postsolved model: ", error);
7940 if (!error.empty()) {
7942 "Error while validating mapping_model model: ", error);
7956 auto mapping_function = [&mapping](
int* ref) {
7969 mapping_function(&mutable_ref);
7975 mapping_function(&mutable_ref);
7983 std::vector<int> new_indices(copy.
variables().size(), -1);
7984 for (
int i = 0; i < copy.
variables().size(); ++i) {
7988 new_indices[i] = strategy.variables_size();
7992 strategy.clear_transformations();
7994 CHECK_LT(transform.index(), new_indices.size());
7995 const int new_index = new_indices[transform.index()];
7996 if (new_index == -1)
continue;
7997 auto* new_transform = strategy.add_transformations();
7998 *new_transform = transform;
7999 CHECK_LT(new_index, strategy.variables().size());
8000 new_transform->set_index(new_index);
8007 absl::flat_hash_set<int> used_vars;
8010 for (
int i = 0; i < mutable_hint->vars_size(); ++i) {
8011 const int old_ref = mutable_hint->
vars(i);
8012 int64_t old_value = mutable_hint->values(i);
8016 if (old_value <
context.MinOf(old_ref)) {
8017 old_value =
context.MinOf(old_ref);
8019 if (old_value >
context.MaxOf(old_ref)) {
8020 old_value =
context.MaxOf(old_ref);
8029 const int image = mapping[
var];
8031 if (!used_vars.insert(image).second)
continue;
8032 mutable_hint->set_vars(new_size, image);
8033 mutable_hint->set_values(new_size,
value);
8038 mutable_hint->mutable_vars()->Truncate(new_size);
8039 mutable_hint->mutable_values()->Truncate(new_size);
8046 std::vector<IntegerVariableProto> new_variables;
8047 for (
int i = 0; i < mapping.size(); ++i) {
8048 const int image = mapping[i];
8049 if (image < 0)
continue;
8050 if (image >= new_variables.size()) {
8068ConstraintProto CopyConstraintForDuplicateDetection(
const ConstraintProto&
ct) {
8069 ConstraintProto copy =
ct;
8072 copy.mutable_linear()->clear_domain();
8078ConstraintProto CopyObjectiveForDuplicateDetection(
8079 const CpObjectiveProto& objective) {
8080 ConstraintProto copy;
8081 *copy.mutable_linear()->mutable_vars() = objective.vars();
8082 *copy.mutable_linear()->mutable_coeffs() = objective.coeffs();
8090 std::vector<std::pair<int, int>> result;
8095 absl::flat_hash_map<uint64_t, int> equiv_constraints;
8100 s = copy.SerializeAsString();
8105 for (
int c = 0; c < num_constraints; ++c) {
8115 s = copy.SerializeAsString();
8117 const uint64_t
hash = absl::Hash<std::string>()(s);
8118 const auto [it, inserted] = equiv_constraints.insert({
hash, c});
8121 const int other_c_with_same_hash = it->second;
8124 : CopyConstraintForDuplicateDetection(
8126 if (s == copy.SerializeAsString()) {
8127 result.push_back({c, other_c_with_same_hash});
#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)
We call domain any subset of Int64 = [kint64min, kint64max].
Domain InverseMultiplicationBy(const int64_t coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
bool Contains(int64_t value) const
Returns true iff value is in Domain.
Domain ContinuousMultiplicationBy(int64_t coeff) const
Returns a superset of MultiplicationBy() to avoid the explosion in the representation size.
Domain AdditionWith(const Domain &domain) const
Returns {x ∈ Int64, ∃ a ∈ D, ∃ b ∈ domain, x = a + b}.
ClosedInterval front() const
int64_t Size() const
Returns the number of elements in the domain.
Domain UnionWith(const Domain &domain) const
Returns the union of D and domain.
Domain MultiplicationBy(int64_t coeff, bool *exact=nullptr) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e * coeff}.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
bool IsEmpty() const
Returns true if this is the empty set.
int64_t SmallestValue() const
Returns the value closest to zero.
Domain RelaxIfTooComplex() const
If NumIntervals() is too large, this return a superset of the domain.
static Domain FromValues(std::vector< int64_t > values)
Creates a domain from the union of an unsorted list of integer values.
Domain SquareSuperset() const
Returns a superset of {x ∈ Int64, ∃ y ∈ D, x = y * y }.
Domain DivisionBy(int64_t coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e / coeff}.
DomainIteratorBeginEnd Values() const &
Domain PositiveModuloBySuperset(const Domain &modulo) const
Returns a superset of {x ∈ Int64, ∃ e ∈ D, ∃ m ∈ modulo, x = e % m }.
static int64_t GCD64(int64_t x, int64_t y)
bool LoggingIsEnabled() const
void Set(IntegerType index)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
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.
::operations_research::sat::LinearExpressionProto * add_exprs()
::PROTOBUF_NAMESPACE_ID::RepeatedField< int32_t > * mutable_literals()
void add_literals(int32_t value)
int32_t literals(int index) const
const ::operations_research::sat::BoolArgumentProto & at_most_one() const
::operations_research::sat::IntervalConstraintProto * mutable_interval()
::operations_research::sat::NoOverlap2DConstraintProto * mutable_no_overlap_2d()
::operations_research::sat::ElementConstraintProto * mutable_element()
::operations_research::sat::NoOverlapConstraintProto * mutable_no_overlap()
ConstraintCase constraint_case() const
const ::operations_research::sat::LinearConstraintProto & linear() const
void set_name(ArgT0 &&arg0, ArgT... args)
int32_t enforcement_literal(int index) const
::PROTOBUF_NAMESPACE_ID::RepeatedField< int32_t > * mutable_enforcement_literal()
::operations_research::sat::BoolArgumentProto * mutable_bool_and()
const ::operations_research::sat::BoolArgumentProto & exactly_one() const
PROTOBUF_ATTRIBUTE_REINITIALIZES void Clear() final
::operations_research::sat::AllDifferentConstraintProto * mutable_all_diff()
void Swap(ConstraintProto *other)
::operations_research::sat::BoolArgumentProto * mutable_exactly_one()
::operations_research::sat::LinearConstraintProto * mutable_linear()
void add_enforcement_literal(int32_t value)
::operations_research::sat::BoolArgumentProto * mutable_bool_or()
::operations_research::sat::CumulativeConstraintProto * mutable_cumulative()
CpSolverStatus Presolve()
void RemoveEmptyConstraints()
CpModelPresolver(PresolveContext *context, std::vector< int > *postsolve_mapping)
bool PresolveOneConstraint(int c)
::PROTOBUF_NAMESPACE_ID::RepeatedField< int32_t > * mutable_assumptions()
::operations_research::sat::DecisionStrategyProto * add_search_strategy()
const std::string & name() const
const ::operations_research::sat::CpObjectiveProto & objective() const
::operations_research::sat::DecisionStrategyProto * mutable_search_strategy(int index)
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
bool has_floating_point_objective() const
const ::operations_research::sat::DecisionStrategyProto & search_strategy(int index) const
const ::operations_research::sat::PartialVariableAssignment & solution_hint() const
bool has_objective() const
::operations_research::sat::PartialVariableAssignment * mutable_solution_hint()
::operations_research::sat::ConstraintProto * mutable_constraints(int index)
const ::operations_research::sat::SymmetryProto & symmetry() const
bool has_solution_hint() const
::operations_research::sat::IntegerVariableProto * mutable_variables(int index)
int variables_size() const
::operations_research::sat::ConstraintProto * add_constraints()
const ::operations_research::sat::FloatObjectiveProto & floating_point_objective() const
::operations_research::sat::IntegerVariableProto * add_variables()
::operations_research::sat::CpObjectiveProto * mutable_objective()
int32_t assumptions(int index) const
void clear_solution_hint()
int constraints_size() const
bool has_symmetry() const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
::PROTOBUF_NAMESPACE_ID::RepeatedField< int32_t > * mutable_vars()
::operations_research::sat::LinearExpressionProto * mutable_capacity()
void add_intervals(int32_t value)
int32_t variables(int index) const
static constexpr VariableSelectionStrategy CHOOSE_FIRST
const ::operations_research::sat::DecisionStrategyProto_AffineTransformation & transformations(int index) const
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)
void Swap(IntegerVariableProto *other)
void CopyFrom(const IntegerVariableProto &from)
void add_domain(int64_t value)
::operations_research::sat::LinearExpressionProto * mutable_start()
::PROTOBUF_NAMESPACE_ID::RepeatedField< int64_t > * mutable_coeffs()
void set_coeffs(int index, int64_t value)
void add_vars(int32_t value)
int64_t domain(int index) const
int32_t vars(int index) const
int64_t coeffs(int index) const
::PROTOBUF_NAMESPACE_ID::RepeatedField< int32_t > * mutable_vars()
void add_domain(int64_t value)
void set_vars(int index, int32_t value)
void set_offset(int64_t value)
ModelCopy(PresolveContext *context)
bool ImportAndSimplifyConstraints(const CpModelProto &in_model, const std::vector< int > &ignored_constraints, bool first_copy=false)
void set_boxes_with_null_area_can_overlap(bool value)
void add_x_intervals(int32_t value)
void add_intervals(int32_t value)
::PROTOBUF_NAMESPACE_ID::RepeatedField< int32_t > * mutable_intervals()
int32_t vars(int index) const
bool VariableIsRemovable(int ref) const
int64_t MaxOf(int ref) const
bool CanonicalizeAffineVariable(int ref, int64_t coeff, int64_t mod, int64_t rhs)
SparseBitset< int64_t > modified_domains
bool ExpressionIsALiteral(const LinearExpressionProto &expr, int *literal=nullptr) const
bool StoreAbsRelation(int target_ref, int ref)
bool VariableWithCostIsUnique(int ref) const
bool ConstraintIsInactive(int ct_index) const
bool ConstraintVariableUsageIsConsistent()
const absl::flat_hash_set< int > & VarToConstraints(int var) const
bool ModelIsExpanded() const
void AddImplication(int a, int b)
bool ModelIsUnsat() 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
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64_t value)
ABSL_MUST_USE_RESULT bool CanonicalizeObjective(bool simplify_domain=true)
bool StoreBooleanEqualityRelation(int ref_a, int ref_b)
int64_t StartMin(int ct_ref) 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)
std::vector< int > tmp_literals
ABSL_MUST_USE_RESULT bool ScaleFloatingPointObjective()
std::vector< absl::flat_hash_set< int > > var_to_ub_only_constraints
bool ObjectiveDomainIsConstraining() const
CpModelProto * mapping_model
ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective(int var_in_equality, int64_t coeff_in_equality, const ConstraintProto &equality, std::vector< int > *new_vars_in_objective=nullptr)
int GetOrCreateVarValueEncoding(int ref, int64_t value)
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
int64_t num_presolve_operations
void InitializeNewDomains()
int GetVariableRepresentative(int ref) const
void MarkVariableAsRemoved(int ref)
bool InsertVarValueEncoding(int literal, int ref, int64_t value)
ModelRandomGenerator * random()
DomainDeductions deductions
std::vector< Domain > tmp_left_domains
void CanonicalizeDomainOfSizeTwo(int var)
const std::vector< int > & ConstraintToVars(int c) const
int64_t FixedValue(int ref) const
bool LiteralIsTrue(int lit) const
const absl::flat_hash_map< int, int64_t > & ObjectiveMap() const
CpModelProto * working_model
bool IntervalIsConstant(int ct_ref) const
bool DomainContains(int ref, int64_t value) const
bool LiteralIsFalse(int lit) const
void UpdateRuleStats(const std::string &name, int num_times=1)
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
bool StoreAffineRelation(int ref_x, int ref_y, int64_t coeff, int64_t offset, bool debug_no_recursion=false)
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
int LiteralForExpressionMax(const LinearExpressionProto &expr) const
int64_t EndMax(int ct_ref) const
bool ConstraintIsOptional(int ct_ref) const
int GetOrCreateConstantVar(int64_t cst)
const SatParameters & params() const
bool ExpressionIsAffineBoolean(const LinearExpressionProto &expr) const
int64_t SizeMax(int ct_ref) const
bool ExploitExactlyOneInObjective(absl::Span< const int > exactly_one)
Domain DomainSuperSetOf(const LinearExpressionProto &expr) const
absl::flat_hash_set< int > tmp_literal_set
void ReadObjectiveFromProto()
int64_t SizeMin(int ct_ref) const
bool CanBeUsedAsLiteral(int ref) const
bool VariableWasRemoved(int ref) const
void RegisterVariablesUsedInAssumptions()
void ExploitFixedDomain(int var)
int64_t MinOf(int ref) const
bool VariableIsOnlyUsedInEncodingAndMaybeInObjective(int ref) const
bool GetAbsRelation(int target_ref, int *ref)
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64_t value)
const Domain & ObjectiveDomain() const
double merge_no_overlap_work_limit() const
bool enumerate_all_solutions() const
bool cp_model_use_sat_presolve() const
bool permute_presolve_constraint_order() const
::operations_research::sat::SatParameters_SearchBranching search_branching() const
bool keep_all_feasible_solutions_in_presolve() const
int32_t debug_max_num_presolve_operations() const
int32_t max_presolve_iterations() const
double merge_at_most_one_work_limit() const
bool cp_model_presolve() const
bool fill_tightened_domains_in_response() const
void set_presolve_blocked_clause(bool value)
int32_t symmetry_level() const
bool presolve_extract_integer_enforcement() const
bool permute_variable_randomly() const
int32_t presolve_substitution_level() const
int32_t cp_model_probing_level() const
static constexpr SearchBranching FIXED_SEARCH
CpModelProto const * model_proto
ModelSharedTimeLimit * time_limit
GurobiMPCallbackContext * context
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)
void swap(IdMap< K, V > &a, IdMap< K, V > &b)
bool DetectAndExploitSymmetriesInPresolve(PresolveContext *context)
bool RefIsPositive(int ref)
void GetOverlappingIntervalComponents(std::vector< IndexedInterval > *intervals, std::vector< std::vector< int > > *components)
const LiteralIndex kNoLiteralIndex(-1)
std::vector< absl::Span< int > > GetOverlappingRectangleComponents(const std::vector< Rectangle > &rectangles, absl::Span< int > active_rectangles)
bool HasEnforcementLiteral(const ConstraintProto &ct)
void ExpandCpModel(PresolveContext *context)
constexpr int kAffineRelationConstraint
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void DetectDominanceRelations(const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
bool LinearExpressionProtosAreEqual(const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
std::string ValidateCpModel(const CpModelProto &model, bool after_presolve)
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool SolveDiophantineEquationOfSizeTwo(int64_t &a, int64_t &b, int64_t &cte, int64_t &x0, int64_t &y0)
void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(const CpModelProto &in_model, PresolveContext *context)
int ReindexArcs(IntContainer *tails, IntContainer *heads)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
bool ImportConstraintsWithBasicPresolveIntoContext(const CpModelProto &in_model, PresolveContext *context)
std::vector< std::pair< int, int > > FindDuplicateConstraints(const CpModelProto &model_proto)
int64_t FloorSquareRoot(int64_t a)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
CpSolverStatus PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
bool LoadModelForProbing(PresolveContext *context, Model *local_model)
void ConstructOverlappingSets(bool already_sorted, std::vector< IndexedInterval > *intervals, std::vector< std::vector< int > > *result)
constexpr int kObjectiveConstraint
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
bool ExploitDominanceRelations(const VarDomination &var_domination, PresolveContext *context)
int GetSingleRefFromExpression(const LinearExpressionProto &expr)
bool ExpressionContainsSingleRef(const LinearExpressionProto &expr)
void ApplyVariableMapping(const std::vector< int > &mapping, const PresolveContext &context)
bool SubstituteVariable(int var, int64_t var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
Collection of objects used to extend the Constraint Solver library.
int64_t CapAdd(int64_t x, int64_t y)
int64_t CapSub(int64_t x, int64_t y)
int64_t CapProd(int64_t x, int64_t y)
std::optional< int64_t > end
#define SOLVER_LOG(logger,...)