24#include "absl/base/attributes.h"
25#include "absl/container/btree_map.h"
26#include "absl/container/flat_hash_map.h"
27#include "absl/container/flat_hash_set.h"
28#include "absl/log/check.h"
29#include "absl/meta/type_traits.h"
30#include "absl/types/span.h"
31#include "google/protobuf/message.h"
71std::pair<IntegerValue, IntegerValue> GetMinAndMaxNotEncoded(
73 const absl::flat_hash_set<IntegerValue>& encoded_values,
79 if (domains ==
nullptr || index >= domains->size()) {
86 for (
const int64_t v : (*domains)[index].
Values()) {
87 if (!encoded_values.contains(IntegerValue(v))) {
88 min = IntegerValue(v);
94 const Domain negated_domain = (*domains)[index].Negation();
95 for (
const int64_t v : negated_domain.Values()) {
96 if (!encoded_values.contains(IntegerValue(-v))) {
97 max = IntegerValue(-v);
110void CollectAffineExpressionWithSingleVariable(
112 std::vector<std::pair<IntegerValue, IntegerValue>>* affines) {
118 if (expr.vars().empty()) {
119 affines->push_back({IntegerValue(0), IntegerValue(expr.offset())});
121 CHECK_EQ(expr.vars().size(), 1);
122 const IntegerVariable affine_var = mapping->Integer(expr.vars(0));
127 CHECK_EQ(affine_var, *var);
129 {IntegerValue(expr.coeffs(0)), IntegerValue(expr.offset())});
133 {IntegerValue(-expr.coeffs(0)), IntegerValue(expr.offset())});
144 int* num_tight,
int* num_loose) {
147 if (encoder ==
nullptr || integer_trail ==
nullptr)
return;
149 std::vector<Literal> at_most_one_ct;
150 absl::flat_hash_set<IntegerValue> encoded_values;
151 std::vector<ValueLiteralPair> encoding;
153 const std::vector<ValueLiteralPair>& initial_encoding =
154 encoder->PartialDomainEncoding(var);
155 if (initial_encoding.empty())
return;
156 for (
const auto value_literal : initial_encoding) {
157 const Literal literal = value_literal.literal;
165 encoding.push_back(value_literal);
166 at_most_one_ct.push_back(literal);
167 encoded_values.insert(value_literal.value);
170 if (encoded_values.empty())
return;
177 const auto [min_not_encoded, max_not_encoded] =
178 GetMinAndMaxNotEncoded(var, encoded_values, model);
183 const IntegerValue rhs = encoding[0].value;
187 encoding_ct.
AddTerm(var, IntegerValue(1));
188 for (
const auto value_literal : encoding) {
189 const Literal lit = value_literal.literal;
192 const IntegerValue delta = value_literal.value - rhs;
193 if (delta != IntegerValue(0)) {
194 CHECK_GE(delta, IntegerValue(0));
215 if (min_not_encoded == max_not_encoded) {
216 const IntegerValue rhs = min_not_encoded;
218 encoding_ct.
AddTerm(var, IntegerValue(1));
219 for (
const auto value_literal : encoding) {
221 rhs - value_literal.value));
235 const IntegerValue d_min = min_not_encoded;
237 lower_bound_ct.
AddTerm(var, IntegerValue(1));
238 for (
const auto value_literal : encoding) {
240 d_min - value_literal.value));
250 const IntegerValue d_max = max_not_encoded;
252 upper_bound_ct.
AddTerm(var, IntegerValue(1));
253 for (
const auto value_literal : encoding) {
255 d_max - value_literal.value));
272 if (integer_trail ==
nullptr || encoder ==
nullptr)
return;
274 const auto& greater_than_encoding = encoder->PartialGreaterThanEncoding(var);
275 if (greater_than_encoding.empty())
return;
280 IntegerValue prev_used_bound = integer_trail->LowerBound(var);
282 builder.
AddTerm(var, IntegerValue(1));
284 for (
const auto entry : greater_than_encoding) {
285 if (entry.value <= prev_used_bound)
continue;
287 const LiteralIndex literal_index = entry.literal.Index();
288 const IntegerValue diff = prev_used_bound - entry.value;
297 prev_used_bound = entry.value;
298 prev_literal_index = literal_index;
308 IntegerValue prev_used_bound = integer_trail->LowerBound(
NegationOf(var));
310 builder.
AddTerm(var, IntegerValue(-1));
311 for (
const auto entry :
312 encoder->PartialGreaterThanEncoding(
NegationOf(var))) {
313 if (entry.value <= prev_used_bound)
continue;
314 const IntegerValue diff = prev_used_bound - entry.value;
318 prev_used_bound = entry.value;
328bool AllLiteralsHaveViews(
const IntegerEncoder& encoder,
329 absl::Span<const Literal> literals) {
330 for (
const Literal lit : literals) {
331 if (!encoder.LiteralOrNegationHasView(lit))
return false;
343 CHECK(lc.AddLiteralTerm(mapping->Literal(
NegatedRef(enforcement_ref)),
347 CHECK(lc.AddLiteralTerm(mapping->Literal(ref), IntegerValue(1)));
368 {enforcement, mapping->
Literal(ref).Negated()});
389 if (activity_helper !=
nullptr) {
390 std::vector<int> negated_lits;
394 for (absl::Span<const int> part :
397 for (
const int negated_ref : part) {
402 mapping->Literal(
NegatedRef(enforcement_ref)), IntegerValue(-1)));
413 mapping->Literal(
NegatedRef(enforcement_ref)), IntegerValue(-1)));
436 const std::vector<Literal> literals =
438 if (AllLiteralsHaveViews(*encoder, literals)) {
440 for (
const Literal lit : literals) {
455 if (num_literals == 1) {
460 encoder->GetOrCreateLiteralAssociatedToEquality(var, IntegerValue(1));
464 if (num_literals == 2) {
467 encoder->GetOrCreateLiteralAssociatedToEquality(var, IntegerValue(1));
473 encoder->AssociateToIntegerEqualValue(lit.
Negated(), var2, IntegerValue(1));
478 std::vector<Literal> literals;
480 for (
int i = 0;
i < num_literals; ++
i) {
483 encoder->GetOrCreateLiteralAssociatedToEquality(var, IntegerValue(1));
484 literals.push_back(lit);
502 absl::btree_map<int, std::vector<Literal>> incoming_arc_constraints;
503 absl::btree_map<int, std::vector<Literal>> outgoing_arc_constraints;
504 for (
int i = 0;
i < num_arcs;
i++) {
508 outgoing_arc_constraints[tail].push_back(arc);
509 incoming_arc_constraints[head].push_back(arc);
511 for (
const auto* node_map :
512 {&outgoing_arc_constraints, &incoming_arc_constraints}) {
513 for (
const auto& entry : *node_map) {
514 const std::vector<Literal>& exactly_one = entry.second;
515 if (exactly_one.size() > 1) {
518 for (
const Literal l : exactly_one) {
542 absl::btree_map<int, std::vector<Literal>> incoming_arc_constraints;
543 absl::btree_map<int, std::vector<Literal>> outgoing_arc_constraints;
544 for (
int i = 0;
i < num_arcs;
i++) {
548 outgoing_arc_constraints[tail].push_back(arc);
549 incoming_arc_constraints[head].push_back(arc);
551 for (
const auto* node_map :
552 {&outgoing_arc_constraints, &incoming_arc_constraints}) {
553 for (
const auto& entry : *node_map) {
554 if (entry.first == 0)
continue;
555 const std::vector<Literal>& exactly_one = entry.second;
556 if (exactly_one.size() > 1) {
559 for (
const Literal l : exactly_one) {
571 for (
const Literal& incoming_arc : incoming_arc_constraints[0]) {
572 CHECK(zero_node_balance_lc.
AddLiteralTerm(incoming_arc, IntegerValue(1)));
574 for (
const Literal& outgoing_arc : outgoing_arc_constraints[0]) {
575 CHECK(zero_node_balance_lc.
AddLiteralTerm(outgoing_arc, IntegerValue(-1)));
591 num_nodes, tails, heads, literals, m));
596 std::vector<int> tails(ct.
routes().
tails().begin(),
598 std::vector<int> heads(ct.
routes().
heads().begin(),
604 for (
int i = 0;
i < ct.
routes().tails_size(); ++
i) {
605 num_nodes = std::max(num_nodes, 1 + ct.
routes().
tails(
i));
606 num_nodes = std::max(num_nodes, 1 + ct.
routes().
heads(
i));
609 if (num_dimensions == 0) {
614 std::vector<AffineExpression> flat_node_dim_expressions(
616 for (
int d = 0; d < num_dimensions; ++d) {
618 for (
int n = 0; n < node_exprs.size(); ++n) {
621 flat_node_dim_expressions[n * num_dimensions + d];
622 if (expr.
vars().empty()) {
632 num_nodes, tails, heads, literals, flat_node_dim_expressions, m));
652 absl::Span<const AffineExpression> demands,
659 if (!integer_trail->
IsFixed(capacity)) {
665 for (
int i = 0;
i < intervals.size(); ++
i) {
666 if (repository->IsAbsent(intervals[
i]))
continue;
668 horizon, integer_trail->
UpperBound(repository->End(intervals[
i])));
671 const IntegerValue capacity_value = integer_trail->
FixedValue(capacity);
672 for (
int i = 0;
i < intervals.size(); ++
i) {
673 if (!repository->IsPresent(intervals[
i]))
continue;
675 if (integer_trail->
IsFixed(demands[
i]) &&
676 integer_trail->
FixedValue(demands[
i]) == capacity_value &&
679 integer_trail->
LowerBound(repository->Size(intervals[
i])) > 0) {
688std::optional<AffineExpression> DetectMakespanFromPrecedences(
689 const SchedulingConstraintHelper& helper,
Model* model) {
690 if (helper.NumTasks() == 0)
return {};
692 const absl::Span<const AffineExpression> ends = helper.Ends();
693 std::vector<IntegerVariable> end_vars;
694 for (
const AffineExpression&
end : ends) {
697 if (
end.coeff != 1)
return {};
698 end_vars.push_back(
end.var);
701 std::vector<FullIntegerPrecedence> output;
704 for (
const auto& p : output) {
706 if (p.indices.size() != ends.size())
continue;
711 for (
int i = 0;
i < p.indices.size(); ++
i) {
721 std::min(min_delta, p.offsets[
i] - ends[p.indices[
i]].constant);
723 VLOG(2) <<
"Makespan detected >= ends + " << min_delta;
738 std::vector<IntervalVariable> intervals =
740 const IntegerValue one(1);
741 std::vector<AffineExpression> demands(intervals.size(), one);
744 std::optional<AffineExpression> makespan;
745 const std::optional<int> makespan_index =
747 if (makespan_index.has_value()) {
748 makespan = repository->
Start(intervals[makespan_index.value()]);
750 intervals.erase(intervals.begin() + makespan_index.value());
758 if (!makespan.has_value()) {
759 makespan = DetectMakespanFromPrecedences(*helper, model);
774 std::vector<IntervalVariable> intervals =
776 std::vector<AffineExpression> demands =
779 const std::optional<int> makespan_index =
781 std::optional<AffineExpression> makespan;
783 if (makespan_index.has_value()) {
785 makespan = repository->
Start(intervals[makespan_index.value()]);
786 demands.erase(demands.begin() + makespan_index.value());
787 intervals.erase(intervals.begin() + makespan_index.value());
796 if (!makespan.has_value()) {
797 makespan = DetectMakespanFromPrecedences(*helper, model);
815 const std::optional<AffineExpression>& makespan,
817 const int num_intervals = helper->
NumTasks();
822 int num_variable_energies = 0;
823 int num_optionals = 0;
824 int64_t sizes_gcd = 0;
825 int64_t demands_gcd = 0;
826 int64_t num_active_intervals = 0;
828 for (
int index = 0; index < num_intervals; ++index) {
829 if (helper->
IsAbsent(index))
continue;
835 if (demands_helper->
EnergyMin(index) > 0) {
843 num_variable_energies++;
845 if (sizes_gcd != 1) {
847 sizes_gcd = std::gcd(helper->
SizeMin(index).value(), sizes_gcd);
852 if (demands_gcd != 1) {
855 std::gcd(demands_helper->
DemandMin(index).value(), demands_gcd);
860 num_active_intervals++;
861 min_of_starts = std::min(min_of_starts, helper->
StartMin(index));
862 max_of_ends = std::max(max_of_ends, helper->
EndMax(index));
865 VLOG(2) <<
"Span [" << min_of_starts <<
".." << max_of_ends <<
"] with "
866 << num_optionals <<
" optional intervals, and "
867 << num_variable_energies <<
" variable energy tasks out of "
868 << num_active_intervals <<
"/" << num_intervals <<
" intervals"
869 << (makespan.has_value() ?
", and 1 makespan" :
"")
870 <<
" sizes_gcd: " << sizes_gcd <<
" demands_gcd: " << demands_gcd;
873 if (num_active_intervals == 0)
return;
877 if (num_variable_energies + num_optionals == 0 && sizes_gcd == 1 &&
883 if (sizes_gcd != 1 && !makespan.has_value()) {
884 VLOG(2) <<
"Cumulative relaxation: sizes_gcd = " << sizes_gcd
885 <<
", demands_gcd = " << demands_gcd
886 <<
", no makespan, capacity is " << capacity.
DebugString();
889 if (!integer_trail->
IsFixed(capacity)) demands_gcd = 1;
891 for (
int index = 0; index < num_intervals; ++index) {
892 if (helper->
IsAbsent(index))
continue;
893 if (helper->
SizeMax(index) == 0 ||
899 const IntegerValue energy_min = demands_helper->
EnergyMin(index);
900 if (energy_min == 0)
continue;
901 DCHECK_EQ(energy_min % (sizes_gcd * demands_gcd), 0);
903 energy_min / sizes_gcd / demands_gcd)) {
908 std::vector<LiteralValueValue> product =
910 if (!product.empty()) {
914 DCHECK_EQ(entry.left_value % sizes_gcd, 0);
915 entry.left_value /= sizes_gcd;
916 DCHECK_EQ(entry.right_value % demands_gcd, 0);
917 entry.right_value /= demands_gcd;
922 const IntegerValue local_size =
924 DCHECK_EQ(local_size % sizes_gcd, 0);
925 if (demands_gcd == 1) {
927 local_size / sizes_gcd);
929 const IntegerValue local_demand =
931 DCHECK_EQ(local_demand % demands_gcd, 0);
932 lc.
AddConstant(local_size * local_demand / sizes_gcd / demands_gcd);
939 if (integer_trail->
IsFixed(capacity)) {
940 const IntegerValue span = max_of_ends - min_of_starts;
941 const IntegerValue fixed_capacity = integer_trail->
FixedValue(capacity);
946 DCHECK_EQ(demands_gcd, 1);
947 lc.
AddTerm(capacity, -(max_of_ends - min_of_starts) / sizes_gcd);
956 for (
int index = 0; index < num_intervals; ++index) {
957 if (helper->
IsAbsent(index))
continue;
959 const IntegerValue energy_min = demands_helper->
EnergyMin(index);
960 if (energy_min == 0)
continue;
965 const std::vector<LiteralValueValue>& product =
967 if (!product.empty()) {
975 demands_helper->
Demands()[index],
986 IntegerValue max_for_overflow_check = std::max(-min_of_starts, max_of_ends);
987 if (makespan.has_value()) {
988 max_for_overflow_check = std::max(
989 max_for_overflow_check, integer_trail->
UpperBound(makespan.value()));
997 makespan.has_value() ? makespan.value() : max_of_ends;
1003 absl::Span<const int> component,
Model* model,
1006 std::optional<Rectangle> bounding_box;
1008 for (
const int b : component) {
1011 if (curr_bounding_box.
x_min > curr_bounding_box.
x_max ||
1012 curr_bounding_box.
y_min > curr_bounding_box.
y_max) {
1016 if (bounding_box.has_value()) {
1017 bounding_box->GrowToInclude(
1024 if (!bounding_box.has_value()) {
1029 const IntegerValue max_area = bounding_box->CapArea();
1033 for (
const int b : component) {
1039 const std::vector<LiteralValueValue> energy =
1040 product_decomposer->
TryToDecompose(x_size_affine, y_size_affine);
1041 if (!energy.empty()) {
1051 const Literal presence_literal =
1055 const auto& [x_size, y_size] =
1057 const IntegerValue area_min = x_size * y_size;
1066 manager->
Add(std::move(ct));
1076 std::vector<IntervalVariable> x_intervals =
1078 std::vector<IntervalVariable> y_intervals =
1083 intervals_repository->GetOrCreate2DHelper(x_intervals, y_intervals);
1087 result.only_run_at_level_zero =
true;
1090 &no_overlap_helper->x_helper(), model, &result.vars,
1093 &no_overlap_helper->y_helper(), model, &result.vars,
1095 result.generate_cuts = [no_overlap_helper, model, product_decomposer,
1096 last_level_zero_bound_change_idx = int64_t{-1}](
1098 if (last_level_zero_bound_change_idx ==
1099 no_overlap_helper->LastLevelZeroChangeIdx()) {
1102 last_level_zero_bound_change_idx =
1103 no_overlap_helper->LastLevelZeroChangeIdx();
1104 for (
const auto& component :
1105 no_overlap_helper->connected_components().AsVectorOfSpan()) {
1107 component, model, no_overlap_helper, manager, product_decomposer);
1121 for (
int i = 0;
i < ct.
lin_max().exprs_size(); ++
i) {
1137 IntegerVariable var;
1138 std::vector<std::pair<IntegerValue, IntegerValue>> affines;
1140 CollectAffineExpressionWithSingleVariable(ct, mapping, &var, &affines);
1157 IntegerVariable var;
1158 std::vector<std::pair<IntegerValue, IntegerValue>> affines;
1160 CollectAffineExpressionWithSingleVariable(ct, mapping, &var, &affines);
1172 target_expr, var, affines,
"AffineMax", model));
1180 absl::Span<const Literal> alternative_literals,
1181 absl::Span<const LinearExpression> exprs,
1183 const int num_exprs = exprs.size();
1187 for (
int i = 0;
i < num_exprs; ++
i) {
1190 local_expr.
vars.push_back(target);
1191 local_expr.
coeffs = exprs[
i].coeffs;
1192 local_expr.
coeffs.push_back(IntegerValue(1));
1195 local_expr.
coeffs, exprs[
i].offset, model);
1202 std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
1203 num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
1207 absl::flat_hash_map<std::pair<int, IntegerVariable>, IntegerValue> cache;
1208 for (
int i = 0;
i < num_exprs; ++
i) {
1209 for (
int j = 0; j < exprs[
i].vars.size(); ++j) {
1210 cache[std::make_pair(
i, exprs[
i].vars[j])] = exprs[
i].coeffs[j];
1213 const auto get_coeff = [&cache](IntegerVariable var,
int index) {
1214 const auto it = cache.find(std::make_pair(index, var));
1215 if (it == cache.end())
return IntegerValue(0);
1220 std::vector<IntegerVariable> active_vars;
1221 for (
int i = 0;
i + 1 < num_exprs; ++
i) {
1222 for (
int j =
i + 1; j < num_exprs; ++j) {
1223 active_vars = exprs[
i].vars;
1224 active_vars.insert(active_vars.end(), exprs[j].vars.begin(),
1225 exprs[j].vars.end());
1227 for (
const IntegerVariable x_var : active_vars) {
1228 const IntegerValue diff = get_coeff(x_var, j) - get_coeff(x_var,
i);
1229 if (diff == 0)
continue;
1233 sum_of_max_corner_diff[
i][j] += std::max(diff * lb, diff * ub);
1234 sum_of_max_corner_diff[j][
i] += std::max(-diff * lb, -diff * ub);
1239 for (
int i = 0;
i < num_exprs; ++
i) {
1241 lc.
AddTerm(target, IntegerValue(1));
1242 for (
int j = 0; j < exprs[
i].vars.size(); ++j) {
1243 lc.
AddTerm(exprs[
i].vars[j], -exprs[
i].coeffs[j]);
1245 for (
int j = 0; j < num_exprs; ++j) {
1247 -exprs[j].offset - sum_of_max_corner_diff[
i][j]));
1254 bool linearize_enforced_constraints,
1267 const IntegerValue rhs_domain_min = IntegerValue(ct.
linear().
domain(0));
1268 const IntegerValue rhs_domain_max =
1270 if (rhs_domain_min == std::numeric_limits<int64_t>::min() &&
1271 rhs_domain_max == std::numeric_limits<int64_t>::max())
1276 for (
int i = 0;
i < ct.
linear().vars_size();
i++) {
1279 lc.
AddTerm(mapping->Integer(ref), IntegerValue(coeff));
1286 if (!linearize_enforced_constraints)
return;
1294 if (!mapping->IsHalfEncodingConstraint(&ct) && ct.
linear().
vars_size() <= 1 &&
1299 std::vector<Literal> enforcing_literals;
1302 enforcing_literals.push_back(mapping->Literal(enforcement_ref));
1306 std::vector<std::pair<int, int64_t>> bool_terms;
1307 IntegerValue min_activity(0);
1308 IntegerValue max_activity(0);
1310 for (
int i = 0;
i < ct.
linear().vars_size();
i++) {
1313 const IntegerVariable int_var = mapping->Integer(ref);
1318 const IntegerValue lb = integer_trail->LowerBound(int_var);
1319 const IntegerValue ub = integer_trail->UpperBound(int_var);
1320 if (lb == 0 && ub == 1 && activity_helper !=
nullptr) {
1321 bool_terms.push_back({ref, coeff.value()});
1324 min_activity += coeff * lb;
1325 max_activity += coeff * ub;
1327 min_activity += coeff * ub;
1328 max_activity += coeff * lb;
1332 if (activity_helper !=
nullptr) {
1339 if (rhs_domain_min > min_activity) {
1344 const IntegerValue term =
CapSubI(rhs_domain_min, min_activity);
1346 for (
const Literal& literal : enforcing_literals) {
1349 for (
int i = 0;
i < ct.
linear().vars_size();
i++) {
1352 const IntegerVariable int_var = mapping->Integer(ref);
1360 if (rhs_domain_max < max_activity) {
1365 const IntegerValue term =
CapSubI(rhs_domain_max, max_activity);
1367 for (
const Literal& literal : enforcing_literals) {
1370 for (
int i = 0;
i < ct.
linear().vars_size();
i++) {
1373 const IntegerVariable int_var = mapping->Integer(ref);
1396 int linearization_level,
Model* model,
1400 DCHECK_GT(linearization_level, 0);
1405 if (linearization_level > 1) {
1411 if (linearization_level > 1) {
1428 int_prod.
exprs(1))) {
1439 const bool is_affine_max =
1441 if (is_affine_max) {
1446 if (linearization_level > 1) {
1447 if (is_affine_max) {
1462 ct, linearization_level > 1, model,
1463 relaxation, activity_helper);
1468 if (linearization_level > 1) {
1475 if (linearization_level > 1) {
1495 if (linearization_level > 1) {
1511 LOG(INFO) <<
"Possible overflow in linearization of: "
1512 << google::protobuf::ShortFormat(ct);
1532 IntegerValue x_lb = integer_trail->
LowerBound(x);
1533 IntegerValue x_ub = integer_trail->
UpperBound(x);
1534 IntegerValue y_lb = integer_trail->
LowerBound(y);
1535 IntegerValue y_ub = integer_trail->
UpperBound(y);
1538 if (x_lb < 0 && x_ub > 0)
return;
1539 if (y_lb < 0 && y_ub > 0)
return;
1553 z, x, y, linearization_level, m));
1565 IntegerValue x_lb = integer_trail->LowerBound(x);
1566 IntegerValue x_ub = integer_trail->UpperBound(x);
1568 if (x_lb == x_ub)
return;
1571 if (x_lb < 0 && x_ub > 0)
return;
1576 const IntegerValue tmp = x_ub;
1582 if (x_ub > (int64_t{1} << 31))
return;
1591 if (x_lb + 1 < x_ub) {
1607 const IntegerValue x_lb = integer_trail->LowerBound(x);
1608 const IntegerValue x_ub = integer_trail->UpperBound(x);
1611 if (x_lb < 0 && x_ub > 0)
return;
1623 int linearization_level,
Model* m,
1630 const std::vector<AffineExpression> exprs =
1637 if (integer_trail->IsFixed(expr)) {
1638 union_of_domains = union_of_domains.
UnionWith(
1639 Domain(integer_trail->FixedValue(expr).value()));
1641 union_of_domains = union_of_domains.
UnionWith(
1642 integer_trail->InitialVariableDomain(expr.var)
1643 .MultiplicationBy(expr.coeff.value())
1644 .AdditionWith(
Domain(expr.constant.value())));
1648 if (union_of_domains.
Size() == num_exprs) {
1650 int64_t sum_of_values = 0;
1651 for (
const int64_t v : union_of_domains.
Values()) {
1659 }
else if (num_exprs <=
1661 linearization_level > 1) {
1670 if (intervals_repository->
IsAbsent(interval)) {
1675 if (!intervals_repository->
IsPresent(interval)) {
1680 if (intervals_repository->
MinSize(interval) !=
1681 intervals_repository->
MaxSize(interval)) {
1691 const std::optional<AffineExpression>& makespan,
1694 helper, demands_helper, capacity, m));
1699 helper, demands_helper, capacity, m));
1703 bool has_variable_part =
false;
1707 has_variable_part =
true;
1712 has_variable_part =
true;
1716 if (has_variable_part || !integer_trail->
IsFixed(capacity)) {
1718 helper, demands_helper, capacity, makespan, m));
1723 const std::optional<AffineExpression>& makespan,
1731 bool has_variable_or_optional_part =
false;
1735 has_variable_or_optional_part =
true;
1739 if (has_variable_or_optional_part) {
1750 std::vector<IntervalVariable> x_intervals =
1752 std::vector<IntervalVariable> y_intervals =
1764 bool has_variable_part =
false;
1765 for (
int i = 0;
i < x_intervals.size(); ++
i) {
1767 if (intervals_repository->
IsAbsent(x_intervals[
i]) ||
1768 intervals_repository->
IsAbsent(y_intervals[
i])) {
1773 if (!intervals_repository->
IsPresent(x_intervals[
i]) ||
1774 !intervals_repository->
IsPresent(y_intervals[
i])) {
1775 has_variable_part =
true;
1780 if (intervals_repository->
MinSize(x_intervals[
i]) !=
1781 intervals_repository->
MaxSize(x_intervals[
i]) ||
1782 intervals_repository->
MinSize(y_intervals[
i]) !=
1783 intervals_repository->
MaxSize(y_intervals[
i])) {
1784 has_variable_part =
true;
1789 if (!has_variable_part)
return;
1806 const IntegerVariable target =
1808 std::vector<LinearExpression> exprs;
1810 for (
int i = 0;
i < ct.
lin_max().exprs_size(); ++
i) {
1817 const std::vector<Literal> alternative_literals =
1827 std::vector<IntegerVariable> z_vars;
1829 for (
const Literal lit : alternative_literals) {
1830 z_vars.push_back(encoder->GetLiteralView(lit));
1849 int num_exactly_one_elements = 0;
1850 for (
const IntegerVariable var :
1851 element_encodings->GetElementEncodedVariables()) {
1852 for (
const auto& [index, literal_value_list] :
1853 element_encodings->Get(var)) {
1855 for (
const auto& literal_value : literal_value_list) {
1856 min_value = std::min(min_value, literal_value.value);
1860 builder.
AddTerm(var, IntegerValue(-1));
1861 for (
const auto& [value, literal] : literal_value_list) {
1862 const IntegerValue delta_min = value - min_value;
1863 if (delta_min != 0) {
1870 ++num_exactly_one_elements;
1878 if (num_exactly_one_elements != 0) {
1881 "[ElementLinearRelaxation]"
1882 " #from_exactly_one:",
1883 num_exactly_one_elements);
1895 activity_bound_helper.AddAllAtMostOnes(model_proto);
1899 for (
const auto& ct : model_proto.
constraints()) {
1901 &relaxation, &activity_bound_helper);
1905 int num_loose_equality_encoding_relaxations = 0;
1906 int num_tight_equality_encoding_relaxations = 0;
1907 int num_inequality_encoding_relaxations = 0;
1910 if (mapping->IsBoolean(
i))
continue;
1912 const IntegerVariable var = mapping->Integer(
i);
1917 var, *m, &relaxation, &num_tight_equality_encoding_relaxations,
1918 &num_loose_equality_encoding_relaxations);
1933 ++num_inequality_encoding_relaxations;
1951 if (num_tight_equality_encoding_relaxations != 0 ||
1952 num_loose_equality_encoding_relaxations != 0 ||
1953 num_inequality_encoding_relaxations != 0) {
1955 "[EncodingLinearRelaxation]"
1956 " #tight_equality:",
1957 num_tight_equality_encoding_relaxations,
1958 " #loose_equality:", num_loose_equality_encoding_relaxations,
1959 " #inequality:", num_inequality_encoding_relaxations);
1964 "[LinearRelaxationBeforeCliqueExpansion]"
1975 for (
const std::vector<Literal>& at_most_one : relaxation.
at_most_ones) {
1976 if (at_most_one.empty())
continue;
1979 for (
const Literal literal : at_most_one) {
1982 const bool unused ABSL_ATTRIBUTE_UNUSED =
1999 if (lc.
lb > 0 || lc.
ub < 0) {
2034 "[FinalLinearRelaxation]"
DomainIteratorBeginEnd Values() const &
Domain UnionWith(const Domain &domain) const
static IntegralType FloorOfRatio(IntegralType numerator, IntegralType denominator)
int64_t ComputeMaxActivity(absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > *conditional=nullptr)
int64_t ComputeMinActivity(absl::Span< const std::pair< int, int64_t > > terms, std::vector< std::array< int64_t, 2 > > *conditional=nullptr)
std::vector< absl::Span< const int > > PartitionLiteralsIntoAmo(absl::Span< const int > literals)
Similar algo as above for this simpler case.
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 1;
::int32_t literals(int index) const
int heads_size() const
repeated int32 heads = 4;
::int32_t heads(int index) const
int tails_size() const
repeated int32 tails = 3;
::int32_t literals(int index) const
int literals_size() const
repeated int32 literals = 5;
::int32_t tails(int index) const
ConstraintCase constraint_case() const
::int32_t enforcement_literal(int index) const
const ::operations_research::sat::BoolArgumentProto & exactly_one() const
const ::operations_research::sat::NoOverlapConstraintProto & no_overlap() const
const ::operations_research::sat::AllDifferentConstraintProto & all_diff() const
const ::operations_research::sat::LinearConstraintProto & linear() const
const ::operations_research::sat::BoolArgumentProto & at_most_one() const
const ::operations_research::sat::RoutesConstraintProto & routes() const
const ::operations_research::sat::LinearArgumentProto & lin_max() const
const ::operations_research::sat::BoolArgumentProto & bool_and() const
const ::operations_research::sat::BoolArgumentProto & bool_or() const
const ::operations_research::sat::LinearArgumentProto & int_prod() const
const ::operations_research::sat::CircuitConstraintProto & circuit() const
const ::operations_research::sat::CumulativeConstraintProto & cumulative() const
int enforcement_literal_size() const
repeated int32 enforcement_literal = 2;
bool has_no_overlap_2d() const
.operations_research.sat.NoOverlap2DConstraintProto no_overlap_2d = 21;
const ::operations_research::sat::NoOverlap2DConstraintProto & no_overlap_2d() const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
std::vector< sat::Literal > Literals(const ProtoIndices &indices) const
IntegerVariable Integer(int ref) const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
const ::operations_research::sat::LinearExpressionProto & demands(int index) const
::int32_t intervals(int index) const
const ::operations_research::sat::LinearExpressionProto & capacity() const
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue FixedValue(IntegerVariable i) const
Checks that the variable is fixed and returns its value.
bool IsFixed(IntegerVariable i) const
Checks if the variable is fixed.
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit)
SchedulingDemandHelper * GetOrCreateDemandHelper(SchedulingConstraintHelper *helper, absl::Span< const AffineExpression > demands)
AffineExpression Start(IntervalVariable i) const
bool IsAbsent(IntervalVariable i) const
IntegerValue MaxSize(IntervalVariable i) const
Return the maximum size of the given IntervalVariable.
IntegerValue MinSize(IntervalVariable i) const
Return the minimum size of the given IntervalVariable.
SchedulingConstraintHelper * GetOrCreateHelper(const std::vector< IntervalVariable > &variables, bool register_as_disjunctive_helper=false)
NoOverlap2DConstraintHelper * GetOrCreate2DHelper(const std::vector< IntervalVariable > &x_variables, const std::vector< IntervalVariable > &y_variables)
bool IsPresent(IntervalVariable i) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
int exprs_size() const
repeated .operations_research.sat.LinearExpressionProto exprs = 2;
const ::operations_research::sat::LinearExpressionProto & target() const
void AddQuadraticLowerBound(AffineExpression left, AffineExpression right, IntegerTrail *integer_trail, bool *is_quadratic=nullptr)
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff=IntegerValue(1))
void AddTerm(IntegerVariable var, IntegerValue coeff)
void AddLinearExpression(const LinearExpression &expr)
void AddConstant(IntegerValue value)
Adds the corresponding term to the current linear expression.
void Clear()
Clears all added terms and constants. Keeps the original bounds.
LinearConstraint BuildConstraint(IntegerValue lb, IntegerValue ub)
ABSL_MUST_USE_RESULT bool AddDecomposedProduct(absl::Span< const LiteralValueValue > product)
ConstraintIndex Add(LinearConstraint ct, bool *added=nullptr, bool *folded=nullptr)
void RegisterWith(GenericLiteralWatcher *watcher)
::int32_t vars(int index) const
int vars_size() const
repeated int32 vars = 1;
::int64_t coeffs(int index) const
::int64_t domain(int index) const
int domain_size() const
repeated int64 domain = 3;
::int64_t coeffs(int index) const
::int32_t vars(int index) const
int vars_size() const
repeated int32 vars = 1;
Literal(int signed_value)
T Add(std::function< T(Model *)> f)
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
SchedulingConstraintHelper & y_helper() const
Rectangle GetLevelZeroBoundingRectangle(int index) const
bool IsPresent(int index) const
std::pair< IntegerValue, IntegerValue > GetLevelZeroBoxSizesMin(int index) const
SchedulingConstraintHelper & x_helper() const
::int32_t y_intervals(int index) const
::int32_t x_intervals(int index) const
::int32_t intervals(int index) const
void ComputeFullPrecedences(absl::Span< const IntegerVariable > vars, std::vector< FullIntegerPrecedence > *output)
Helper class to express a product as a linear constraint.
std::vector< LiteralValueValue > TryToDecompose(const AffineExpression &left, const AffineExpression &right)
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
::int32_t heads(int index) const
const ::operations_research::sat::RoutesConstraintProto_NodeExpressions & dimensions(int index) const
int literals_size() const
repeated int32 literals = 3;
int dimensions_size() const
repeated .operations_research.sat.RoutesConstraintProto.NodeExpressions dimensions = 6;
int heads_size() const
repeated int32 heads = 2;
::int32_t literals(int index) const
::int32_t tails(int index) const
int tails_size() const
repeated int32 tails = 1;
::int32_t linearization_level() const
double merge_at_most_one_work_limit() const
bool add_lin_max_cuts() const
::int32_t max_all_diff_cut_size() const
void NotifyThatModelIsUnsat()
int CurrentDecisionLevel() const
ABSL_MUST_USE_RESULT bool FinishPropagation()
bool SizeIsFixed(int t) const
int NumTasks() const
Returns the number of task.
absl::Span< const AffineExpression > Sizes() const
bool IsPresent(int t) const
Literal PresenceLiteral(int index) const
IntegerValue SizeMax(int t) const
IntegerValue StartMin(int t) const
IntegerValue SizeMin(int t) const
ABSL_MUST_USE_RESULT bool SynchronizeAndSetTimeDirection(bool is_forward)
IntegerValue EndMax(int t) const
bool IsAbsent(int t) const
bool IsOptional(int t) const
bool DemandIsFixed(int t) const
bool CacheAllEnergyValues()
const std::vector< std::vector< LiteralValueValue > > & DecomposedEnergies() const
IntegerValue DemandMax(int t) const
const std::vector< AffineExpression > & Demands() const
IntegerValue DemandMin(int t) const
IntegerValue EnergyMin(int t) const
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
std::vector< typename Map::mapped_type > Values(const Map &map, const Keys &keys)
void AppendNoOverlapRelaxationAndCutGenerator(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AppendCumulativeRelaxationAndCutGenerator(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
CutGenerator CreateCumulativeCompletionTimeCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
void AddSquareCutGenerator(const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
void AppendExactlyOneRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
bool BuildMaxAffineUpConstraint(const LinearExpression &target, IntegerVariable var, absl::Span< const std::pair< IntegerValue, IntegerValue > > affines, Model *model, LinearConstraintBuilder *builder)
std::optional< int > DetectMakespan(absl::Span< const IntervalVariable > intervals, absl::Span< const AffineExpression > demands, const AffineExpression &capacity, Model *model)
void AddCumulativeCutGenerator(const AffineExpression &capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const std::optional< AffineExpression > &makespan, Model *m, LinearRelaxation *relaxation)
void AppendLinMaxRelaxationPart2(IntegerVariable target, absl::Span< const Literal > alternative_literals, absl::Span< const LinearExpression > exprs, Model *model, LinearRelaxation *relaxation)
void AppendRoutesRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
CutGenerator CreatePositiveMultiplicationCutGenerator(AffineExpression z, AffineExpression x, AffineExpression y, int linearization_level, Model *model)
A cut generator for z = x * y (x and y >= 0).
CutGenerator CreateStronglyConnectedGraphCutGenerator(int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, Model *model)
bool ProdOverflow(IntegerValue t, IntegerValue value)
CutGenerator CreateNoOverlap2dEnergyCutGenerator(NoOverlap2DConstraintHelper *helper, Model *model)
const LiteralIndex kNoLiteralIndex(-1)
void AddMaxAffineCutGenerator(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AddCircuitCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x, AffineExpression square, IntegerValue x_value, Model *model)
CutGenerator CreateCumulativePrecedenceCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
LinearRelaxation ComputeLinearRelaxation(const CpModelProto &model_proto, Model *m)
Builds the linear relaxation of a CpModelProto.
bool HasEnforcementLiteral(const ConstraintProto &ct)
Small utility functions to deal with half-reified constraints.
void AppendLinearConstraintRelaxation(const ConstraintProto &ct, bool linearize_enforced_constraints, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
void AddIntProdCutGenerator(const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
Cut generators.
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
void AddRoutesCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
CutGenerator CreateCumulativeEnergyCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, const std::optional< AffineExpression > &makespan, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
bool PossibleOverflow(const IntegerTrail &integer_trail, const LinearConstraint &constraint)
CutGenerator CreateLinMaxCutGenerator(const IntegerVariable target, absl::Span< const LinearExpression > exprs, absl::Span< const IntegerVariable > z_vars, Model *model)
void AddIntegerVariableFromIntervals(const SchedulingConstraintHelper *helper, Model *model, std::vector< IntegerVariable > *vars, int mask)
CutGenerator CreateAllDifferentCutGenerator(absl::Span< const AffineExpression > exprs, Model *model)
void AddCumulativeRelaxation(const AffineExpression &capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const std::optional< AffineExpression > &makespan, Model *model, LinearRelaxation *relaxation)
Scheduling relaxations and cut generators.
CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x, int linearization_level, Model *model)
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
void TryToLinearizeConstraint(const CpModelProto &, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
Adds linearization of different types of constraints.
IntegerVariable PositiveVariable(IntegerVariable i)
CutGenerator CreateCumulativeTimeTableCutGenerator(SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
int64_t SafeDoubleToInt64(double value)
void AppendLinMaxRelaxationPart1(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
CutGenerator CreateNoOverlapCompletionTimeCutGenerator(SchedulingConstraintHelper *helper, Model *model)
CutGenerator CreateMaxAffineCutGenerator(LinearExpression target, IntegerVariable var, std::vector< std::pair< IntegerValue, IntegerValue > > affines, const std::string cut_name, Model *model)
int ReindexArcs(IntContainer *tails, IntContainer *heads, absl::flat_hash_map< int, int > *mapping_output=nullptr)
void AppendCircuitRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
Routing relaxation and cut generators.
CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator(NoOverlap2DConstraintHelper *helper, Model *model)
void AppendElementEncodingRelaxation(Model *m, LinearRelaxation *relaxation)
LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x, AffineExpression square, IntegerValue x_lb, IntegerValue x_ub, Model *model)
void AppendMaxAffineRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AppendNoOverlap2dRelaxationForComponent(absl::Span< const int > component, Model *model, NoOverlap2DConstraintHelper *no_overlap_helper, LinearConstraintManager *manager, ProductDecomposer *product_decomposer)
bool ExpressionsContainsOnlyOneVar(const ExpressionList &exprs)
Returns true if there exactly one variable appearing in all the expressions.
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64_t lb, int64_t ub)
CutGenerator CreateNoOverlapEnergyCutGenerator(SchedulingConstraintHelper *helper, const std::optional< AffineExpression > &makespan, Model *model)
CutGenerator CreateCVRPCutGenerator(int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, absl::Span< const AffineExpression > flat_node_dim_expressions, Model *model)
bool IntervalIsVariable(const IntervalVariable interval, IntervalsRepository *intervals_repository)
void AppendSquareRelaxation(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
CutGenerator CreateNoOverlapPrecedenceCutGenerator(SchedulingConstraintHelper *helper, Model *model)
void AddLinMaxCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
std::function< void(Model *)> ExactlyOneConstraint(absl::Span< const Literal > literals)
LinearExpression PositiveVarExpr(const LinearExpression &expr)
Returns the same expression with positive variables.
void AppendBoolAndRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
void AddAllDiffRelaxationAndCutGenerator(const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
void AppendNoOverlap2dRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
Adds the energetic relaxation sum(areas) <= bounding box area.
PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var)
void AppendAtMostOneRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AddNoOverlapCutGenerator(SchedulingConstraintHelper *helper, const std::optional< AffineExpression > &makespan, Model *m, LinearRelaxation *relaxation)
void AddNoOverlap2dCutGenerator(const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
bool VariableIsPositive(IntegerVariable i)
std::vector< Literal > CreateAlternativeLiteralsWithView(int num_literals, Model *model, LinearRelaxation *relaxation)
IntegerValue CapSubI(IntegerValue a, IntegerValue b)
bool LinearExpressionProtosAreEqual(const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
Returns true iff a == b * b_scaling.
bool AtMinOrMaxInt64I(IntegerValue t)
LinearConstraintPropagator< false > IntegerSumLE
void AppendBoolOrRelaxation(const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
void AppendRelaxationForEqualityEncoding(IntegerVariable var, const Model &model, LinearRelaxation *relaxation, int *num_tight, int *num_loose)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
var * coeff + constant >= bound.
AffineExpression Negated() const
std::string DebugString() const
IntegerLiteral LowerOrEqual(IntegerValue bound) const
var * coeff + constant <= bound.
std::unique_ptr< IntegerValue[]> coeffs
std::unique_ptr< IntegerVariable[]> vars
std::vector< IntegerVariable > vars
std::vector< IntegerValue > coeffs
std::vector< CutGenerator > cut_generators
std::vector< std::vector< Literal > > at_most_ones
std::vector< LinearConstraint > linear_constraints
#define SOLVER_LOG(logger,...)