29 #include "absl/base/attributes.h"
30 #include "absl/container/btree_map.h"
31 #include "absl/container/btree_set.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/numeric/int128.h"
36 #include "absl/strings/str_cat.h"
37 #include "absl/types/span.h"
46 #include "ortools/sat/cp_model.pb.h"
61 #include "ortools/sat/sat_parameters.pb.h"
80 bool LinearConstraintIsClean(
const LinearConstraintProto& linear) {
81 const int num_vars = linear.vars().size();
82 for (
int i = 0; i < num_vars; ++i) {
84 if (linear.coeffs(i) == 0)
return false;
91 bool CpModelPresolver::RemoveConstraint(ConstraintProto*
ct) {
102 std::vector<int> interval_mapping(context_->
working_model->constraints_size(),
104 int new_num_constraints = 0;
105 const int old_num_non_empty_constraints =
107 for (
int c = 0; c < old_num_non_empty_constraints; ++c) {
108 const auto type = context_->
working_model->constraints(c).constraint_case();
109 if (type == ConstraintProto::CONSTRAINT_NOT_SET)
continue;
110 if (type == ConstraintProto::kDummyConstraint)
continue;
111 if (type == ConstraintProto::kInterval) {
112 interval_mapping[c] = new_num_constraints;
114 context_->
working_model->mutable_constraints(new_num_constraints++)
117 context_->
working_model->mutable_constraints()->DeleteSubrange(
118 new_num_constraints, old_num_non_empty_constraints - new_num_constraints);
119 for (ConstraintProto& ct_ref :
122 [&interval_mapping](
int* ref) {
123 *ref = interval_mapping[*ref];
130 bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto*
ct) {
135 const int old_size =
ct->enforcement_literal().size();
137 for (
const int literal :
ct->enforcement_literal()) {
146 return RemoveConstraint(
ct);
153 return RemoveConstraint(
ct);
160 const int64_t obj_coeff =
164 context_->
UpdateRuleStats(
"enforcement: literal with unique direction");
166 return RemoveConstraint(
ct);
182 return RemoveConstraint(
ct);
186 ct->set_enforcement_literal(new_size++,
literal);
188 ct->mutable_enforcement_literal()->Truncate(new_size);
189 return new_size != old_size;
192 bool CpModelPresolver::PresolveBoolXor(ConstraintProto*
ct) {
197 bool changed =
false;
198 int num_true_literals = 0;
200 for (
const int literal :
ct->bool_xor().literals()) {
221 ct->mutable_bool_xor()->set_literals(new_size++,
literal);
225 if (num_true_literals % 2 == 0) {
229 return RemoveConstraint(
ct);
231 }
else if (new_size == 1) {
232 if (num_true_literals % 2 == 0) {
235 "bool_xor: cannot fix last literal");
240 "bool_xor: cannot fix last literal");
244 return RemoveConstraint(
ct);
245 }
else if (new_size == 2) {
246 const int a =
ct->bool_xor().literals(0);
247 const int b =
ct->bool_xor().literals(1);
249 if (num_true_literals % 2 == 0) {
253 return RemoveConstraint(
ct);
257 if (num_true_literals % 2 == 1) {
261 return RemoveConstraint(
ct);
264 if (num_true_literals % 2 == 0) {
271 return RemoveConstraint(
ct);
274 if (num_true_literals % 2 == 1) {
276 ct->mutable_bool_xor()->set_literals(new_size++, true_literal);
278 if (num_true_literals > 1) {
279 context_->
UpdateRuleStats(
"bool_xor: remove even number of true literals");
282 ct->mutable_bool_xor()->mutable_literals()->Truncate(new_size);
286 bool CpModelPresolver::PresolveBoolOr(ConstraintProto*
ct) {
293 for (
const int literal :
ct->enforcement_literal()) {
296 ct->clear_enforcement_literal();
304 bool changed =
false;
307 for (
const int literal :
ct->bool_or().literals()) {
314 return RemoveConstraint(
ct);
322 return RemoveConstraint(
ct);
326 return RemoveConstraint(
ct);
345 return RemoveConstraint(
ct);
358 ct->mutable_bool_or()->mutable_literals()->Clear();
360 ct->mutable_bool_or()->add_literals(lit);
368 ABSL_MUST_USE_RESULT
bool CpModelPresolver::MarkConstraintAsFalse(
369 ConstraintProto*
ct) {
372 ct->mutable_bool_or()->clear_literals();
373 for (
const int lit :
ct->enforcement_literal()) {
376 ct->clear_enforcement_literal();
384 bool CpModelPresolver::PresolveBoolAnd(ConstraintProto*
ct) {
389 for (
const int literal :
ct->bool_and().literals()) {
392 return RemoveConstraint(
ct);
395 bool changed =
false;
398 const absl::flat_hash_set<int> enforcement_literals_set(
399 ct->enforcement_literal().begin(),
ct->enforcement_literal().end());
400 for (
const int literal :
ct->bool_and().literals()) {
403 return MarkConstraintAsFalse(
ct);
409 if (enforcement_literals_set.contains(
literal)) {
416 return MarkConstraintAsFalse(
ct);
426 return MarkConstraintAsFalse(
ct);
444 ct->mutable_bool_and()->mutable_literals()->Clear();
446 ct->mutable_bool_and()->add_literals(lit);
455 if (
ct->enforcement_literal().size() == 1 &&
456 ct->bool_and().literals().size() == 1) {
457 const int enforcement =
ct->enforcement_literal(0);
467 ct->bool_and().literals(0));
475 bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto*
ct) {
476 bool is_at_most_one =
ct->constraint_case() == ConstraintProto::kAtMostOne;
477 const std::string
name = is_at_most_one ?
"at_most_one: " :
"exactly_one: ";
478 auto* literals = is_at_most_one
479 ?
ct->mutable_at_most_one()->mutable_literals()
480 :
ct->mutable_exactly_one()->mutable_literals();
484 std::sort(literals->begin(), literals->end());
488 for (
const int literal : *literals) {
495 int num_positive = 0;
496 int num_negative = 0;
497 for (
const int other : *literals) {
518 return RemoveConstraint(
ct);
524 std::vector<std::pair<int, int64_t>> singleton_literal_with_cost;
527 bool changed =
false;
529 for (
const int literal : *literals) {
532 for (
const int other : *literals) {
537 return RemoveConstraint(
ct);
547 singleton_literal_with_cost.push_back({
literal, 0});
554 singleton_literal_with_cost.push_back({
literal, it->second});
558 singleton_literal_with_cost.push_back({
literal, -it->second});
566 bool transform_to_at_most_one =
false;
567 if (!singleton_literal_with_cost.empty()) {
571 if (singleton_literal_with_cost.size() > 1) {
573 singleton_literal_with_cost.begin(),
574 singleton_literal_with_cost.end(),
575 [](
const std::pair<int, int64_t>&
a,
576 const std::pair<int, int64_t>&
b) { return a.second < b.second; });
577 for (
int i = 1; i < singleton_literal_with_cost.size(); ++i) {
580 singleton_literal_with_cost[i].first)) {
584 singleton_literal_with_cost.resize(1);
587 const int literal = singleton_literal_with_cost[0].first;
588 const int64_t literal_cost = singleton_literal_with_cost[0].second;
589 if (is_at_most_one && literal_cost >= 0) {
602 if (!is_at_most_one) transform_to_at_most_one =
true;
603 is_at_most_one =
true;
610 context_->
mapping_model->add_constraints()->mutable_exactly_one();
612 mapping_exo->add_literals(lit);
614 mapping_exo->add_literals(
literal);
618 if (!is_at_most_one && !transform_to_at_most_one &&
623 if (transform_to_at_most_one) {
626 literals =
ct->mutable_at_most_one()->mutable_literals();
638 bool CpModelPresolver::PresolveAtMostOne(ConstraintProto*
ct) {
642 const bool changed = PresolveAtMostOrExactlyOne(
ct);
643 if (
ct->constraint_case() != ConstraintProto::kAtMostOne)
return changed;
646 const auto& literals =
ct->at_most_one().literals();
647 if (literals.empty()) {
649 return RemoveConstraint(
ct);
653 if (literals.size() == 1) {
655 return RemoveConstraint(
ct);
661 bool CpModelPresolver::PresolveExactlyOne(ConstraintProto*
ct) {
664 const bool changed = PresolveAtMostOrExactlyOne(
ct);
665 if (
ct->constraint_case() != ConstraintProto::kExactlyOne)
return changed;
668 const auto& literals =
ct->exactly_one().literals();
669 if (literals.empty()) {
674 if (literals.size() == 1) {
677 return RemoveConstraint(
ct);
681 if (literals.size() == 2) {
685 return RemoveConstraint(
ct);
691 bool CpModelPresolver::CanonicalizeLinearArgument(
const ConstraintProto&
ct,
692 LinearArgumentProto*
proto) {
696 bool changed = CanonicalizeLinearExpression(
ct,
proto->mutable_target());
697 for (LinearExpressionProto& exp : *(
proto->mutable_exprs())) {
698 changed |= CanonicalizeLinearExpression(
ct, &exp);
703 bool CpModelPresolver::PresolveLinMax(ConstraintProto*
ct) {
708 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
709 min_offset =
std::min(min_offset, expr.offset());
712 LinearArgumentProto* lin_max =
ct->mutable_lin_max();
713 lin_max->mutable_target()->set_offset(lin_max->target().offset() -
715 for (LinearExpressionProto& expr : *(lin_max->mutable_exprs())) {
716 expr.set_offset(expr.offset() - min_offset);
721 const LinearExpressionProto& target =
ct->lin_max().target();
724 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
726 for (
const LinearExpressionProto& e :
ct->lin_max().exprs()) {
728 LinearConstraintProto* prec =
729 context_->
working_model->add_constraints()->mutable_linear();
736 return RemoveConstraint(
ct);
743 int64_t infered_min = context_->
MinOf(target);
745 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
750 if (target.vars().empty()) {
751 if (!Domain(infered_min, infered_max).Contains(target.offset())) {
753 return MarkConstraintAsFalse(
ct);
756 if (target.vars().size() <= 1) {
758 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
759 rhs_domain = rhs_domain.UnionWith(
761 {infered_min, infered_max}));
763 bool reduced =
false;
774 const int64_t target_min = context_->
MinOf(target);
775 const int64_t target_max = context_->
MaxOf(target);
776 bool changed =
false;
783 bool has_greater_or_equal_to_target_min =
false;
785 int index_to_keep = -1;
786 for (
int i = 0; i <
ct->lin_max().exprs_size(); ++i) {
787 const LinearExpressionProto& expr =
ct->lin_max().exprs(i);
788 if (context_->
MinOf(expr) >= target_min) {
789 const int64_t expr_max = context_->
MaxOf(expr);
790 if (expr_max > max_at_index_to_keep) {
791 max_at_index_to_keep = expr_max;
794 has_greater_or_equal_to_target_min =
true;
799 for (
int i = 0; i <
ct->lin_max().exprs_size(); ++i) {
800 const LinearExpressionProto& expr =
ct->lin_max().exprs(i);
801 const int64_t expr_max = context_->
MaxOf(expr);
804 if (expr_max < target_min)
continue;
805 if (expr_max == target_min && has_greater_or_equal_to_target_min &&
806 i != index_to_keep) {
809 *
ct->mutable_lin_max()->mutable_exprs(new_size) = expr;
812 if (new_size < ct->lin_max().exprs_size()) {
814 ct->mutable_lin_max()->mutable_exprs()->DeleteSubrange(
815 new_size,
ct->lin_max().exprs_size() - new_size);
820 if (
ct->lin_max().exprs().empty()) {
822 return MarkConstraintAsFalse(
ct);
827 if (
ct->lin_max().exprs().size() == 1) {
829 ConstraintProto* new_ct = context_->
working_model->add_constraints();
831 auto* arg = new_ct->mutable_linear();
832 const LinearExpressionProto&
a =
ct->lin_max().target();
833 const LinearExpressionProto&
b =
ct->lin_max().exprs(0);
834 for (
int i = 0; i <
a.vars().size(); ++i) {
835 arg->add_vars(
a.vars(i));
836 arg->add_coeffs(
a.coeffs(i));
838 for (
int i = 0; i <
b.vars().size(); ++i) {
839 arg->add_vars(
b.vars(i));
840 arg->add_coeffs(-
b.coeffs(i));
842 arg->add_domain(
b.offset() -
a.offset());
843 arg->add_domain(
b.offset() -
a.offset());
845 return RemoveConstraint(
ct);
853 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
854 const int64_t value_min = context_->
MinOf(expr);
855 bool modified =
false;
863 const int64_t value_max = context_->
MaxOf(expr);
864 if (value_max > target_max) {
865 context_->
UpdateRuleStats(
"TODO lin_max: linear expression above max.");
869 if (abort)
return changed;
873 if (target_min == target_max) {
874 bool all_booleans =
true;
875 std::vector<int> literals;
876 const int64_t fixed_target = target_min;
877 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
878 const int64_t value_min = context_->
MinOf(expr);
879 const int64_t value_max = context_->
MaxOf(expr);
880 CHECK_LE(value_max, fixed_target) <<
"Presolved above";
881 if (value_max < fixed_target)
continue;
883 if (value_min == value_max && value_max == fixed_target) {
885 return RemoveConstraint(
ct);
888 CHECK_EQ(value_max, fixed_target);
891 all_booleans =
false;
895 if (literals.empty()) {
896 return MarkConstraintAsFalse(
ct);
901 for (
const int lit : literals) {
902 ct->mutable_bool_or()->add_literals(lit);
909 changed |= PresolveLinMaxWhenAllBoolean(
ct);
914 bool CpModelPresolver::PresolveLinMaxWhenAllBoolean(ConstraintProto*
ct) {
918 const LinearExpressionProto& target =
ct->lin_max().target();
921 const int64_t target_min = context_->
MinOf(target);
922 const int64_t target_max = context_->
MaxOf(target);
925 bool min_is_reachable =
false;
926 std::vector<int> min_literals;
927 std::vector<int> literals_above_min;
928 std::vector<int> max_literals;
930 for (
const LinearExpressionProto& expr :
ct->lin_max().exprs()) {
932 const int64_t value_min = context_->
MinOf(expr);
933 const int64_t value_max = context_->
MaxOf(expr);
938 if (value_min > target_min) {
943 if (value_max > target_max) {
950 if (value_min == value_max) {
951 if (value_min == target_min) min_is_reachable =
true;
955 CHECK_LE(value_min, target_min);
956 if (value_min == target_min) {
960 CHECK_LE(value_max, target_max);
961 if (value_max == target_max) {
962 max_literals.push_back(ref);
963 literals_above_min.push_back(ref);
964 }
else if (value_max > target_min) {
965 literals_above_min.push_back(ref);
966 }
else if (value_max == target_min) {
967 min_literals.push_back(ref);
974 ConstraintProto* clause = context_->
working_model->add_constraints();
975 clause->add_enforcement_literal(target_ref);
976 clause->mutable_bool_or();
977 for (
const int lit : max_literals) {
978 clause->mutable_bool_or()->add_literals(lit);
982 for (
const int lit : literals_above_min) {
986 if (!min_is_reachable) {
988 ConstraintProto* clause = context_->
working_model->add_constraints();
989 clause->add_enforcement_literal(
NegatedRef(target_ref));
990 clause->mutable_bool_or();
991 for (
const int lit : min_literals) {
992 clause->mutable_bool_or()->add_literals(lit);
997 return RemoveConstraint(
ct);
1001 bool CpModelPresolver::PresolveIntAbs(ConstraintProto*
ct) {
1002 CHECK_EQ(
ct->enforcement_literal_size(), 0);
1004 const LinearExpressionProto& target_expr =
ct->lin_max().target();
1005 const LinearExpressionProto& expr =
ct->lin_max().exprs(0);
1006 DCHECK_EQ(expr.vars_size(), 1);
1011 const Domain new_target_domain =
1012 expr_domain.
UnionWith(expr_domain.Negation())
1014 bool target_domain_modified =
false;
1016 &target_domain_modified)) {
1019 if (expr_domain.IsFixed()) {
1021 return RemoveConstraint(
ct);
1023 if (target_domain_modified) {
1024 context_->
UpdateRuleStats(
"int_abs: propagate domain from x to abs(x)");
1030 const Domain target_domain =
1033 const Domain new_expr_domain =
1034 target_domain.
UnionWith(target_domain.Negation());
1035 bool expr_domain_modified =
false;
1037 &expr_domain_modified)) {
1042 if (context_->
IsFixed(target_expr)) {
1044 return RemoveConstraint(
ct);
1046 if (expr_domain_modified) {
1047 context_->
UpdateRuleStats(
"int_abs: propagate domain from abs(x) to x");
1052 if (context_->
MinOf(expr) >= 0) {
1054 ConstraintProto* new_ct = context_->
working_model->add_constraints();
1055 new_ct->set_name(
ct->name());
1056 auto* arg = new_ct->mutable_linear();
1061 if (!CanonicalizeLinear(new_ct))
return false;
1063 return RemoveConstraint(
ct);
1066 if (context_->
MaxOf(expr) <= 0) {
1068 ConstraintProto* new_ct = context_->
working_model->add_constraints();
1069 new_ct->set_name(
ct->name());
1070 auto* arg = new_ct->mutable_linear();
1075 if (!CanonicalizeLinear(new_ct))
return false;
1077 return RemoveConstraint(
ct);
1089 return RemoveConstraint(
ct);
1110 bool CpModelPresolver::PresolveIntProd(ConstraintProto*
ct) {
1115 bool domain_modified =
false;
1118 for (
const LinearExpressionProto& expr :
ct->int_prod().exprs()) {
1123 &domain_modified)) {
1129 int64_t constant_factor = 1;
1131 bool changed =
false;
1132 LinearArgumentProto*
proto =
ct->mutable_int_prod();
1133 for (
int i = 0; i <
ct->int_prod().exprs().size(); ++i) {
1134 LinearExpressionProto expr =
ct->int_prod().exprs(i);
1135 if (context_->
IsFixed(expr)) {
1141 const int64_t coeff = expr.coeffs(0);
1142 const int64_t offset = expr.offset();
1145 static_cast<uint64_t
>(std::abs(offset)));
1147 constant_factor =
CapProd(constant_factor, gcd);
1148 expr.set_coeffs(0, coeff / gcd);
1149 expr.set_offset(offset / gcd);
1152 *
proto->mutable_exprs(new_size++) = expr;
1154 proto->mutable_exprs()->erase(
proto->mutable_exprs()->begin() + new_size,
1155 proto->mutable_exprs()->end());
1157 if (
ct->int_prod().exprs().empty()) {
1159 Domain(constant_factor))) {
1163 return RemoveConstraint(
ct);
1166 if (constant_factor == 0) {
1171 return RemoveConstraint(
ct);
1182 constant_factor = 1;
1186 if (
ct->int_prod().exprs().size() == 1) {
1187 LinearConstraintProto*
const lin =
1188 context_->
working_model->add_constraints()->mutable_linear();
1193 -constant_factor, lin);
1195 context_->
UpdateRuleStats(
"int_prod: linearize product by constant.");
1196 return RemoveConstraint(
ct);
1199 if (constant_factor != 1) {
1207 const LinearExpressionProto old_target =
ct->int_prod().target();
1208 if (!context_->
IsFixed(old_target)) {
1209 const int ref = old_target.vars(0);
1210 const int64_t coeff = old_target.coeffs(0);
1211 const int64_t offset = old_target.offset();
1222 if (context_->
IsFixed(old_target)) {
1223 const int64_t target_value = context_->
FixedValue(old_target);
1224 if (target_value % constant_factor != 0) {
1226 "int_prod: constant factor does not divide constant target");
1229 proto->clear_target();
1230 proto->mutable_target()->set_offset(target_value / constant_factor);
1232 "int_prod: divide product and fixed target by constant factor");
1235 const AffineRelation::Relation r =
1237 const absl::int128 temp_coeff =
1238 absl::int128(old_target.coeffs(0)) * absl::int128(r.coeff);
1239 CHECK_EQ(temp_coeff % absl::int128(constant_factor), 0);
1240 const absl::int128 temp_offset =
1241 absl::int128(old_target.coeffs(0)) * absl::int128(r.offset) +
1242 absl::int128(old_target.offset());
1243 CHECK_EQ(temp_offset % absl::int128(constant_factor), 0);
1244 const absl::int128 new_coeff = temp_coeff / absl::int128(constant_factor);
1245 const absl::int128 new_offset =
1246 temp_offset / absl::int128(constant_factor);
1259 "int_prod: overflow during simplification.");
1263 proto->mutable_target()->set_coeffs(0,
static_cast<int64_t
>(new_coeff));
1264 proto->mutable_target()->set_vars(0, r.representative);
1265 proto->mutable_target()->set_offset(
static_cast<int64_t
>(new_offset));
1266 context_->
UpdateRuleStats(
"int_prod: divide product by constant factor");
1273 bool is_square =
false;
1274 if (
ct->int_prod().exprs_size() == 2 &&
1276 ct->int_prod().exprs(1))) {
1281 for (
const LinearExpressionProto& expr :
ct->int_prod().exprs()) {
1287 &domain_modified)) {
1290 if (domain_modified) {
1292 is_square ?
"int_square" :
"int_prod",
": reduced target domain."));
1297 const int64_t target_max = context_->
MaxOf(
ct->int_prod().target());
1298 DCHECK_GE(target_max, 0);
1300 bool expr_reduced =
false;
1302 {-sqrt_max, sqrt_max}, &expr_reduced)) {
1310 if (
ct->int_prod().exprs_size() == 2) {
1311 LinearExpressionProto
a =
ct->int_prod().exprs(0);
1312 LinearExpressionProto
b =
ct->int_prod().exprs(1);
1313 const LinearExpressionProto product =
ct->int_prod().target();
1320 context_->
UpdateRuleStats(
"int_square: fix variable to zero or one.");
1321 return RemoveConstraint(
ct);
1326 const LinearExpressionProto target_expr =
ct->int_prod().target();
1331 std::vector<int> literals;
1332 for (
const LinearExpressionProto& expr :
ct->int_prod().exprs()) {
1337 literals.push_back(lit);
1343 ConstraintProto* new_ct = context_->
working_model->add_constraints();
1344 new_ct->add_enforcement_literal(target);
1345 auto* arg = new_ct->mutable_bool_and();
1346 for (
const int lit : literals) {
1347 arg->add_literals(lit);
1351 ConstraintProto* new_ct = context_->
working_model->add_constraints();
1352 auto* arg = new_ct->mutable_bool_or();
1353 arg->add_literals(target);
1354 for (
const int lit : literals) {
1359 return RemoveConstraint(
ct);
1362 bool CpModelPresolver::PresolveIntDiv(ConstraintProto*
ct) {
1365 const LinearExpressionProto target =
ct->int_div().target();
1366 const LinearExpressionProto expr =
ct->int_div().exprs(0);
1367 const LinearExpressionProto div =
ct->int_div().exprs(1);
1374 return RemoveConstraint(
ct);
1380 return RemoveConstraint(
ct);
1384 if (!context_->
IsFixed(div))
return false;
1386 const int64_t divisor = context_->
FixedValue(div);
1389 if (divisor == 1 || divisor == -1) {
1390 LinearConstraintProto*
const lin =
1391 context_->
working_model->add_constraints()->mutable_linear();
1398 return RemoveConstraint(
ct);
1403 bool domain_modified =
false;
1404 const Domain target_implied_domain =
1408 &domain_modified)) {
1411 if (domain_modified) {
1413 if (target_implied_domain.IsFixed()) {
1415 "int_div: target has been fixed by propagating X / cte");
1418 "int_div: updated domain of target in target = X / cte");
1424 if (context_->
IsFixed(target) &&
1426 1 + std::abs(context_->
FixedValue(target)))) !=
1429 int64_t d = divisor;
1435 const Domain expr_implied_domain =
1437 ? Domain(t * d, (t + 1) * d - 1)
1438 : (t == 0 ? Domain(1 - d, d - 1) : Domain((t - 1) * d + 1, t * d));
1439 bool domain_modified =
false;
1441 &domain_modified)) {
1444 if (domain_modified) {
1449 return RemoveConstraint(
ct);
1455 if (context_->
MinOf(target) >= 0 && context_->
MinOf(expr) >= 0 &&
1459 LinearConstraintProto*
const lin =
1460 context_->
working_model->add_constraints()->mutable_linear();
1462 lin->add_domain(divisor - 1);
1467 "int_div: linearize positive division with a constant divisor");
1469 return RemoveConstraint(
ct);
1477 bool CpModelPresolver::PresolveIntMod(ConstraintProto*
ct) {
1480 const LinearExpressionProto target =
ct->int_mod().target();
1481 const LinearExpressionProto expr =
ct->int_mod().exprs(0);
1482 const LinearExpressionProto mod =
ct->int_mod().exprs(1);
1484 if (context_->
MinOf(target) > 0) {
1485 bool domain_changed =
false;
1491 if (domain_changed) {
1493 "int_mod: non negative target implies positive expression");
1497 if (context_->
MinOf(target) >= context_->
MaxOf(mod) ||
1498 context_->
MaxOf(target) <= -context_->
MaxOf(mod)) {
1500 "int_mod: incompatible target and mod");
1503 if (context_->
MaxOf(target) < 0) {
1504 bool domain_changed =
false;
1510 if (domain_changed) {
1512 "int_mod: non positive target implies negative expression");
1517 context_->
FixedValue(mod) > 1 &&
ct->enforcement_literal().empty() &&
1518 expr.vars().size() == 1) {
1520 const int64_t fixed_mod = context_->
FixedValue(mod);
1521 const int64_t fixed_target = context_->
FixedValue(target);
1525 fixed_target - expr.offset())) {
1530 return RemoveConstraint(
ct);
1533 bool domain_changed =
false;
1542 if (domain_changed) {
1551 bool CpModelPresolver::ExploitEquivalenceRelations(
int c, ConstraintProto*
ct) {
1552 bool changed =
false;
1557 if (
ct->constraint_case() == ConstraintProto::kLinear) {
1558 for (
int& ref : *
ct->mutable_enforcement_literal()) {
1570 bool work_to_do =
false;
1573 if (r.representative !=
var) {
1578 if (!work_to_do)
return false;
1582 [&changed,
this](
int* ref) {
1593 bool CpModelPresolver::DivideLinearByGcd(ConstraintProto*
ct) {
1598 const int num_vars =
ct->linear().vars().size();
1599 for (
int i = 0; i < num_vars; ++i) {
1600 const int64_t magnitude = std::abs(
ct->linear().coeffs(i));
1602 if (gcd == 1)
break;
1606 for (
int i = 0; i < num_vars; ++i) {
1607 ct->mutable_linear()->set_coeffs(i,
ct->linear().coeffs(i) / gcd);
1611 if (
ct->linear().domain_size() == 0) {
1612 return MarkConstraintAsFalse(
ct);
1618 template <
typename ProtoWithVarsAndCoeffs>
1619 bool CpModelPresolver::CanonicalizeLinearExpressionInternal(
1620 const ConstraintProto&
ct, ProtoWithVarsAndCoeffs*
proto, int64_t* offset) {
1626 int64_t sum_of_fixed_terms = 0;
1627 bool remapped =
false;
1628 const int old_size =
proto->vars().size();
1629 DCHECK_EQ(old_size,
proto->coeffs().size());
1630 for (
int i = 0; i < old_size; ++i) {
1638 const int ref =
proto->vars(i);
1640 const int64_t coeff =
1642 if (coeff == 0)
continue;
1650 if (r.representative !=
var) {
1652 sum_of_fixed_terms += coeff * r.
offset;
1655 new_var = r.representative;
1656 new_coeff = coeff * r.coeff;
1661 bool removed =
false;
1662 for (
const int enf :
ct.enforcement_literal()) {
1666 sum_of_fixed_terms += new_coeff;
1675 context_->
UpdateRuleStats(
"linear: enforcement literal in expression");
1679 tmp_terms_.push_back({new_var, new_coeff});
1681 proto->clear_vars();
1682 proto->clear_coeffs();
1683 std::sort(tmp_terms_.begin(), tmp_terms_.end());
1684 int current_var = 0;
1685 int64_t current_coeff = 0;
1686 for (
const auto& entry : tmp_terms_) {
1688 if (entry.first == current_var) {
1689 current_coeff += entry.second;
1691 if (current_coeff != 0) {
1692 proto->add_vars(current_var);
1693 proto->add_coeffs(current_coeff);
1695 current_var = entry.first;
1696 current_coeff = entry.second;
1699 if (current_coeff != 0) {
1700 proto->add_vars(current_var);
1701 proto->add_coeffs(current_coeff);
1706 if (
proto->vars().size() < old_size) {
1709 *offset = sum_of_fixed_terms;
1710 return remapped ||
proto->vars().size() < old_size;
1713 bool CpModelPresolver::CanonicalizeLinearExpression(
1714 const ConstraintProto&
ct, LinearExpressionProto* exp) {
1716 const bool result = CanonicalizeLinearExpressionInternal(
ct, exp, &offset);
1717 exp->set_offset(exp->offset() + offset);
1721 bool CpModelPresolver::CanonicalizeLinear(ConstraintProto*
ct) {
1722 if (
ct->constraint_case() != ConstraintProto::kLinear)
return false;
1725 if (
ct->linear().domain().empty()) {
1727 return MarkConstraintAsFalse(
ct);
1732 CanonicalizeLinearExpressionInternal(*
ct,
ct->mutable_linear(), &offset);
1736 ct->mutable_linear());
1738 changed |= DivideLinearByGcd(
ct);
1741 if (!
ct->linear().coeffs().empty() &&
ct->linear().coeffs(0) < 0) {
1742 for (int64_t& ref_coeff : *
ct->mutable_linear()->mutable_coeffs()) {
1743 ref_coeff = -ref_coeff;
1746 ct->mutable_linear());
1752 bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto*
ct) {
1753 if (
ct->constraint_case() != ConstraintProto::kLinear ||
1758 absl::btree_set<int> index_to_erase;
1759 const int num_vars =
ct->linear().vars().size();
1765 for (
int i = 0; i < num_vars; ++i) {
1766 const int var =
ct->linear().vars(i);
1767 const int64_t coeff =
ct->linear().coeffs(i);
1774 if (std::abs(coeff) != 1)
continue;
1777 const auto term_domain =
1779 if (!exact)
continue;
1783 if (new_rhs.NumIntervals() > 100)
continue;
1790 index_to_erase.insert(i);
1803 if (index_to_erase.empty()) {
1804 int num_singletons = 0;
1805 for (
const int var :
ct->linear().vars()) {
1813 if (num_singletons == num_vars) {
1815 std::vector<Domain> domains;
1816 std::vector<int64_t> coeffs;
1817 std::vector<int64_t> costs;
1818 for (
int i = 0; i < num_vars; ++i) {
1819 const int var =
ct->linear().vars(i);
1822 coeffs.push_back(
ct->linear().coeffs(i));
1825 BasicKnapsackSolver solver;
1826 const auto& result = solver.Solve(domains, coeffs, costs,
1828 if (!result.solved) {
1830 "TODO independent linear: minimize single linear constraint");
1831 }
else if (result.infeasible) {
1833 "independent linear: no DP solution to simple constraint");
1834 return MarkConstraintAsFalse(
ct);
1836 if (
ct->enforcement_literal().empty()) {
1839 for (
int i = 0; i < num_vars; ++i) {
1841 Domain(result.solution[i]))) {
1845 return RemoveConstraint(
ct);
1850 if (
ct->enforcement_literal().size() == 1) {
1851 indicator =
ct->enforcement_literal(0);
1855 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
1856 new_ct->mutable_bool_or()->add_literals(indicator);
1859 for (
int i = 0; i < num_vars; ++i) {
1860 const int64_t best_value =
1861 costs[i] > 0 ? domains[i].Min() : domains[i].Max();
1862 const int64_t other_value = result.solution[i];
1863 if (best_value == other_value) {
1865 Domain(best_value))) {
1872 other_value - best_value,
1879 best_value - other_value, other_value)) {
1885 "independent linear: with enforcement, but solved by DP");
1886 return RemoveConstraint(
ct);
1892 if (index_to_erase.empty()) {
1894 if (context_->
params().presolve_substitution_level() <= 0)
return false;
1895 if (!
ct->enforcement_literal().empty())
return false;
1899 if (rhs.Min() != rhs.Max())
return false;
1901 for (
int i = 0; i < num_vars; ++i) {
1902 const int var =
ct->linear().vars(i);
1903 const int64_t coeff =
ct->linear().coeffs(i);
1924 if (objective_coeff % coeff != 0)
continue;
1930 if (std::abs(objective_coeff) != 1)
continue;
1934 const auto term_domain =
1936 if (!exact)
continue;
1938 if (new_rhs.NumIntervals() > 100)
continue;
1961 context_->
UpdateRuleStats(
"linear: singleton column define objective.");
1964 return RemoveConstraint(
ct);
1980 "linear: singleton column in equality and in objective.");
1982 index_to_erase.insert(i);
1986 if (index_to_erase.empty())
return false;
1997 if (!
ct->enforcement_literal().empty()) {
1998 for (
const int i : index_to_erase) {
1999 const int var =
ct->linear().vars(i);
2000 auto* l = context_->
mapping_model->add_constraints()->mutable_linear();
2014 for (
int i = 0; i < num_vars; ++i) {
2015 if (index_to_erase.count(i)) {
2019 ct->mutable_linear()->set_coeffs(new_size,
ct->linear().coeffs(i));
2020 ct->mutable_linear()->set_vars(new_size,
ct->linear().vars(i));
2023 ct->mutable_linear()->mutable_vars()->Truncate(new_size);
2024 ct->mutable_linear()->mutable_coeffs()->Truncate(new_size);
2026 DivideLinearByGcd(
ct);
2032 bool CpModelPresolver::AddVarAffineRepresentativeFromLinearEquality(
2033 int target_index, ConstraintProto*
ct) {
2035 const int num_variables =
ct->linear().vars().size();
2036 for (
int i = 0; i < num_variables; ++i) {
2037 if (i == target_index)
continue;
2038 const int64_t magnitude = std::abs(
ct->linear().coeffs(i));
2040 if (gcd == 1)
return false;
2046 const int ref =
ct->linear().vars(target_index);
2047 const int64_t coeff =
ct->linear().coeffs(target_index);
2048 const int64_t rhs =
ct->linear().domain(0);
2052 if (coeff % gcd == 0)
return false;
2060 return CanonicalizeLinear(
ct);
2074 bool CpModelPresolver::PresolveLinearEqualityWithModulo(ConstraintProto*
ct) {
2076 if (
ct->constraint_case() != ConstraintProto::kLinear)
return false;
2077 if (
ct->linear().domain().size() != 2)
return false;
2078 if (
ct->linear().domain(0) !=
ct->linear().domain(1))
return false;
2079 if (!
ct->enforcement_literal().empty())
return false;
2081 const int num_variables =
ct->linear().vars().size();
2082 if (num_variables < 2)
return false;
2084 std::vector<int> mod2_indices;
2085 std::vector<int> mod3_indices;
2086 std::vector<int> mod5_indices;
2088 int64_t min_magnitude;
2089 int num_smallest = 0;
2091 for (
int i = 0; i < num_variables; ++i) {
2092 const int64_t magnitude = std::abs(
ct->linear().coeffs(i));
2093 if (num_smallest == 0 || magnitude < min_magnitude) {
2094 min_magnitude = magnitude;
2097 }
else if (magnitude == min_magnitude) {
2101 if (magnitude % 2 != 0) mod2_indices.push_back(i);
2102 if (magnitude % 3 != 0) mod3_indices.push_back(i);
2103 if (magnitude % 5 != 0) mod5_indices.push_back(i);
2106 if (mod2_indices.size() == 2) {
2108 std::vector<int> literals;
2109 for (
const int i : mod2_indices) {
2110 const int ref =
ct->linear().vars(i);
2115 literals.push_back(ref);
2118 const int64_t rhs = std::abs(
ct->linear().domain(0));
2119 context_->
UpdateRuleStats(
"linear: only two odd Booleans in equality");
2131 if (mod2_indices.size() == 1) {
2132 return AddVarAffineRepresentativeFromLinearEquality(mod2_indices[0],
ct);
2134 if (mod3_indices.size() == 1) {
2135 return AddVarAffineRepresentativeFromLinearEquality(mod3_indices[0],
ct);
2137 if (mod5_indices.size() == 1) {
2138 return AddVarAffineRepresentativeFromLinearEquality(mod5_indices[0],
ct);
2140 if (num_smallest == 1) {
2141 return AddVarAffineRepresentativeFromLinearEquality(smallest_index,
ct);
2147 bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto*
ct) {
2148 DCHECK_EQ(
ct->linear().vars().size(), 1);
2153 ?
ct->linear().coeffs(0)
2154 : -
ct->linear().coeffs(0);
2159 rhs.InverseMultiplicationBy(coeff))) {
2162 return RemoveConstraint(
ct);
2168 const bool zero_ok = rhs.Contains(0);
2169 const bool one_ok = rhs.Contains(
ct->linear().coeffs(0));
2171 if (!zero_ok && !one_ok) {
2172 return MarkConstraintAsFalse(
ct);
2174 if (zero_ok && one_ok) {
2175 return RemoveConstraint(
ct);
2177 const int ref =
ct->linear().vars(0);
2181 ct->mutable_bool_and()->add_literals(ref);
2192 if (
ct->linear().coeffs(0) == 1 &&
2197 context_->
UpdateRuleStats(
"linear1: remove abs from abs(x) in domain");
2198 const Domain implied_abs_target_domain =
2201 .IntersectionWith(context_->
DomainOf(
ct->linear().vars(0)));
2203 if (implied_abs_target_domain.IsEmpty()) {
2204 return MarkConstraintAsFalse(
ct);
2207 const Domain new_abs_var_domain =
2208 implied_abs_target_domain
2209 .UnionWith(implied_abs_target_domain.Negation())
2210 .IntersectionWith(context_->
DomainOf(abs_arg));
2212 if (new_abs_var_domain.IsEmpty()) {
2213 return MarkConstraintAsFalse(
ct);
2218 ct->mutable_linear()->add_vars(abs_arg);
2219 ct->mutable_linear()->add_coeffs(1);
2225 if (
ct->enforcement_literal_size() != 1)
return false;
2229 const int lit =
ct->enforcement_literal(0);
2230 const int var =
ct->linear().vars(0);
2231 const Domain var_domain = context_->
DomainOf(
var);
2235 if (rhs.IsEmpty()) {
2237 return MarkConstraintAsFalse(
ct);
2239 if (rhs == var_domain) {
2241 return RemoveConstraint(
ct);
2244 if (rhs.IsFixed()) {
2245 const int64_t
value = rhs.FixedValue();
2248 if (lit == encoding_lit)
return false;
2265 const Domain complement = rhs.Complement().IntersectionWith(var_domain);
2266 if (complement.IsFixed()) {
2267 const int64_t
value = complement.FixedValue();
2270 if (
NegatedRef(lit) == encoding_lit)
return false;
2289 bool CpModelPresolver::PresolveLinearOfSizeTwo(ConstraintProto*
ct) {
2290 DCHECK_EQ(
ct->linear().vars().size(), 2);
2292 const LinearConstraintProto& arg =
ct->linear();
2293 const int var1 = arg.vars(0);
2294 const int var2 = arg.vars(1);
2295 const int64_t coeff1 = arg.coeffs(0);
2296 const int64_t coeff2 = arg.coeffs(1);
2307 const bool is_equality =
2308 arg.domain_size() == 2 && arg.domain(0) == arg.domain(1);
2311 int64_t value_on_true, coeff;
2314 value_on_true = coeff1;
2319 value_on_true = coeff2;
2328 const Domain rhs_if_true =
2329 rhs.AdditionWith(Domain(-value_on_true)).InverseMultiplicationBy(coeff);
2330 const Domain rhs_if_false = rhs.InverseMultiplicationBy(coeff);
2331 const bool implied_false =
2333 const bool implied_true =
2335 if (implied_true && implied_false) {
2337 return MarkConstraintAsFalse(
ct);
2338 }
else if (implied_true) {
2339 context_->
UpdateRuleStats(
"linear2: Boolean with one feasible value.");
2342 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2343 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
2344 new_ct->mutable_bool_and()->add_literals(lit);
2348 ct->mutable_linear()->Clear();
2349 ct->mutable_linear()->add_vars(
var);
2350 ct->mutable_linear()->add_coeffs(1);
2352 return PresolveLinearOfSizeOne(
ct) ||
true;
2353 }
else if (implied_false) {
2354 context_->
UpdateRuleStats(
"linear2: Boolean with one feasible value.");
2357 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2358 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
2359 new_ct->mutable_bool_and()->add_literals(
NegatedRef(lit));
2363 ct->mutable_linear()->Clear();
2364 ct->mutable_linear()->add_vars(
var);
2365 ct->mutable_linear()->add_coeffs(1);
2367 return PresolveLinearOfSizeOne(
ct) ||
true;
2368 }
else if (
ct->enforcement_literal().empty() &&
2377 const Domain var_domain = context_->
DomainOf(
var);
2378 if (!var_domain.IsIncludedIn(rhs_if_true)) {
2379 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2380 new_ct->add_enforcement_literal(lit);
2381 new_ct->mutable_linear()->add_vars(
var);
2382 new_ct->mutable_linear()->add_coeffs(1);
2384 new_ct->mutable_linear());
2388 if (!var_domain.IsIncludedIn(rhs_if_false)) {
2389 ConstraintProto* new_ct = context_->
working_model->add_constraints();
2390 new_ct->add_enforcement_literal(
NegatedRef(lit));
2391 new_ct->mutable_linear()->add_vars(
var);
2392 new_ct->mutable_linear()->add_coeffs(1);
2394 new_ct->mutable_linear());
2408 const int64_t rhs = arg.domain(0);
2409 if (
ct->enforcement_literal().empty()) {
2417 }
else if (coeff2 == 1) {
2419 }
else if (coeff1 == -1) {
2421 }
else if (coeff2 == -1) {
2433 if (added)
return RemoveConstraint(
ct);
2443 "linear2: implied ax + by = cte has no solutions");
2444 return MarkConstraintAsFalse(
ct);
2446 const Domain reduced_domain =
2452 .InverseMultiplicationBy(-
a));
2454 if (reduced_domain.IsEmpty()) {
2456 "linear2: implied ax + by = cte has no solutions");
2457 return MarkConstraintAsFalse(
ct);
2460 if (reduced_domain.Size() == 1) {
2461 const int64_t z = reduced_domain.FixedValue();
2462 const int64_t value1 = x0 +
b * z;
2463 const int64_t value2 = y0 -
a * z;
2467 DCHECK_EQ(coeff1 * value1 + coeff2 * value2, rhs);
2469 ConstraintProto* imply1 = context_->
working_model->add_constraints();
2470 *imply1->mutable_enforcement_literal() =
ct->enforcement_literal();
2471 imply1->mutable_linear()->add_vars(var1);
2472 imply1->mutable_linear()->add_coeffs(1);
2473 imply1->mutable_linear()->add_domain(value1);
2474 imply1->mutable_linear()->add_domain(value1);
2476 ConstraintProto* imply2 = context_->
working_model->add_constraints();
2477 *imply2->mutable_enforcement_literal() =
ct->enforcement_literal();
2478 imply2->mutable_linear()->add_vars(var2);
2479 imply2->mutable_linear()->add_coeffs(1);
2480 imply2->mutable_linear()->add_domain(value2);
2481 imply2->mutable_linear()->add_domain(value2);
2483 "linear2: implied ax + by = cte has only one solution");
2485 return RemoveConstraint(
ct);
2492 bool CpModelPresolver::PresolveSmallLinear(ConstraintProto*
ct) {
2493 if (
ct->constraint_case() != ConstraintProto::kLinear)
return false;
2496 if (
ct->linear().vars().empty()) {
2499 if (rhs.Contains(0)) {
2500 return RemoveConstraint(
ct);
2502 return MarkConstraintAsFalse(
ct);
2504 }
else if (
ct->linear().vars().size() == 1) {
2505 return PresolveLinearOfSizeOne(
ct);
2506 }
else if (
ct->linear().vars().size() == 2) {
2507 return PresolveLinearOfSizeTwo(
ct);
2513 bool CpModelPresolver::PresolveDiophantine(ConstraintProto*
ct) {
2514 if (
ct->constraint_case() != ConstraintProto::kLinear)
return false;
2515 if (
ct->linear().vars().size() <= 1)
return false;
2519 const LinearConstraintProto& linear_constraint =
ct->linear();
2520 if (linear_constraint.domain_size() != 2)
return false;
2521 if (linear_constraint.domain(0) != linear_constraint.domain(1))
return false;
2523 std::vector<int64_t> lbs(linear_constraint.vars_size());
2524 std::vector<int64_t> ubs(linear_constraint.vars_size());
2525 for (
int i = 0; i < linear_constraint.vars_size(); ++i) {
2526 lbs[i] = context_->
MinOf(linear_constraint.vars(i));
2527 ubs[i] = context_->
MaxOf(linear_constraint.vars(i));
2530 linear_constraint.coeffs(), linear_constraint.domain(0), lbs, ubs);
2532 if (!diophantine_solution.has_solutions) {
2534 return MarkConstraintAsFalse(
ct);
2536 if (diophantine_solution.no_reformulation_needed)
return false;
2539 for (
const std::vector<absl::int128>&
b : diophantine_solution.kernel_basis) {
2542 "diophantine: couldn't apply due to int64_t overflow");
2548 "diophantine: couldn't apply due to int64_t overflow");
2552 const int num_replaced_variables =
2553 static_cast<int>(diophantine_solution.special_solution.size());
2554 const int num_new_variables =
2555 static_cast<int>(diophantine_solution.kernel_vars_lbs.size());
2556 DCHECK_EQ(num_new_variables + 1, num_replaced_variables);
2557 for (
int i = 0; i < num_new_variables; ++i) {
2561 "diophantine: couldn't apply due to int64_t overflow");
2571 std::vector<int> new_variables(num_new_variables);
2572 for (
int i = 0; i < num_new_variables; ++i) {
2573 new_variables[i] = context_->
working_model->variables_size();
2576 static_cast<int64_t
>(diophantine_solution.kernel_vars_lbs[i]));
2578 static_cast<int64_t
>(diophantine_solution.kernel_vars_ubs[i]));
2579 if (!
ct->name().empty()) {
2580 var->set_name(absl::StrCat(
"u_diophantine_",
ct->name(),
"_", i));
2590 for (
int i = 0; i < num_replaced_variables; ++i) {
2591 ConstraintProto* identity = context_->
working_model->add_constraints();
2592 LinearConstraintProto* lin = identity->mutable_linear();
2593 if (!
ct->name().empty()) {
2594 identity->set_name(absl::StrCat(
"c_diophantine_",
ct->name(),
"_", i));
2596 *identity->mutable_enforcement_literal() =
ct->enforcement_literal();
2598 linear_constraint.vars(diophantine_solution.index_permutation[i]));
2601 static_cast<int64_t
>(diophantine_solution.special_solution[i]));
2603 static_cast<int64_t
>(diophantine_solution.special_solution[i]));
2604 for (
int j =
std::max(1, i); j < num_replaced_variables; ++j) {
2605 lin->add_vars(new_variables[j - 1]);
2607 -
static_cast<int64_t
>(diophantine_solution.kernel_basis[j - 1][i]));
2609 for (
int j = num_replaced_variables; j < linear_constraint.vars_size();
2612 linear_constraint.vars(diophantine_solution.index_permutation[j]));
2614 -
static_cast<int64_t
>(diophantine_solution.kernel_basis[j - 1][i]));
2623 "diophantine: couldn't apply due to overflowing activity of new "
2626 context_->
working_model->mutable_constraints()->DeleteSubrange(
2627 context_->
working_model->constraints_size() - i - 1, i + 1);
2628 context_->
working_model->mutable_variables()->DeleteSubrange(
2629 context_->
working_model->variables_size() - num_new_variables,
2637 std::string log_eq = absl::StrCat(linear_constraint.domain(0),
" = ");
2638 const int terms_to_show = std::min<int>(15, linear_constraint.vars_size());
2639 for (
int i = 0; i < terms_to_show; ++i) {
2640 if (i > 0) absl::StrAppend(&log_eq,
" + ");
2643 linear_constraint.coeffs(diophantine_solution.index_permutation[i]),
2645 linear_constraint.vars(diophantine_solution.index_permutation[i]));
2647 if (terms_to_show < linear_constraint.vars_size()) {
2648 absl::StrAppend(&log_eq,
"+ ... (", linear_constraint.vars_size(),
2651 VLOG(2) <<
"[Diophantine] " << log_eq;
2656 return RemoveConstraint(
ct);
2671 void CpModelPresolver::TryToReduceCoefficientsOfLinearConstraint(
2672 int c, ConstraintProto*
ct) {
2673 if (
ct->constraint_case() != ConstraintProto::kLinear)
return;
2677 const LinearConstraintProto& lin =
ct->linear();
2679 if (rhs.NumIntervals() != 1)
return;
2684 int64_t max_variation = 0;
2687 int64_t max_variation;
2690 std::vector<Entry> entries;
2691 std::vector<int> vars;
2692 std::vector<int64_t> coeffs;
2693 std::vector<int64_t> magnitudes;
2694 std::vector<int64_t> lbs;
2695 std::vector<int64_t> ubs;
2696 int64_t max_magnitude = 0;
2697 const int num_terms = lin.vars().size();
2698 for (
int i = 0; i < num_terms; ++i) {
2699 const int64_t coeff = lin.coeffs(i);
2700 const int64_t magnitude = std::abs(lin.coeffs(i));
2701 if (magnitude == 0)
continue;
2702 max_magnitude =
std::max(max_magnitude, magnitude);
2707 lb = context_->
MinOf(lin.vars(i));
2708 ub = context_->
MaxOf(lin.vars(i));
2710 lb = -context_->
MaxOf(lin.vars(i));
2711 ub = -context_->
MinOf(lin.vars(i));
2713 lb_sum += lb * magnitude;
2714 ub_sum += ub * magnitude;
2717 if (lb == ub)
return;
2719 vars.push_back(lin.vars(i));
2722 coeffs.push_back(coeff);
2723 magnitudes.push_back(magnitude);
2724 entries.push_back({magnitude, magnitude * (ub - lb), i});
2725 max_variation += entries.back().max_variation;
2730 if (lb_sum > rhs.Max() || rhs.Min() > ub_sum) {
2731 (void)MarkConstraintAsFalse(
ct);
2735 const IntegerValue rhs_ub(
CapSub(rhs.Max(), lb_sum));
2736 const IntegerValue rhs_lb(
CapSub(ub_sum, rhs.Min()));
2737 const bool use_ub = max_variation > rhs_ub;
2738 const bool use_lb = max_variation > rhs_lb;
2739 if (!use_ub && !use_lb) {
2740 (void)RemoveConstraint(
ct);
2746 if (max_magnitude <= 1)
return;
2751 lb_feasible_.
Reset(rhs_lb.value());
2752 lb_infeasible_.
Reset(rhs.Min() - lb_sum - 1);
2755 ub_feasible_.
Reset(rhs_ub.value());
2756 ub_infeasible_.
Reset(ub_sum - rhs.Max() - 1);
2762 int64_t max_error = max_variation;
2764 entries.begin(), entries.end(),
2765 [](
const Entry&
a,
const Entry&
b) { return a.magnitude > b.magnitude; });
2766 std::vector<int64_t> divisors;
2768 for (
int i = 0; i < entries.size(); ++i) {
2769 const Entry& e = entries[i];
2771 max_error -= e.max_variation;
2777 range += e.max_variation / e.magnitude;
2778 if (i + 1 < entries.size() && e.magnitude == entries[i + 1].magnitude) {
2781 const int64_t saved_range =
range;
2784 if (e.magnitude > 1) {
2789 divisors.push_back(e.magnitude);
2793 bool simplify_lb =
false;
2804 if (lb_infeasible_.
CurrentMax() + max_error <= lb_infeasible_.
Bound()) {
2810 bool simplify_ub =
false;
2817 if (ub_infeasible_.
CurrentMax() + max_error <= ub_infeasible_.
Bound()) {
2824 if (max_error == 0)
break;
2825 if (simplify_lb && simplify_ub) {
2828 LinearConstraintProto* mutable_linear =
ct->mutable_linear();
2829 mutable_linear->clear_vars();
2830 mutable_linear->clear_coeffs();
2831 int64_t shift_lb = 0;
2832 int64_t shift_ub = 0;
2833 for (
int j = 0; j <= i; ++j) {
2834 const int index = entries[j].index;
2835 const int64_t m = magnitudes[
index];
2836 shift_lb += lbs[
index] * m;
2837 shift_ub += ubs[
index] * m;
2838 mutable_linear->add_vars(vars[
index]);
2839 mutable_linear->add_coeffs(coeffs[
index]);
2846 const int64_t new_rhs_lb =
2847 use_lb ? shift_ub - lb_feasible_.
CurrentMax() : shift_lb;
2848 const int64_t new_rhs_ub =
2849 use_ub ? shift_lb + ub_feasible_.
CurrentMax() : shift_ub;
2850 if (new_rhs_lb > new_rhs_ub) {
2851 (void)MarkConstraintAsFalse(
ct);
2856 DivideLinearByGcd(
ct);
2865 if (DivideLinearByGcd(
ct)) {
2876 const int64_t new_rhs_lb =
2877 use_lb ? ub_sum - lb_feasible_.
CurrentMax() : lb_sum;
2878 const int64_t new_rhs_ub =
2879 use_ub ? lb_sum + ub_feasible_.
CurrentMax() : ub_sum;
2880 if (new_rhs_lb > new_rhs_ub) {
2881 (void)MarkConstraintAsFalse(
ct);
2889 if (divisors.size() > 3) divisors.resize(3);
2890 for (
const int64_t divisor : divisors) {
2894 divisor, magnitudes, lbs, ubs, rhs.Max(), &new_ub)) {
2899 int64_t minus_new_lb;
2900 for (
int i = 0; i < lbs.size(); ++i) {
2906 divisor, magnitudes, lbs, ubs, -rhs.Min(), &minus_new_lb)) {
2907 for (
int i = 0; i < lbs.size(); ++i) {
2917 LinearConstraintProto* mutable_linear =
ct->mutable_linear();
2918 mutable_linear->clear_vars();
2919 mutable_linear->clear_coeffs();
2920 for (
int i = 0; i < coeffs.size(); ++i) {
2921 const int64_t new_coeff =
ClosestMultiple(coeffs[i], divisor) / divisor;
2922 if (new_coeff == 0)
continue;
2923 mutable_linear->add_vars(vars[i]);
2924 mutable_linear->add_coeffs(new_coeff);
2926 const Domain new_rhs = Domain(-minus_new_lb, new_ub);
2927 if (new_rhs.IsEmpty()) {
2928 (void)MarkConstraintAsFalse(
ct);
2942 bool RhsCanBeFixedToMin(int64_t coeff,
const Domain& var_domain,
2943 const Domain& terms,
const Domain& rhs) {
2944 if (var_domain.NumIntervals() != 1)
return false;
2945 if (std::abs(coeff) != 1)
return false;
2953 if (coeff == 1 && terms.Max() + var_domain.Min() <= rhs.Min()) {
2956 if (coeff == -1 && terms.Max() - var_domain.Max() <= rhs.Min()) {
2962 bool RhsCanBeFixedToMax(int64_t coeff,
const Domain& var_domain,
2963 const Domain& terms,
const Domain& rhs) {
2964 if (var_domain.NumIntervals() != 1)
return false;
2965 if (std::abs(coeff) != 1)
return false;
2967 if (coeff == 1 && terms.Min() + var_domain.Max() >= rhs.Max()) {
2970 if (coeff == -1 && terms.Min() - var_domain.Min() >= rhs.Max()) {
2976 int FixLiteralFromSet(
const absl::flat_hash_set<int>& literals_at_true,
2977 LinearConstraintProto* linear) {
2980 const int num_terms = linear->vars().size();
2982 for (
int i = 0; i < num_terms; ++i) {
2983 const int var = linear->vars(i);
2984 const int64_t coeff = linear->coeffs(i);
2985 if (literals_at_true.contains(
var)) {
2990 linear->set_vars(new_size,
var);
2991 linear->set_coeffs(new_size, coeff);
2998 linear->mutable_vars()->Truncate(new_size);
2999 linear->mutable_coeffs()->Truncate(new_size);
3014 void CpModelPresolver::DetectAndProcessAtMostOneInLinear(
3015 int ct_index, ConstraintProto*
ct, ActivityBoundHelper* helper) {
3016 if (
ct->constraint_case() != ConstraintProto::kLinear)
return;
3017 if (
ct->linear().vars().size() <= 2)
return;
3021 Domain non_boolean_domain(0);
3022 const int num_ct_terms =
ct->linear().vars().size();
3024 int64_t max_magnitude = 0;
3025 for (
int i = 0; i < num_ct_terms; ++i) {
3027 int ref =
ct->linear().vars(i);
3028 int64_t coeff =
ct->linear().coeffs(i);
3034 tmp_terms_.push_back({ref, coeff});
3035 min_magnitude =
std::min(min_magnitude, std::abs(coeff));
3036 max_magnitude =
std::max(max_magnitude, std::abs(coeff));
3038 non_boolean_domain =
3042 .RelaxIfTooComplex();
3043 temp_ct_.mutable_linear()->add_vars(ref);
3044 temp_ct_.mutable_linear()->add_coeffs(coeff);
3049 if (tmp_terms_.empty())
return;
3060 if (non_boolean_domain == Domain(0) && rhs.NumIntervals() == 1 &&
3061 min_magnitude < max_magnitude) {
3062 int64_t min_activity = 0;
3063 int64_t max_activity = 0;
3064 for (
const auto [ref, coeff] : tmp_terms_) {
3066 max_activity += coeff;
3068 min_activity += coeff;
3071 const int64_t transformed_rhs = rhs.Max() - min_activity;
3072 if (min_activity >= rhs.Min() && max_magnitude <= transformed_rhs) {
3073 std::vector<int> literals;
3074 for (
const auto [ref, coeff] : tmp_terms_) {
3075 if (coeff + min_magnitude > transformed_rhs)
continue;
3076 literals.push_back(coeff > 0 ? ref :
NegatedRef(ref));
3078 if (helper->IsAmo(literals)) {
3082 for (
int i = 0; i < num_ct_terms; ++i) {
3084 if (
ct->linear().coeffs(i) > 0) {
3085 ct->mutable_linear()->set_coeffs(i, 1);
3087 ct->mutable_linear()->set_coeffs(i, -1);
3098 const int64_t min_bool_activity =
3099 helper->ComputeMinActivity(tmp_terms_, &conditional_mins_);
3100 const int64_t max_bool_activity =
3101 helper->ComputeMaxActivity(tmp_terms_, &conditional_maxs_);
3105 const Domain activity = non_boolean_domain.AdditionWith(
3106 Domain(min_bool_activity, max_bool_activity));
3107 if (activity.IntersectionWith(rhs).IsEmpty()) {
3109 context_->
UpdateRuleStats(
"linear + amo: infeasible linear constraint");
3110 (void)MarkConstraintAsFalse(
ct);
3113 }
else if (activity.IsIncludedIn(rhs)) {
3122 std::vector<int> new_enforcement;
3123 std::vector<int> must_be_true;
3124 for (
int i = 0; i < tmp_terms_.size(); ++i) {
3125 const int ref = tmp_terms_[i].first;
3127 const Domain bool0(conditional_mins_[i][0], conditional_maxs_[i][0]);
3128 const Domain activity0 = bool0.AdditionWith(non_boolean_domain);
3129 if (activity0.IntersectionWith(rhs).IsEmpty()) {
3131 must_be_true.push_back(ref);
3132 }
else if (activity0.IsIncludedIn(rhs)) {
3134 new_enforcement.push_back(ref);
3137 const Domain bool1(conditional_mins_[i][1], conditional_maxs_[i][1]);
3138 const Domain activity1 = bool1.AdditionWith(non_boolean_domain);
3139 if (activity1.IntersectionWith(rhs).IsEmpty()) {
3142 }
else if (activity1.IsIncludedIn(rhs)) {
3153 if (
ct->enforcement_literal().empty() && !must_be_true.empty()) {
3157 must_be_true.size());
3158 for (
const int lit : must_be_true) {
3163 if (!new_enforcement.empty()) {
3164 context_->
UpdateRuleStats(
"linear + amo: extracted enforcement literal",
3165 new_enforcement.size());
3166 for (
const int ref : new_enforcement) {
3167 ct->add_enforcement_literal(ref);
3171 if (!
ct->enforcement_literal().empty()) {
3172 const int old_enf_size =
ct->enforcement_literal().size();
3173 if (!helper->PresolveEnforcement(
ct->linear().vars(),
ct, &temp_set_)) {
3179 if (
ct->enforcement_literal().size() < old_enf_size) {
3180 context_->
UpdateRuleStats(
"linear + amo: simplified enforcement list");
3184 for (
const int lit : must_be_true) {
3189 "linear + amo: advanced infeasible linear constraint");
3190 (void)MarkConstraintAsFalse(
ct);
3197 if (
ct->enforcement_literal().size() == 1 && !must_be_true.empty()) {
3202 ConstraintProto* new_ct = context_->
working_model->add_constraints();
3203 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
3204 for (
const int lit : must_be_true) {
3205 new_ct->mutable_bool_and()->add_literals(lit);
3206 temp_set_.insert(lit);
3211 const int num_fixed = FixLiteralFromSet(temp_set_,
ct->mutable_linear());
3212 if (num_fixed > new_enforcement.size()) {
3214 "linear + amo: fixed literal implied by enforcement");
3216 if (num_fixed > 0) {
3222 if (
ct->enforcement_literal().empty() && !temp_ct_.linear().vars().empty()) {
3225 Domain(min_bool_activity, max_bool_activity).Negation()),
3226 temp_ct_.mutable_linear());
3227 PropagateDomainsInLinear(-1, &temp_ct_);
3231 bool CpModelPresolver::PropagateDomainsInLinear(
int ct_index,
3232 ConstraintProto*
ct) {
3233 if (
ct->constraint_case() != ConstraintProto::kLinear)
return false;
3239 const int num_vars =
ct->linear().vars_size();
3240 term_domains.resize(num_vars + 1);
3241 left_domains.resize(num_vars + 1);
3242 left_domains[0] = Domain(0);
3243 for (
int i = 0; i < num_vars; ++i) {
3244 const int var =
ct->linear().vars(i);
3245 const int64_t coeff =
ct->linear().coeffs(i);
3248 left_domains[i + 1] =
3251 const Domain& implied_rhs = left_domains[num_vars];
3255 if (implied_rhs.IsIncludedIn(old_rhs)) {
3257 return RemoveConstraint(
ct);
3261 Domain rhs = old_rhs.SimplifyUsingImpliedDomain(implied_rhs);
3262 if (rhs.IsEmpty()) {
3264 return MarkConstraintAsFalse(
ct);
3266 if (rhs != old_rhs) {
3267 if (ct_index != -1) context_->
UpdateRuleStats(
"linear: simplified rhs");
3272 if (
ct->enforcement_literal().size() > 1)
return false;
3274 bool new_bounds =
false;
3275 bool recanonicalize =
false;
3276 Domain negated_rhs = rhs.Negation();
3277 Domain right_domain(0);
3279 Domain implied_term_domain;
3280 term_domains[num_vars] = Domain(0);
3281 for (
int i = num_vars - 1; i >= 0; --i) {
3282 const int var =
ct->linear().vars(i);
3283 const int64_t var_coeff =
ct->linear().coeffs(i);
3285 right_domain.AdditionWith(term_domains[i + 1]).RelaxIfTooComplex();
3286 implied_term_domain = left_domains[i].AdditionWith(right_domain);
3287 new_domain = implied_term_domain.AdditionWith(negated_rhs)
3288 .InverseMultiplicationBy(-var_coeff);
3290 if (
ct->enforcement_literal().empty()) {
3295 }
else if (
ct->enforcement_literal().size() == 1) {
3306 recanonicalize =
true;
3311 if (ct_index == -1)
continue;
3312 if (!
ct->enforcement_literal().empty())
continue;
3324 if (rhs.Min() != rhs.Max() &&
3327 const bool same_sign = (var_coeff > 0) == (obj_coeff > 0);
3329 if (same_sign && RhsCanBeFixedToMin(var_coeff, context_->
DomainOf(
var),
3330 implied_term_domain, rhs)) {
3331 rhs = Domain(rhs.Min());
3334 if (!same_sign && RhsCanBeFixedToMax(var_coeff, context_->
DomainOf(
var),
3335 implied_term_domain, rhs)) {
3336 rhs = Domain(rhs.Max());
3342 negated_rhs = rhs.Negation();
3346 right_domain = Domain(0);
3360 if (
ct->linear().vars().size() <= 2)
continue;
3365 if (rhs.Min() != rhs.Max())
continue;
3371 if (context_->
DomainOf(
var) != new_domain)
continue;
3372 if (std::abs(var_coeff) != 1)
continue;
3373 if (context_->
params().presolve_substitution_level() <= 0)
continue;
3379 bool is_in_objective =
false;
3381 is_in_objective =
true;
3387 if (is_in_objective) col_size--;
3388 const int row_size =
ct->linear().vars_size();
3392 const int num_entries_added = (row_size - 1) * (col_size - 1);
3393 const int num_entries_removed = col_size + row_size - 1;
3395 if (num_entries_added > num_entries_removed) {
3401 std::vector<int> others;
3409 if (c == ct_index)
continue;
3410 if (context_->
working_model->constraints(c).constraint_case() !=
3411 ConstraintProto::kLinear) {
3415 for (
const int ref :
3416 context_->
working_model->constraints(c).enforcement_literal()) {
3422 others.push_back(c);
3424 if (abort)
continue;
3427 for (
const int c : others) {
3437 CanonicalizeLinear(context_->
working_model->mutable_constraints(c));
3446 if (is_in_objective &&
3452 absl::StrCat(
"linear: variable substitution ", others.size()));
3463 const int ct_index = context_->
mapping_model->constraints().size();
3465 LinearConstraintProto* mapping_linear_ct =
3468 std::swap(mapping_linear_ct->mutable_vars()->at(0),
3469 mapping_linear_ct->mutable_vars()->at(i));
3470 std::swap(mapping_linear_ct->mutable_coeffs()->at(0),
3471 mapping_linear_ct->mutable_coeffs()->at(i));
3472 return RemoveConstraint(
ct);
3476 if (ct_index == -1) {
3479 "linear: reduced variable domains in derived constraint");
3487 if (recanonicalize)
return CanonicalizeLinear(
ct);
3493 void CpModelPresolver::LowerThanCoeffStrengthening(
bool from_lower_bound,
3494 int64_t min_magnitude,
3496 ConstraintProto*
ct) {
3497 const LinearConstraintProto& arg =
ct->linear();
3498 const int64_t second_threshold = rhs - min_magnitude;
3499 const int num_vars = arg.vars_size();
3512 if (min_magnitude <= second_threshold) {
3514 int64_t max_magnitude_left = 0;
3515 int64_t max_activity_left = 0;
3516 int64_t activity_when_coeff_are_one = 0;
3518 for (
int i = 0; i < num_vars; ++i) {
3519 const int64_t magnitude = std::abs(arg.coeffs(i));
3520 if (magnitude <= second_threshold) {
3522 max_magnitude_left =
std::max(max_magnitude_left, magnitude);
3523 const int64_t bound_diff =
3524 context_->
MaxOf(arg.vars(i)) - context_->
MinOf(arg.vars(i));
3525 activity_when_coeff_are_one += magnitude;
3526 max_activity_left += magnitude * bound_diff;
3529 CHECK_GT(min_magnitude, 0);
3530 CHECK_LE(min_magnitude, max_magnitude_left);
3533 int64_t new_rhs = 0;
3534 bool set_all_to_one =
false;
3535 if (max_activity_left <= rhs) {
3538 new_rhs = activity_when_coeff_are_one;
3539 set_all_to_one =
true;
3540 }
else if (rhs / min_magnitude == rhs / max_magnitude_left) {
3543 new_rhs = rhs / min_magnitude;
3544 set_all_to_one =
true;
3545 }
else if (gcd > 1) {
3548 new_rhs = rhs / gcd;
3552 int64_t rhs_offset = 0;
3553 for (
int i = 0; i < num_vars; ++i) {
3554 const int ref = arg.vars(i);
3555 const int64_t coeff = from_lower_bound ? arg.coeffs(i) : -arg.coeffs(i);
3558 const int64_t magnitude = std::abs(coeff);
3559 if (magnitude > rhs) {
3560 new_coeff = new_rhs + 1;
3561 }
else if (magnitude > second_threshold) {
3562 new_coeff = new_rhs;
3564 new_coeff = set_all_to_one ? 1 : magnitude / gcd;
3570 ct->mutable_linear()->set_coeffs(i, new_coeff);
3571 rhs_offset += new_coeff * context_->
MinOf(ref);
3573 ct->mutable_linear()->set_coeffs(i, -new_coeff);
3574 rhs_offset -= new_coeff * context_->
MaxOf(ref);
3578 ct->mutable_linear());
3583 int64_t rhs_offset = 0;
3584 for (
int i = 0; i < num_vars; ++i) {
3585 int ref = arg.vars(i);
3586 int64_t coeff = arg.coeffs(i);
3593 if (
ct->enforcement_literal().empty()) {
3597 ref, Domain(from_lower_bound ? context_->
MinOf(ref)
3598 : context_->
MaxOf(ref))));
3604 if (coeff > second_threshold && coeff < rhs) {
3606 "linear: coefficient strengthening by increasing it.");
3607 if (from_lower_bound) {
3609 rhs_offset -= (coeff - rhs) * context_->
MinOf(ref);
3612 rhs_offset -= (coeff - rhs) * context_->
MaxOf(ref);
3614 ct->mutable_linear()->set_coeffs(i, arg.coeffs(i) > 0 ? rhs : -rhs);
3617 if (rhs_offset != 0) {
3619 ct->mutable_linear());
3630 void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
3631 int ct_index, ConstraintProto*
ct) {
3632 if (
ct->constraint_case() != ConstraintProto::kLinear)
return;
3635 const LinearConstraintProto& arg =
ct->linear();
3636 const int num_vars = arg.vars_size();
3640 if (num_vars <= 1)
return;
3642 int64_t min_sum = 0;
3643 int64_t max_sum = 0;
3644 int64_t max_coeff_magnitude = 0;
3646 for (
int i = 0; i < num_vars; ++i) {
3647 const int ref = arg.vars(i);
3648 const int64_t coeff = arg.coeffs(i);
3649 const int64_t term_a = coeff * context_->
MinOf(ref);
3650 const int64_t term_b = coeff * context_->
MaxOf(ref);
3651 max_coeff_magnitude =
std::max(max_coeff_magnitude, std::abs(coeff));
3652 min_coeff_magnitude =
std::min(min_coeff_magnitude, std::abs(coeff));
3653 min_sum +=
std::min(term_a, term_b);
3654 max_sum +=
std::max(term_a, term_b);
3656 if (max_coeff_magnitude == 1)
return;
3664 const auto& domain =
ct->linear().domain();
3665 const int64_t ub_threshold = domain[domain.size() - 2] - min_sum;
3666 const int64_t lb_threshold = max_sum - domain[1];
3667 if (max_coeff_magnitude + min_coeff_magnitude <
3668 std::max(ub_threshold, lb_threshold)) {
3673 if (domain.size() == 2 && min_coeff_magnitude > 1 &&
3674 min_coeff_magnitude < max_coeff_magnitude) {
3675 const int64_t rhs_min = domain[0];
3676 const int64_t rhs_max = domain[1];
3677 if (min_sum >= rhs_min &&
3678 max_coeff_magnitude + min_coeff_magnitude > rhs_max - min_sum) {
3679 LowerThanCoeffStrengthening(
true,
3680 min_coeff_magnitude, rhs_max - min_sum,
ct);
3683 if (max_sum <= rhs_max &&
3684 max_coeff_magnitude + min_coeff_magnitude > max_sum - rhs_min) {
3685 LowerThanCoeffStrengthening(
false,
3686 min_coeff_magnitude, max_sum - rhs_min,
ct);
3706 const bool lower_bounded = min_sum < rhs_domain.Min();
3707 const bool upper_bounded = max_sum > rhs_domain.Max();
3708 if (!lower_bounded && !upper_bounded)
return;
3709 if (lower_bounded && upper_bounded) {
3714 if (max_coeff_magnitude <
std::max(ub_threshold, lb_threshold))
return;
3717 ConstraintProto* new_ct1 = context_->
working_model->add_constraints();
3719 if (!
ct->name().empty()) {
3720 new_ct1->set_name(absl::StrCat(
ct->name(),
" (part 1)"));
3723 new_ct1->mutable_linear());
3725 ConstraintProto* new_ct2 = context_->
working_model->add_constraints();
3727 if (!
ct->name().empty()) {
3728 new_ct2->set_name(absl::StrCat(
ct->name(),
" (part 2)"));
3731 new_ct2->mutable_linear());
3742 const int64_t threshold = lower_bounded ? ub_threshold : lb_threshold;
3751 threshold - min_coeff_magnitude);
3759 if (rhs_domain.NumIntervals() > 1) {
3760 second_threshold = threshold;
3768 const bool only_extract_booleans =
3769 !context_->
params().presolve_extract_integer_enforcement() ||
3775 int64_t rhs_offset = 0;
3776 bool some_integer_encoding_were_extracted =
false;
3777 LinearConstraintProto* mutable_arg =
ct->mutable_linear();
3778 for (
int i = 0; i < arg.vars_size(); ++i) {
3779 int ref = arg.vars(i);
3780 int64_t coeff = arg.coeffs(i);
3789 if (context_->
IsFixed(ref) || coeff < threshold ||
3790 (only_extract_booleans && !is_boolean)) {
3791 mutable_arg->set_vars(new_size, mutable_arg->vars(i));
3793 int64_t new_magnitude = std::abs(arg.coeffs(i));
3794 if (coeff > threshold) {
3797 new_magnitude = threshold;
3799 }
else if (coeff > second_threshold && coeff < threshold) {
3802 new_magnitude = second_threshold;
3804 "linear: advanced coefficient strenghtening.");
3806 if (coeff != new_magnitude) {
3807 if (lower_bounded) {
3809 rhs_offset -= (coeff - new_magnitude) * context_->
MinOf(ref);
3812 rhs_offset -= (coeff - new_magnitude) * context_->
MaxOf(ref);
3816 mutable_arg->set_coeffs(
3817 new_size, arg.coeffs(i) > 0 ? new_magnitude : -new_magnitude);
3825 some_integer_encoding_were_extracted =
true;
3827 "linear: extracted integer enforcement literal");
3829 if (lower_bounded) {
3830 ct->add_enforcement_literal(is_boolean
3833 ref, context_->
MinOf(ref)));
3834 rhs_offset -= coeff * context_->
MinOf(ref);
3836 ct->add_enforcement_literal(is_boolean
3839 ref, context_->
MaxOf(ref)));
3840 rhs_offset -= coeff * context_->
MaxOf(ref);
3843 mutable_arg->mutable_vars()->Truncate(new_size);
3844 mutable_arg->mutable_coeffs()->Truncate(new_size);
3846 if (some_integer_encoding_were_extracted || new_size == 1) {
3852 void CpModelPresolver::ExtractAtMostOneFromLinear(ConstraintProto*
ct) {
3857 const LinearConstraintProto& arg =
ct->linear();
3858 const int num_vars = arg.vars_size();
3859 int64_t min_sum = 0;
3860 int64_t max_sum = 0;
3861 for (
int i = 0; i < num_vars; ++i) {
3862 const int ref = arg.vars(i);
3863 const int64_t coeff = arg.coeffs(i);
3864 const int64_t term_a = coeff * context_->
MinOf(ref);
3865 const int64_t term_b = coeff * context_->
MaxOf(ref);
3866 min_sum +=
std::min(term_a, term_b);
3867 max_sum +=
std::max(term_a, term_b);
3869 for (
const int type : {0, 1}) {
3870 std::vector<int> at_most_one;
3871 for (
int i = 0; i < num_vars; ++i) {
3872 const int ref = arg.vars(i);
3873 const int64_t coeff = arg.coeffs(i);
3874 if (context_->
MinOf(ref) != 0)
continue;
3875 if (context_->
MaxOf(ref) != 1)
continue;
3880 if (min_sum + 2 * std::abs(coeff) > rhs.Max()) {
3881 at_most_one.push_back(coeff > 0 ? ref :
NegatedRef(ref));
3884 if (max_sum - 2 * std::abs(coeff) < rhs.Min()) {
3885 at_most_one.push_back(coeff > 0 ?
NegatedRef(ref) : ref);
3889 if (at_most_one.size() > 1) {
3895 ConstraintProto* new_ct = context_->
working_model->add_constraints();
3896 new_ct->set_name(
ct->name());
3897 for (
const int ref : at_most_one) {
3898 new_ct->mutable_at_most_one()->add_literals(ref);
3907 bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto*
ct) {
3908 if (
ct->constraint_case() != ConstraintProto::kLinear)
return false;
3911 const LinearConstraintProto& arg =
ct->linear();
3912 const int num_vars = arg.vars_size();
3914 int64_t max_coeff = 0;
3915 int64_t min_sum = 0;
3916 int64_t max_sum = 0;
3917 for (
int i = 0; i < num_vars; ++i) {
3919 const int var = arg.vars(i);
3920 const int64_t coeff = arg.coeffs(i);
3923 if (context_->
MinOf(
var) != 0)
return false;
3924 if (context_->
MaxOf(
var) != 1)
return false;
3928 min_coeff =
std::min(min_coeff, coeff);
3929 max_coeff =
std::max(max_coeff, coeff);
3933 min_coeff =
std::min(min_coeff, -coeff);
3934 max_coeff =
std::max(max_coeff, -coeff);
3937 CHECK_LE(min_coeff, max_coeff);
3946 if ((!rhs_domain.Contains(min_sum) &&
3947 min_sum + min_coeff > rhs_domain.Max()) ||
3948 (!rhs_domain.Contains(max_sum) &&
3949 max_sum - min_coeff < rhs_domain.Min())) {
3950 context_->
UpdateRuleStats(
"linear: all booleans and trivially false");
3951 return MarkConstraintAsFalse(
ct);
3953 if (Domain(min_sum, max_sum).IsIncludedIn(rhs_domain)) {
3955 return RemoveConstraint(
ct);
3962 DCHECK(!rhs_domain.IsEmpty());
3963 if (min_sum + min_coeff > rhs_domain.Max()) {
3966 const auto copy = arg;
3967 ct->mutable_bool_and()->clear_literals();
3968 for (
int i = 0; i < num_vars; ++i) {
3969 ct->mutable_bool_and()->add_literals(
3970 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
3972 PresolveBoolAnd(
ct);
3974 }
else if (max_sum - min_coeff < rhs_domain.Min()) {
3977 const auto copy = arg;
3978 ct->mutable_bool_and()->clear_literals();
3979 for (
int i = 0; i < num_vars; ++i) {
3980 ct->mutable_bool_and()->add_literals(
3981 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
3983 PresolveBoolAnd(
ct);
3985 }
else if (min_sum + min_coeff >= rhs_domain.Min() &&
3986 rhs_domain.front().end >= max_sum) {
3989 const auto copy = arg;
3990 ct->mutable_bool_or()->clear_literals();
3991 for (
int i = 0; i < num_vars; ++i) {
3992 ct->mutable_bool_or()->add_literals(
3993 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
3997 }
else if (max_sum - min_coeff <= rhs_domain.Max() &&
3998 rhs_domain.back().start <= min_sum) {
4001 const auto copy = arg;
4002 ct->mutable_bool_or()->clear_literals();
4003 for (
int i = 0; i < num_vars; ++i) {
4004 ct->mutable_bool_or()->add_literals(
4005 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
4010 min_sum + max_coeff <= rhs_domain.Max() &&
4011 min_sum + 2 * min_coeff > rhs_domain.Max() &&
4012 rhs_domain.back().start <= min_sum) {
4016 const auto copy = arg;
4017 ct->mutable_at_most_one()->clear_literals();
4018 for (
int i = 0; i < num_vars; ++i) {
4019 ct->mutable_at_most_one()->add_literals(
4020 copy.coeffs(i) > 0 ? copy.vars(i) :
NegatedRef(copy.vars(i)));
4024 max_sum - max_coeff >= rhs_domain.Min() &&
4025 max_sum - 2 * min_coeff < rhs_domain.Min() &&
4026 rhs_domain.front().end >= max_sum) {
4030 const auto copy = arg;
4031 ct->mutable_at_most_one()->clear_literals();
4032 for (
int i = 0; i < num_vars; ++i) {
4033 ct->mutable_at_most_one()->add_literals(
4034 copy.coeffs(i) > 0 ?
NegatedRef(copy.vars(i)) : copy.vars(i));
4038 min_sum < rhs_domain.Min() &&
4039 min_sum + min_coeff >= rhs_domain.Min() &&
4040 min_sum + 2 * min_coeff > rhs_domain.Max() &&
4041 min_sum + max_coeff <= rhs_domain.Max()) {
4044 ConstraintProto* exactly_one = context_->
working_model->add_constraints();
4045 exactly_one->set_name(
ct->name());
4046 for (
int i = 0; i < num_vars; ++i) {
4047 exactly_one->mutable_exactly_one()->add_literals(
4048 arg.coeffs(i) > 0 ? arg.vars(i) :
NegatedRef(arg.vars(i)));
4051 return RemoveConstraint(
ct);
4053 max_sum > rhs_domain.Max() &&
4054 max_sum - min_coeff <= rhs_domain.Max() &&
4055 max_sum - 2 * min_coeff < rhs_domain.Min() &&
4056 max_sum - max_coeff >= rhs_domain.Min()) {
4059 ConstraintProto* exactly_one = context_->
working_model->add_constraints();
4060 exactly_one->set_name(
ct->name());
4061 for (
int i = 0; i < num_vars; ++i) {
4062 exactly_one->mutable_exactly_one()->add_literals(
4063 arg.coeffs(i) > 0 ?
NegatedRef(arg.vars(i)) : arg.vars(i));
4066 return RemoveConstraint(
ct);
4073 if (num_vars > 3)
return false;
4078 const int max_mask = (1 << arg.vars_size());
4079 for (
int mask = 0; mask < max_mask; ++mask) {
4081 for (
int i = 0; i < num_vars; ++i) {
4082 if ((mask >> i) & 1)
value += arg.coeffs(i);
4084 if (rhs_domain.Contains(
value))
continue;
4087 ConstraintProto* new_ct = context_->
working_model->add_constraints();
4088 auto* new_arg = new_ct->mutable_bool_or();
4090 *new_ct->mutable_enforcement_literal() =
ct->enforcement_literal();
4092 for (
int i = 0; i < num_vars; ++i) {
4093 new_arg->add_literals(((mask >> i) & 1) ?
NegatedRef(arg.vars(i))
4099 return RemoveConstraint(
ct);
4102 bool CpModelPresolver::PresolveInterval(
int c, ConstraintProto*
ct) {
4104 IntervalConstraintProto*
interval =
ct->mutable_interval();
4107 if (!
ct->enforcement_literal().empty() && context_->
SizeMax(c) < 0) {
4108 context_->
UpdateRuleStats(
"interval: negative size implies unperformed");
4109 return MarkConstraintAsFalse(
ct);
4112 if (
ct->enforcement_literal().empty()) {
4113 bool domain_changed =
false;
4120 if (domain_changed) {
4122 "interval: performed intervals must have a positive size");
4131 return RemoveConstraint(
ct);
4134 bool changed =
false;
4135 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_start());
4136 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_size());
4137 changed |= CanonicalizeLinearExpression(*
ct,
interval->mutable_end());
4142 bool CpModelPresolver::PresolveInverse(ConstraintProto*
ct) {
4143 const int size =
ct->inverse().f_direct().size();
4144 bool changed =
false;
4147 for (
const int ref :
ct->inverse().f_direct()) {
4149 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
4153 for (
const int ref :
ct->inverse().f_inverse()) {
4155 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
4165 absl::flat_hash_set<int> direct_vars;
4166 for (
const int ref :
ct->inverse().f_direct()) {
4167 const auto [it, inserted] = direct_vars.insert(
PositiveRef(ref));
4173 absl::flat_hash_set<int> inverse_vars;
4174 for (
const int ref :
ct->inverse().f_inverse()) {
4175 const auto [it, inserted] = inverse_vars.insert(
PositiveRef(ref));
4185 const auto filter_inverse_domain =
4186 [
this, size, &changed](
const auto& direct,
const auto& inverse) {
4188 std::vector<absl::flat_hash_set<int64_t>> inverse_values(size);
4189 for (
int i = 0; i < size; ++i) {
4190 const Domain domain = context_->
DomainOf(inverse[i]);
4191 for (
const int64_t j : domain.Values()) {
4192 inverse_values[i].insert(j);
4199 std::vector<int64_t> possible_values;
4200 for (
int i = 0; i < size; ++i) {
4201 possible_values.clear();
4202 const Domain domain = context_->
DomainOf(direct[i]);
4203 bool removed_value =
false;
4204 for (
const int64_t j : domain.Values()) {
4205 if (inverse_values[j].contains(i)) {
4206 possible_values.push_back(j);
4208 removed_value =
true;
4211 if (removed_value) {
4215 VLOG(1) <<
"Empty domain for a variable in ExpandInverse()";
4223 if (!filter_inverse_domain(
ct->inverse().f_direct(),
4224 ct->inverse().f_inverse())) {
4228 if (!filter_inverse_domain(
ct->inverse().f_inverse(),
4229 ct->inverse().f_direct())) {
4240 bool CpModelPresolver::PresolveElement(ConstraintProto*
ct) {
4243 if (
ct->element().vars().empty()) {
4248 const int index_ref =
ct->element().index();
4249 const int target_ref =
ct->element().target();
4254 bool all_constants =
true;
4255 std::vector<int64_t> constants;
4256 bool all_included_in_target_domain =
true;
4260 index_ref, Domain(0,
ct->element().vars_size() - 1))) {
4268 std::vector<int64_t> possible_indices;
4269 const Domain& index_domain = context_->
DomainOf(index_ref);
4270 for (
const int64_t index_value : index_domain.Values()) {
4271 const int ref =
ct->element().vars(index_value);
4272 const int64_t target_value =
4273 target_ref == index_ref ? index_value : -index_value;
4275 possible_indices.push_back(target_value);
4278 if (possible_indices.size() < index_domain.Size()) {
4284 "element: reduced index domain when target equals index");
4290 Domain infered_domain;
4291 const Domain& initial_index_domain = context_->
DomainOf(index_ref);
4292 const Domain& target_domain = context_->
DomainOf(target_ref);
4293 std::vector<int64_t> possible_indices;
4294 for (
const int64_t
value : initial_index_domain.Values()) {
4296 CHECK_LT(
value,
ct->element().vars_size());
4297 const int ref =
ct->element().vars(
value);
4300 Domain domain = context_->
DomainOf(ref);
4301 if (ref == index_ref) {
4302 domain = Domain(
value);
4304 domain = Domain(-
value);
4309 if (domain.IntersectionWith(target_domain).IsEmpty())
continue;
4310 possible_indices.push_back(
value);
4311 if (domain.IsFixed()) {
4312 constants.push_back(domain.Min());
4314 all_constants =
false;
4316 if (!domain.IsIncludedIn(target_domain)) {
4317 all_included_in_target_domain =
false;
4319 infered_domain = infered_domain.UnionWith(domain);
4321 if (possible_indices.size() < initial_index_domain.Size()) {
4328 bool domain_modified =
false;
4330 &domain_modified)) {
4333 if (domain_modified) {
4339 if (context_->
IsFixed(index_ref)) {
4340 const int var =
ct->element().vars(context_->
MinOf(index_ref));
4341 if (
var != target_ref) {
4342 LinearConstraintProto*
const lin =
4343 context_->
working_model->add_constraints()->mutable_linear();
4345 lin->add_coeffs(-1);
4346 lin->add_vars(target_ref);
4353 return RemoveConstraint(
ct);
4359 if (all_constants && context_->
IsFixed(target_ref)) {
4361 return RemoveConstraint(
ct);
4366 if (context_->
MinOf(index_ref) == 0 && context_->
MaxOf(index_ref) == 1 &&
4368 const int64_t v0 = constants[0];
4369 const int64_t v1 = constants[1];
4371 LinearConstraintProto*
const lin =
4372 context_->
working_model->add_constraints()->mutable_linear();
4373 lin->add_vars(target_ref);
4375 lin->add_vars(index_ref);
4376 lin->add_coeffs(v0 - v1);
4377 lin->add_domain(v0);
4378 lin->add_domain(v0);
4380 context_->
UpdateRuleStats(
"element: linearize constant element of size 2");
4381 return RemoveConstraint(
ct);
4385 const AffineRelation::Relation r_index =
4387 if (r_index.representative != index_ref) {
4389 if (context_->
DomainOf(r_index.representative).
Size() >
4395 const int64_t r_min = context_->
MinOf(r_ref);
4396 const int64_t r_max = context_->
MaxOf(r_ref);
4397 const int array_size =
ct->element().vars_size();
4399 context_->
UpdateRuleStats(
"TODO element: representative has bad domain");
4400 }
else if (r_index.offset >= 0 && r_index.offset < array_size &&
4401 r_index.offset + r_max * r_index.coeff >= 0 &&
4402 r_index.offset + r_max * r_index.coeff < array_size) {
4404 ElementConstraintProto*
const element =
4405 context_->
working_model->add_constraints()->mutable_element();
4406 for (int64_t v = 0; v <= r_max; ++v) {
4407 const int64_t scaled_index = v * r_index.coeff + r_index.offset;
4408 CHECK_GE(scaled_index, 0);
4409 CHECK_LT(scaled_index, array_size);
4410 element->add_vars(
ct->element().vars(scaled_index));
4412 element->set_index(r_ref);
4413 element->set_target(target_ref);
4415 if (r_index.coeff == 1) {
4421 return RemoveConstraint(
ct);
4426 DCHECK(!context_->
IsFixed(index_ref));
4435 absl::flat_hash_map<int, int> local_var_occurrence_counter;
4436 local_var_occurrence_counter[
PositiveRef(index_ref)]++;
4437 local_var_occurrence_counter[
PositiveRef(target_ref)]++;
4441 DCHECK_GE(
value, 0);
4442 DCHECK_LT(
value,
ct->element().vars_size());
4443 const int ref =
ct->element().vars(
value);
4449 local_var_occurrence_counter.at(
PositiveRef(index_ref)) == 1) {
4450 if (all_constants) {
4454 context_->
UpdateRuleStats(
"element: trivial target domain reduction");
4457 return RemoveConstraint(
ct);
4463 if (!context_->
IsFixed(target_ref) &&
4465 local_var_occurrence_counter.at(
PositiveRef(target_ref)) == 1) {
4466 if (all_included_in_target_domain) {
4470 return RemoveConstraint(
ct);
4479 bool CpModelPresolver::PresolveTable(ConstraintProto*
ct) {
4482 if (
ct->table().vars().empty()) {
4484 return RemoveConstraint(
ct);
4487 const int initial_num_vars =
ct->table().vars_size();
4488 bool changed =
true;
4491 std::vector<AffineRelation::Relation> affine_relations;
4492 std::vector<int64_t> old_var_lb;
4493 std::vector<int64_t> old_var_ub;
4495 for (
int v = 0; v < initial_num_vars; ++v) {
4496 const int ref =
ct->table().vars(v);
4498 affine_relations.push_back(r);
4499 old_var_lb.push_back(context_->
MinOf(ref));
4500 old_var_ub.push_back(context_->
MaxOf(ref));
4501 if (r.representative != ref) {
4503 ct->mutable_table()->set_vars(v, r.representative);
4505 "table: replace variable by canonical affine one");
4514 std::vector<int> old_index_of_duplicate_to_new_index_of_first_occurrence(
4515 initial_num_vars, -1);
4517 std::vector<int> old_index_to_new_index(initial_num_vars, -1);
4520 absl::flat_hash_map<int, int> first_visit;
4521 for (
int p = 0; p < initial_num_vars; ++p) {
4522 const int ref =
ct->table().vars(p);
4524 const auto& it = first_visit.find(
var);
4525 if (it != first_visit.end()) {
4526 const int previous = it->second;
4527 old_index_of_duplicate_to_new_index_of_first_occurrence[p] = previous;
4531 ct->mutable_table()->set_vars(num_vars, ref);
4532 first_visit[
var] = num_vars;
4533 old_index_to_new_index[p] = num_vars;
4538 if (num_vars < initial_num_vars) {
4539 ct->mutable_table()->mutable_vars()->Truncate(num_vars);
4546 std::vector<std::vector<int64_t>> new_tuples;
4547 const int initial_num_tuples =
ct->table().values_size() / initial_num_vars;
4548 std::vector<absl::flat_hash_set<int64_t>> new_domains(num_vars);
4551 std::vector<int64_t> tuple(num_vars);
4552 new_tuples.reserve(initial_num_tuples);
4553 for (
int i = 0; i < initial_num_tuples; ++i) {
4554 bool delete_row =
false;
4556 for (
int j = 0; j < initial_num_vars; ++j) {
4557 const int64_t old_value =
ct->table().values(i * initial_num_vars + j);
4561 if (old_value < old_var_lb[j] || old_value > old_var_ub[j]) {
4567 const AffineRelation::Relation& r = affine_relations[j];
4568 const int64_t
value = (old_value - r.offset) / r.coeff;
4569 if (
value * r.coeff + r.offset != old_value) {
4574 const int mapped_position = old_index_to_new_index[j];
4575 if (mapped_position == -1) {
4576 const int new_index_of_first_occurrence =
4577 old_index_of_duplicate_to_new_index_of_first_occurrence[j];
4578 if (
value != tuple[new_index_of_first_occurrence]) {
4583 const int ref =
ct->table().vars(mapped_position);
4588 tuple[mapped_position] =
value;
4595 new_tuples.push_back(tuple);
4596 for (
int j = 0; j < num_vars; ++j) {
4597 new_domains[j].insert(tuple[j]);
4601 if (new_tuples.size() < initial_num_tuples) {
4608 ct->mutable_table()->clear_values();
4609 for (
const std::vector<int64_t>& t : new_tuples) {
4610 for (
const int64_t v : t) {
4611 ct->mutable_table()->add_values(v);
4617 if (
ct->table().negated())
return changed;
4620 for (
int j = 0; j < num_vars; ++j) {
4621 const int ref =
ct->table().vars(j);
4625 new_domains[j].
end())),
4633 if (num_vars == 1) {
4636 return RemoveConstraint(
ct);
4641 for (
int j = 0; j < num_vars; ++j) prod *= new_domains[j].size();
4642 if (prod == new_tuples.size()) {
4644 return RemoveConstraint(
ct);
4650 if (new_tuples.size() > 0.7 * prod) {
4652 std::vector<std::vector<int64_t>> var_to_values(num_vars);
4653 for (
int j = 0; j < num_vars; ++j) {
4654 var_to_values[j].assign(new_domains[j].begin(), new_domains[j].
end());
4656 std::vector<std::vector<int64_t>> all_tuples(prod);
4657 for (
int i = 0; i < prod; ++i) {
4658 all_tuples[i].resize(num_vars);
4660 for (
int j = 0; j < num_vars; ++j) {
4661 all_tuples[i][j] = var_to_values[j][
index % var_to_values[j].size()];
4662 index /= var_to_values[j].size();
4668 std::vector<std::vector<int64_t>> diff(prod - new_tuples.size());
4669 std::set_difference(all_tuples.begin(), all_tuples.end(),
4670 new_tuples.begin(), new_tuples.end(), diff.begin());
4673 ct->mutable_table()->set_negated(!
ct->table().negated());
4674 ct->mutable_table()->clear_values();
4675 for (
const std::vector<int64_t>& t : diff) {
4676 for (
const int64_t v : t)
ct->mutable_table()->add_values(v);
4683 bool CpModelPresolver::PresolveAllDiff(ConstraintProto*
ct) {
4687 AllDifferentConstraintProto& all_diff = *
ct->mutable_all_diff();
4689 bool constraint_has_changed =
false;
4690 for (LinearExpressionProto& exp :
4691 *(
ct->mutable_all_diff()->mutable_exprs())) {
4692 constraint_has_changed |= CanonicalizeLinearExpression(*
ct, &exp);
4696 const int size = all_diff.exprs_size();
4699 return RemoveConstraint(
ct);
4703 return RemoveConstraint(
ct);
4706 bool something_was_propagated =
false;
4707 std::vector<LinearExpressionProto> kept_expressions;
4708 for (
int i = 0; i < size; ++i) {
4709 if (!context_->
IsFixed(all_diff.exprs(i))) {
4710 kept_expressions.push_back(all_diff.exprs(i));
4714 const int64_t
value = context_->
MinOf(all_diff.exprs(i));
4715 bool propagated =
false;
4716 for (
int j = 0; j < size; ++j) {
4717 if (i == j)
continue;
4720 Domain(
value).Complement())) {
4728 something_was_propagated =
true;
4735 kept_expressions.begin(), kept_expressions.end(),
4736 [](
const LinearExpressionProto& expr_a,
4737 const LinearExpressionProto& expr_b) {
4738 DCHECK_EQ(expr_a.vars_size(), 1);
4739 DCHECK_EQ(expr_b.vars_size(), 1);
4740 const int ref_a = expr_a.vars(0);
4741 const int ref_b = expr_b.vars(0);
4742 const int64_t coeff_a = expr_a.coeffs(0);
4743 const int64_t coeff_b = expr_b.coeffs(0);
4744 const int64_t abs_coeff_a = std::abs(coeff_a);
4745 const int64_t abs_coeff_b = std::abs(coeff_b);
4746 const int64_t offset_a = expr_a.offset();
4747 const int64_t offset_b = expr_b.offset();
4748 const int64_t abs_offset_a = std::abs(offset_a);
4749 const int64_t abs_offset_b = std::abs(offset_b);
4750 return std::tie(ref_a, abs_coeff_a, coeff_a, abs_offset_a, offset_a) <
4751 std::tie(ref_b, abs_coeff_b, coeff_b, abs_offset_b, offset_b);
4757 for (
int i = 1; i < kept_expressions.size(); ++i) {
4759 kept_expressions[i - 1], 1)) {
4761 "Duplicate variable in all_diff");
4764 kept_expressions[i - 1], -1)) {
4765 bool domain_modified =
false;
4767 Domain(0).Complement(),
4768 &domain_modified)) {
4771 if (domain_modified) {
4773 "all_diff: remove 0 from expression appearing with its "
4779 if (kept_expressions.size() < all_diff.exprs_size()) {
4780 all_diff.clear_exprs();
4781 for (
const LinearExpressionProto& expr : kept_expressions) {
4782 *all_diff.add_exprs() = expr;
4785 something_was_propagated =
true;
4786 constraint_has_changed =
true;
4787 if (kept_expressions.size() <= 1)
continue;
4791 CHECK_GE(all_diff.exprs_size(), 2);
4793 for (
int i = 1; i < all_diff.exprs_size(); ++i) {
4796 if (all_diff.exprs_size() == domain.Size()) {
4797 absl::flat_hash_map<int64_t, std::vector<LinearExpressionProto>>
4799 for (
const LinearExpressionProto& expr : all_diff.exprs()) {
4800 for (
const int64_t v : context_->
DomainOf(expr.vars(0)).
Values()) {
4801 value_to_exprs[expr.coeffs(0) * v + expr.offset()].push_back(expr);
4804 bool propagated =
false;
4805 for (
const auto& it : value_to_exprs) {
4806 if (it.second.size() == 1 && !context_->
IsFixed(it.second.front())) {
4807 const LinearExpressionProto& expr = it.second.
front();
4816 "all_diff: propagated mandatory values in permutation");
4817 something_was_propagated =
true;
4820 if (!something_was_propagated)
break;
4823 return constraint_has_changed;
4830 void AddImplication(
int lhs,
int rhs, CpModelProto*
proto,
4831 absl::flat_hash_map<int, int>* ref_to_bool_and) {
4832 if (ref_to_bool_and->contains(lhs)) {
4833 const int ct_index = (*ref_to_bool_and)[lhs];
4834 proto->mutable_constraints(ct_index)->mutable_bool_and()->add_literals(rhs);
4835 }
else if (ref_to_bool_and->contains(
NegatedRef(rhs))) {
4836 const int ct_index = (*ref_to_bool_and)[
NegatedRef(rhs)];
4837 proto->mutable_constraints(ct_index)->mutable_bool_and()->add_literals(
4840 (*ref_to_bool_and)[lhs] =
proto->constraints_size();
4841 ConstraintProto*
ct =
proto->add_constraints();
4842 ct->add_enforcement_literal(lhs);
4843 ct->mutable_bool_and()->add_literals(rhs);
4847 template <
typename ClauseContainer>
4848 void ExtractClauses(
bool use_bool_and,
const ClauseContainer& container,
4849 CpModelProto*
proto) {
4856 absl::flat_hash_map<int, int> ref_to_bool_and;
4857 for (
int i = 0; i < container.NumClauses(); ++i) {
4858 const std::vector<Literal>& clause = container.Clause(i);
4859 if (clause.empty())
continue;
4864 if (use_bool_and && clause.size() == 2) {
4865 const int a = clause[0].IsPositive()
4866 ? clause[0].Variable().value()
4868 const int b = clause[1].IsPositive()
4869 ? clause[1].Variable().value()
4876 ConstraintProto*
ct =
proto->add_constraints();
4877 for (
const Literal l : clause) {
4878 if (l.IsPositive()) {
4879 ct->mutable_bool_or()->add_literals(l.Variable().value());
4881 ct->mutable_bool_or()->add_literals(
NegatedRef(l.Variable().value()));
4889 bool CpModelPresolver::PresolveNoOverlap(ConstraintProto*
ct) {
4891 NoOverlapConstraintProto*
proto =
ct->mutable_no_overlap();
4892 bool changed =
false;
4897 absl::flat_hash_set<int> visited_intervals;
4898 absl::flat_hash_set<int> duplicate_intervals;
4906 const int initial_num_intervals =
proto->intervals_size();
4908 visited_intervals.clear();
4910 for (
int i = 0; i < initial_num_intervals; ++i) {
4918 ConstraintProto* interval_ct =
4923 if (!MarkConstraintAsFalse(interval_ct)) {
4927 "no_overlap: unperform duplicate non zero-sized intervals");
4941 "no_overlap: zero the size of performed duplicate intervals");
4945 const int performed_literal = interval_ct->enforcement_literal(0);
4946 ConstraintProto* size_eq_zero =
4948 size_eq_zero->add_enforcement_literal(performed_literal);
4949 size_eq_zero->mutable_linear()->add_domain(0);
4950 size_eq_zero->mutable_linear()->add_domain(0);
4952 interval_ct->interval().size(), 1,
4953 size_eq_zero->mutable_linear());
4955 "no_overlap: make duplicate intervals as unperformed or zero "
4964 if (new_size < initial_num_intervals) {
4965 proto->mutable_intervals()->Truncate(new_size);
4972 if (
proto->intervals_size() > 1) {
4973 std::vector<IndexedInterval> indexed_intervals;
4974 for (
int i = 0; i <
proto->intervals().size(); ++i) {
4976 indexed_intervals.push_back({
index,
4980 std::vector<std::vector<int>> components;
4983 if (components.size() > 1) {
4984 for (
const std::vector<int>& intervals : components) {
4985 if (intervals.size() <= 1)
continue;
4987 NoOverlapConstraintProto* new_no_overlap =
4988 context_->
working_model->add_constraints()->mutable_no_overlap();
4991 for (
const int i : intervals) {
4992 new_no_overlap->add_intervals(i);
4996 context_->
UpdateRuleStats(
"no_overlap: split into disjoint components");
4997 return RemoveConstraint(
ct);
5001 std::vector<int> constant_intervals;
5002 int64_t size_min_of_non_constant_intervals =
5004 for (
int i = 0; i <
proto->intervals_size(); ++i) {
5009 size_min_of_non_constant_intervals =
5010 std::min(size_min_of_non_constant_intervals,
5015 bool move_constraint_last =
false;
5016 if (!constant_intervals.empty()) {
5018 std::sort(constant_intervals.begin(), constant_intervals.end(),
5019 [
this](
int i1,
int i2) {
5020 const int64_t s1 = context_->StartMin(i1);
5021 const int64_t e1 = context_->EndMax(i1);
5022 const int64_t s2 = context_->StartMin(i2);
5023 const int64_t e2 = context_->EndMax(i2);
5024 return std::tie(s1, e1) < std::tie(s2, e2);
5030 for (
int i = 0; i + 1 < constant_intervals.size(); ++i) {
5031 if (context_->
EndMax(constant_intervals[i]) >
5032 context_->
StartMin(constant_intervals[i + 1])) {
5038 if (constant_intervals.size() ==
proto->intervals_size()) {
5040 return RemoveConstraint(
ct);
5043 absl::flat_hash_set<int> intervals_to_remove;
5047 for (
int i = 0; i + 1 < constant_intervals.size(); ++i) {
5048 const int start = i;
5049 while (i + 1 < constant_intervals.size() &&
5050 context_->
StartMin(constant_intervals[i + 1]) -
5051 context_->
EndMax(constant_intervals[i]) <
5052 size_min_of_non_constant_intervals) {
5055 if (i ==
start)
continue;
5056 for (
int j =
start; j <= i; ++j) {
5057 intervals_to_remove.insert(constant_intervals[j]);
5059 const int64_t new_start = context_->
StartMin(constant_intervals[
start]);
5060 const int64_t new_end = context_->
EndMax(constant_intervals[i]);
5062 IntervalConstraintProto* new_interval =
5063 context_->
working_model->add_constraints()->mutable_interval();
5064 new_interval->mutable_start()->set_offset(new_start);
5065 new_interval->mutable_size()->set_offset(new_end - new_start);
5066 new_interval->mutable_end()->set_offset(new_end);
5067 move_constraint_last =
true;
5071 if (!intervals_to_remove.empty()) {
5073 const int old_size =
proto->intervals_size();
5074 for (
int i = 0; i < old_size; ++i) {
5081 CHECK_LT(new_size, old_size);
5082 proto->mutable_intervals()->Truncate(new_size);
5084 "no_overlap: merge constant contiguous intervals");
5085 intervals_to_remove.clear();
5086 constant_intervals.clear();
5092 if (
proto->intervals_size() == 1) {
5094 return RemoveConstraint(
ct);
5096 if (
proto->intervals().empty()) {
5098 return RemoveConstraint(
ct);
5104 if (move_constraint_last) {
5108 return RemoveConstraint(
ct);
5114 bool CpModelPresolver::PresolveNoOverlap2D(
int c, ConstraintProto*
ct) {
5119 const NoOverlap2DConstraintProto&
proto =
ct->no_overlap_2d();
5120 const int initial_num_boxes =
proto.x_intervals_size();
5122 bool has_zero_sizes =
false;
5123 bool x_constant =
true;
5124 bool y_constant =
true;
5128 std::vector<Rectangle> bounding_boxes;
5129 std::vector<int> active_boxes;
5130 for (
int i = 0; i <
proto.x_intervals_size(); ++i) {
5131 const int x_interval_index =
proto.x_intervals(i);
5132 const int y_interval_index =
proto.y_intervals(i);
5139 if (
proto.boxes_with_null_area_can_overlap() &&
5140 (context_->
SizeMax(x_interval_index) == 0 ||
5141 context_->
SizeMax(y_interval_index) == 0)) {
5142 if (
proto.boxes_with_null_area_can_overlap())
continue;
5143 has_zero_sizes =
true;
5145 ct->mutable_no_overlap_2d()->set_x_intervals(new_size, x_interval_index);
5146 ct->mutable_no_overlap_2d()->set_y_intervals(new_size, y_interval_index);
5147 bounding_boxes.push_back(
5148 {IntegerValue(context_->
StartMin(x_interval_index)),
5149 IntegerValue(context_->
EndMax(x_interval_index)),
5150 IntegerValue(context_->
StartMin(y_interval_index)),
5151 IntegerValue(context_->
EndMax(y_interval_index))});
5152 active_boxes.push_back(new_size);
5164 bounding_boxes, absl::MakeSpan(active_boxes));
5165 if (components.size() > 1) {
5166 for (
const absl::Span<int> boxes : components) {
5167 if (boxes.size() <= 1)
continue;
5169 NoOverlap2DConstraintProto* new_no_overlap_2d =
5170 context_->
working_model->add_constraints()->mutable_no_overlap_2d();
5171 for (
const int b : boxes) {
5172 new_no_overlap_2d->add_x_intervals(
proto.x_intervals(
b));
5173 new_no_overlap_2d->add_y_intervals(
proto.y_intervals(
b));
5177 context_->
UpdateRuleStats(
"no_overlap_2d: split into disjoint components");
5178 return RemoveConstraint(
ct);
5181 if (!has_zero_sizes && (x_constant || y_constant)) {
5183 "no_overlap_2d: a dimension is constant, splitting into many no "
5185 std::vector<IndexedInterval> indexed_intervals;
5186 for (
int i = 0; i < new_size; ++i) {
5187 int x =
proto.x_intervals(i);
5188 int y =
proto.y_intervals(i);
5190 indexed_intervals.push_back({x, IntegerValue(context_->
StartMin(y)),
5191 IntegerValue(context_->
EndMax(y))});
5193 std::vector<std::vector<int>> no_overlaps;
5196 for (
const std::vector<int>& no_overlap : no_overlaps) {
5197 ConstraintProto* new_ct = context_->
working_model->add_constraints();
5200 for (
const int i : no_overlap) {
5201 new_ct->mutable_no_overlap()->add_intervals(i);
5205 return RemoveConstraint(
ct);
5208 if (new_size < initial_num_boxes) {
5210 ct->mutable_no_overlap_2d()->mutable_x_intervals()->Truncate(new_size);
5211 ct->mutable_no_overlap_2d()->mutable_y_intervals()->Truncate(new_size);
5214 if (new_size == 0) {
5216 return RemoveConstraint(
ct);
5219 if (new_size == 1) {
5221 return RemoveConstraint(
ct);
5224 return new_size < initial_num_boxes;
5228 LinearExpressionProto ConstantExpressionProto(int64_t
value) {
5229 LinearExpressionProto expr;
5230 expr.set_offset(
value);
5235 void CpModelPresolver::DetectDuplicateIntervals(
5236 int c, google::protobuf::RepeatedField<int32_t>* intervals) {
5237 bool changed =
false;
5238 const int size = intervals->size();
5239 for (
int i = 0; i < size; ++i) {
5240 const int index = (*intervals)[i];
5242 if (
index != new_index) {
5244 intervals->Set(i, new_index);
5250 bool CpModelPresolver::PresolveCumulative(ConstraintProto*
ct) {
5253 CumulativeConstraintProto*
proto =
ct->mutable_cumulative();
5255 bool changed = CanonicalizeLinearExpression(*
ct,
proto->mutable_capacity());
5256 for (LinearExpressionProto& exp :
5257 *(
ct->mutable_cumulative()->mutable_demands())) {
5258 changed |= CanonicalizeLinearExpression(*
ct, &exp);
5261 const int64_t capacity_max = context_->
MaxOf(
proto->capacity());
5265 bool domain_changed =
false;
5267 proto->capacity(), Domain(0, capacity_max), &domain_changed)) {
5270 if (domain_changed) {
5280 absl::flat_hash_map<int, int> interval_to_i;
5282 for (
int i = 0; i <
proto->intervals_size(); ++i) {
5283 const auto [it, inserted] =
5284 interval_to_i.insert({
proto->intervals(i), new_size});
5287 const int old_index = it->second;
5288 proto->mutable_demands(old_index)->set_offset(
5289 proto->demands(old_index).offset() +
5292 "cumulative: merged demand of identical interval");
5296 "TODO cumulative: merged demand of identical interval");
5299 proto->set_intervals(new_size,
proto->intervals(i));
5300 *
proto->mutable_demands(new_size) =
proto->demands(i);
5303 if (new_size < proto->intervals_size()) {
5305 proto->mutable_intervals()->Truncate(new_size);
5306 proto->mutable_demands()->erase(
5307 proto->mutable_demands()->begin() + new_size,
5308 proto->mutable_demands()->end());
5316 int num_zero_demand_removed = 0;
5317 int num_zero_size_removed = 0;
5318 int num_incompatible_intervals = 0;
5319 for (
int i = 0; i <
proto->intervals_size(); ++i) {
5322 const LinearExpressionProto& demand_expr =
proto->demands(i);
5323 const int64_t demand_max = context_->
MaxOf(demand_expr);
5324 if (demand_max == 0) {
5325 num_zero_demand_removed++;
5332 num_zero_size_removed++;
5340 context_->
MinOf(demand_expr) > capacity_max)) {
5342 ConstraintProto* interval_ct =
5344 DCHECK_EQ(interval_ct->enforcement_literal_size(), 1);
5345 const int literal = interval_ct->enforcement_literal(0);
5349 num_incompatible_intervals++;
5353 "cumulative: performed demand exceeds capacity.");
5358 *
proto->mutable_demands(new_size) =
proto->demands(i);
5362 if (new_size < proto->intervals_size()) {
5364 proto->mutable_intervals()->Truncate(new_size);
5365 proto->mutable_demands()->erase(
5366 proto->mutable_demands()->begin() + new_size,
5367 proto->mutable_demands()->end());
5370 if (num_zero_demand_removed > 0) {
5372 "cumulative: removed intervals with no demands");
5374 if (num_zero_size_removed > 0) {
5376 "cumulative: removed intervals with a size of zero");
5378 if (num_incompatible_intervals > 0) {
5380 "cumulative: removed intervals that can't be performed");
5386 for (
int i = 0; i <
proto->demands_size(); ++i) {
5388 const LinearExpressionProto& demand_expr =
proto->demands(i);
5390 bool domain_changed =
false;
5395 if (domain_changed) {
5397 "cumulative: fit demand in [0..capacity_max]");
5409 if (
proto->intervals_size() > 1) {
5410 std::vector<IndexedInterval> indexed_intervals;
5411 for (
int i = 0; i <
proto->intervals().size(); ++i) {
5413 indexed_intervals.push_back({i, IntegerValue(context_->
StartMin(
index)),
5416 std::vector<std::vector<int>> components;
5419 if (components.size() > 1) {
5420 for (
const std::vector<int>& component : components) {
5421 CumulativeConstraintProto* new_cumulative =
5422 context_->
working_model->add_constraints()->mutable_cumulative();
5423 for (
const int i : component) {
5424 new_cumulative->add_intervals(
proto->intervals(i));
5425 *new_cumulative->add_demands() =
proto->demands(i);
5427 *new_cumulative->mutable_capacity() =
proto->capacity();
5430 context_->
UpdateRuleStats(
"cumulative: split into disjoint components");
5431 return RemoveConstraint(
ct);
5439 absl::btree_map<int64_t, int64_t> time_to_demand_deltas;
5440 const int64_t capacity_min = context_->
MinOf(
proto->capacity());
5441 for (
int i = 0; i <
proto->intervals_size(); ++i) {
5443 const int64_t demand_max = context_->
MaxOf(
proto->demands(i));
5454 int num_possible_overloads = 0;
5455 int64_t current_load = 0;
5456 absl::flat_hash_map<int64_t, int64_t> num_possible_overloads_before;
5457 for (
const auto& it : time_to_demand_deltas) {
5458 num_possible_overloads_before[it.first] = num_possible_overloads;
5459 current_load += it.second;
5460 if (current_load > capacity_min) {
5461 ++num_possible_overloads;
5464 CHECK_EQ(current_load, 0);
5467 if (num_possible_overloads == 0) {
5469 "cumulative: max profile is always under the min capacity");
5470 return RemoveConstraint(
ct);
5480 for (
int i = 0; i <
proto->intervals_size(); ++i) {
5498 const int num_diff = num_possible_overloads_before.at(
end_max) -
5499 num_possible_overloads_before.at(
start_min);
5500 if (num_diff == 0)
continue;
5502 proto->set_intervals(new_size,
proto->intervals(i));
5503 *
proto->mutable_demands(new_size) =
proto->demands(i);
5507 if (new_size < proto->intervals_size()) {
5509 proto->mutable_intervals()->Truncate(new_size);
5510 proto->mutable_demands()->erase(
5511 proto->mutable_demands()->begin() + new_size,
5512 proto->mutable_demands()->end());
5514 "cumulative: remove never conflicting intervals.");
5518 if (
proto->intervals().empty()) {
5520 return RemoveConstraint(
ct);
5524 int64_t max_of_performed_demand_mins = 0;
5525 int64_t sum_of_max_demands = 0;
5526 for (
int i = 0; i <
proto->intervals_size(); ++i) {
5527 const ConstraintProto& interval_ct =
5530 const LinearExpressionProto& demand_expr =
proto->demands(i);
5531 sum_of_max_demands += context_->
MaxOf(demand_expr);
5533 if (interval_ct.enforcement_literal().empty()) {
5534 max_of_performed_demand_mins =
std::max(max_of_performed_demand_mins,
5535 context_->
MinOf(demand_expr));
5539 const LinearExpressionProto& capacity_expr =
proto->capacity();
5540 if (max_of_performed_demand_mins > context_->
MinOf(capacity_expr)) {
5543 capacity_expr, Domain(max_of_performed_demand_mins,
5549 if (max_of_performed_demand_mins > context_->
MaxOf(capacity_expr)) {
5550 context_->
UpdateRuleStats(
"cumulative: cannot fit performed demands");
5554 if (sum_of_max_demands <= context_->MinOf(capacity_expr)) {
5555 context_->
UpdateRuleStats(
"cumulative: capacity exceeds sum of demands");
5556 return RemoveConstraint(
ct);
5562 for (
int i = 0; i <
ct->cumulative().demands_size(); ++i) {
5563 const LinearExpressionProto& demand_expr =
ct->cumulative().demands(i);
5564 if (!context_->
IsFixed(demand_expr)) {
5570 if (gcd == 1)
break;
5574 for (
int i = 0; i <
ct->cumulative().demands_size(); ++i) {
5575 const int64_t
demand = context_->
MinOf(
ct->cumulative().demands(i));
5576 *
proto->mutable_demands(i) = ConstantExpressionProto(
demand / gcd);
5579 const int64_t old_capacity = context_->
MinOf(
proto->capacity());
5580 *
proto->mutable_capacity() = ConstantExpressionProto(old_capacity / gcd);
5582 "cumulative: divide demands and capacity by gcd");
5586 const int num_intervals =
proto->intervals_size();
5587 const LinearExpressionProto& capacity_expr =
proto->capacity();
5589 std::vector<LinearExpressionProto> start_exprs(num_intervals);
5591 int num_duration_one = 0;
5592 int num_greater_half_capacity = 0;
5594 bool has_optional_interval =
false;
5595 for (
int i = 0; i < num_intervals; ++i) {
5599 const ConstraintProto&
ct =
5601 const IntervalConstraintProto&
interval =
ct.interval();
5604 const LinearExpressionProto& demand_expr =
proto->demands(i);
5613 const int64_t demand_min = context_->
MinOf(demand_expr);
5614 const int64_t demand_max = context_->
MaxOf(demand_expr);
5615 if (demand_min > capacity_max / 2) {
5616 num_greater_half_capacity++;
5618 if (demand_min > capacity_max) {
5619 context_->
UpdateRuleStats(
"cumulative: demand_min exceeds capacity max");
5623 CHECK_EQ(
ct.enforcement_literal().size(), 1);
5629 }
else if (demand_max > capacity_max) {
5630 if (
ct.enforcement_literal().empty()) {
5632 "cumulative: demand_max exceeds capacity max.");
5642 "cumulative: demand_max of optional interval exceeds capacity.");
5647 if (num_greater_half_capacity == num_intervals) {
5648 if (num_duration_one == num_intervals && !has_optional_interval) {
5650 ConstraintProto* new_ct = context_->
working_model->add_constraints();
5651 auto* arg = new_ct->mutable_all_diff();
5652 for (
const LinearExpressionProto& expr : start_exprs) {
5653 *arg->add_exprs() = expr;
5655 if (!context_->
IsFixed(capacity_expr)) {
5656 const int64_t capacity_min = context_->
MinOf(capacity_expr);
5657 for (
const LinearExpressionProto& expr :
proto->demands()) {
5658 if (capacity_min >= context_->
MaxOf(expr))
continue;
5659 LinearConstraintProto* fit =
5660 context_->
working_model->add_constraints()->mutable_linear();
5668 return RemoveConstraint(
ct);
5673 for (
int i = 0; i <
proto->demands_size(); ++i) {
5674 const LinearExpressionProto& demand_expr =
proto->demands(i);
5675 const int64_t demand_max = context_->
MaxOf(demand_expr);
5676 if (demand_max > context_->
MinOf(capacity_expr)) {
5677 ConstraintProto* capacity_gt =
5679 *capacity_gt->mutable_enforcement_literal() =
5681 .enforcement_literal();
5682 capacity_gt->mutable_linear()->add_domain(0);
5683 capacity_gt->mutable_linear()->add_domain(
5686 capacity_gt->mutable_linear());
5688 capacity_gt->mutable_linear());
5692 ConstraintProto* new_ct = context_->
working_model->add_constraints();
5693 auto* arg = new_ct->mutable_no_overlap();
5698 return RemoveConstraint(
ct);
5705 bool CpModelPresolver::PresolveRoutes(ConstraintProto*
ct) {
5708 RoutesConstraintProto&
proto = *
ct->mutable_routes();
5710 const int old_size =
proto.literals_size();
5712 std::vector<bool> has_incoming_or_outgoing_arcs;
5713 const int num_arcs =
proto.literals_size();
5714 for (
int i = 0; i < num_arcs; ++i) {
5715 const int ref =
proto.literals(i);
5719 if (
tail >= has_incoming_or_outgoing_arcs.size()) {
5720 has_incoming_or_outgoing_arcs.resize(
tail + 1,
false);
5722 if (
head >= has_incoming_or_outgoing_arcs.size()) {
5723 has_incoming_or_outgoing_arcs.resize(
head + 1,
false);
5730 proto.set_literals(new_size, ref);
5734 has_incoming_or_outgoing_arcs[
tail] =
true;
5735 has_incoming_or_outgoing_arcs[
head] =
true;
5738 if (old_size > 0 && new_size == 0) {
5743 "routes: graph with nodes and no arcs");
5748 for (
int n = 0; n < has_incoming_or_outgoing_arcs.size(); ++n) {
5749 if (!has_incoming_or_outgoing_arcs[n]) {
5751 "routes: node ", n,
" misses incoming or outgoing arcs"));
5755 if (new_size < num_arcs) {
5756 proto.mutable_literals()->Truncate(new_size);
5757 proto.mutable_tails()->Truncate(new_size);
5758 proto.mutable_heads()->Truncate(new_size);
5765 bool CpModelPresolver::PresolveCircuit(ConstraintProto*
ct) {
5768 CircuitConstraintProto&
proto = *
ct->mutable_circuit();
5772 ct->mutable_circuit()->mutable_heads());
5776 std::vector<std::vector<int>> incoming_arcs;
5777 std::vector<std::vector<int>> outgoing_arcs;
5779 const int num_arcs =
proto.literals_size();
5780 for (
int i = 0; i < num_arcs; ++i) {
5781 const int ref =
proto.literals(i);
5789 incoming_arcs[
head].push_back(ref);
5790 outgoing_arcs[
tail].push_back(ref);
5794 for (
int i = 0; i < num_nodes; ++i) {
5795 if (incoming_arcs[i].empty() || outgoing_arcs[i].empty()) {
5796 return MarkConstraintAsFalse(
ct);
5805 bool loop_again =
true;
5806 int num_fixed_at_true = 0;
5807 while (loop_again) {
5809 for (
const auto* node_to_refs : {&incoming_arcs, &outgoing_arcs}) {
5810 for (
const std::vector<int>& refs : *node_to_refs) {
5811 if (refs.size() == 1) {
5813 ++num_fixed_at_true;
5822 for (
const int ref : refs) {
5832 if (num_true == 1) {
5833 for (
const int ref : refs) {
5834 if (ref != true_ref) {
5835 if (!context_->
IsFixed(ref)) {
5846 if (num_fixed_at_true > 0) {
5853 int circuit_start = -1;
5854 std::vector<int>
next(num_nodes, -1);
5855 std::vector<int> new_in_degree(num_nodes, 0);
5856 std::vector<int> new_out_degree(num_nodes, 0);
5857 for (
int i = 0; i < num_arcs; ++i) {
5858 const int ref =
proto.literals(i);
5866 circuit_start =
proto.tails(i);
5870 ++new_out_degree[
proto.tails(i)];
5871 ++new_in_degree[
proto.heads(i)];
5874 proto.set_literals(new_size, ref);
5884 for (
int i = 0; i < num_nodes; ++i) {
5885 if (new_in_degree[i] == 0 || new_out_degree[i] == 0) {
5891 if (circuit_start != -1) {
5892 std::vector<bool> visited(num_nodes,
false);
5893 int current = circuit_start;
5894 while (current != -1 && !visited[current]) {
5895 visited[current] =
true;
5896 current =
next[current];
5898 if (current == circuit_start) {
5901 std::vector<bool> has_self_arc(num_nodes,
false);
5902 for (
int i = 0; i < num_arcs; ++i) {
5903 if (visited[
proto.tails(i)])
continue;
5905 has_self_arc[
proto.tails(i)] =
true;
5911 for (
int n = 0; n < num_nodes; ++n) {
5912 if (!visited[n] && !has_self_arc[n]) {
5914 return MarkConstraintAsFalse(
ct);
5918 return RemoveConstraint(
ct);
5922 if (num_true == new_size) {
5924 return RemoveConstraint(
ct);
5930 for (
int i = 0; i < num_nodes; ++i) {
5931 for (
const std::vector<int>* arc_literals :
5932 {&incoming_arcs[i], &outgoing_arcs[i]}) {
5933 std::vector<int> literals;
5934 for (
const int ref : *arc_literals) {
5940 literals.push_back(ref);
5942 if (literals.size() == 2 && literals[0] !=
NegatedRef(literals[1])) {
5951 if (new_size < num_arcs) {
5952 proto.mutable_tails()->Truncate(new_size);
5953 proto.mutable_heads()->Truncate(new_size);
5954 proto.mutable_literals()->Truncate(new_size);
5961 bool CpModelPresolver::PresolveAutomaton(ConstraintProto*
ct) {
5964 AutomatonConstraintProto&
proto = *
ct->mutable_automaton();
5965 if (
proto.vars_size() == 0 ||
proto.transition_label_size() == 0) {
5969 bool all_have_same_affine_relation =
true;
5970 std::vector<AffineRelation::Relation> affine_relations;
5971 for (
int v = 0; v <
proto.vars_size(); ++v) {
5972 const int var =
ct->automaton().vars(v);
5974 affine_relations.push_back(r);
5975 if (r.representative ==
var) {
5976 all_have_same_affine_relation =
false;
5979 if (v > 0 && (r.coeff != affine_relations[v - 1].coeff ||
5980 r.offset != affine_relations[v - 1].offset)) {
5981 all_have_same_affine_relation =
false;
5986 if (all_have_same_affine_relation) {
5987 for (
int v = 0; v <
proto.vars_size(); ++v) {
5990 const AffineRelation::Relation rep = affine_relations.front();
5992 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
5993 const int64_t label =
proto.transition_label(t);
5994 int64_t inverse_label = (label - rep.offset) / rep.coeff;
5995 if (inverse_label * rep.coeff + rep.offset == label) {
5996 if (new_size != t) {
5997 proto.set_transition_tail(new_size,
proto.transition_tail(t));
5998 proto.set_transition_head(new_size,
proto.transition_head(t));
6000 proto.set_transition_label(new_size, inverse_label);
6004 if (new_size <
proto.transition_tail_size()) {
6005 proto.mutable_transition_tail()->Truncate(new_size);
6006 proto.mutable_transition_label()->Truncate(new_size);
6007 proto.mutable_transition_head()->Truncate(new_size);
6014 std::vector<absl::flat_hash_set<int64_t>> reachable_states;
6015 std::vector<absl::flat_hash_set<int64_t>> reachable_labels;
6019 bool removed_values =
false;
6021 for (
int time = 0;
time < reachable_labels.size(); ++
time) {
6025 {reachable_labels[time].begin(), reachable_labels[time].end()}),
6031 if (removed_values) {
6037 for (
int t = 0; t <
proto.transition_tail_size(); ++t) {
6038 const int64_t label =
proto.transition_label(t);
6039 if (hull.Contains(label)) {
6040 if (new_size != t) {
6041 proto.set_transition_tail(new_size,
proto.transition_tail(t));
6042 proto.set_transition_label(new_size, label);
6043 proto.set_transition_head(new_size,
proto.transition_head(t));
6048 if (new_size <
proto.transition_tail_size()) {
6049 proto.mutable_transition_tail()->Truncate(new_size);
6050 proto.mutable_transition_label()->Truncate(new_size);
6051 proto.mutable_transition_head()->Truncate(new_size);
6059 bool CpModelPresolver::PresolveReservoir(ConstraintProto*
ct) {
6063 ReservoirConstraintProto&
proto = *
ct->mutable_reservoir();
6064 bool changed =
false;
6065 for (LinearExpressionProto& exp : *(
proto.mutable_time_exprs())) {
6066 changed |= CanonicalizeLinearExpression(*
ct, &exp);
6068 for (LinearExpressionProto& exp : *(
proto.mutable_level_changes())) {
6069 changed |= CanonicalizeLinearExpression(*
ct, &exp);
6072 if (
proto.active_literals().empty()) {
6074 for (
int i = 0; i <
proto.time_exprs_size(); ++i) {
6075 proto.add_active_literals(true_literal);
6080 const auto& demand_is_null = [&](
int i) {
6088 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
6089 if (demand_is_null(i)) num_zeros++;
6092 if (num_zeros > 0) {
6095 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
6096 if (demand_is_null(i))
continue;
6097 *
proto.mutable_level_changes(new_size) =
proto.level_changes(i);
6098 *
proto.mutable_time_exprs(new_size) =
proto.time_exprs(i);
6099 proto.set_active_literals(new_size,
proto.active_literals(i));
6103 proto.mutable_level_changes()->erase(
6104 proto.mutable_level_changes()->begin() + new_size,
6105 proto.mutable_level_changes()->end());
6106 proto.mutable_time_exprs()->erase(
6107 proto.mutable_time_exprs()->begin() + new_size,
6108 proto.mutable_time_exprs()->end());
6109 proto.mutable_active_literals()->Truncate(new_size);
6112 "reservoir: remove zero level_changes or inactive events.");
6116 for (
const LinearExpressionProto& level_change :
proto.level_changes()) {
6117 if (!context_->
IsFixed(level_change))
return changed;
6120 const int num_events =
proto.level_changes_size();
6121 int64_t gcd =
proto.level_changes().empty()
6124 int num_positives = 0;
6125 int num_negatives = 0;
6126 int64_t max_sum_of_positive_level_changes = 0;
6127 int64_t min_sum_of_negative_level_changes = 0;
6128 for (
int i = 0; i < num_events; ++i) {
6133 max_sum_of_positive_level_changes +=
demand;
6137 min_sum_of_negative_level_changes +=
demand;
6141 if (min_sum_of_negative_level_changes >=
proto.min_level() &&
6142 max_sum_of_positive_level_changes <=
proto.max_level()) {
6144 return RemoveConstraint(
ct);
6147 if (min_sum_of_negative_level_changes >
proto.max_level() ||
6148 max_sum_of_positive_level_changes <
proto.min_level()) {
6153 if (min_sum_of_negative_level_changes >
proto.min_level()) {
6154 proto.set_min_level(min_sum_of_negative_level_changes);
6156 "reservoir: increase min_level to reachable value");
6159 if (max_sum_of_positive_level_changes <
proto.max_level()) {
6160 proto.set_max_level(max_sum_of_positive_level_changes);
6161 context_->
UpdateRuleStats(
"reservoir: reduce max_level to reachable value");
6164 if (
proto.min_level() <= 0 &&
proto.max_level() >= 0 &&
6165 (num_positives == 0 || num_negatives == 0)) {
6169 context_->
working_model->add_constraints()->mutable_linear();
6170 int64_t fixed_contrib = 0;
6171 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
6175 const int active =
proto.active_literals(i);
6177 sum->add_vars(active);
6181 sum->add_coeffs(-
demand);
6185 sum->add_domain(
proto.min_level() - fixed_contrib);
6186 sum->add_domain(
proto.max_level() - fixed_contrib);
6188 return RemoveConstraint(
ct);
6192 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
6193 proto.mutable_level_changes(i)->set_offset(
6195 proto.mutable_level_changes(i)->clear_vars();
6196 proto.mutable_level_changes(i)->clear_coeffs();
6202 const Domain reduced_domain = Domain({
proto.min_level(),
proto.max_level()})
6203 .InverseMultiplicationBy(gcd);
6204 proto.set_min_level(reduced_domain.Min());
6205 proto.set_max_level(reduced_domain.Max());
6207 "reservoir: simplify level_changes and levels by gcd.");
6210 if (num_positives == 1 && num_negatives > 0) {
6212 "TODO reservoir: one producer, multiple consumers.");
6215 absl::flat_hash_set<std::tuple<int, int64_t, int64_t, int>> time_active_set;
6216 for (
int i = 0; i <
proto.level_changes_size(); ++i) {
6217 const LinearExpressionProto&
time =
proto.time_exprs(i);
6221 const std::tuple<int, int64_t, int64_t, int> key = std::make_tuple(
6224 proto.active_literals(i));
6225 if (time_active_set.contains(key)) {
6226 context_->
UpdateRuleStats(
"TODO reservoir: merge synchronized events.");
6229 time_active_set.insert(key);
6239 void CpModelPresolver::ExtractBoolAnd() {
6240 absl::flat_hash_map<int, int> ref_to_bool_and;
6241 const int num_constraints = context_->
working_model->constraints_size();
6242 std::vector<int> to_remove;
6243 for (
int c = 0; c < num_constraints; ++c) {
6247 if (
ct.constraint_case() == ConstraintProto::kBoolOr &&
6248 ct.bool_or().literals().size() == 2) {
6252 to_remove.push_back(c);
6256 if (
ct.constraint_case() == ConstraintProto::kAtMostOne &&
6257 ct.at_most_one().literals().size() == 2) {
6258 AddImplication(
ct.at_most_one().literals(0),
6261 to_remove.push_back(c);
6267 for (
const int c : to_remove) {
6268 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
6269 CHECK(RemoveConstraint(
ct));
6276 void CpModelPresolver::Probe() {
6284 auto* implication_graph =
model.GetOrCreate<BinaryImplicationGraph>();
6285 auto* sat_solver =
model.GetOrCreate<SatSolver>();
6286 auto* mapping =
model.GetOrCreate<CpModelMapping>();
6287 auto* prober =
model.GetOrCreate<Prober>();
6300 int64_t work_done = 0;
6301 const int64_t work_limit = 1e8;
6303 const auto& assignment = sat_solver->Assignment();
6304 prober->SetPropagationCallback([&](Literal decision) {
6305 if (work_done > work_limit)
return;
6306 const int decision_var =
6307 mapping->GetProtoVariableFromBooleanVariable(decision.Variable());
6308 if (decision_var < 0)
return;
6311 if (c < 0)
continue;
6313 if (
ct.enforcement_literal().size() > 2) {
6327 bool decision_is_positive =
false;
6328 bool has_false_literal =
false;
6329 bool simplification_possible =
false;
6330 for (
const int ref :
ct.enforcement_literal()) {
6332 const Literal lit = mapping->Literal(ref);
6335 decision_is_positive = assignment.LiteralIsTrue(lit);
6336 if (!decision_is_positive)
break;
6339 if (assignment.LiteralIsFalse(lit)) {
6341 has_false_literal =
true;
6342 }
else if (assignment.LiteralIsTrue(lit)) {
6344 simplification_possible =
true;
6347 if (!decision_is_positive)
continue;
6349 if (has_false_literal) {
6351 auto* mutable_ct = context_->
working_model->mutable_constraints(c);
6352 mutable_ct->Clear();
6353 mutable_ct->add_enforcement_literal(decision_ref);
6354 mutable_ct->mutable_bool_and()->add_literals(
NegatedRef(false_ref));
6356 "probing: reduced enforced constraint to implication.");
6361 if (simplification_possible) {
6363 auto* mutable_enforcements =
6365 ->mutable_enforcement_literal();
6366 for (
const int ref :
ct.enforcement_literal()) {
6368 assignment.LiteralIsTrue(mapping->Literal(ref))) {
6371 mutable_enforcements->Set(new_size++, ref);
6373 mutable_enforcements->Truncate(new_size);
6380 if (
ct.constraint_case() != ConstraintProto::kBoolOr)
continue;
6381 if (
ct.bool_or().literals().size() <= 2)
continue;
6385 bool decision_is_negative =
false;
6386 bool has_true_literal =
false;
6387 bool simplification_possible =
false;
6388 for (
const int ref :
ct.bool_or().literals()) {
6390 const Literal lit = mapping->Literal(ref);
6393 decision_is_negative = assignment.LiteralIsFalse(lit);
6394 if (!decision_is_negative)
break;
6397 if (assignment.LiteralIsTrue(lit)) {
6399 has_true_literal =
true;
6400 }
else if (assignment.LiteralIsFalse(lit)) {
6402 simplification_possible =
true;
6405 if (!decision_is_negative)
continue;
6407 if (has_true_literal) {
6410 auto* mutable_bool_or =
6412 ->mutable_bool_or();
6413 mutable_bool_or->mutable_literals()->Clear();
6414 mutable_bool_or->add_literals(decision_ref);
6415 mutable_bool_or->add_literals(true_ref);
6421 if (simplification_possible) {
6423 auto* mutable_bool_or =
6425 ->mutable_bool_or();
6426 for (
const int ref :
ct.bool_or().literals()) {
6428 assignment.LiteralIsFalse(mapping->Literal(ref))) {
6431 mutable_bool_or->set_literals(new_size++, ref);
6433 mutable_bool_or->mutable_literals()->Truncate(new_size);
6441 prober->ProbeBooleanVariables(
6442 context_->
params().probing_deterministic_time_limit());
6444 model.GetOrCreate<TimeLimit>()->GetElapsedDeterministicTime());
6445 if (work_done > 0) {
6447 "[Probing] implications and bool_or (work_done=", work_done,
6448 ").", (work_done > work_limit ?
" Aborted." :
""));
6450 if (sat_solver->ModelIsUnsat() || !implication_graph->DetectEquivalences()) {
6455 CHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
6456 for (
int i = 0; i < sat_solver->LiteralTrail().
Index(); ++i) {
6457 const Literal l = sat_solver->LiteralTrail()[i];
6458 const int var = mapping->GetProtoVariableFromBooleanVariable(l.Variable());
6465 const int num_variables = context_->
working_model->variables().size();
6466 auto* integer_trail =
model.GetOrCreate<IntegerTrail>();
6467 for (
int var = 0;
var < num_variables; ++
var) {
6470 if (!mapping->IsBoolean(
var)) {
6473 integer_trail->InitialVariableDomain(mapping->Integer(
var)))) {
6480 const Literal l = mapping->Literal(
var);
6481 const Literal r = implication_graph->RepresentativeOf(l);
6484 mapping->GetProtoVariableFromBooleanVariable(r.Variable());
6495 std::vector<std::vector<Literal>> cliques;
6497 int64_t num_literals_before = 0;
6498 const int num_constraints = context_->
working_model->constraints_size();
6499 for (
int c = 0; c < num_constraints; ++c) {
6500 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
6501 if (
ct->constraint_case() == ConstraintProto::kAtMostOne) {
6502 std::vector<Literal> clique;
6503 for (
const int ref :
ct->at_most_one().literals()) {
6504 clique.push_back(mapping->Literal(ref));
6506 num_literals_before += clique.size();
6507 cliques.push_back(clique);
6510 }
else if (
ct->constraint_case() == ConstraintProto::kBoolAnd) {
6511 if (
ct->enforcement_literal().size() != 1)
continue;
6512 const Literal enforcement =
6513 mapping->Literal(
ct->enforcement_literal(0));
6514 for (
const int ref :
ct->bool_and().literals()) {
6515 if (ref ==
ct->enforcement_literal(0))
continue;
6516 num_literals_before += 2;
6517 cliques.push_back({enforcement, mapping->Literal(ref).Negated()});
6523 const int64_t num_old_cliques = cliques.size();
6525 implication_graph->TransformIntoMaxCliques(
6532 int num_new_cliques = 0;
6533 int64_t num_literals_after = 0;
6534 for (
const std::vector<Literal>& clique : cliques) {
6535 if (clique.empty())
continue;
6537 num_literals_after += clique.size();
6539 for (
const Literal
literal : clique) {
6541 mapping->GetProtoVariableFromBooleanVariable(
literal.Variable());
6542 if (
var < 0)
continue;
6544 ct->mutable_at_most_one()->add_literals(
var);
6551 PresolveAtMostOne(
ct);
6554 if (num_new_cliques != num_old_cliques) {
6555 context_->
UpdateRuleStats(
"at_most_one: transformed into max clique.");
6558 if (num_old_cliques != num_new_cliques ||
6559 num_literals_before != num_literals_after) {
6560 SOLVER_LOG(logger_,
"[MaxClique] Merged ", num_old_cliques,
"(",
6561 num_literals_before,
" literals) into ", num_new_cliques,
"(",
6562 num_literals_after,
" literals) at_most_ones. ",
6570 void CpModelPresolver::PresolvePureSatPart() {
6575 const int num_variables = context_->
working_model->variables_size();
6576 SatPostsolver sat_postsolver(num_variables);
6577 SatPresolver sat_presolver(&sat_postsolver, logger_);
6578 sat_presolver.SetNumVariables(num_variables);
6579 sat_presolver.SetTimeLimit(context_->
time_limit());
6581 SatParameters params = context_->
params();
6588 if (params.debug_postsolve_with_full_solver()) {
6589 params.set_presolve_blocked_clause(
false);
6595 params.set_presolve_use_bva(
false);
6596 sat_presolver.SetParameters(params);
6599 absl::flat_hash_set<int> used_variables;
6600 auto convert = [&used_variables](
int ref) {
6602 if (
RefIsPositive(ref))
return Literal(BooleanVariable(ref),
true);
6603 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
6611 for (
int c = 0; c < context_->
working_model->constraints_size(); ++c) {
6613 if (
ct.constraint_case() == ConstraintProto::kBoolOr ||
6614 ct.constraint_case() == ConstraintProto::kBoolAnd) {
6633 std::vector<Literal> clause;
6634 int num_removed_constraints = 0;
6635 for (
int i = 0; i < context_->
working_model->constraints_size(); ++i) {
6638 if (
ct.constraint_case() == ConstraintProto::kBoolOr) {
6639 ++num_removed_constraints;
6641 for (
const int ref :
ct.bool_or().literals()) {
6642 clause.push_back(convert(ref));
6644 for (
const int ref :
ct.enforcement_literal()) {
6645 clause.push_back(convert(ref).Negated());
6647 sat_presolver.AddClause(clause);
6654 if (
ct.constraint_case() == ConstraintProto::kBoolAnd) {
6657 const int left_size =
ct.enforcement_literal().size();
6658 const int right_size =
ct.bool_and().literals().size();
6659 if (left_size > 1 && right_size > 1 &&
6660 (left_size + 1) * right_size > 1000) {
6664 ++num_removed_constraints;
6665 std::vector<Literal> clause;
6666 for (
const int ref :
ct.enforcement_literal()) {
6667 clause.push_back(convert(ref).Negated());
6670 for (
const int ref :
ct.bool_and().literals()) {
6671 clause.back() = convert(ref);
6672 sat_presolver.AddClause(clause);
6682 if (num_removed_constraints == 0)
return;
6692 std::vector<bool> can_be_removed(num_variables,
false);
6693 for (
int i = 0; i < num_variables; ++i) {
6695 can_be_removed[i] =
true;
6701 if (used_variables.contains(i) && context_->
IsFixed(i)) {
6703 sat_presolver.AddClause({convert(i)});
6705 sat_presolver.AddClause({convert(
NegatedRef(i))});
6713 const int num_passes = params.presolve_use_bva() ? 4 : 1;
6714 for (
int i = 0; i < num_passes; ++i) {
6715 const int old_num_clause = sat_postsolver.NumClauses();
6716 if (!sat_presolver.Presolve(can_be_removed)) {
6717 VLOG(1) <<
"UNSAT during SAT presolve.";
6720 if (old_num_clause == sat_postsolver.NumClauses())
break;
6724 const int new_num_variables = sat_presolver.NumVariables();
6725 if (new_num_variables > context_->
working_model->variables_size()) {
6726 VLOG(1) <<
"New variables added by the SAT presolver.";
6728 i < new_num_variables; ++i) {
6729 IntegerVariableProto* var_proto =
6731 var_proto->add_domain(0);
6732 var_proto->add_domain(1);
6738 ExtractClauses(
true, sat_presolver, context_->
working_model);
6746 ExtractClauses(
false, sat_postsolver,
6750 void CpModelPresolver::ShiftObjectiveWithExactlyOnes() {
6760 std::vector<int> exos;
6761 const int num_constraints = context_->
working_model->constraints_size();
6762 for (
int c = 0; c < num_constraints; ++c) {
6764 if (!
ct.enforcement_literal().empty())
continue;
6765 if (
ct.constraint_case() == ConstraintProto::kExactlyOne) {
6782 for (
int i = 0; i < 3; ++i) {
6783 for (
const int c : exos) {
6785 const int num_terms =
ct.exactly_one().literals().size();
6786 if (num_terms <= 1)
continue;
6789 for (
int i = 0; i < num_terms; ++i) {
6790 const int literal =
ct.exactly_one().literals(i);
6793 if (obj < min_obj) {
6794 second_min = min_obj;
6796 }
else if (obj < second_min) {
6800 if (second_min == 0)
continue;
6809 if (num_shifts > 0) {
6810 context_->
UpdateRuleStats(
"objective: shifted cost with exactly ones",
6829 void CpModelPresolver::ExpandObjective() {
6841 const int num_variables = context_->
working_model->variables_size();
6842 const int num_constraints = context_->
working_model->constraints_size();
6845 const auto get_index = [](
int var,
bool to_lb) {
6846 return 2 *
var + (to_lb ? 0 : 1);
6848 const auto get_lit_index = [](
int lit) {
6851 const int num_nodes = 2 * num_variables;
6852 std::vector<std::vector<int>> index_graph(num_nodes);
6856 std::vector<int> index_to_best_c(num_nodes, -1);
6857 std::vector<int> index_to_best_size(num_nodes, 0);
6862 int num_propagations = 0;
6863 int num_tight_variables = 0;
6864 int num_tight_constraints = 0;
6865 const int kNumEntriesThreshold = 1e8;
6866 for (
int c = 0; c < num_constraints; ++c) {
6870 if (!
ct.enforcement_literal().empty())
continue;
6874 if (
ct.constraint_case() == ConstraintProto::kExactlyOne) {
6875 const int num_terms =
ct.exactly_one().literals().size();
6876 ++num_tight_constraints;
6877 num_tight_variables += num_terms;
6878 for (
int i = 0; i < num_terms; ++i) {
6880 const int neg_index = get_lit_index(
ct.exactly_one().literals(i)) ^ 1;
6882 const int old_c = index_to_best_c[neg_index];
6883 if (old_c == -1 || num_terms > index_to_best_size[neg_index]) {
6884 index_to_best_c[neg_index] = c;
6885 index_to_best_size[neg_index] = num_terms;
6888 for (
int j = 0; j < num_terms; ++j) {
6889 if (j == i)
continue;
6890 const int other_index = get_lit_index(
ct.exactly_one().literals(j));
6892 index_graph[neg_index].push_back(other_index);
6899 if (
ct.constraint_case() != ConstraintProto::kLinear ||
6900 ct.linear().domain().size() != 2 ||
6901 ct.linear().domain(0) !=
ct.linear().domain(1)) {
6907 const auto [min_activity, max_activity] =
6910 bool is_tight =
false;
6911 const int64_t rhs =
ct.linear().domain(0);
6912 const int num_terms =
ct.linear().vars_size();
6913 for (
int i = 0; i < num_terms; ++i) {
6914 const int var =
ct.linear().vars(i);
6915 const int64_t coeff =
ct.linear().coeffs(i);
6916 if (std::abs(coeff) != 1)
continue;
6919 const int index = get_index(
var, coeff > 0);
6922 const int64_t implied_shifted_ub = rhs - min_activity;
6923 if (implied_shifted_ub <= var_range) {
6924 if (implied_shifted_ub < var_range) ++num_propagations;
6926 ++num_tight_variables;
6928 const int neg_index =
index ^ 1;
6929 const int old_c = index_to_best_c[neg_index];
6930 if (old_c == -1 || num_terms > index_to_best_size[neg_index]) {
6931 index_to_best_c[neg_index] = c;
6932 index_to_best_size[neg_index] = num_terms;
6935 for (
int j = 0; j < num_terms; ++j) {
6936 if (j == i)
continue;
6937 const int other_index =
6938 get_index(
ct.linear().vars(j),
ct.linear().coeffs(j) > 0);
6940 index_graph[neg_index].push_back(other_index);
6943 const int64_t implied_shifted_lb = max_activity - rhs;
6944 if (implied_shifted_lb <= var_range) {
6945 if (implied_shifted_lb < var_range) ++num_propagations;
6947 ++num_tight_variables;
6949 const int old_c = index_to_best_c[
index];
6950 if (old_c == -1 || num_terms > index_to_best_size[
index]) {
6951 index_to_best_c[
index] = c;
6952 index_to_best_size[
index] = num_terms;
6955 for (
int j = 0; j < num_terms; ++j) {
6956 if (j == i)
continue;
6957 const int other_index =
6958 get_index(
ct.linear().vars(j),
ct.linear().coeffs(j) < 0);
6960 index_graph[
index].push_back(other_index);
6964 if (is_tight) ++num_tight_constraints;
6970 if (num_propagations > 0) {
6990 if (!topo_order.ok()) {
6991 std::vector<std::vector<int>> components;
6993 index_graph, &components);
6994 for (
const std::vector<int>& compo : components) {
6995 if (compo.size() == 1)
continue;
6997 const int rep_var = compo[0] / 2;
6998 const bool rep_to_lp = (compo[0] % 2) == 0;
6999 for (
int i = 1; i < compo.size(); ++i) {
7000 const int var = compo[i] / 2;
7001 const bool to_lb = (compo[i] % 2) == 0;
7005 const int64_t rep_coeff = rep_to_lp ? 1 : -1;
7006 const int64_t var_coeff = to_lb ? 1 : -1;
7007 const int64_t offset =
7009 (rep_to_lp ? -context_->
MinOf(rep_var) : context_->
MaxOf(rep_var));
7011 rep_coeff * offset)) {
7024 int num_expands = 0;
7026 for (
const int index : *topo_order) {
7027 if (index_graph[
index].empty())
continue;
7031 if (obj_coeff == 0)
continue;
7033 const bool to_lb = (
index % 2) == 0;
7034 if (obj_coeff > 0 == to_lb) {
7035 const ConstraintProto&
ct =
7037 if (
ct.constraint_case() == ConstraintProto::kExactlyOne) {
7039 for (
const int lit :
ct.exactly_one().literals()) {
7060 int64_t objective_coeff_in_expanded_constraint = 0;
7061 const int num_terms =
ct.linear().vars().size();
7062 for (
int i = 0; i < num_terms; ++i) {
7063 if (
ct.linear().vars(i) ==
var) {
7064 objective_coeff_in_expanded_constraint =
ct.linear().coeffs(i);
7068 if (objective_coeff_in_expanded_constraint == 0) {
7074 var, objective_coeff_in_expanded_constraint,
ct)) {
7084 if (num_expands > 0) {
7089 logger_,
"[ExpandObjective]",
" #propagations=", num_propagations,
7090 " #entries=",
num_entries,
" #tight_variables=", num_tight_variables,
7091 " #tight_constraints=", num_tight_constraints,
" #expands=", num_expands,
7095 void CpModelPresolver::MergeNoOverlapConstraints() {
7098 const int num_constraints = context_->
working_model->constraints_size();
7099 int old_num_no_overlaps = 0;
7100 int old_num_intervals = 0;
7103 std::vector<int> disjunctive_index;
7104 std::vector<std::vector<Literal>> cliques;
7105 for (
int c = 0; c < num_constraints; ++c) {
7107 if (
ct.constraint_case() != ConstraintProto::kNoOverlap)
continue;
7108 std::vector<Literal> clique;
7109 for (
const int i :
ct.no_overlap().intervals()) {
7110 clique.push_back(Literal(BooleanVariable(i),
true));
7112 cliques.push_back(clique);
7113 disjunctive_index.push_back(c);
7115 old_num_no_overlaps++;
7116 old_num_intervals += clique.size();
7118 if (old_num_no_overlaps == 0)
return;
7122 local_model.GetOrCreate<Trail>()->Resize(num_constraints);
7123 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
7124 graph->Resize(num_constraints);
7125 for (
const std::vector<Literal>& clique : cliques) {
7128 CHECK(graph->AddAtMostOne(clique));
7130 CHECK(graph->DetectEquivalences());
7131 graph->TransformIntoMaxCliques(
7136 int new_num_no_overlaps = 0;
7137 int new_num_intervals = 0;
7138 for (
int i = 0; i < cliques.size(); ++i) {
7139 const int ct_index = disjunctive_index[i];
7140 ConstraintProto*
ct =
7143 if (cliques[i].empty())
continue;
7144 for (
const Literal l : cliques[i]) {
7145 CHECK(l.IsPositive());
7146 ct->mutable_no_overlap()->add_intervals(l.Variable().value());
7148 new_num_no_overlaps++;
7149 new_num_intervals += cliques[i].size();
7151 if (old_num_intervals != new_num_intervals ||
7152 old_num_no_overlaps != new_num_no_overlaps) {
7153 VLOG(1) << absl::StrCat(
"Merged ", old_num_no_overlaps,
" no-overlaps (",
7154 old_num_intervals,
" intervals) into ",
7155 new_num_no_overlaps,
" no-overlaps (",
7156 new_num_intervals,
" intervals).");
7165 void CpModelPresolver::TransformIntoMaxCliques() {
7168 auto convert = [](
int ref) {
7169 if (
RefIsPositive(ref))
return Literal(BooleanVariable(ref),
true);
7170 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
7172 const int num_constraints = context_->
working_model->constraints_size();
7176 std::vector<std::vector<Literal>> cliques;
7178 for (
int c = 0; c < num_constraints; ++c) {
7179 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
7180 if (
ct->constraint_case() == ConstraintProto::kAtMostOne) {
7181 std::vector<Literal> clique;
7182 for (
const int ref :
ct->at_most_one().literals()) {
7183 clique.push_back(convert(ref));
7185 cliques.push_back(clique);
7186 if (RemoveConstraint(
ct)) {
7189 }
else if (
ct->constraint_case() == ConstraintProto::kBoolAnd) {
7190 if (
ct->enforcement_literal().size() != 1)
continue;
7191 const Literal enforcement = convert(
ct->enforcement_literal(0));
7192 for (
const int ref :
ct->bool_and().literals()) {
7193 if (ref ==
ct->enforcement_literal(0))
continue;
7194 cliques.push_back({enforcement, convert(ref).Negated()});
7196 if (RemoveConstraint(
ct)) {
7202 int64_t num_literals_before = 0;
7203 const int num_old_cliques = cliques.size();
7207 const int num_variables = context_->
working_model->variables().size();
7208 local_model.GetOrCreate<Trail>()->Resize(num_variables);
7209 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
7210 graph->Resize(num_variables);
7211 for (
const std::vector<Literal>& clique : cliques) {
7212 num_literals_before += clique.size();
7213 if (!graph->AddAtMostOne(clique)) {
7217 if (!graph->DetectEquivalences()) {
7220 graph->TransformIntoMaxCliques(
7227 for (
int var = 0;
var < num_variables; ++
var) {
7228 const Literal l = Literal(BooleanVariable(
var),
true);
7229 if (graph->RepresentativeOf(l) != l) {
7230 const Literal r = graph->RepresentativeOf(l);
7232 var, r.IsPositive() ? r.Variable().value()
7237 int num_new_cliques = 0;
7238 int64_t num_literals_after = 0;
7239 for (
const std::vector<Literal>& clique : cliques) {
7240 if (clique.empty())
continue;
7242 num_literals_after += clique.size();
7244 for (
const Literal
literal : clique) {
7246 ct->mutable_at_most_one()->add_literals(
literal.Variable().value());
7248 ct->mutable_at_most_one()->add_literals(
7254 PresolveAtMostOne(
ct);
7257 if (num_new_cliques != num_old_cliques) {
7258 context_->
UpdateRuleStats(
"at_most_one: transformed into max clique.");
7261 if (num_old_cliques != num_new_cliques ||
7262 num_literals_before != num_literals_after) {
7263 SOLVER_LOG(logger_,
"[MaxClique] Merged ", num_old_cliques,
"(",
7264 num_literals_before,
" literals) into ", num_new_cliques,
"(",
7265 num_literals_after,
" literals) at_most_ones.");
7271 bool IsAffineIntAbs(ConstraintProto*
ct) {
7272 if (
ct->constraint_case() != ConstraintProto::kLinMax ||
7273 ct->lin_max().exprs_size() != 2 ||
7274 ct->lin_max().target().vars_size() > 1 ||
7275 ct->lin_max().exprs(0).vars_size() != 1 ||
7276 ct->lin_max().exprs(1).vars_size() != 1) {
7280 const LinearArgumentProto& lin_max =
ct->lin_max();
7281 if (lin_max.exprs(0).offset() != -lin_max.exprs(1).offset())
return false;
7287 const int64_t left_coeff =
RefIsPositive(lin_max.exprs(0).vars(0))
7288 ? lin_max.exprs(0).coeffs(0)
7289 : -lin_max.exprs(0).coeffs(0);
7290 const int64_t right_coeff =
RefIsPositive(lin_max.exprs(1).vars(0))
7291 ? lin_max.exprs(1).coeffs(0)
7292 : -lin_max.exprs(1).coeffs(0);
7293 return left_coeff == -right_coeff;
7300 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
7303 if (ExploitEquivalenceRelations(c,
ct)) {
7308 if (PresolveEnforcementLiteral(
ct)) {
7313 switch (
ct->constraint_case()) {
7314 case ConstraintProto::kBoolOr:
7315 return PresolveBoolOr(
ct);
7316 case ConstraintProto::kBoolAnd:
7317 return PresolveBoolAnd(
ct);
7318 case ConstraintProto::kAtMostOne:
7319 return PresolveAtMostOne(
ct);
7320 case ConstraintProto::kExactlyOne:
7321 return PresolveExactlyOne(
ct);
7322 case ConstraintProto::kBoolXor:
7323 return PresolveBoolXor(
ct);
7324 case ConstraintProto::kLinMax:
7325 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_lin_max())) {
7328 if (IsAffineIntAbs(
ct)) {
7329 return PresolveIntAbs(
ct);
7331 return PresolveLinMax(
ct);
7333 case ConstraintProto::kIntProd:
7334 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_int_prod())) {
7337 return PresolveIntProd(
ct);
7338 case ConstraintProto::kIntDiv:
7339 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_int_div())) {
7342 return PresolveIntDiv(
ct);
7343 case ConstraintProto::kIntMod:
7344 if (CanonicalizeLinearArgument(*
ct,
ct->mutable_int_mod())) {
7347 return PresolveIntMod(
ct);
7348 case ConstraintProto::kLinear: {
7349 if (CanonicalizeLinear(
ct)) {
7352 if (PropagateDomainsInLinear(c,
ct)) {
7355 if (PresolveSmallLinear(
ct)) {
7358 if (PresolveLinearEqualityWithModulo(
ct)) {
7362 if (RemoveSingletonInLinear(
ct)) {
7367 if (PresolveSmallLinear(
ct)) {
7371 if (PresolveSmallLinear(
ct)) {
7374 if (PresolveLinearOnBooleans(
ct)) {
7379 const int old_num_enforcement_literals =
ct->enforcement_literal_size();
7380 ExtractEnforcementLiteralFromLinearConstraint(c,
ct);
7381 if (
ct->enforcement_literal_size() > old_num_enforcement_literals) {
7382 if (DivideLinearByGcd(
ct)) {
7385 if (PresolveSmallLinear(
ct)) {
7390 if (PresolveDiophantine(
ct)) {
7394 TryToReduceCoefficientsOfLinearConstraint(c,
ct);
7397 case ConstraintProto::kInterval:
7398 return PresolveInterval(c,
ct);
7399 case ConstraintProto::kInverse:
7400 return PresolveInverse(
ct);
7401 case ConstraintProto::kElement:
7402 return PresolveElement(
ct);
7403 case ConstraintProto::kTable:
7404 return PresolveTable(
ct);
7405 case ConstraintProto::kAllDiff:
7406 return PresolveAllDiff(
ct);
7407 case ConstraintProto::kNoOverlap:
7408 DetectDuplicateIntervals(c,
7409 ct->mutable_no_overlap()->mutable_intervals());
7410 return PresolveNoOverlap(
ct);
7411 case ConstraintProto::kNoOverlap2D:
7412 DetectDuplicateIntervals(
7413 c,
ct->mutable_no_overlap_2d()->mutable_x_intervals());
7414 DetectDuplicateIntervals(
7415 c,
ct->mutable_no_overlap_2d()->mutable_y_intervals());
7416 return PresolveNoOverlap2D(c,
ct);
7417 case ConstraintProto::kCumulative:
7418 DetectDuplicateIntervals(c,
7419 ct->mutable_cumulative()->mutable_intervals());
7420 return PresolveCumulative(
ct);
7421 case ConstraintProto::kCircuit:
7422 return PresolveCircuit(
ct);
7423 case ConstraintProto::kRoutes:
7424 return PresolveRoutes(
ct);
7425 case ConstraintProto::kAutomaton:
7426 return PresolveAutomaton(
ct);
7427 case ConstraintProto::kReservoir:
7428 return PresolveReservoir(
ct);
7435 bool CpModelPresolver::ProcessSetPPCSubset(
int subset_c,
int superset_c,
7436 absl::flat_hash_set<int>* tmp_set,
7437 bool* remove_subset,
7438 bool* remove_superset,
7439 bool* stop_processing_superset) {
7440 ConstraintProto* subset_ct =
7442 ConstraintProto* superset_ct =
7445 if ((subset_ct->constraint_case() == ConstraintProto::kBoolOr ||
7446 subset_ct->constraint_case() == ConstraintProto::kExactlyOne) &&
7447 (superset_ct->constraint_case() == ConstraintProto::kAtMostOne ||
7448 superset_ct->constraint_case() == ConstraintProto::kExactlyOne)) {
7452 if (subset_ct->constraint_case() == ConstraintProto::kBoolOr) {
7453 tmp_set->insert(subset_ct->bool_or().literals().begin(),
7454 subset_ct->bool_or().literals().end());
7456 tmp_set->insert(subset_ct->exactly_one().literals().begin(),
7457 subset_ct->exactly_one().literals().end());
7463 superset_ct->constraint_case() == ConstraintProto::kAtMostOne
7464 ? superset_ct->at_most_one().literals()
7465 : superset_ct->exactly_one().literals()) {
7466 if (tmp_set->contains(
literal))
continue;
7472 if (superset_ct->constraint_case() != ConstraintProto::kExactlyOne) {
7473 ConstraintProto copy = *superset_ct;
7474 (*superset_ct->mutable_exactly_one()->mutable_literals()) =
7475 copy.at_most_one().literals();
7478 *remove_subset =
true;
7482 if ((subset_ct->constraint_case() == ConstraintProto::kBoolOr ||
7483 subset_ct->constraint_case() == ConstraintProto::kExactlyOne) &&
7484 superset_ct->constraint_case() == ConstraintProto::kBoolOr) {
7486 *remove_superset =
true;
7490 if (subset_ct->constraint_case() == ConstraintProto::kAtMostOne &&
7491 (superset_ct->constraint_case() == ConstraintProto::kAtMostOne ||
7492 superset_ct->constraint_case() == ConstraintProto::kExactlyOne)) {
7494 *remove_subset =
true;
7500 if (subset_ct->constraint_case() == ConstraintProto::kExactlyOne &&
7501 superset_ct->constraint_case() == ConstraintProto::kLinear) {
7505 tmp_set->insert(subset_ct->exactly_one().literals().begin(),
7506 subset_ct->exactly_one().literals().end());
7509 int num_matches = 0;
7511 Domain reachable(0);
7512 std::vector<std::pair<int64_t, int>> coeff_counts;
7513 for (
int i = 0; i < superset_ct->linear().vars().size(); ++i) {
7514 const int var = superset_ct->linear().vars(i);
7515 const int64_t coeff = superset_ct->linear().coeffs(i);
7516 if (tmp_set->contains(
var)) {
7518 min_sum =
std::min(min_sum, coeff);
7519 max_sum =
std::max(max_sum, coeff);
7520 coeff_counts.push_back({superset_ct->linear().coeffs(i), 1});
7526 .RelaxIfTooComplex();
7527 temp_ct_.mutable_linear()->add_vars(
var);
7528 temp_ct_.mutable_linear()->add_coeffs(coeff);
7538 if (num_matches != tmp_set->size())
return true;
7539 if (subset_ct->constraint_case() == ConstraintProto::kExactlyOne) {
7545 reachable = reachable.AdditionWith(Domain(min_sum, max_sum));
7547 if (reachable.IsIncludedIn(superset_rhs)) {
7549 context_->
UpdateRuleStats(
"setppc: removed trivial linear constraint");
7550 *remove_superset =
true;
7553 if (reachable.IntersectionWith(superset_rhs).IsEmpty()) {
7555 context_->
UpdateRuleStats(
"setppc: removed infeasible linear constraint");
7556 *stop_processing_superset =
true;
7557 return MarkConstraintAsFalse(superset_ct);
7562 if (superset_ct->enforcement_literal().empty()) {
7563 CHECK_GT(num_matches, 0);
7566 temp_ct_.mutable_linear());
7567 PropagateDomainsInLinear(-1, &temp_ct_);
7573 std::sort(coeff_counts.begin(), coeff_counts.end());
7575 for (
int i = 0; i < coeff_counts.size(); ++i) {
7577 coeff_counts[i].first == coeff_counts[new_size - 1].first) {
7578 coeff_counts[new_size - 1].second++;
7581 coeff_counts[new_size++] = coeff_counts[i];
7583 coeff_counts.resize(new_size);
7585 int64_t best_count = 0;
7586 for (
const auto [coeff, count] : coeff_counts) {
7587 if (count > best_count) {
7594 for (
int i = 0; i < superset_ct->linear().vars().size(); ++i) {
7595 const int var = superset_ct->linear().vars(i);
7596 int64_t coeff = superset_ct->linear().coeffs(i);
7597 if (tmp_set->contains(
var)) {
7598 if (coeff == best)
continue;
7601 superset_ct->mutable_linear()->set_vars(new_size,
var);
7602 superset_ct->mutable_linear()->set_coeffs(new_size, coeff);
7606 superset_ct->mutable_linear()->mutable_vars()->Truncate(new_size);
7607 superset_ct->mutable_linear()->mutable_coeffs()->Truncate(new_size);
7610 superset_ct->mutable_linear());
7626 void CpModelPresolver::ProcessSetPPC() {
7629 if (context_->
params().presolve_inclusion_work_limit() == 0)
return;
7635 std::vector<int> relevant_constraints;
7636 CompactVectorVector<int> storage;
7638 detector.SetWorkLimit(context_->
params().presolve_inclusion_work_limit());
7642 ActivityBoundHelper amo_in_linear;
7646 std::vector<int> temp_literals;
7647 const int num_constraints = context_->
working_model->constraints_size();
7648 for (
int c = 0; c < num_constraints; ++c) {
7649 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
7650 const auto type =
ct->constraint_case();
7651 if (type == ConstraintProto::kBoolOr ||
7652 type == ConstraintProto::kAtMostOne ||
7653 type == ConstraintProto::kExactlyOne) {
7662 temp_literals.clear();
7663 for (
const int ref :
7664 type == ConstraintProto::kAtMostOne ?
ct->at_most_one().literals()
7665 : type == ConstraintProto::kBoolOr ?
ct->bool_or().literals()
7666 :
ct->exactly_one().literals()) {
7667 temp_literals.push_back(
7672 relevant_constraints.push_back(c);
7673 detector.AddPotentialSet(storage.Add(temp_literals));
7674 }
else if (type == ConstraintProto::kLinear) {
7679 DetectAndProcessAtMostOneInLinear(c,
ct, &amo_in_linear);
7681 if (
ct->constraint_case() != ConstraintProto::kLinear)
continue;
7692 const int size =
ct->linear().vars().size();
7693 if (size <= 2)
continue;
7698 temp_literals.clear();
7699 for (
int i = 0; i < size; ++i) {
7700 const int var =
ct->linear().vars(i);
7703 temp_literals.push_back(
7706 if (temp_literals.size() > 2) {
7708 relevant_constraints.push_back(c);
7709 detector.AddPotentialSuperset(storage.Add(temp_literals));
7714 int64_t num_inclusions = 0;
7715 absl::flat_hash_set<int> tmp_set;
7716 detector.DetectInclusions([&](
int subset,
int superset) {
7718 bool remove_subset =
false;
7719 bool remove_superset =
false;
7720 bool stop_processing_superset =
false;
7721 const int subset_c = relevant_constraints[subset];
7722 const int superset_c = relevant_constraints[superset];
7723 detector.IncreaseWorkDone(storage[subset].size());
7724 detector.IncreaseWorkDone(storage[superset].size());
7725 if (!ProcessSetPPCSubset(subset_c, superset_c, &tmp_set, &remove_subset,
7726 &remove_superset, &stop_processing_superset)) {
7730 if (remove_subset) {
7731 context_->
working_model->mutable_constraints(subset_c)->Clear();
7733 detector.StopProcessingCurrentSubset();
7735 if (remove_superset) {
7736 context_->
working_model->mutable_constraints(superset_c)->Clear();
7738 detector.StopProcessingCurrentSuperset();
7740 if (stop_processing_superset) {
7742 detector.StopProcessingCurrentSuperset();
7747 " #relevant_constraints=", relevant_constraints.size(),
7748 " #num_inclusions=", num_inclusions,
7749 " work=", detector.work_done(),
" time=",
wall_timer.
Get(),
"s");
7752 void CpModelPresolver::DetectIncludedEnforcement() {
7755 if (context_->
params().presolve_inclusion_work_limit() == 0)
return;
7761 std::vector<int> relevant_constraints;
7762 CompactVectorVector<int> storage;
7764 detector.SetWorkLimit(context_->
params().presolve_inclusion_work_limit());
7766 std::vector<int> temp_literals;
7767 const int num_constraints = context_->
working_model->constraints_size();
7768 for (
int c = 0; c < num_constraints; ++c) {
7769 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
7770 if (
ct->enforcement_literal().size() <= 1)
continue;
7773 if (
ct->constraint_case() == ConstraintProto::kBoolAnd) {
7781 temp_literals.clear();
7782 for (
const int ref :
ct->enforcement_literal()) {
7783 temp_literals.push_back(
7788 relevant_constraints.push_back(c);
7792 if (
ct->constraint_case() == ConstraintProto::kBoolAnd) {
7793 detector.AddPotentialSet(storage.Add(temp_literals));
7795 detector.AddPotentialSuperset(storage.Add(temp_literals));
7799 int64_t num_inclusions = 0;
7800 detector.DetectInclusions([&](
int subset,
int superset) {
7802 const int subset_c = relevant_constraints[subset];
7803 const int superset_c = relevant_constraints[superset];
7804 ConstraintProto* subset_ct =
7806 ConstraintProto* superset_ct =
7808 if (subset_ct->constraint_case() != ConstraintProto::kBoolAnd)
return;
7811 for (
const int ref : subset_ct->bool_and().literals()) {
7812 context_->tmp_literal_set.insert(ref);
7818 for (const int ref : superset_ct->enforcement_literal()) {
7819 if (context_->tmp_literal_set.contains(ref)) {
7820 context_->UpdateRuleStats(
"bool_and: filtered enforcement");
7821 } else if (context_->tmp_literal_set.contains(NegatedRef(ref))) {
7822 context_->UpdateRuleStats(
"bool_and: never enforced");
7823 superset_ct->Clear();
7824 context_->UpdateConstraintVariableUsage(superset_c);
7825 detector.StopProcessingCurrentSuperset();
7828 superset_ct->set_enforcement_literal(new_size++, ref);
7831 if (new_size < superset_ct->bool_and().literals().size()) {
7833 superset_ct->mutable_enforcement_literal()->
Truncate(new_size);
7837 if (superset_ct->constraint_case() == ConstraintProto::kBoolAnd) {
7839 for (const int ref : superset_ct->bool_and().literals()) {
7840 if (context_->tmp_literal_set.contains(ref)) {
7841 context_->UpdateRuleStats(
"bool_and: filtered literal");
7842 } else if (context_->tmp_literal_set.contains(NegatedRef(ref))) {
7843 context_->UpdateRuleStats(
"bool_and: must be false");
7844 if (!MarkConstraintAsFalse(superset_ct)) return;
7845 context_->UpdateConstraintVariableUsage(superset_c);
7846 detector.StopProcessingCurrentSuperset();
7849 superset_ct->mutable_bool_and()->set_literals(new_size++, ref);
7852 if (new_size < superset_ct->bool_and().literals().size()) {
7854 superset_ct->mutable_bool_and()->mutable_literals()->
Truncate(new_size);
7858 if (superset_ct->constraint_case() == ConstraintProto::kLinear) {
7859 context_->UpdateRuleStats(
"TODO bool_and enforcement in linear enf");
7863 SOLVER_LOG(logger_,
"[DetectIncludedEnforcement]",
7864 " #relevant_constraints=", relevant_constraints.size(),
7865 " #num_inclusions=", num_inclusions,
7866 " work=", detector.work_done(),
" time=",
wall_timer.
Get(),
"s");
7877 bool CpModelPresolver::ProcessEncodingFromLinear(
7878 const int linear_encoding_ct_index,
7879 const ConstraintProto& at_most_or_exactly_one, int64_t* num_unique_terms,
7880 int64_t* num_multiple_terms) {
7882 bool in_exactly_one =
false;
7883 absl::flat_hash_map<int, int> var_to_ref;
7884 if (at_most_or_exactly_one.constraint_case() == ConstraintProto::kAtMostOne) {
7885 for (
const int ref : at_most_or_exactly_one.at_most_one().literals()) {
7890 CHECK_EQ(at_most_or_exactly_one.constraint_case(),
7891 ConstraintProto::kExactlyOne);
7892 in_exactly_one =
true;
7893 for (
const int ref : at_most_or_exactly_one.exactly_one().literals()) {
7900 const ConstraintProto& linear_encoding =
7901 context_->working_model->constraints(linear_encoding_ct_index);
7902 int64_t rhs = linear_encoding.linear().domain(0);
7904 std::vector<std::pair<int, int64_t>> ref_to_coeffs;
7905 const int num_terms = linear_encoding.linear().vars().size();
7906 for (
int i = 0; i < num_terms; ++i) {
7907 const int ref = linear_encoding.linear().vars(i);
7908 const int64_t coeff = linear_encoding.linear().coeffs(i);
7909 const auto it = var_to_ref.find(
PositiveRef(ref));
7911 if (it == var_to_ref.end()) {
7913 CHECK_EQ(std::abs(coeff), 1);
7914 target_ref = coeff == 1 ? ref :
NegatedRef(ref);
7920 if (it->second == ref) {
7922 ref_to_coeffs.push_back({ref, coeff});
7926 ref_to_coeffs.push_back({
NegatedRef(ref), -coeff});
7930 context_->CanBeUsedAsLiteral(target_ref)) {
7934 context_->UpdateRuleStats(
"encoding: candidate linear is all Boolean now.");
7939 std::vector<int64_t> all_values;
7940 absl::btree_map<int64_t, std::vector<int>> value_to_refs;
7941 for (
const auto& [ref, coeff] : ref_to_coeffs) {
7942 const int64_t
value = rhs - coeff;
7943 all_values.push_back(
value);
7944 value_to_refs[
value].push_back(ref);
7948 for (
const auto& [
var, ref] : var_to_ref) {
7949 all_values.push_back(rhs);
7950 value_to_refs[rhs].push_back(ref);
7952 if (!in_exactly_one) {
7955 all_values.push_back(rhs);
7959 const Domain new_domain = Domain::FromValues(all_values);
7960 bool domain_reduced =
false;
7961 if (!context_->IntersectDomainWith(target_ref, new_domain, &domain_reduced)) {
7964 if (domain_reduced) {
7965 context_->UpdateRuleStats(
"encoding: reduced target domain");
7968 if (context_->CanBeUsedAsLiteral(target_ref)) {
7970 context_->UpdateRuleStats(
"encoding: candidate linear is all Boolean now.");
7975 absl::flat_hash_set<int64_t> value_set;
7976 for (
const int64_t v : context_->DomainOf(target_ref).Values()) {
7977 value_set.insert(v);
7979 for (
const auto& [
value, literals] : value_to_refs) {
7981 if (!value_set.contains(
value)) {
7982 for (
const int lit : literals) {
7983 if (!context_->SetLiteralToFalse(lit))
return false;
7988 if (literals.size() == 1 && (in_exactly_one ||
value != rhs)) {
7991 ++*num_unique_terms;
7992 if (!context_->InsertVarValueEncoding(literals[0], target_ref,
value)) {
7996 ++*num_multiple_terms;
7997 const int associated_lit =
7998 context_->GetOrCreateVarValueEncoding(target_ref,
value);
7999 for (
const int lit : literals) {
8000 context_->AddImplication(lit, associated_lit);
8005 if (in_exactly_one ||
value != rhs) {
8011 context_->working_model->add_constraints()->mutable_bool_or();
8012 for (
const int lit : literals) bool_or->add_literals(lit);
8013 bool_or->add_literals(
NegatedRef(associated_lit));
8019 context_->working_model->mutable_constraints(linear_encoding_ct_index)
8021 context_->UpdateNewConstraintsVariableUsage();
8022 context_->UpdateConstraintVariableUsage(linear_encoding_ct_index);
8026 void CpModelPresolver::DetectDuplicateConstraints() {
8027 if (context_->time_limit()->LimitReached())
return;
8028 if (context_->ModelIsUnsat())
return;
8034 if (context_->working_model->has_objective()) {
8035 if (!context_->CanonicalizeObjective())
return;
8036 context_->WriteObjectiveToProto();
8044 const std::vector<std::pair<int, int>> duplicates =
8046 for (
const auto& [dup, rep] : duplicates) {
8053 : context_->working_model->constraints(rep).constraint_case();
8057 if (type == ConstraintProto::kLinear) {
8059 context_->working_model->constraints(rep).linear());
8061 context_->working_model->constraints(dup).linear());
8062 if (rep_domain != d) {
8063 context_->UpdateRuleStats(
"duplicate: merged rhs of linear constraint");
8064 const Domain rhs = rep_domain.IntersectionWith(d);
8065 if (rhs.IsEmpty()) {
8066 if (!MarkConstraintAsFalse(
8067 context_->working_model->mutable_constraints(rep))) {
8068 SOLVER_LOG(logger_,
"Unsat after merging two linear constraints");
8075 context_->UpdateConstraintVariableUsage(rep);
8079 ->mutable_linear());
8084 context_->UpdateRuleStats(
8085 "duplicate: linear constraint parallel to objective");
8086 const Domain objective_domain =
8089 context_->working_model->constraints(dup).linear());
8090 if (objective_domain != d) {
8091 context_->UpdateRuleStats(
"duplicate: updated objective domain");
8092 const Domain new_domain = objective_domain.IntersectionWith(d);
8093 if (new_domain.IsEmpty()) {
8094 return (
void)context_->NotifyThatModelIsUnsat(
8095 "Constraint parallel to the objective makes the objective domain "
8099 context_->working_model->mutable_objective());
8102 context_->ReadObjectiveFromProto();
8105 context_->working_model->mutable_constraints(dup)->Clear();
8106 context_->UpdateConstraintVariableUsage(dup);
8107 context_->UpdateRuleStats(
"duplicate: removed constraint");
8114 const std::vector<std::pair<int, int>> duplicates_without_enforcement =
8116 for (
const auto& [dup, rep] : duplicates_without_enforcement) {
8117 auto* dup_ct = context_->working_model->mutable_constraints(dup);
8118 auto* rep_ct = context_->working_model->mutable_constraints(rep);
8119 if (rep_ct->constraint_case() == ConstraintProto::CONSTRAINT_NOT_SET) {
8125 if (dup_ct->enforcement_literal().empty() ||
8126 rep_ct->enforcement_literal().empty()) {
8127 context_->UpdateRuleStats(
"duplicate: removed enforced constraint");
8128 rep_ct->mutable_enforcement_literal()->Clear();
8129 context_->UpdateConstraintVariableUsage(rep);
8131 context_->UpdateConstraintVariableUsage(dup);
8138 const int a = rep_ct->enforcement_literal(0);
8139 const int b = dup_ct->enforcement_literal(0);
8140 if (context_->IsFixed(
a) || context_->IsFixed(
b))
continue;
8151 if (context_->VariableWithCostIsUniqueAndRemovable(
a) &&
8152 context_->VariableWithCostIsUniqueAndRemovable(
b)) {
8156 context_->UpdateRuleStats(
"duplicate: dual fixing enforcement.");
8157 if (!context_->SetLiteralToFalse(
a))
return;
8161 context_->UpdateRuleStats(
"duplicate: dual fixing enforcement.");
8162 if (!context_->SetLiteralToFalse(
b))
return;
8168 context_->UpdateRuleStats(
"duplicate: dual equivalence of enforcement");
8169 context_->StoreBooleanEqualityRelation(
a,
b);
8173 if (dup_ct->enforcement_literal().size() == 1 &&
8174 rep_ct->enforcement_literal().size() == 1) {
8176 context_->UpdateConstraintVariableUsage(dup);
8179 context_->UpdateRuleStats(
8180 "TODO duplicate: identical constraint with different enforcements");
8202 bool has_all_diff =
false;
8203 std::vector<std::pair<uint64_t, int>> hashes;
8204 std::vector<std::pair<int, int>> different_vars;
8205 const int num_constraints = context_->working_model->constraints_size();
8206 for (
int c = 0; c < num_constraints; ++c) {
8207 const ConstraintProto&
ct = context_->working_model->constraints(c);
8208 if (
ct.constraint_case() == ConstraintProto::kAllDiff) {
8209 has_all_diff =
true;
8212 if (
ct.constraint_case() != ConstraintProto::kLinear)
continue;
8213 if (
ct.linear().vars().size() == 1)
continue;
8217 if (
ct.linear().vars().size() == 2 &&
ct.enforcement_literal().empty() &&
8218 ct.linear().coeffs(0) == -
ct.linear().coeffs(1) &&
8220 different_vars.push_back({
ct.linear().vars(0),
ct.linear().vars(1)});
8224 if (
ct.enforcement_literal().size() > 1)
continue;
8229 hashes.push_back({
hash, c});
8231 std::sort(hashes.begin(), hashes.end());
8234 while (
next < hashes.size() && hashes[
next].first == hashes[
start].first) {
8237 absl::Span<const std::pair<uint64_t, int>>
range(&hashes[
start],
8239 if (
range.size() <= 1)
continue;
8240 if (
range.size() > 10)
continue;
8242 for (
int i = 0; i <
range.size(); ++i) {
8243 const ConstraintProto& ct1 =
8244 context_->working_model->constraints(
range[i].second);
8245 const int num_terms = ct1.linear().vars().size();
8246 for (
int j = i + 1; j <
range.size(); ++j) {
8247 const ConstraintProto& ct2 =
8248 context_->working_model->constraints(
range[j].second);
8249 if (ct2.linear().vars().size() != num_terms)
continue;
8255 if (absl::MakeSpan(ct1.linear().vars().data(), num_terms) !=
8256 absl::MakeSpan(ct2.linear().vars().data(), num_terms)) {
8259 if (absl::MakeSpan(ct1.linear().coeffs().data(), num_terms) !=
8260 absl::MakeSpan(ct2.linear().coeffs().data(), num_terms)) {
8264 if (ct1.enforcement_literal().empty() &&
8265 ct2.enforcement_literal().empty()) {
8266 (void)context_->NotifyThatModelIsUnsat(
8267 "two incompatible linear constraint");
8270 if (ct1.enforcement_literal().empty()) {
8271 context_->UpdateRuleStats(
8272 "incompatible linear: set enforcement to false");
8273 if (!context_->SetLiteralToFalse(ct2.enforcement_literal(0))) {
8278 if (ct2.enforcement_literal().empty()) {
8279 context_->UpdateRuleStats(
8280 "incompatible linear: set enforcement to false");
8281 if (!context_->SetLiteralToFalse(ct1.enforcement_literal(0))) {
8288 if (ct1.linear().vars().size() == 2 &&
8289 ct1.linear().coeffs(0) == -ct1.linear().coeffs(1) &&
8292 ct1.enforcement_literal(0) ==
8294 different_vars.push_back(
8295 {ct1.linear().vars(0), ct1.linear().vars(1)});
8298 context_->UpdateRuleStats(
"incompatible linear: add implication");
8299 context_->AddImplication(ct1.enforcement_literal(0),
8317 if (context_->params().infer_all_diffs() && !has_all_diff &&
8318 different_vars.size() > 2) {
8322 std::vector<std::vector<Literal>> cliques;
8323 absl::flat_hash_set<int> used_var;
8326 const int num_variables = context_->working_model->variables().size();
8327 local_model.GetOrCreate<Trail>()->Resize(num_variables);
8328 auto* graph = local_model.GetOrCreate<BinaryImplicationGraph>();
8329 graph->Resize(num_variables);
8330 for (
const auto [var1, var2] : different_vars) {
8334 (void)context_->NotifyThatModelIsUnsat(
"x != y with x == y");
8339 CHECK(graph->AddAtMostOne({Literal(BooleanVariable(var1), true),
8340 Literal(BooleanVariable(var2), true)}));
8341 if (!used_var.contains(var1)) {
8342 used_var.insert(var1);
8343 cliques.push_back({Literal(BooleanVariable(var1),
true),
8344 Literal(BooleanVariable(var2),
true)});
8346 if (!used_var.contains(var2)) {
8347 used_var.insert(var2);
8348 cliques.push_back({Literal(BooleanVariable(var1),
true),
8349 Literal(BooleanVariable(var2),
true)});
8352 CHECK(graph->DetectEquivalences());
8353 graph->TransformIntoMaxCliques(&cliques, 1e8);
8355 int num_cliques = 0;
8356 int64_t cumulative_size = 0;
8357 for (
const std::vector<Literal>& clique : cliques) {
8358 if (clique.size() <= 2)
continue;
8361 cumulative_size += clique.size();
8362 context_->UpdateRuleStats(
"all_diff: inferred from x != y constraints");
8364 context_->working_model->add_constraints()->mutable_all_diff();
8365 for (
const Literal l : clique) {
8366 auto* expr = new_ct->add_exprs();
8367 expr->add_vars(l.Variable().value());
8368 expr->add_coeffs(1);
8372 " #different=", different_vars.size(),
" #cliques=", num_cliques,
8373 " #size=", cumulative_size,
" time=", local_time.
Get(),
"s");
8376 context_->UpdateNewConstraintsVariableUsage();
8377 SOLVER_LOG(logger_,
"[DetectDuplicateConstraints]",
8378 " #duplicates=", duplicates.size(),
8379 " #without_enforcements=", duplicates_without_enforcement.size(),
8383 void CpModelPresolver::DetectDominatedLinearConstraints() {
8384 if (context_->time_limit()->LimitReached())
return;
8385 if (context_->ModelIsUnsat())
return;
8386 if (context_->params().presolve_inclusion_work_limit() == 0)
return;
8394 detector.SetWorkLimit(context_->params().presolve_inclusion_work_limit());
8398 std::vector<int> constraint_indices_to_clean;
8402 absl::flat_hash_map<int, Domain> cached_expr_domain;
8404 const int num_constraints = context_->working_model->constraints().size();
8405 for (
int c = 0; c < num_constraints; ++c) {
8406 const ConstraintProto&
ct = context_->working_model->constraints(c);
8407 if (
ct.constraint_case() != ConstraintProto::kLinear)
continue;
8410 if (!
ct.enforcement_literal().empty())
continue;
8412 if (!LinearConstraintIsClean(
ct.linear())) {
8419 DCHECK_LT(c, context_->ConstraintToVarsGraph().size());
8420 detector.AddPotentialSet(c);
8422 const auto [min_activity, max_activity] =
8423 context_->ComputeMinMaxActivity(
ct.linear());
8424 cached_expr_domain[c] = Domain(min_activity, max_activity);
8427 int64_t num_inclusions = 0;
8428 absl::flat_hash_map<int, int64_t> coeff_map;
8429 detector.DetectInclusions([&](
int subset_c,
int superset_c) {
8433 const ConstraintProto subset_ct =
8434 context_->working_model->constraints(subset_c);
8435 const LinearConstraintProto& subset_lin = subset_ct.linear();
8437 detector.IncreaseWorkDone(subset_lin.vars().size());
8438 for (
int i = 0; i < subset_lin.vars().size(); ++i) {
8439 coeff_map[subset_lin.vars(i)] = subset_lin.coeffs(i);
8445 bool perfect_match =
true;
8452 const ConstraintProto& superset_ct =
8453 context_->working_model->constraints(superset_c);
8454 const LinearConstraintProto& superset_lin = superset_ct.linear();
8455 int64_t diff_min_activity = 0;
8456 int64_t diff_max_activity = 0;
8457 detector.IncreaseWorkDone(superset_lin.vars().size());
8458 for (
int i = 0; i < superset_lin.vars().size(); ++i) {
8459 const int var = superset_lin.vars(i);
8460 int64_t coeff = superset_lin.coeffs(i);
8461 const auto it = coeff_map.find(
var);
8462 if (it != coeff_map.end()) {
8463 const int64_t subset_coeff = it->second;
8464 if (perfect_match) {
8465 if (coeff % subset_coeff == 0) {
8466 const int64_t div = coeff / subset_coeff;
8470 } else if (factor != div) {
8471 perfect_match = false;
8474 perfect_match = false;
8479 coeff -= subset_coeff;
8481 if (coeff == 0)
continue;
8483 diff_min_activity += coeff * context_->MinOf(
var);
8484 diff_max_activity += coeff * context_->MaxOf(
var);
8486 diff_min_activity += coeff * context_->MaxOf(
var);
8487 diff_max_activity += coeff * context_->MinOf(
var);
8491 const Domain diff_domain(diff_min_activity, diff_max_activity);
8497 const Domain implied_superset_domain =
8498 subset_ct_domain.AdditionWith(diff_domain)
8499 .IntersectionWith(cached_expr_domain[superset_c]);
8500 if (implied_superset_domain.IsIncludedIn(superset_ct_domain)) {
8501 context_->UpdateRuleStats(
8502 "linear inclusion: redundant containing constraint");
8503 context_->working_model->mutable_constraints(superset_c)->Clear();
8504 constraint_indices_to_clean.push_back(superset_c);
8505 detector.StopProcessingCurrentSuperset();
8510 const Domain implied_subset_domain =
8511 superset_ct_domain.AdditionWith(diff_domain.Negation())
8512 .IntersectionWith(cached_expr_domain[subset_c]);
8513 if (implied_subset_domain.IsIncludedIn(subset_ct_domain)) {
8514 context_->UpdateRuleStats(
8515 "linear inclusion: redundant included constraint");
8516 context_->working_model->mutable_constraints(subset_c)->Clear();
8517 constraint_indices_to_clean.push_back(subset_c);
8518 detector.StopProcessingCurrentSubset();
8525 if (perfect_match) {
8526 CHECK_NE(factor, 0);
8527 if (subset_ct_domain.IsFixed()) {
8534 context_->UpdateRuleStats(
"linear inclusion: subset is equality");
8536 auto* mutable_linear =
8537 context_->working_model->mutable_constraints(superset_c)
8539 for (
int i = 0; i < mutable_linear->vars().size(); ++i) {
8540 const int var = mutable_linear->vars(i);
8541 const int64_t coeff = mutable_linear->coeffs(i);
8542 const auto it = coeff_map.find(
var);
8543 if (it != coeff_map.end()) {
8544 CHECK_EQ(factor * it->second, coeff);
8547 mutable_linear->set_vars(new_size,
var);
8548 mutable_linear->set_coeffs(new_size, coeff);
8551 mutable_linear->mutable_vars()->Truncate(new_size);
8552 mutable_linear->mutable_coeffs()->Truncate(new_size);
8554 subset_ct_domain.MultiplicationBy(-factor)),
8556 constraint_indices_to_clean.push_back(superset_c);
8557 detector.StopProcessingCurrentSuperset();
8564 auto* mutable_linear = temp_ct_.mutable_linear();
8565 for (
int i = 0; i < superset_lin.vars().size(); ++i) {
8566 const int var = superset_lin.vars(i);
8567 const int64_t coeff = superset_lin.coeffs(i);
8568 const auto it = coeff_map.find(
var);
8569 if (it != coeff_map.end())
continue;
8570 mutable_linear->add_vars(
var);
8571 mutable_linear->add_coeffs(coeff);
8574 subset_ct_domain.MultiplicationBy(-factor)),
8576 PropagateDomainsInLinear(-1, &temp_ct_);
8577 if (context_->ModelIsUnsat()) detector.Stop();
8579 if (superset_ct_domain.IsFixed()) {
8580 if (subset_lin.vars().size() + 1 == superset_lin.vars().size()) {
8583 context_->UpdateRuleStats(
8584 "linear inclusion: subset + singleton is equality");
8585 context_->working_model->mutable_constraints(subset_c)->Clear();
8586 constraint_indices_to_clean.push_back(subset_c);
8587 detector.StopProcessingCurrentSubset();
8592 context_->UpdateRuleStats(
8593 "TODO linear inclusion: superset is equality");
8598 for (
const int c : constraint_indices_to_clean) {
8599 context_->UpdateConstraintVariableUsage(c);
8602 SOLVER_LOG(logger_,
"[DetectDominatedLinearConstraints]",
8603 " #relevant_constraints=", detector.num_potential_supersets(),
8604 " #work_done=", detector.work_done(),
8605 " #num_inclusions=", num_inclusions,
8606 " #num_redundant=", constraint_indices_to_clean.size(),
8617 void CpModelPresolver::FindBigLinearOverlap() {
8618 if (context_->time_limit()->LimitReached())
return;
8619 if (context_->ModelIsUnsat())
return;
8620 if (context_->params().presolve_inclusion_work_limit() == 0)
return;
8625 const int num_constraints = context_->working_model->constraints_size();
8626 std::vector<std::pair<int, int>> to_sort;
8627 for (
int c = 0; c < num_constraints; ++c) {
8628 const ConstraintProto&
ct = context_->working_model->constraints(c);
8629 if (
ct.constraint_case() != ConstraintProto::kLinear)
continue;
8630 const int size =
ct.linear().vars().size();
8631 if (size < 5)
continue;
8632 to_sort.push_back({-size, c});
8634 std::sort(to_sort.begin(), to_sort.end());
8636 std::vector<int> sorted_linear;
8637 for (
int i = 0; i < to_sort.size(); ++i) {
8638 sorted_linear.push_back(to_sort[i].second);
8642 double work_done = 0;
8643 const double work_limit = 1e9;
8645 int64_t num_blocks = 0;
8646 int64_t nz_reduction = 0;
8647 absl::flat_hash_map<int, int64_t> coeff_map;
8648 absl::flat_hash_set<int> processed;
8649 for (
int i = 0; i < sorted_linear.size(); ++i) {
8650 const int c = sorted_linear[i];
8651 if (c < 0)
continue;
8652 if (work_done > work_limit)
break;
8656 const ConstraintProto&
ct = context_->working_model->constraints(c);
8657 const int num_terms =
ct.linear().vars().size();
8658 work_done += num_terms;
8659 for (
int k = 0; k < num_terms; ++k) {
8660 coeff_map[
ct.linear().vars(k)] =
ct.linear().coeffs(k);
8669 std::vector<int> block = {i};
8670 std::vector<std::pair<int, int64_t>> common_part;
8672 for (
int j = 0; j < sorted_linear.size(); ++j) {
8673 if (i == j)
continue;
8674 const int other_c = sorted_linear[j];
8675 if (other_c < 0)
continue;
8676 const ConstraintProto&
ct = context_->working_model->constraints(other_c);
8679 const int num_terms =
ct.linear().vars().size();
8680 const int best_saved_nz = block.size() * (num_terms - 1) - 2;
8681 if (best_saved_nz <= saved_nz)
break;
8683 work_done += num_terms;
8684 common_part.clear();
8685 for (
int k = 0; k < num_terms; ++k) {
8686 const auto it = coeff_map.find(
ct.linear().vars(k));
8687 if (it != coeff_map.end() && it->second ==
ct.linear().coeffs(k)) {
8688 common_part.push_back({
ct.linear().vars(k),
ct.linear().coeffs(k)});
8697 const int64_t new_saved_nz = block.size() * (common_part.size() - 1) - 2;
8698 if (new_saved_nz > saved_nz) {
8699 saved_nz = new_saved_nz;
8702 for (
const auto [
var, coeff] : common_part) {
8703 coeff_map[
var] = coeff;
8716 if (block.size() > 1) {
8717 context_->UpdateRuleStats(
"linear matrix: common rectangle");
8719 nz_reduction += saved_nz;
8722 int64_t min_activity = 0;
8723 int64_t max_activity = 0;
8724 common_part.clear();
8725 for (
const auto [
var, coeff] : coeff_map) {
8726 common_part.push_back({
var, coeff});
8727 gcd = std::gcd(gcd, std::abs(coeff));
8729 min_activity += coeff * context_->MinOf(
var);
8730 max_activity += coeff * context_->MaxOf(
var);
8732 min_activity += coeff * context_->MaxOf(
var);
8733 max_activity += coeff * context_->MinOf(
var);
8739 context_->NewIntVar(Domain(min_activity / gcd, max_activity / gcd));
8743 context_->working_model->add_constraints()->mutable_linear();
8744 std::sort(common_part.begin(), common_part.end());
8745 for (
const auto [
var, coeff] : common_part) {
8746 new_linear->add_vars(
var);
8747 new_linear->add_coeffs(coeff / gcd);
8749 new_linear->add_vars(new_var);
8750 new_linear->add_coeffs(-1);
8751 new_linear->add_domain(0);
8752 new_linear->add_domain(0);
8753 context_->UpdateNewConstraintsVariableUsage();
8756 for (
const int j : block) {
8757 const int c = sorted_linear[j];
8758 sorted_linear[j] = -1;
8759 auto* mutable_linear =
8760 context_->working_model->mutable_constraints(c)->mutable_linear();
8761 const int num_terms = mutable_linear->vars().size();
8763 for (
int k = 0; k < num_terms; ++k) {
8764 if (coeff_map.contains(mutable_linear->vars(k)))
continue;
8765 mutable_linear->set_vars(new_size, mutable_linear->vars(k));
8766 mutable_linear->set_coeffs(new_size, mutable_linear->coeffs(k));
8769 CHECK_EQ(new_size, num_terms - common_part.size());
8770 mutable_linear->mutable_vars()->Truncate(new_size);
8771 mutable_linear->mutable_coeffs()->Truncate(new_size);
8772 mutable_linear->add_vars(new_var);
8773 mutable_linear->add_coeffs(gcd);
8775 context_->UpdateConstraintVariableUsage(c);
8780 DCHECK(context_->ConstraintVariableUsageIsConsistent());
8781 SOLVER_LOG(logger_,
"[FindBigLinearOverlap]",
" #blocks=", num_blocks,
8782 " #saved_nz=", nz_reduction,
" #linears=", sorted_linear.size(),
8783 " #work_done=", work_done,
"/", work_limit,
8787 void CpModelPresolver::ExtractEncodingFromLinear() {
8788 if (context_->time_limit()->LimitReached())
return;
8789 if (context_->ModelIsUnsat())
return;
8790 if (context_->params().presolve_inclusion_work_limit() == 0)
return;
8796 std::vector<int> relevant_constraints;
8797 CompactVectorVector<int> storage;
8799 detector.SetWorkLimit(context_->params().presolve_inclusion_work_limit());
8805 std::vector<int> vars;
8806 const int num_constraints = context_->working_model->constraints().size();
8807 for (
int c = 0; c < num_constraints; ++c) {
8808 const ConstraintProto&
ct = context_->working_model->constraints(c);
8809 switch (
ct.constraint_case()) {
8810 case ConstraintProto::kAtMostOne: {
8812 for (
const int ref :
ct.at_most_one().literals()) {
8815 relevant_constraints.push_back(c);
8816 detector.AddPotentialSuperset(storage.Add(vars));
8819 case ConstraintProto::kExactlyOne: {
8821 for (
const int ref :
ct.exactly_one().literals()) {
8824 relevant_constraints.push_back(c);
8825 detector.AddPotentialSuperset(storage.Add(vars));
8828 case ConstraintProto::kLinear: {
8830 if (!
ct.enforcement_literal().empty())
continue;
8831 if (
ct.linear().domain().size() != 2)
continue;
8832 if (
ct.linear().domain(0) !=
ct.linear().domain(1))
continue;
8836 bool is_candidate =
true;
8837 int num_integers = 0;
8839 const int num_terms =
ct.linear().vars().size();
8840 for (
int i = 0; i < num_terms; ++i) {
8841 const int ref =
ct.linear().vars(i);
8842 if (context_->CanBeUsedAsLiteral(ref)) {
8846 if (std::abs(
ct.linear().coeffs(i)) != 1) {
8847 is_candidate =
false;
8850 if (num_integers == 2) {
8851 is_candidate =
false;
8859 if (is_candidate && num_integers == 1 && vars.size() > 1) {
8860 relevant_constraints.push_back(c);
8861 detector.AddPotentialSubset(storage.Add(vars));
8871 int64_t num_exactly_one_encodings = 0;
8872 int64_t num_at_most_one_encodings = 0;
8873 int64_t num_literals = 0;
8874 int64_t num_unique_terms = 0;
8875 int64_t num_multiple_terms = 0;
8877 detector.DetectInclusions([&](
int subset,
int superset) {
8878 const int subset_c = relevant_constraints[subset];
8879 const int superset_c = relevant_constraints[superset];
8880 const ConstraintProto& superset_ct =
8881 context_->working_model->constraints(superset_c);
8882 if (superset_ct.constraint_case() == ConstraintProto::kAtMostOne) {
8883 ++num_at_most_one_encodings;
8885 ++num_exactly_one_encodings;
8887 num_literals += storage[subset].size();
8888 context_->UpdateRuleStats(
"encoding: extracted from linear");
8890 if (!ProcessEncodingFromLinear(subset_c, superset_ct, &num_unique_terms,
8891 &num_multiple_terms)) {
8895 detector.StopProcessingCurrentSubset();
8898 SOLVER_LOG(logger_,
"[ExtractEncodingFromLinear]",
8899 " #potential_supersets=", detector.num_potential_supersets(),
8900 " #potential_subsets=", detector.num_potential_subsets(),
8901 " #at_most_one_encodings=", num_at_most_one_encodings,
8902 " #exactly_one_encodings=", num_exactly_one_encodings,
8903 " #unique_terms=", num_unique_terms,
8904 " #multiple_terms=", num_multiple_terms,
8905 " #literals=", num_literals,
" time=",
wall_timer.
Get(),
"s");
8919 void CpModelPresolver::LookAtVariableWithDegreeTwo(
int var) {
8921 CHECK(context_->ConstraintVariableGraphIsUpToDate());
8922 if (context_->ModelIsUnsat())
return;
8923 if (context_->keep_all_feasible_solutions)
return;
8924 if (context_->IsFixed(
var))
return;
8925 if (!context_->ModelIsExpanded())
return;
8926 if (!context_->CanBeUsedAsLiteral(
var))
return;
8933 if (context_->VarToConstraints(
var).size() != 2)
return;
8937 Domain union_of_domain;
8938 int num_positive = 0;
8939 std::vector<int> constraint_indices_to_remove;
8940 for (
const int c : context_->VarToConstraints(
var)) {
8945 constraint_indices_to_remove.push_back(c);
8946 const ConstraintProto&
ct = context_->working_model->constraints(c);
8947 if (
ct.enforcement_literal().size() != 1 ||
8949 ct.constraint_case() != ConstraintProto::kLinear ||
8950 ct.linear().vars().size() != 1) {
8954 if (
ct.enforcement_literal(0) ==
var) ++num_positive;
8955 if (ct_var != -1 &&
PositiveRef(
ct.linear().vars(0)) != ct_var) {
8960 union_of_domain = union_of_domain.UnionWith(
8963 ?
ct.linear().coeffs(0)
8964 : -
ct.linear().coeffs(0)));
8967 if (num_positive != 1)
return;
8968 if (!context_->IntersectDomainWith(ct_var, union_of_domain))
return;
8970 context_->UpdateRuleStats(
"variables: removable enforcement literal");
8971 for (
const int c : constraint_indices_to_remove) {
8972 *context_->mapping_model->add_constraints() =
8973 context_->working_model->constraints(c);
8974 context_->mapping_model
8975 ->mutable_constraints(context_->mapping_model->constraints().size() - 1)
8976 ->set_name(
"removable enforcement literal");
8977 context_->working_model->mutable_constraints(c)->Clear();
8978 context_->UpdateConstraintVariableUsage(c);
8980 context_->MarkVariableAsRemoved(
var);
8985 absl::Span<const int> AtMostOneOrExactlyOneLiterals(
const ConstraintProto&
ct) {
8986 if (
ct.constraint_case() == ConstraintProto::kAtMostOne) {
8987 return {
ct.at_most_one().literals()};
8989 return {
ct.exactly_one().literals()};
8995 void CpModelPresolver::ProcessVariableInTwoAtMostOrExactlyOne(
int var) {
8997 DCHECK(context_->ConstraintVariableGraphIsUpToDate());
8998 if (context_->ModelIsUnsat())
return;
8999 if (context_->keep_all_feasible_solutions)
return;
9000 if (context_->IsFixed(
var))
return;
9001 if (context_->VariableWasRemoved(
var))
return;
9002 if (!context_->ModelIsExpanded())
return;
9003 if (!context_->CanBeUsedAsLiteral(
var))
return;
9007 if (context_->VarToConstraints(
var).size() != 3)
return;
9008 cost = context_->ObjectiveMap().at(
var);
9010 if (context_->VarToConstraints(
var).size() != 2)
return;
9018 for (
const int c : context_->VarToConstraints(
var)) {
9019 if (c < 0)
continue;
9020 const ConstraintProto&
ct = context_->working_model->constraints(c);
9021 if (
ct.constraint_case() != ConstraintProto::kAtMostOne &&
9022 ct.constraint_case() != ConstraintProto::kExactlyOne) {
9033 if (c1 == -1 || c2 == -1)
return;
9046 context_->tmp_literals.clear();
9048 const ConstraintProto& ct1 = context_->working_model->constraints(c1);
9049 if (AtMostOneOrExactlyOneLiterals(ct1).size() <= 1)
return;
9050 for (
const int lit : AtMostOneOrExactlyOneLiterals(ct1)) {
9054 context_->tmp_literals.push_back(lit);
9058 const ConstraintProto& ct2 = context_->working_model->constraints(c2);
9059 if (AtMostOneOrExactlyOneLiterals(ct2).size() <= 1)
return;
9060 for (
const int lit : AtMostOneOrExactlyOneLiterals(ct2)) {
9064 context_->tmp_literals.push_back(lit);
9073 int64_t cost_shift = 0;
9074 absl::Span<const int> literals;
9075 if (ct1.constraint_case() == ConstraintProto::kExactlyOne) {
9077 literals = ct1.exactly_one().literals();
9078 }
else if (ct2.constraint_case() == ConstraintProto::kExactlyOne) {
9080 literals = ct2.exactly_one().literals();
9084 if (context_->keep_all_feasible_solutions)
return;
9087 literals = ct1.at_most_one().literals();
9090 literals = ct2.at_most_one().literals();
9094 if (!context_->ShiftCostInExactlyOne(literals, cost_shift))
return;
9095 DCHECK(!context_->ObjectiveMap().contains(
var));
9096 context_->mapping_model->add_constraints()
9097 ->mutable_exactly_one()
9098 ->mutable_literals()
9099 ->Assign(literals.begin(), literals.end());
9102 const int new_ct_index = context_->working_model->constraints().size();
9103 ConstraintProto* new_ct = context_->working_model->add_constraints();
9104 if (ct1.constraint_case() == ConstraintProto::kExactlyOne &&
9105 ct2.constraint_case() == ConstraintProto::kExactlyOne) {
9106 for (
const int lit : context_->tmp_literals) {
9107 new_ct->mutable_exactly_one()->add_literals(lit);
9112 for (
const int lit : context_->tmp_literals) {
9113 new_ct->mutable_at_most_one()->add_literals(lit);
9117 context_->UpdateNewConstraintsVariableUsage();
9118 context_->working_model->mutable_constraints(c1)->Clear();
9119 context_->UpdateConstraintVariableUsage(c1);
9120 context_->working_model->mutable_constraints(c2)->Clear();
9121 context_->UpdateConstraintVariableUsage(c2);
9123 context_->UpdateRuleStats(
9124 "at_most_one: resolved two constraints with opposite literal");
9125 context_->MarkVariableAsRemoved(
var);
9130 DCHECK_NE(new_ct->constraint_case(), ConstraintProto::CONSTRAINT_NOT_SET);
9131 if (PresolveAtMostOrExactlyOne(new_ct)) {
9132 context_->UpdateConstraintVariableUsage(new_ct_index);
9144 void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(
int var) {
9145 if (context_->ModelIsUnsat())
return;
9146 if (context_->keep_all_feasible_solutions)
return;
9147 if (context_->IsFixed(
var))
return;
9148 if (context_->VariableWasRemoved(
var))
return;
9149 if (context_->CanBeUsedAsLiteral(
var))
return;
9150 if (!context_->VariableIsOnlyUsedInEncodingAndMaybeInObjective(
var))
return;
9151 if (context_->params().search_branching() == SatParameters::FIXED_SEARCH) {
9165 if (context_->VariableWithCostIsUniqueAndRemovable(
var)) {
9167 for (
const int c : context_->VarToConstraints(
var)) {
9168 if (c < 0)
continue;
9169 CHECK_EQ(unique_c, -1);
9172 CHECK_NE(unique_c, -1);
9173 const ConstraintProto&
ct = context_->working_model->constraints(unique_c);
9174 const int64_t
cost = context_->ObjectiveCoeff(
var);
9175 if (
ct.linear().vars(0) ==
var) {
9179 if (implied.IsEmpty()) {
9180 if (!MarkConstraintAsFalse(
9181 context_->working_model->mutable_constraints(unique_c))) {
9184 context_->UpdateConstraintVariableUsage(unique_c);
9188 int64_t value1, value2;
9190 context_->UpdateRuleStats(
"variables: fix singleton var in linear1");
9191 return (
void)context_->IntersectDomainWith(
var, Domain(implied.Min()));
9192 }
else if (
cost > 0) {
9193 value1 = context_->MinOf(
var);
9194 value2 = implied.
Min();
9196 value1 = context_->MaxOf(
var);
9197 value2 = implied.Max();
9202 context_->UpdateRuleStats(
"variables: reduced domain to two values");
9203 return (
void)context_->IntersectDomainWith(
9204 var, Domain::FromValues({value1, value2}));
9214 absl::flat_hash_set<int64_t> values_set;
9215 absl::flat_hash_map<int64_t, std::vector<int>> value_to_equal_literals;
9216 absl::flat_hash_map<int64_t, std::vector<int>> value_to_not_equal_literals;
9218 for (
const int c : context_->VarToConstraints(
var)) {
9219 if (c < 0)
continue;
9220 const ConstraintProto&
ct = context_->working_model->constraints(c);
9221 CHECK_EQ(
ct.constraint_case(), ConstraintProto::kLinear);
9222 CHECK_EQ(
ct.linear().vars().size(), 1);
9223 int64_t coeff =
ct.linear().coeffs(0);
9224 if (std::abs(coeff) != 1 ||
ct.enforcement_literal().size() != 1) {
9230 const Domain var_domain = context_->DomainOf(
var);
9234 if (rhs.IsEmpty()) {
9235 if (!context_->SetLiteralToFalse(
ct.enforcement_literal(0))) {
9239 }
else if (rhs.IsFixed()) {
9240 if (!var_domain.Contains(rhs.FixedValue())) {
9241 if (!context_->SetLiteralToFalse(
ct.enforcement_literal(0))) {
9245 values_set.insert(rhs.FixedValue());
9246 value_to_equal_literals[rhs.FixedValue()].push_back(
9247 ct.enforcement_literal(0));
9251 if (complement.IsEmpty()) {
9256 if (complement.IsFixed()) {
9257 if (var_domain.Contains(complement.FixedValue())) {
9258 values_set.insert(complement.FixedValue());
9259 value_to_not_equal_literals[complement.FixedValue()].push_back(
9260 ct.enforcement_literal(0));
9269 context_->UpdateRuleStats(
"TODO variables: only used in linear1.");
9271 }
else if (value_to_not_equal_literals.empty() &&
9272 value_to_equal_literals.empty()) {
9279 std::vector<int64_t> encoded_values(values_set.begin(), values_set.end());
9280 std::sort(encoded_values.begin(), encoded_values.end());
9281 CHECK(!encoded_values.empty());
9282 const bool is_fully_encoded =
9283 encoded_values.size() == context_->DomainOf(
var).Size();
9288 for (
const int64_t v : encoded_values) {
9289 const int encoding_lit = context_->GetOrCreateVarValueEncoding(
var, v);
9290 const auto eq_it = value_to_equal_literals.find(v);
9291 if (eq_it != value_to_equal_literals.end()) {
9292 for (
const int lit : eq_it->second) {
9293 context_->AddImplication(lit, encoding_lit);
9296 const auto neq_it = value_to_not_equal_literals.find(v);
9297 if (neq_it != value_to_not_equal_literals.end()) {
9298 for (
const int lit : neq_it->second) {
9299 context_->AddImplication(lit,
NegatedRef(encoding_lit));
9303 context_->UpdateNewConstraintsVariableUsage();
9306 Domain other_values;
9307 if (!is_fully_encoded) {
9308 other_values = context_->DomainOf(
var).IntersectionWith(
9309 Domain::FromValues(encoded_values).Complement());
9316 const int64_t obj_coeff = context_->ObjectiveMap().at(
var);
9317 if (is_fully_encoded) {
9321 obj_coeff > 0 ? encoded_values.front() : encoded_values.back();
9325 if (context_->ObjectiveDomainIsConstraining() &&
9326 !other_values.IsFixed()) {
9337 Domain(obj_coeff > 0 ? other_values.Min() : other_values.Max());
9338 min_value = other_values.FixedValue();
9343 int64_t accumulated = std::abs(min_value);
9344 for (
const int64_t
value : encoded_values) {
9347 context_->UpdateRuleStats(
9348 "TODO variables: only used in objective and in encoding");
9353 ConstraintProto encoding_ct;
9354 LinearConstraintProto* linear = encoding_ct.mutable_linear();
9355 const int64_t coeff_in_equality = -1;
9356 linear->add_vars(
var);
9357 linear->add_coeffs(coeff_in_equality);
9359 linear->add_domain(-min_value);
9360 linear->add_domain(-min_value);
9361 for (
const int64_t
value : encoded_values) {
9362 if (
value == min_value)
continue;
9363 const int enf = context_->GetOrCreateVarValueEncoding(
var,
value);
9364 const int64_t coeff =
value - min_value;
9366 linear->add_vars(enf);
9367 linear->add_coeffs(coeff);
9370 linear->set_domain(0, encoding_ct.linear().domain(0) - coeff);
9371 linear->set_domain(1, encoding_ct.linear().domain(1) - coeff);
9373 linear->add_coeffs(-coeff);
9376 if (!context_->SubstituteVariableInObjective(
var, coeff_in_equality,
9378 context_->UpdateRuleStats(
9379 "TODO variables: only used in objective and in encoding");
9382 context_->UpdateRuleStats(
9383 "variables: only used in objective and in encoding");
9385 context_->UpdateRuleStats(
"variables: only used in encoding");
9389 auto copy = context_->VarToConstraints(
var);
9390 for (
const int c : copy) {
9391 if (c < 0)
continue;
9392 context_->working_model->mutable_constraints(c)->Clear();
9393 context_->UpdateConstraintVariableUsage(c);
9398 for (
const int64_t
value : encoded_values) {
9399 const int enf = context_->GetOrCreateVarValueEncoding(
var,
value);
9400 ConstraintProto*
ct = context_->mapping_model->add_constraints();
9401 ct->add_enforcement_literal(enf);
9402 ct->mutable_linear()->add_vars(
var);
9403 ct->mutable_linear()->add_coeffs(1);
9404 ct->mutable_linear()->add_domain(
value);
9405 ct->mutable_linear()->add_domain(
value);
9409 ConstraintProto* new_ct = context_->working_model->add_constraints();
9410 if (is_fully_encoded) {
9412 for (
const int64_t
value : encoded_values) {
9413 new_ct->mutable_exactly_one()->add_literals(
9414 context_->GetOrCreateVarValueEncoding(
var,
value));
9416 PresolveExactlyOne(new_ct);
9419 ConstraintProto* mapping_ct = context_->mapping_model->add_constraints();
9420 mapping_ct->mutable_linear()->add_vars(
var);
9421 mapping_ct->mutable_linear()->add_coeffs(1);
9424 for (
const int64_t
value : encoded_values) {
9425 const int literal = context_->GetOrCreateVarValueEncoding(
var,
value);
9427 new_ct->mutable_at_most_one()->add_literals(
literal);
9429 PresolveAtMostOne(new_ct);
9432 context_->UpdateNewConstraintsVariableUsage();
9433 context_->MarkVariableAsRemoved(
var);
9436 void CpModelPresolver::TryToSimplifyDomain(
int var) {
9438 CHECK(context_->ConstraintVariableGraphIsUpToDate());
9439 if (context_->ModelIsUnsat())
return;
9440 if (context_->IsFixed(
var))
return;
9441 if (context_->VariableWasRemoved(
var))
return;
9442 if (context_->VariableIsNotUsedAnymore(
var))
return;
9444 const AffineRelation::Relation r = context_->GetAffineRelation(
var);
9445 if (r.representative !=
var)
return;
9448 const Domain& domain = context_->DomainOf(
var);
9451 if (domain.Size() == 2 && (domain.Min() != 0 || domain.Max() != 1)) {
9452 context_->CanonicalizeDomainOfSizeTwo(
var);
9456 if (domain.NumIntervals() != domain.Size())
return;
9458 const int64_t var_min = domain.Min();
9459 int64_t gcd = domain[1].start - var_min;
9461 const ClosedInterval& i = domain[
index];
9462 DCHECK_EQ(i.start, i.end);
9463 const int64_t shifted_value = i.start - var_min;
9464 DCHECK_GT(shifted_value, 0);
9466 gcd = MathUtil::GCD64(gcd, shifted_value);
9467 if (gcd == 1)
break;
9469 if (gcd == 1)
return;
9472 context_->CanonicalizeAffineVariable(
var, 1, gcd, var_min);
9476 void CpModelPresolver::EncodeAllAffineRelations() {
9477 int64_t num_added = 0;
9478 for (
int var = 0;
var < context_->working_model->variables_size(); ++
var) {
9479 if (context_->IsFixed(
var))
continue;
9481 const AffineRelation::Relation r = context_->GetAffineRelation(
var);
9482 if (r.representative ==
var)
continue;
9484 if (!context_->keep_all_feasible_solutions) {
9488 if (context_->VariableIsNotUsedAnymore(
var))
continue;
9489 if (!PresolveAffineRelationIfAny(
var))
break;
9490 if (context_->VariableIsNotUsedAnymore(
var))
continue;
9491 if (context_->IsFixed(
var))
continue;
9495 ConstraintProto*
ct = context_->working_model->add_constraints();
9496 auto* arg =
ct->mutable_linear();
9499 arg->add_vars(r.representative);
9500 arg->add_coeffs(-r.coeff);
9501 arg->add_domain(r.offset);
9502 arg->add_domain(r.offset);
9503 context_->UpdateNewConstraintsVariableUsage();
9508 context_->RemoveAllVariablesFromAffineRelationConstraint();
9510 if (num_added > 0) {
9511 SOLVER_LOG(logger_, num_added,
" affine relations still in the model.");
9516 bool CpModelPresolver::PresolveAffineRelationIfAny(
int var) {
9517 const AffineRelation::Relation r = context_->GetAffineRelation(
var);
9518 if (r.representative ==
var)
return true;
9521 if (!context_->PropagateAffineRelation(
var))
return false;
9527 if (context_->IsFixed(
var))
return true;
9529 DCHECK(!context_->VariableIsNotUsedAnymore(r.representative));
9534 if (context_->VariableIsUniqueAndRemovable(
var)) {
9536 ConstraintProto*
ct = context_->mapping_model->add_constraints();
9537 auto* arg =
ct->mutable_linear();
9540 arg->add_vars(r.representative);
9541 arg->add_coeffs(-r.coeff);
9542 arg->add_domain(r.offset);
9543 arg->add_domain(r.offset);
9544 context_->RemoveVariableFromAffineRelation(
var);
9549 void CpModelPresolver::PresolveToFixPoint() {
9550 if (context_->ModelIsUnsat())
return;
9553 const int64_t max_num_operations =
9554 context_->params().debug_max_num_presolve_operations() > 0
9555 ? context_->params().debug_max_num_presolve_operations()
9561 absl::flat_hash_set<std::pair<int, int>> var_constraint_pair_already_called;
9563 TimeLimit*
time_limit = context_->time_limit();
9566 std::vector<bool> in_queue(context_->working_model->constraints_size(),
9568 std::deque<int> queue;
9569 for (
int c = 0; c < in_queue.size(); ++c) {
9570 if (context_->working_model->constraints(c).constraint_case() !=
9571 ConstraintProto::CONSTRAINT_NOT_SET) {
9581 if (context_->params().permute_presolve_constraint_order()) {
9582 std::shuffle(queue.begin(), queue.end(), *context_->random());
9584 std::sort(queue.begin(), queue.end(), [
this](
int a,
int b) {
9585 const int score_a = context_->ConstraintToVars(a).size();
9586 const int score_b = context_->ConstraintToVars(b).size();
9587 return score_a < score_b || (score_a == score_b && a < b);
9594 constexpr
int kMaxNumLoops = 1000;
9596 i < kMaxNumLoops && !queue.empty() && !context_->ModelIsUnsat(); ++i) {
9598 if (context_->num_presolve_operations > max_num_operations)
break;
9599 while (!queue.empty() && !context_->ModelIsUnsat()) {
9601 if (context_->num_presolve_operations > max_num_operations)
break;
9602 const int c = queue.front();
9603 in_queue[c] =
false;
9606 const int old_num_constraint =
9607 context_->working_model->constraints_size();
9608 const bool changed = PresolveOneConstraint(c);
9609 if (context_->ModelIsUnsat()) {
9610 SOLVER_LOG(logger_,
"Unsat after presolving constraint #", c,
9611 " (warning, dump might be inconsistent): ",
9612 context_->working_model->constraints(c).ShortDebugString());
9616 const int new_num_constraints =
9617 context_->working_model->constraints_size();
9618 if (new_num_constraints > old_num_constraint) {
9619 context_->UpdateNewConstraintsVariableUsage();
9620 in_queue.resize(new_num_constraints,
true);
9621 for (
int c = old_num_constraint; c < new_num_constraints; ++c) {
9629 context_->UpdateConstraintVariableUsage(c);
9633 if (context_->ModelIsUnsat())
return;
9635 in_queue.resize(context_->working_model->constraints_size(),
false);
9636 const auto& vector_that_can_grow_during_iter =
9637 context_->var_with_reduced_small_degree.PositionsSetAtLeastOnce();
9638 for (
int i = 0; i < vector_that_can_grow_during_iter.size(); ++i) {
9639 const int v = vector_that_can_grow_during_iter[i];
9640 if (context_->VariableIsNotUsedAnymore(v))
continue;
9644 if (!PresolveAffineRelationIfAny(v))
return;
9646 const int degree = context_->VarToConstraints(v).size();
9647 if (degree == 0)
continue;
9648 if (degree == 2) LookAtVariableWithDegreeTwo(v);
9649 if (degree == 2 || degree == 3) {
9651 ProcessVariableInTwoAtMostOrExactlyOne(v);
9652 in_queue.resize(context_->working_model->constraints_size(),
false);
9659 if (degree != 1)
continue;
9660 const int c = *context_->VarToConstraints(v).begin();
9661 if (c < 0)
continue;
9666 if (var_constraint_pair_already_called.contains(
9667 std::pair<int, int>(v, c))) {
9670 var_constraint_pair_already_called.insert({v, c});
9677 context_->var_with_reduced_small_degree.SparseClearAll();
9679 for (
int i = 0; i < 2; ++i) {
9683 if (context_->ModelIsUnsat())
return;
9685 in_queue.resize(context_->working_model->constraints_size(),
false);
9686 const auto& vector_that_can_grow_during_iter =
9687 context_->modified_domains.PositionsSetAtLeastOnce();
9688 for (
int i = 0; i < vector_that_can_grow_during_iter.size(); ++i) {
9689 const int v = vector_that_can_grow_during_iter[i];
9690 if (context_->VariableIsNotUsedAnymore(v))
continue;
9691 if (!PresolveAffineRelationIfAny(v))
return;
9692 if (context_->VariableIsNotUsedAnymore(v))
continue;
9694 TryToSimplifyDomain(v);
9697 if (context_->ModelIsUnsat())
return;
9698 context_->UpdateNewConstraintsVariableUsage();
9700 if (!context_->CanonicalizeOneObjectiveVariable(v))
return;
9702 in_queue.resize(context_->working_model->constraints_size(),
false);
9703 for (
const int c : context_->VarToConstraints(v)) {
9704 if (c >= 0 && !in_queue[c]) {
9710 context_->modified_domains.SparseClearAll();
9713 if (!queue.empty() || i == 1)
break;
9716 for (
int v = 0; v < context_->working_model->variables().size(); ++v) {
9717 ProcessVariableOnlyUsedInEncoding(v);
9726 if (!context_->keep_all_feasible_solutions &&
9727 context_->working_model->assumptions().empty()) {
9728 VarDomination var_dom;
9729 DualBoundStrengthening dual_bound_strengthening;
9731 &dual_bound_strengthening);
9732 if (!dual_bound_strengthening.Strengthen(context_))
return;
9733 if (dual_bound_strengthening.NumDeletedConstraints() > 0) {
9750 std::sort(queue.begin(), queue.end());
9753 if (context_->ModelIsUnsat())
return;
9763 const int num_constraints = context_->working_model->constraints_size();
9764 for (
int c = 0; c < num_constraints; ++c) {
9765 ConstraintProto*
ct = context_->working_model->mutable_constraints(c);
9766 switch (
ct->constraint_case()) {
9767 case ConstraintProto::kNoOverlap:
9769 if (PresolveNoOverlap(
ct)) {
9770 context_->UpdateConstraintVariableUsage(c);
9773 case ConstraintProto::kNoOverlap2D:
9775 if (PresolveNoOverlap2D(c,
ct)) {
9776 context_->UpdateConstraintVariableUsage(c);
9779 case ConstraintProto::kCumulative:
9781 if (PresolveCumulative(
ct)) {
9782 context_->UpdateConstraintVariableUsage(c);
9785 case ConstraintProto::kBoolOr: {
9788 for (
const auto& pair :
9789 context_->deductions.ProcessClause(
ct->bool_or().literals())) {
9790 bool modified =
false;
9791 if (!context_->IntersectDomainWith(pair.first, pair.second,
9796 context_->UpdateRuleStats(
"deductions: reduced variable domain");
9806 context_->deductions.MarkProcessingAsDoneForNow();
9812 const CpModelProto& in_model) {
9813 if (context_->
params().ignore_names()) {
9816 in_model.variables_size());
9817 for (
const IntegerVariableProto& var_proto : in_model.variables()) {
9818 *context_->
working_model->add_variables()->mutable_domain() =
9822 *context_->
working_model->mutable_variables() = in_model.variables();
9832 const CpModelProto& in_model,
const std::vector<int>& ignored_constraints,
9834 const absl::flat_hash_set<int> ignored_constraints_set(
9835 ignored_constraints.begin(), ignored_constraints.end());
9837 const bool ignore_names = context_->
params().ignore_names();
9841 std::vector<int> constraints_using_intervals;
9843 starting_constraint_index_ = context_->
working_model->constraints_size();
9844 for (
int c = 0; c < in_model.constraints_size(); ++c) {
9845 if (ignored_constraints_set.contains(c))
continue;
9847 const ConstraintProto&
ct = in_model.constraints(c);
9848 if (OneEnforcementLiteralIsFalse(
ct))
continue;
9853 switch (
ct.constraint_case()) {
9854 case ConstraintProto::CONSTRAINT_NOT_SET:
9856 case ConstraintProto::kBoolOr:
9858 if (!CopyBoolOrWithDupSupport(
ct))
return CreateUnsatModel();
9860 if (!CopyBoolOr(
ct))
return CreateUnsatModel();
9863 case ConstraintProto::kBoolAnd:
9864 if (!CopyBoolAnd(
ct))
return CreateUnsatModel();
9866 case ConstraintProto::kLinear:
9867 if (!CopyLinear(
ct))
return CreateUnsatModel();
9869 case ConstraintProto::kAtMostOne:
9870 if (!CopyAtMostOne(
ct))
return CreateUnsatModel();
9872 case ConstraintProto::kExactlyOne:
9873 if (!CopyExactlyOne(
ct))
return CreateUnsatModel();
9875 case ConstraintProto::kInterval:
9876 if (!CopyInterval(
ct, c, ignore_names))
return CreateUnsatModel();
9878 case ConstraintProto::kNoOverlap:
9880 constraints_using_intervals.push_back(c);
9882 CopyAndMapNoOverlap(
ct);
9885 case ConstraintProto::kNoOverlap2D:
9887 constraints_using_intervals.push_back(c);
9889 CopyAndMapNoOverlap2D(
ct);
9892 case ConstraintProto::kCumulative:
9894 constraints_using_intervals.push_back(c);
9896 CopyAndMapCumulative(
ct);
9900 ConstraintProto* new_ct = context_->
working_model->add_constraints();
9904 new_ct->clear_name();
9911 DCHECK(first_copy || constraints_using_intervals.empty());
9912 for (
const int c : constraints_using_intervals) {
9913 const ConstraintProto&
ct = in_model.constraints(c);
9914 switch (
ct.constraint_case()) {
9915 case ConstraintProto::kNoOverlap:
9916 CopyAndMapNoOverlap(
ct);
9918 case ConstraintProto::kNoOverlap2D:
9919 CopyAndMapNoOverlap2D(
ct);
9921 case ConstraintProto::kCumulative:
9922 CopyAndMapCumulative(
ct);
9925 LOG(DFATAL) <<
"Shouldn't be here.";
9932 void ModelCopy::CopyEnforcementLiterals(
const ConstraintProto& orig,
9933 ConstraintProto* dest) {
9934 temp_enforcement_literals_.clear();
9935 for (
const int lit : orig.enforcement_literal()) {
9937 skipped_non_zero_++;
9940 temp_enforcement_literals_.push_back(lit);
9942 dest->mutable_enforcement_literal()->Add(temp_enforcement_literals_.begin(),
9943 temp_enforcement_literals_.end());
9946 bool ModelCopy::OneEnforcementLiteralIsFalse(
const ConstraintProto&
ct)
const {
9947 for (
const int lit :
ct.enforcement_literal()) {
9955 bool ModelCopy::CopyBoolOr(
const ConstraintProto&
ct) {
9956 temp_literals_.clear();
9957 for (
const int lit :
ct.enforcement_literal()) {
9961 for (
const int lit :
ct.bool_or().literals()) {
9966 skipped_non_zero_++;
9968 temp_literals_.push_back(lit);
9974 ->mutable_literals()
9975 ->Add(temp_literals_.begin(), temp_literals_.end());
9976 return !temp_literals_.empty();
9979 bool ModelCopy::CopyBoolOrWithDupSupport(
const ConstraintProto&
ct) {
9980 temp_literals_.clear();
9981 tmp_literals_set_.clear();
9982 for (
const int enforcement_lit :
ct.enforcement_literal()) {
9993 skipped_non_zero_++;
9996 if (tmp_literals_set_.contains(
NegatedRef(lit))) {
10000 const auto [it, inserted] = tmp_literals_set_.insert(lit);
10001 if (inserted) temp_literals_.push_back(lit);
10003 for (
const int lit :
ct.bool_or().literals()) {
10009 skipped_non_zero_++;
10012 if (tmp_literals_set_.contains(
NegatedRef(lit))) {
10016 const auto [it, inserted] = tmp_literals_set_.insert(lit);
10017 if (inserted) temp_literals_.push_back(lit);
10021 ->mutable_bool_or()
10022 ->mutable_literals()
10023 ->Add(temp_literals_.begin(), temp_literals_.end());
10024 return !temp_literals_.empty();
10027 bool ModelCopy::CopyBoolAnd(
const ConstraintProto&
ct) {
10028 bool at_least_one_false =
false;
10029 int num_non_fixed_literals = 0;
10030 for (
const int lit :
ct.bool_and().literals()) {
10032 at_least_one_false =
true;
10036 num_non_fixed_literals++;
10040 if (at_least_one_false) {
10041 ConstraintProto* new_ct = context_->
working_model->add_constraints();
10042 BoolArgumentProto* bool_or = new_ct->mutable_bool_or();
10045 for (
const int lit :
ct.enforcement_literal()) {
10047 skipped_non_zero_++;
10052 return !bool_or->literals().empty();
10053 }
else if (num_non_fixed_literals > 0) {
10054 ConstraintProto* new_ct = context_->
working_model->add_constraints();
10055 CopyEnforcementLiterals(
ct, new_ct);
10056 BoolArgumentProto* bool_and = new_ct->mutable_bool_and();
10057 bool_and->mutable_literals()->Reserve(num_non_fixed_literals);
10058 for (
const int lit :
ct.bool_and().literals()) {
10060 skipped_non_zero_++;
10063 bool_and->add_literals(lit);
10069 bool ModelCopy::CopyLinear(
const ConstraintProto&
ct) {
10070 non_fixed_variables_.clear();
10071 non_fixed_coefficients_.clear();
10072 int64_t offset = 0;
10073 int64_t min_activity = 0;
10074 int64_t max_activity = 0;
10075 for (
int i = 0; i <
ct.linear().vars_size(); ++i) {
10076 const int ref =
ct.linear().vars(i);
10077 const int64_t coeff =
ct.linear().coeffs(i);
10078 if (coeff == 0)
continue;
10079 if (context_->
IsFixed(ref)) {
10080 offset += coeff * context_->
MinOf(ref);
10081 skipped_non_zero_++;
10086 min_activity += coeff * context_->
MinOf(ref);
10087 max_activity += coeff * context_->
MaxOf(ref);
10089 min_activity += coeff * context_->
MaxOf(ref);
10090 max_activity += coeff * context_->
MinOf(ref);
10095 non_fixed_variables_.push_back(ref);
10096 non_fixed_coefficients_.push_back(coeff);
10098 non_fixed_variables_.push_back(
NegatedRef(ref));
10099 non_fixed_coefficients_.push_back(-coeff);
10103 const Domain implied(min_activity, max_activity);
10104 const Domain new_rhs =
10108 if (implied.IsIncludedIn(new_rhs))
return true;
10111 if (implied.IntersectionWith(new_rhs).IsEmpty()) {
10112 if (
ct.enforcement_literal().empty())
return false;
10113 temp_literals_.clear();
10114 for (
const int literal :
ct.enforcement_literal()) {
10116 skipped_non_zero_++;
10122 ->mutable_bool_or()
10123 ->mutable_literals()
10124 ->Add(temp_literals_.begin(), temp_literals_.end());
10125 return !temp_literals_.empty();
10128 ConstraintProto* new_ct = context_->
working_model->add_constraints();
10129 CopyEnforcementLiterals(
ct, new_ct);
10130 LinearConstraintProto* linear = new_ct->mutable_linear();
10131 linear->mutable_vars()->Add(non_fixed_variables_.begin(),
10132 non_fixed_variables_.end());
10133 linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(),
10134 non_fixed_coefficients_.end());
10139 bool ModelCopy::CopyAtMostOne(
const ConstraintProto&
ct) {
10141 temp_literals_.clear();
10142 for (
const int lit :
ct.at_most_one().literals()) {
10144 skipped_non_zero_++;
10147 temp_literals_.push_back(lit);
10151 if (temp_literals_.size() <= 1)
return true;
10152 if (num_true > 1)
return false;
10155 ConstraintProto* new_ct = context_->
working_model->add_constraints();
10156 CopyEnforcementLiterals(
ct, new_ct);
10157 new_ct->mutable_at_most_one()->mutable_literals()->Add(temp_literals_.begin(),
10158 temp_literals_.end());
10162 bool ModelCopy::CopyExactlyOne(
const ConstraintProto&
ct) {
10164 temp_literals_.clear();
10165 for (
const int lit :
ct.exactly_one().literals()) {
10167 skipped_non_zero_++;
10170 temp_literals_.push_back(lit);
10174 if (temp_literals_.empty() || num_true > 1)
return false;
10175 if (temp_literals_.size() == 1 && num_true == 1)
return true;
10178 ConstraintProto* new_ct = context_->
working_model->add_constraints();
10179 CopyEnforcementLiterals(
ct, new_ct);
10180 new_ct->mutable_exactly_one()->mutable_literals()->Add(temp_literals_.begin(),
10181 temp_literals_.end());
10185 bool ModelCopy::CopyInterval(
const ConstraintProto&
ct,
int c,
10186 bool ignore_names) {
10187 CHECK_EQ(starting_constraint_index_, 0)
10188 <<
"Adding new interval constraints to partially filled model is not "
10190 interval_mapping_[c] = context_->
working_model->constraints_size();
10191 ConstraintProto* new_ct = context_->
working_model->add_constraints();
10192 if (ignore_names) {
10193 *new_ct->mutable_enforcement_literal() =
ct.enforcement_literal();
10194 *new_ct->mutable_interval()->mutable_start() =
ct.interval().start();
10195 *new_ct->mutable_interval()->mutable_size() =
ct.interval().size();
10196 *new_ct->mutable_interval()->mutable_end() =
ct.interval().end();
10204 void ModelCopy::CopyAndMapNoOverlap(
const ConstraintProto&
ct) {
10207 context_->
working_model->add_constraints()->mutable_no_overlap();
10208 new_ct->mutable_intervals()->Reserve(
ct.no_overlap().intervals().size());
10209 for (
const int index :
ct.no_overlap().intervals()) {
10210 const auto it = interval_mapping_.find(
index);
10211 if (it == interval_mapping_.end())
continue;
10212 new_ct->add_intervals(it->second);
10216 void ModelCopy::CopyAndMapNoOverlap2D(
const ConstraintProto&
ct) {
10219 context_->
working_model->add_constraints()->mutable_no_overlap_2d();
10220 new_ct->set_boxes_with_null_area_can_overlap(
10221 ct.no_overlap_2d().boxes_with_null_area_can_overlap());
10223 const int num_intervals =
ct.no_overlap_2d().x_intervals().size();
10224 new_ct->mutable_x_intervals()->Reserve(num_intervals);
10225 new_ct->mutable_y_intervals()->Reserve(num_intervals);
10226 for (
int i = 0; i < num_intervals; ++i) {
10227 const auto x_it = interval_mapping_.find(
ct.no_overlap_2d().x_intervals(i));
10228 if (x_it == interval_mapping_.end())
continue;
10229 const auto y_it = interval_mapping_.find(
ct.no_overlap_2d().y_intervals(i));
10230 if (y_it == interval_mapping_.end())
continue;
10231 new_ct->add_x_intervals(x_it->second);
10232 new_ct->add_y_intervals(y_it->second);
10236 void ModelCopy::CopyAndMapCumulative(
const ConstraintProto&
ct) {
10239 context_->
working_model->add_constraints()->mutable_cumulative();
10240 *new_ct->mutable_capacity() =
ct.cumulative().capacity();
10242 const int num_intervals =
ct.cumulative().intervals().size();
10243 new_ct->mutable_intervals()->Reserve(num_intervals);
10244 new_ct->mutable_demands()->Reserve(num_intervals);
10245 for (
int i = 0; i < num_intervals; ++i) {
10246 const auto it = interval_mapping_.find(
ct.cumulative().intervals(i));
10247 if (it == interval_mapping_.end())
continue;
10248 new_ct->add_intervals(it->second);
10249 *new_ct->add_demands() =
ct.cumulative().demands(i);
10253 bool ModelCopy::CreateUnsatModel() {
10255 context_->
working_model->add_constraints()->mutable_bool_or();
10268 return context->NotifyThatModelIsUnsat();
10273 if (!in_model.name().empty()) {
10274 context->working_model->set_name(in_model.name());
10276 if (in_model.has_objective()) {
10277 *
context->working_model->mutable_objective() = in_model.objective();
10279 if (in_model.has_floating_point_objective()) {
10280 *
context->working_model->mutable_floating_point_objective() =
10281 in_model.floating_point_objective();
10283 if (!in_model.search_strategy().empty()) {
10284 *
context->working_model->mutable_search_strategy() =
10285 in_model.search_strategy();
10287 if (!in_model.assumptions().empty()) {
10288 *
context->working_model->mutable_assumptions() = in_model.assumptions();
10290 if (in_model.has_symmetry()) {
10291 *
context->working_model->mutable_symmetry() = in_model.symmetry();
10293 if (in_model.has_solution_hint()) {
10294 *
context->working_model->mutable_solution_hint() = in_model.solution_hint();
10305 void CpModelPresolver::MergeClauses() {
10307 ClauseWithOneMissingHasher hasher(*context_->
random());
10311 int64_t work_done = 0;
10312 const int64_t work_limit = 1e8;
10314 std::vector<int> to_clean;
10316 int64_t num_collisions = 0;
10317 int64_t num_merges = 0;
10318 int64_t num_saved_literals = 0;
10321 absl::flat_hash_map<uint64_t, int> bool_and_map;
10327 const int num_variables = context_->
working_model->variables_size();
10328 std::vector<int> bool_or_indices;
10329 std::vector<int64_t> literal_score(2 * num_variables, 0);
10330 const auto get_index = [](
int ref) {
10334 const int num_constraints = context_->
working_model->constraints_size();
10335 for (
int c = 0; c < num_constraints; ++c) {
10336 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
10337 if (
ct->constraint_case() == ConstraintProto::kBoolAnd) {
10338 if (
ct->enforcement_literal().size() > 1) {
10340 std::sort(
ct->mutable_enforcement_literal()->begin(),
10341 ct->mutable_enforcement_literal()->end(),
10342 std::greater<int>());
10343 const auto [it, inserted] = bool_and_map.insert(
10344 {hasher.HashOfNegatedLiterals(
ct->enforcement_literal()), c});
10346 to_clean.push_back(c);
10349 ConstraintProto* other_ct =
10351 const absl::Span<const int> s1(
ct->enforcement_literal());
10352 const absl::Span<const int> s2(other_ct->enforcement_literal());
10355 "bool_and: merged constraints with same enforcement");
10356 other_ct->mutable_bool_and()->mutable_literals()->Add(
10357 ct->bool_and().literals().begin(),
10358 ct->bool_and().literals().end());
10366 if (
ct->constraint_case() == ConstraintProto::kAtMostOne) {
10367 const int size =
ct->at_most_one().literals().size();
10368 for (
const int ref :
ct->at_most_one().literals()) {
10369 literal_score[get_index(ref)] += size;
10373 if (
ct->constraint_case() == ConstraintProto::kExactlyOne) {
10374 const int size =
ct->exactly_one().literals().size();
10375 for (
const int ref :
ct->exactly_one().literals()) {
10376 literal_score[get_index(ref)] += size;
10381 if (
ct->constraint_case() != ConstraintProto::kBoolOr)
continue;
10384 if (!
ct->enforcement_literal().empty())
continue;
10385 if (
ct->bool_or().literals().size() <= 2)
continue;
10387 std::sort(
ct->mutable_bool_or()->mutable_literals()->begin(),
10388 ct->mutable_bool_or()->mutable_literals()->end());
10389 hasher.RegisterClause(c,
ct->bool_or().literals());
10390 bool_or_indices.push_back(c);
10393 for (
const int c : bool_or_indices) {
10394 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
10396 bool merged =
false;
10397 work_done +=
ct->bool_or().literals().size();
10398 if (work_done > work_limit)
break;
10399 for (
const int ref :
ct->bool_or().literals()) {
10400 const uint64_t
hash = hasher.HashWithout(c, ref);
10401 const auto it = bool_and_map.find(
hash);
10402 if (it != bool_and_map.end()) {
10404 const int base_c = it->second;
10405 auto* and_ct = context_->
working_model->mutable_constraints(base_c);
10407 ct->bool_or().literals(), and_ct->enforcement_literal(), ref)) {
10409 num_saved_literals +=
ct->bool_or().literals().size() - 1;
10411 and_ct->mutable_bool_and()->add_literals(ref);
10421 int best_ref =
ct->bool_or().literals(0);
10422 int64_t best_score = literal_score[get_index(
NegatedRef(best_ref))];
10423 for (
const int ref :
ct->bool_or().literals()) {
10424 const int64_t score = literal_score[get_index(
NegatedRef(ref))];
10425 if (score > best_score) {
10427 best_score = score;
10431 const uint64_t
hash = hasher.HashWithout(c, best_ref);
10432 const auto [_, inserted] = bool_and_map.insert({
hash, c});
10434 to_clean.push_back(c);
10436 for (
const int lit :
ct->bool_or().literals()) {
10437 if (lit == best_ref)
continue;
10441 ct->mutable_enforcement_literal()->Assign(
10443 ct->mutable_bool_and()->add_literals(best_ref);
10449 for (
const int c : to_clean) {
10450 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
10451 if (
ct->bool_and().literals().size() > 1) {
10459 for (
const int ref :
ct->enforcement_literal()) {
10463 ct->mutable_bool_or()->mutable_literals()->Assign(
10467 SOLVER_LOG(logger_,
"[MergeClauses]",
" #num_collisions=", num_collisions,
10468 " #num_merges=", num_merges,
10469 " #num_saved_literals=", num_saved_literals,
" work=", work_done,
10478 std::vector<int>* postsolve_mapping) {
10484 std::vector<int>* postsolve_mapping)
10485 : postsolve_mapping_(postsolve_mapping),
10487 logger_(
context->logger()) {}
10489 CpSolverStatus CpModelPresolver::InfeasibleStatus() {
10512 context_->
params().keep_all_feasible_solutions_in_presolve() ||
10513 context_->
params().enumerate_all_solutions() ||
10514 context_->
params().fill_tightened_domains_in_response() ||
10516 !context_->
params().cp_model_presolve();
10519 for (
const auto& decision_strategy :
10521 *(context_->
mapping_model->add_search_strategy()) = decision_strategy;
10532 if (context_->
working_model->has_floating_point_objective()) {
10535 "The floating point objective cannot be scaled with enough "
10560 if (!context_->
params().cp_model_presolve()) {
10562 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10571 EncodeAllAffineRelations();
10573 return CpSolverStatus::UNKNOWN;
10578 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10581 if (!PresolveAffineRelationIfAny(
var))
return InfeasibleStatus();
10586 TryToSimplifyDomain(
var);
10587 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10593 for (
int iter = 0; iter < context_->
params().max_presolve_iterations();
10603 PresolveToFixPoint();
10607 ExtractEncodingFromLinear();
10609 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10615 const int num_constraints = context_->
working_model->constraints().size();
10616 for (
int c = 0; c < num_constraints; ++c) {
10617 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
10618 const auto type =
ct->constraint_case();
10619 if (type == ConstraintProto::kAtMostOne ||
10620 type == ConstraintProto::kExactlyOne) {
10624 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10630 const int num_vars = context_->
working_model->variables().size();
10631 for (
int var = 0;
var < num_vars; ++
var) {
10657 if (context_->
params().cp_model_use_sat_presolve()) {
10659 PresolvePureSatPart();
10672 const int old_size = context_->
working_model->constraints_size();
10673 for (
int c = 0; c < old_size; ++c) {
10674 ConstraintProto*
ct = context_->
working_model->mutable_constraints(c);
10675 if (
ct->constraint_case() != ConstraintProto::kLinear)
continue;
10676 ExtractAtMostOneFromLinear(
ct);
10681 if (context_->
params().cp_model_probing_level() > 0) {
10684 PresolveToFixPoint();
10687 TransformIntoMaxCliques();
10694 DetectDuplicateConstraints();
10695 DetectDominatedLinearConstraints();
10697 if (context_->
params().find_big_linear_overlap()) FindBigLinearOverlap();
10698 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10705 if ( (
false)) DetectIncludedEnforcement();
10714 PresolveToFixPoint();
10719 const int64_t num_ops =
10721 if (num_ops == 0)
break;
10723 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10726 MergeNoOverlapConstraints();
10727 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10733 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10734 ShiftObjectiveWithExactlyOnes();
10735 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10741 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10749 EncodeAllAffineRelations();
10750 if (context_->
ModelIsUnsat())
return InfeasibleStatus();
10760 absl::flat_hash_set<int> used_variables;
10761 for (DecisionStrategyProto& strategy :
10763 DecisionStrategyProto copy = strategy;
10764 strategy.clear_variables();
10765 strategy.clear_transformations();
10766 for (
const int ref : copy.variables()) {
10774 if (used_variables.contains(
var))
continue;
10775 used_variables.insert(
var);
10783 if (strategy.variable_selection_strategy() !=
10784 DecisionStrategyProto::CHOOSE_FIRST) {
10785 DecisionStrategyProto::AffineTransformation* t =
10786 strategy.add_transformations();
10787 t->set_index(strategy.variables_size());
10788 t->set_offset(r.
offset);
10789 t->set_positive_coeff(std::abs(r.
coeff));
10791 strategy.add_variables(rep);
10798 strategy.add_variables(ref);
10804 for (
int i = 0; i < context_->
working_model->variables_size(); ++i) {
10807 DCHECK_GT(context_->
working_model->variables(i).domain_size(), 0);
10815 postsolve_mapping_->clear();
10816 std::vector<int> mapping(context_->
working_model->variables_size(), -1);
10817 absl::flat_hash_map<int64_t, int> constant_to_index;
10818 int num_unused_variables = 0;
10819 for (
int i = 0; i < context_->
working_model->variables_size(); ++i) {
10820 if (mapping[i] != -1)
continue;
10829 mapping[r] = postsolve_mapping_->size();
10830 postsolve_mapping_->push_back(r);
10844 ++num_unused_variables;
10853 auto [it, inserted] = constant_to_index.insert(
10854 {context_->
FixedValue(i), postsolve_mapping_->size()});
10856 mapping[i] = it->second;
10862 mapping[i] = postsolve_mapping_->size();
10863 postsolve_mapping_->push_back(i);
10865 context_->
UpdateRuleStats(absl::StrCat(
"presolve: ", num_unused_variables,
10866 " unused variables removed."));
10868 if (context_->
params().permute_variable_randomly()) {
10870 const int n = postsolve_mapping_->size();
10871 std::vector<int> perm(n);
10872 std::iota(perm.begin(), perm.end(), 0);
10873 std::shuffle(perm.begin(), perm.end(), *context_->
random());
10874 for (
int i = 0; i < context_->
working_model->variables_size(); ++i) {
10875 if (mapping[i] != -1) mapping[i] = perm[mapping[i]];
10877 std::vector<int> new_postsolve_mapping(n);
10878 for (
int i = 0; i < n; ++i) {
10879 new_postsolve_mapping[perm[i]] = (*postsolve_mapping_)[i];
10881 *postsolve_mapping_ = std::move(new_postsolve_mapping);
10903 const std::string error =
10905 if (!error.empty()) {
10906 SOLVER_LOG(logger_,
"Error while validating postsolved model: ", error);
10912 if (!error.empty()) {
10914 "Error while validating mapping_model model: ", error);
10919 return CpSolverStatus::UNKNOWN;
10928 auto mapping_function = [&mapping](
int* ref) {
10930 CHECK_GE(image, 0);
10933 for (ConstraintProto& ct_ref : *
proto->mutable_constraints()) {
10939 if (
proto->has_objective()) {
10940 for (
int& mutable_ref : *
proto->mutable_objective()->mutable_vars()) {
10941 mapping_function(&mutable_ref);
10946 for (
int& mutable_ref : *
proto->mutable_assumptions()) {
10947 mapping_function(&mutable_ref);
10952 for (DecisionStrategyProto& strategy : *
proto->mutable_search_strategy()) {
10953 const DecisionStrategyProto copy = strategy;
10954 strategy.clear_variables();
10955 std::vector<int> new_indices(copy.variables().size(), -1);
10956 for (
int i = 0; i < copy.variables().size(); ++i) {
10957 const int ref = copy.variables(i);
10960 new_indices[i] = strategy.variables_size();
10964 strategy.clear_transformations();
10965 for (
const auto& transform : copy.transformations()) {
10966 CHECK_LT(transform.index(), new_indices.size());
10967 const int new_index = new_indices[transform.index()];
10968 if (new_index == -1)
continue;
10969 auto* new_transform = strategy.add_transformations();
10970 *new_transform = transform;
10971 CHECK_LT(new_index, strategy.variables().size());
10972 new_transform->set_index(new_index);
10978 if (
proto->has_solution_hint()) {
10979 absl::flat_hash_set<int> used_vars;
10980 auto* mutable_hint =
proto->mutable_solution_hint();
10982 for (
int i = 0; i < mutable_hint->vars_size(); ++i) {
10983 const int old_ref = mutable_hint->vars(i);
10984 int64_t old_value = mutable_hint->values(i);
10988 if (old_value <
context.MinOf(old_ref)) {
10989 old_value =
context.MinOf(old_ref);
10991 if (old_value >
context.MaxOf(old_ref)) {
10992 old_value =
context.MaxOf(old_ref);
11001 const int image = mapping[
var];
11003 if (!used_vars.insert(image).second)
continue;
11004 mutable_hint->set_vars(new_size, image);
11005 mutable_hint->set_values(new_size,
value);
11009 if (new_size > 0) {
11010 mutable_hint->mutable_vars()->Truncate(new_size);
11011 mutable_hint->mutable_values()->Truncate(new_size);
11013 proto->clear_solution_hint();
11018 std::vector<IntegerVariableProto> new_variables;
11019 for (
int i = 0; i < mapping.size(); ++i) {
11020 const int image = mapping[i];
11021 if (image < 0)
continue;
11022 if (image >= new_variables.size()) {
11023 new_variables.resize(image + 1, IntegerVariableProto());
11025 new_variables[image].Swap(
proto->mutable_variables(i));
11027 proto->clear_variables();
11028 for (IntegerVariableProto& proto_ref : new_variables) {
11029 proto->add_variables()->Swap(&proto_ref);
11033 for (
const IntegerVariableProto& v :
proto->variables()) {
11034 CHECK_GT(v.domain_size(), 0);
11040 ConstraintProto CopyConstraintForDuplicateDetection(
const ConstraintProto&
ct,
11041 bool ignore_enforcement) {
11042 ConstraintProto copy =
ct;
11044 if (ignore_enforcement) {
11045 copy.mutable_enforcement_literal()->Clear();
11046 }
else if (
ct.constraint_case() == ConstraintProto::kLinear) {
11047 copy.mutable_linear()->clear_domain();
11053 ConstraintProto CopyObjectiveForDuplicateDetection(
11054 const CpObjectiveProto& objective) {
11055 ConstraintProto copy;
11056 *copy.mutable_linear()->mutable_vars() = objective.vars();
11057 *copy.mutable_linear()->mutable_coeffs() = objective.coeffs();
11064 const CpModelProto&
model_proto,
bool ignore_enforcement) {
11065 std::vector<std::pair<int, int>> result;
11068 ConstraintProto copy;
11070 absl::flat_hash_map<uint64_t, int> equiv_constraints;
11073 if (
model_proto.has_objective() && !ignore_enforcement) {
11074 copy = CopyObjectiveForDuplicateDetection(
model_proto.objective());
11075 s = copy.SerializeAsString();
11079 const int num_constraints =
model_proto.constraints().size();
11080 for (
int c = 0; c < num_constraints; ++c) {
11081 const auto type =
model_proto.constraints(c).constraint_case();
11082 if (type == ConstraintProto::CONSTRAINT_NOT_SET)
continue;
11086 if (type == ConstraintProto::kInterval)
continue;
11089 if (ignore_enforcement && type == ConstraintProto::kBoolAnd)
continue;
11094 copy = CopyConstraintForDuplicateDetection(
model_proto.constraints(c),
11095 ignore_enforcement);
11096 s = copy.SerializeAsString();
11098 const uint64_t
hash = absl::Hash<std::string>()(s);
11099 const auto [it, inserted] = equiv_constraints.insert({
hash, c});
11102 const int other_c_with_same_hash = it->second;
11104 ? CopyObjectiveForDuplicateDetection(
model_proto.objective())
11105 : CopyConstraintForDuplicateDetection(
11107 ignore_enforcement);
11108 if (s == copy.SerializeAsString()) {
11109 result.push_back({c, other_c_with_same_hash});
We call domain any subset of Int64 = [kint64min, kint64max].
Domain InverseMultiplicationBy(const int64_t coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
Domain Negation() const
Returns {x ∈ Int64, ∃ e ∈ D, x = -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.
int64_t Min() const
Returns the min value of the 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)
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.
CpSolverStatus Presolve()
void RemoveEmptyConstraints()
CpModelPresolver(PresolveContext *context, std::vector< int > *postsolve_mapping)
bool PresolveOneConstraint(int c)
int NumDeductions() const
void AddDeduction(int literal_ref, int var, Domain domain)
int64_t CurrentMax() const
void Reset(int64_t bound)
void AddMultiples(int64_t coeff, int64_t max_value)
bool ImportAndSimplifyConstraints(const CpModelProto &in_model, const std::vector< int > &ignored_constraints, bool first_copy=false)
void ImportVariablesAndMaybeIgnoreNames(const CpModelProto &in_model)
int64_t MaxOf(int ref) const
bool CanonicalizeAffineVariable(int ref, int64_t coeff, int64_t mod, int64_t rhs)
bool ExpressionIsALiteral(const LinearExpressionProto &expr, int *literal=nullptr) const
bool StoreAbsRelation(int target_ref, int ref)
bool VariableWithCostIsUnique(int ref) const
ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective(int var_in_equality, int64_t coeff_in_equality, const ConstraintProto &equality)
bool ConstraintIsInactive(int ct_index) const
bool ConstraintVariableUsageIsConsistent()
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)
bool ConstraintVariableGraphIsUpToDate() const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64_t value)
bool RecomputeSingletonObjectiveDomain()
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)
int64_t ObjectiveCoeff(int var) const
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()
CpModelProto * mapping_model
const std::vector< int > & ConstraintToVars(int c) const
std::pair< int64_t, int64_t > ComputeMinMaxActivity(const ProtoWithVarsAndCoeffs &proto) const
int GetOrCreateVarValueEncoding(int ref, int64_t value)
void UpdateNewConstraintsVariableUsage()
bool VariableIsUniqueAndRemovable(int ref) const
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(const std::string &message="")
SparseBitset< int > modified_domains
Domain DomainOf(int ref) const
int64_t num_presolve_operations
void InitializeNewDomains()
const absl::flat_hash_map< int, int64_t > & ObjectiveMap() const
void MarkVariableAsRemoved(int ref)
DomainDeductions deductions
std::vector< Domain > tmp_left_domains
int GetIntervalRepresentative(int index)
SparseBitset< int > var_with_reduced_small_degree
int64_t FixedValue(int ref) const
bool LiteralIsTrue(int lit) const
int IntervalUsage(int c) const
CpModelProto * working_model
bool HasVarValueEncoding(int ref, int64_t value, int *literal=nullptr)
bool IntervalIsConstant(int ct_ref) const
bool DomainContains(int ref, int64_t value) const
bool LiteralIsFalse(int lit) const
bool ShiftCostInExactlyOne(absl::Span< const int > exactly_one, int64_t shift)
void UpdateRuleStats(const std::string &name, int num_times=1)
const SatParameters & params() const
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)
const absl::flat_hash_set< int > & VarToConstraints(int var) const
ModelRandomGenerator * random()
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
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()
int64_t MinOf(int ref) const
bool GetAbsRelation(int target_ref, int *ref)
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64_t value)
CpModelProto const * model_proto
ModelSharedTimeLimit * time_limit
GurobiMPCallbackContext * context
void Truncate(RepeatedPtrField< T > *array, int new_size)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
void swap(IdMap< K, V > &a, IdMap< K, V > &b)
uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
bool DetectAndExploitSymmetriesInPresolve(PresolveContext *context)
bool RefIsPositive(int ref)
int64_t ClosestMultiple(int64_t value, int64_t base)
const LiteralIndex kNoLiteralIndex(-1)
void GetOverlappingIntervalComponents(std::vector< IndexedInterval > *intervals, std::vector< std::vector< int >> *components)
DiophantineSolution SolveDiophantine(absl::Span< const int64_t > coeffs, int64_t rhs, absl::Span< const int64_t > var_lbs, absl::Span< const int64_t > var_ubs)
IntType CeilOfRatio(IntType numerator, IntType denominator)
std::vector< absl::Span< int > > GetOverlappingRectangleComponents(const std::vector< Rectangle > &rectangles, absl::Span< int > active_rectangles)
bool HasEnforcementLiteral(const ConstraintProto &ct)
bool ClauseIsEnforcementImpliesLiteral(absl::Span< const int > clause, absl::Span< const int > enforcement, int literal)
void ExpandCpModel(PresolveContext *context)
bool IsNegatableInt64(absl::int128 x)
constexpr int kAffineRelationConstraint
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
std::vector< std::pair< int, int > > FindDuplicateConstraints(const CpModelProto &model_proto, bool ignore_enforcement)
void DetectDominanceRelations(const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
void ConstructOverlappingSets(bool already_sorted, std::vector< IndexedInterval > *intervals, std::vector< std::vector< int >> *result)
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)
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
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)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
int ReindexArcs(IntContainer *tails, IntContainer *heads, absl::flat_hash_map< int, int > *mapping_output=nullptr)
void FinalExpansionForLinearConstraint(PresolveContext *context)
int64_t FloorSquareRoot(int64_t a)
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
int64_t SafeDoubleToInt64(double value)
constexpr uint64_t kDefaultFingerprintSeed
CpSolverStatus PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
bool LoadModelForProbing(PresolveContext *context, Model *local_model)
InclusionDetector(const Storage &storage) -> InclusionDetector< Storage >
constexpr int kObjectiveConstraint
bool ImportModelWithBasicPresolveIntoContext(const CpModelProto &in_model, PresolveContext *context)
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 PropagateAutomaton(const AutomatonConstraintProto &proto, const PresolveContext &context, std::vector< absl::flat_hash_set< int64_t >> *states, std::vector< absl::flat_hash_set< int64_t >> *labels)
void ApplyVariableMapping(const std::vector< int > &mapping, const PresolveContext &context)
bool LinearInequalityCanBeReducedWithClosestMultiple(int64_t base, const std::vector< int64_t > &coeffs, const std::vector< int64_t > &lbs, const std::vector< int64_t > &ubs, int64_t rhs, int64_t *new_rhs)
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)
absl::StatusOr< std::vector< int > > FastTopologicalSort(const AdjacencyLists &adj)
std::optional< int64_t > end
const std::optional< Range > & range
void FindStronglyConnectedComponents(const NodeIndex num_nodes, const Graph &graph, SccOutput *components)
#define SOLVER_LOG(logger,...)
#define VLOG(verboselevel)
#define VLOG_IS_ON(verboselevel)