25#include "absl/container/btree_map.h"
26#include "absl/container/btree_set.h"
27#include "absl/container/flat_hash_map.h"
28#include "absl/container/flat_hash_set.h"
29#include "absl/log/check.h"
30#include "absl/meta/type_traits.h"
31#include "absl/strings/str_cat.h"
32#include "absl/types/span.h"
42#include "ortools/sat/cp_model.pb.h"
58#include "ortools/sat/sat_parameters.pb.h"
71template <
typename Values>
72std::vector<int64_t> ValuesFromProto(
const Values& values) {
73 return std::vector<int64_t>(values.begin(), values.end());
76void ComputeLinearBounds(
const LinearConstraintProto& proto,
78 int64_t* sum_min, int64_t* sum_max) {
82 for (
int i = 0;
i < proto.vars_size(); ++
i) {
83 const int64_t coeff = proto.coeffs(
i);
84 const IntegerVariable var = mapping->Integer(proto.vars(
i));
85 const int64_t lb = integer_trail->LowerBound(var).value();
86 const int64_t ub = integer_trail->UpperBound(var).value();
88 (*sum_min) += coeff * lb;
89 (*sum_max) += coeff * ub;
91 (*sum_min) += coeff * ub;
92 (*sum_max) += coeff * lb;
98bool ConstraintIsEq(
const LinearConstraintProto& proto) {
99 return proto.domain_size() == 2 && proto.domain(0) == proto.domain(1);
103bool ConstraintIsNEq(
const LinearConstraintProto& proto,
105 int64_t* single_value) {
108 ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max);
110 const Domain complement =
111 Domain(sum_min, sum_max)
113 if (complement.IsEmpty())
return false;
114 const int64_t value = complement.
Min();
116 if (complement.Size() == 1) {
117 if (single_value !=
nullptr) {
118 *single_value = value;
128 bool view_all_booleans_as_integers,
Model* m) {
130 const int num_proto_variables = model_proto.variables_size();
136 CHECK_EQ(sat_solver->NumVariables(), 0);
138 BooleanVariable new_var(0);
139 std::vector<BooleanVariable> false_variables;
140 std::vector<BooleanVariable> true_variables;
143 mapping->reverse_boolean_map_.resize(num_proto_variables, -1);
144 for (
int i = 0;
i < num_proto_variables; ++
i) {
145 const auto& domain = model_proto.variables(
i).domain();
146 if (domain.size() != 2)
continue;
147 if (domain[0] >= 0 && domain[1] <= 1) {
148 mapping->booleans_[
i] = new_var;
149 mapping->reverse_boolean_map_[new_var] =
i;
150 if (domain[1] == 0) {
151 false_variables.push_back(new_var);
152 }
else if (domain[0] == 1) {
153 true_variables.push_back(new_var);
159 sat_solver->SetNumVariables(new_var.value());
160 for (
const BooleanVariable var : true_variables) {
163 for (
const BooleanVariable var : false_variables) {
170 std::vector<int> var_to_instantiate_as_integer;
171 if (view_all_booleans_as_integers) {
172 var_to_instantiate_as_integer.resize(num_proto_variables);
173 for (
int i = 0;
i < num_proto_variables; ++
i) {
174 var_to_instantiate_as_integer[
i] =
i;
178 absl::flat_hash_set<int> used_variables;
180 const bool some_linerization =
181 m->
GetOrCreate<SatParameters>()->linearization_level() > 0;
184 for (
int c = 0; c < model_proto.constraints_size(); ++c) {
185 const ConstraintProto& ct = model_proto.constraints(c);
193 if (some_linerization) {
194 if (ct.constraint_case() == ConstraintProto::kCircuit) {
195 for (
const int ref : ct.circuit().literals()) {
198 }
else if (ct.constraint_case() == ConstraintProto::kRoutes) {
199 for (
const int ref : ct.routes().literals()) {
208 if (model_proto.has_objective()) {
209 for (
const int obj_var : model_proto.objective().vars()) {
216 for (
int i = 0;
i < num_proto_variables; ++
i) {
218 used_variables.insert(
i);
223 var_to_instantiate_as_integer.assign(used_variables.begin(),
224 used_variables.end());
233 int reservation_size = var_to_instantiate_as_integer.size();
234 for (
const ConstraintProto& ct : model_proto.constraints()) {
235 if (ct.constraint_case() != ConstraintProto::kLinear)
continue;
236 const int ct_size = ct.linear().vars().size();
238 reservation_size +=
static_cast<int>(std::round(std::sqrt(ct_size)));
241 if (model_proto.has_objective()) {
242 reservation_size += 1;
243 const int ct_size = model_proto.objective().vars().size() + 1;
245 reservation_size +=
static_cast<int>(std::round(std::sqrt(ct_size)));
253 mapping->reverse_integer_map_.resize(2 * var_to_instantiate_as_integer.size(),
255 for (
const int i : var_to_instantiate_as_integer) {
256 const auto& var_proto = model_proto.variables(
i);
257 mapping->integers_[
i] =
259 DCHECK_LT(mapping->integers_[
i], mapping->reverse_integer_map_.size());
260 mapping->reverse_integer_map_[mapping->integers_[
i]] =
i;
267 for (
int i = 0;
i < num_proto_variables; ++
i) {
272 encoder->AssociateToIntegerEqualValue(
278 mapping->intervals_.resize(model_proto.constraints_size(),
280 for (
int c = 0; c < model_proto.constraints_size(); ++c) {
281 const ConstraintProto& ct = model_proto.constraints(c);
282 if (ct.constraint_case() != ConstraintProto::ConstraintCase::kInterval) {
287 mapping->
Literal(ct.enforcement_literal(0));
291 mapping->intervals_[c] = intervals_repository->CreateInterval(
292 mapping->Affine(ct.interval().start()),
293 mapping->Affine(ct.interval().end()),
294 mapping->Affine(ct.interval().size()), enforcement_literal.
Index(),
297 mapping->intervals_[c] = intervals_repository->CreateInterval(
298 mapping->Affine(ct.interval().start()),
299 mapping->Affine(ct.interval().end()),
303 mapping->already_loaded_ct_.insert(&ct);
309 const SymmetryProto& symmetry = model_proto.symmetry();
310 if (symmetry.permutations().empty())
return;
313 const int num_vars = model_proto.variables().size();
314 std::vector<bool> can_be_used_in_symmetry(num_vars,
true);
317 for (
int v = 0; v < num_vars; ++v) {
318 if (!mapping->IsBoolean(v)) can_be_used_in_symmetry[v] =
false;
329 const int num_constraints = model_proto.constraints().size();
330 for (
int c = 0; c < num_constraints; ++c) {
331 const ConstraintProto& ct = model_proto.constraints(c);
332 if (ct.constraint_case() != ConstraintProto::kLinear)
continue;
333 if (ct.linear().domain().size() <= 2)
continue;
338 for (
const int ref : ct.linear().vars()) {
345 sat_solver->AddPropagator(symmetry_handler);
346 const int num_literals = 2 * sat_solver->NumVariables();
348 for (
const SparsePermutationProto& perm : symmetry.permutations()) {
349 bool can_be_used =
true;
350 for (
const int var : perm.support()) {
351 if (!can_be_used_in_symmetry[var]) {
356 if (!can_be_used)
continue;
359 auto literal_permutation =
360 std::make_unique<SparsePermutation>(num_literals);
361 int support_index = 0;
362 const int num_cycle = perm.cycle_sizes().size();
363 for (
int i = 0;
i < num_cycle; ++
i) {
364 const int size = perm.cycle_sizes(
i);
365 const int saved_support_index = support_index;
366 for (
int j = 0; j < size; ++j) {
367 const int var = perm.support(support_index++);
368 literal_permutation->AddToCurrentCycle(
369 mapping->Literal(var).Index().value());
371 literal_permutation->CloseCurrentCycle();
375 support_index = saved_support_index;
376 for (
int j = 0; j < size; ++j) {
377 const int var = perm.support(support_index++);
378 literal_permutation->AddToCurrentCycle(
379 mapping->Literal(var).NegatedIndex().value());
381 literal_permutation->CloseCurrentCycle();
383 symmetry_handler->AddSymmetry(std::move(literal_permutation));
387 symmetry_handler->num_permutations(),
388 " symmetry to the SAT solver.");
405 if (sat_solver->ModelIsUnsat())
return;
410 struct EqualityDetectionHelper {
411 const ConstraintProto* ct;
416 bool operator<(
const EqualityDetectionHelper& o)
const {
417 if (literal.
Variable() == o.literal.Variable()) {
418 if (value == o.value)
return is_equality && !o.is_equality;
419 return value < o.value;
421 return literal.
Variable() < o.literal.Variable();
424 std::vector<std::vector<EqualityDetectionHelper>> var_to_equalities(
425 model_proto.variables_size());
437 struct InequalityDetectionHelper {
438 const ConstraintProto* ct;
442 bool operator<(
const InequalityDetectionHelper& o)
const {
443 if (literal.
Variable() == o.literal.Variable()) {
444 return i_lit.
var < o.i_lit.var;
446 return literal.
Variable() < o.literal.Variable();
449 std::vector<InequalityDetectionHelper> inequalities;
452 for (
const ConstraintProto& ct : model_proto.constraints()) {
453 if (ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
456 if (ct.enforcement_literal().size() != 1)
continue;
457 if (ct.linear().vars_size() != 1)
continue;
461 mapping->
Literal(ct.enforcement_literal(0));
462 if (sat_solver->Assignment().LiteralIsFalse(enforcement_literal))
continue;
464 const int ref = ct.linear().vars(0);
468 const Domain domain_if_enforced =
473 if (domain_if_enforced.
IsEmpty()) {
474 if (!sat_solver->AddUnitClause(enforcement_literal.
Negated()))
return;
480 if (domain_if_enforced.
Max() >= domain.
Max() &&
481 domain_if_enforced.
Min() > domain.
Min()) {
482 inequalities.push_back({&ct, enforcement_literal,
484 mapping->Integer(var),
485 IntegerValue(domain_if_enforced.
Min()))});
486 }
else if (domain_if_enforced.
Min() <= domain.
Min() &&
487 domain_if_enforced.
Max() < domain.
Max()) {
488 inequalities.push_back({&ct, enforcement_literal,
490 mapping->Integer(var),
491 IntegerValue(domain_if_enforced.
Max()))});
497 if (domain_if_enforced.
Min() > domain.
Min()) {
501 mapping->Integer(var), IntegerValue(domain_if_enforced.
Min())));
503 if (domain_if_enforced.
Max() < domain.
Max()) {
507 IntegerValue(domain_if_enforced.
Max())));
518 if (inter.
Min() == 0) {
519 detector->ProcessConditionalZero(enforcement_literal,
520 mapping->Integer(var));
522 var_to_equalities[var].push_back(
523 {&ct, enforcement_literal, inter.
Min(),
true});
530 var_to_equalities[var].push_back(
531 {&ct, enforcement_literal, inter.
Min(),
false});
537 int num_inequalities = 0;
538 std::sort(inequalities.begin(), inequalities.end());
539 for (
int i = 0;
i + 1 < inequalities.size();
i++) {
540 if (inequalities[
i].literal != inequalities[
i + 1].literal.Negated()) {
547 if (integer_trail->IntegerLiteralIsTrue(inequalities[
i].i_lit) ||
548 integer_trail->IntegerLiteralIsFalse(inequalities[
i].i_lit)) {
551 if (integer_trail->IntegerLiteralIsTrue(inequalities[
i + 1].i_lit) ||
552 integer_trail->IntegerLiteralIsFalse(inequalities[
i + 1].i_lit)) {
556 const auto pair_a = encoder->Canonicalize(inequalities[
i].i_lit);
557 const auto pair_b = encoder->Canonicalize(inequalities[
i + 1].i_lit);
558 if (pair_a.first == pair_b.second) {
560 encoder->AssociateToIntegerLiteral(inequalities[
i].literal,
561 inequalities[
i].i_lit);
562 mapping->already_loaded_ct_.insert(inequalities[
i].ct);
563 mapping->already_loaded_ct_.insert(inequalities[
i + 1].ct);
568 int num_half_inequalities = 0;
569 for (
const auto inequality : inequalities) {
570 if (mapping->ConstraintIsAlreadyLoaded(inequality.ct))
continue;
573 encoder->GetOrCreateAssociatedLiteral(inequality.i_lit)));
574 if (sat_solver->ModelIsUnsat())
return;
576 ++num_half_inequalities;
577 mapping->already_loaded_ct_.insert(inequality.ct);
578 mapping->is_half_encoding_ct_.insert(inequality.ct);
580 if (!inequalities.empty()) {
581 SOLVER_LOG(logger,
"[Encoding] ", num_inequalities,
582 " literals associated to VAR >= value, and ",
583 num_half_inequalities,
" half-associations.");
589 int num_equalities = 0;
590 int num_half_equalities = 0;
591 int num_fully_encoded = 0;
592 int num_partially_encoded = 0;
593 for (
int i = 0;
i < var_to_equalities.size(); ++
i) {
594 std::vector<EqualityDetectionHelper>& encoding = var_to_equalities[
i];
595 std::sort(encoding.begin(), encoding.end());
596 if (encoding.empty())
continue;
598 absl::flat_hash_set<int64_t> values;
599 const IntegerVariable var = mapping->integers_[
i];
600 for (
int j = 0; j + 1 < encoding.size(); j++) {
601 if ((encoding[j].value != encoding[j + 1].value) ||
602 (encoding[j].literal != encoding[j + 1].literal.Negated()) ||
603 (encoding[j].is_equality !=
true) ||
604 (encoding[j + 1].is_equality !=
false)) {
609 encoder->AssociateToIntegerEqualValue(encoding[j].literal, var,
610 IntegerValue(encoding[j].value));
611 mapping->already_loaded_ct_.insert(encoding[j].ct);
612 mapping->already_loaded_ct_.insert(encoding[j + 1].ct);
613 values.insert(encoding[j].value);
619 if (sat_solver->ModelIsUnsat())
return;
627 for (
const auto equality : encoding) {
628 if (mapping->ConstraintIsAlreadyLoaded(equality.ct))
continue;
629 if (equality.is_equality) {
642 encoder->GetOrCreateAssociatedLiteral(
646 encoder->GetOrCreateAssociatedLiteral(
649 const Literal eq = encoder->GetOrCreateLiteralAssociatedToEquality(
650 var, equality.value);
654 ++num_half_equalities;
655 mapping->already_loaded_ct_.insert(equality.ct);
656 mapping->is_half_encoding_ct_.insert(equality.ct);
660 if (encoder->VariableIsFullyEncoded(var)) {
663 ++num_partially_encoded;
667 if (num_equalities > 0 || num_half_equalities > 0) {
668 SOLVER_LOG(logger,
"[Encoding] ", num_equalities,
669 " literals associated to VAR == value, and ",
670 num_half_equalities,
" half-associations.");
672 if (num_fully_encoded > 0) {
674 "[Encoding] num_fully_encoded_variables:", num_fully_encoded);
676 if (num_partially_encoded > 0) {
677 SOLVER_LOG(logger,
"[Encoding] num_partially_encoded_variables:",
678 num_partially_encoded);
683 int num_element_encoded = 0;
693 int num_support_clauses = 0;
694 int num_dedicated_propagator = 0;
695 std::vector<Literal> clause;
696 std::vector<Literal> selectors;
697 std::vector<AffineExpression> exprs;
698 std::vector<AffineExpression> negated_exprs;
699 for (
int c = 0; c < model_proto.constraints_size(); ++c) {
700 const ConstraintProto& ct = model_proto.constraints(c);
701 if (ct.constraint_case() != ConstraintProto::kExactlyOne)
continue;
704 absl::btree_map<IntegerVariable, std::vector<ValueLiteralPair>>
705 var_to_value_literal_list;
706 for (
const int l : ct.exactly_one().literals()) {
708 for (
const auto& var_value : implied_bounds->GetImpliedValues(literal)) {
709 var_to_value_literal_list[var_value.first].push_back(
710 {var_value.second, literal});
715 std::vector<IntegerVariable> encoded_variables;
716 std::string encoded_variables_str;
719 for (
auto& [var, encoding] : var_to_value_literal_list) {
720 if (encoding.size() < ct.exactly_one().literals_size()) {
721 VLOG(2) <<
"X" << var.value() <<
" has " << encoding.size()
722 <<
" implied values, and a domain of size "
724 ->InitialVariableDomain(var)
730 ++num_element_encoded;
731 element_encodings->
Add(var, encoding, c);
733 encoded_variables.push_back(var);
734 absl::StrAppend(&encoded_variables_str,
" X", var.value());
740 bool need_extra_propagation =
false;
741 std::sort(encoding.begin(), encoding.end(),
743 for (
int i = 0, j = 0;
i < encoding.size();
i = j) {
745 const IntegerValue value = encoding[
i].value;
746 while (j < encoding.size() && encoding[j].value == value) ++j;
750 if (!encoder->IsFixedOrHasAssociatedLiteral(
752 !encoder->IsFixedOrHasAssociatedLiteral(
754 need_extra_propagation =
true;
757 encoder->AssociateToIntegerEqualValue(encoding[
i].literal, var,
761 if (encoder->GetAssociatedEqualityLiteral(var, value) ==
763 need_extra_propagation =
true;
771 ++num_support_clauses;
773 for (
int k =
i; k < j; ++k) clause.push_back(encoding[k].literal);
775 encoder->GetOrCreateLiteralAssociatedToEquality(var, value);
776 clause.push_back(eq_lit.
Negated());
781 sat_solver->AddProblemClause(clause);
784 if (need_extra_propagation) {
785 ++num_dedicated_propagator;
788 negated_exprs.clear();
789 for (
const auto [value, literal] : encoding) {
790 selectors.push_back(literal);
801 NegationOf(var), negated_exprs, selectors, {}, m);
806 if (encoded_variables.size() > 1 && VLOG_IS_ON(1)) {
807 VLOG(1) <<
"exactly_one(" << c <<
") encodes " << encoded_variables.size()
808 <<
" variables at the same time: " << encoded_variables_str;
812 if (num_element_encoded > 0) {
814 "[Encoding] num_element_encoding: ", num_element_encoded);
816 if (num_support_clauses > 0) {
817 SOLVER_LOG(logger,
"[Encoding] Added ", num_support_clauses,
818 " element support clauses, and ", num_dedicated_propagator,
819 " dedicated propagators.");
830 int64_t num_associations = 0;
831 int64_t num_set_to_false = 0;
832 for (
const ConstraintProto& ct : model_proto.constraints()) {
833 if (!ct.enforcement_literal().empty())
continue;
834 if (ct.constraint_case() != ConstraintProto::kLinear)
continue;
835 if (ct.linear().vars_size() != 2)
continue;
836 if (!ConstraintIsEq(ct.linear()))
continue;
838 const IntegerValue rhs(ct.linear().domain(0));
841 IntegerVariable var1 = mapping->Integer(ct.linear().vars(0));
842 IntegerVariable var2 = mapping->Integer(ct.linear().vars(1));
843 IntegerValue coeff1(ct.linear().coeffs(0));
844 IntegerValue coeff2(ct.linear().coeffs(1));
856 if (coeff1 == 0 || coeff2 == 0)
continue;
861 for (
int i = 0;
i < 2; ++
i) {
862 for (
const auto [value1, literal1] :
863 encoder->PartialGreaterThanEncoding(var1)) {
864 const IntegerValue bound2 =
FloorRatio(rhs - value1 * coeff1, coeff2);
866 encoder->AssociateToIntegerLiteral(
869 std::swap(var1, var2);
870 std::swap(coeff1, coeff2);
878 for (
int i = 0;
i < 2; ++
i) {
879 const auto copy = encoder->PartialDomainEncoding(var1);
880 for (
const auto value_literal : copy) {
881 const IntegerValue value1 = value_literal.value;
882 const IntegerValue intermediate = rhs - value1 * coeff1;
883 if (intermediate % coeff2 != 0) {
886 if (!sat_solver->AddUnitClause(value_literal.literal.Negated())) {
892 encoder->AssociateToIntegerEqualValue(value_literal.literal, var2,
893 intermediate / coeff2);
895 std::swap(var1, var2);
896 std::swap(coeff1, coeff2);
900 if (num_associations > 0) {
901 VLOG(1) <<
"Num associations from equivalences = " << num_associations;
903 if (num_set_to_false > 0) {
904 VLOG(1) <<
"Num literals set to false from equivalences = "
910 const SatParameters& parameters = *(m->
GetOrCreate<SatParameters>());
911 if (!parameters.use_optional_variables())
return;
912 if (parameters.enumerate_all_solutions())
return;
915 const int num_proto_variables = model_proto.variables_size();
916 std::vector<bool> already_seen(num_proto_variables,
false);
917 if (model_proto.has_objective()) {
918 for (
const int ref : model_proto.objective().vars()) {
931 std::vector<std::vector<int>> enforcement_intersection(num_proto_variables);
932 absl::btree_set<int> literals_set;
933 for (
int c = 0; c < model_proto.constraints_size(); ++c) {
934 const ConstraintProto& ct = model_proto.constraints(c);
935 if (ct.enforcement_literal().empty()) {
937 already_seen[var] =
true;
938 enforcement_intersection[var].clear();
941 literals_set.clear();
942 literals_set.insert(ct.enforcement_literal().begin(),
943 ct.enforcement_literal().end());
945 if (!already_seen[var]) {
946 enforcement_intersection[var].assign(ct.enforcement_literal().begin(),
947 ct.enforcement_literal().end());
950 std::vector<int>& vector_ref = enforcement_intersection[var];
952 for (
const int literal : vector_ref) {
953 if (literals_set.contains(literal)) {
954 vector_ref[new_size++] = literal;
957 vector_ref.resize(new_size);
959 already_seen[var] =
true;
965 int num_optionals = 0;
966 for (
int var = 0; var < num_proto_variables; ++var) {
967 const IntegerVariableProto& var_proto = model_proto.variables(var);
968 const int64_t min = var_proto.domain(0);
969 const int64_t max = var_proto.domain(var_proto.domain().size() - 1);
970 if (min == max)
continue;
971 if (min == 0 && max == 1)
continue;
972 if (enforcement_intersection[var].empty())
continue;
977 if (num_optionals > 0) {
979 " optional variables. Note that for now we DO NOT do anything "
980 "with this information.");
986 if (model_proto.search_strategy().empty())
return;
990 for (
const DecisionStrategyProto& strategy : model_proto.search_strategy()) {
991 if (strategy.domain_reduction_strategy() ==
992 DecisionStrategyProto::SELECT_MEDIAN_VALUE) {
993 for (
const LinearExpressionProto& expr : strategy.exprs()) {
994 const int var = expr.vars(0);
995 if (!mapping->IsInteger(var))
continue;
996 const IntegerVariable variable = mapping->Integer(var);
997 if (!integer_trail->IsFixed(variable)) {
1010 auto* mapping = m->GetOrCreate<CpModelMapping>();
1012 std::vector<Literal> literals = mapping->Literals(ct.bool_or().literals());
1013 for (
const int ref : ct.enforcement_literal()) {
1014 literals.push_back(mapping->Literal(ref).Negated());
1017 if (literals.size() == 3) {
1018 m->GetOrCreate<ProductDetector>()->ProcessTernaryClause(literals);
1024 std::vector<Literal> literals;
1025 for (
const int ref : ct.enforcement_literal()) {
1026 literals.push_back(mapping->Literal(ref).Negated());
1028 auto* sat_solver = m->GetOrCreate<SatSolver>();
1029 for (
const Literal literal : mapping->Literals(ct.bool_and().literals())) {
1030 literals.push_back(literal);
1031 sat_solver->AddProblemClause(literals);
1032 literals.pop_back();
1040 if (!implications->AddAtMostOne(
1041 mapping->Literals(ct.at_most_one().literals()))) {
1042 m->GetOrCreate<
SatSolver>()->NotifyThatModelIsUnsat();
1047 auto* mapping = m->GetOrCreate<CpModelMapping>();
1049 const auto& literals = mapping->Literals(ct.exactly_one().literals());
1051 if (literals.size() == 3) {
1052 m->GetOrCreate<
ProductDetector>()->ProcessTernaryExactlyOne(literals);
1057 auto* mapping = m->GetOrCreate<CpModelMapping>();
1059 m->Add(
LiteralXorIs(mapping->Literals(ct.bool_xor().literals()),
true));
1066void LoadEquivalenceAC(
const std::vector<Literal> enforcement_literal,
1067 IntegerValue coeff1, IntegerVariable var1,
1068 IntegerValue coeff2, IntegerVariable var2,
1069 const IntegerValue rhs,
Model* m) {
1070 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1071 CHECK(encoder->VariableIsFullyEncoded(var1));
1072 CHECK(encoder->VariableIsFullyEncoded(var2));
1073 absl::flat_hash_map<IntegerValue, Literal> term1_value_to_literal;
1074 for (
const auto value_literal : encoder->FullDomainEncoding(var1)) {
1075 term1_value_to_literal[coeff1 * value_literal.value] =
1076 value_literal.literal;
1078 const auto copy = encoder->FullDomainEncoding(var2);
1079 for (
const auto value_literal : copy) {
1080 const IntegerValue target = rhs - value_literal.value * coeff2;
1081 if (!term1_value_to_literal.contains(target)) {
1083 {value_literal.literal.Negated()}));
1085 const Literal target_literal = term1_value_to_literal[target];
1087 {value_literal.literal.Negated(), target_literal}));
1089 {value_literal.literal, target_literal.Negated()}));
1093 term1_value_to_literal.erase(target);
1099 std::vector<Literal> implied_false;
1100 for (
const auto entry : term1_value_to_literal) {
1101 implied_false.push_back(entry.second);
1103 std::sort(implied_false.begin(), implied_false.end());
1104 for (
const Literal l : implied_false) {
1111void LoadEquivalenceNeqAC(
const std::vector<Literal> enforcement_literal,
1112 IntegerValue coeff1, IntegerVariable var1,
1113 IntegerValue coeff2, IntegerVariable var2,
1114 const IntegerValue rhs,
Model* m) {
1115 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1116 CHECK(encoder->VariableIsFullyEncoded(var1));
1117 CHECK(encoder->VariableIsFullyEncoded(var2));
1118 absl::flat_hash_map<IntegerValue, Literal> term1_value_to_literal;
1119 for (
const auto value_literal : encoder->FullDomainEncoding(var1)) {
1120 term1_value_to_literal[coeff1 * value_literal.value] =
1121 value_literal.literal;
1123 const auto copy = encoder->FullDomainEncoding(var2);
1124 for (
const auto value_literal : copy) {
1125 const IntegerValue target_value = rhs - value_literal.value * coeff2;
1126 const auto& it = term1_value_to_literal.find(target_value);
1127 if (it != term1_value_to_literal.end()) {
1128 const Literal target_literal = it->second;
1130 enforcement_literal,
1131 {value_literal.literal.Negated(), target_literal.Negated()}));
1136bool IsPartOfProductEncoding(
const ConstraintProto& ct) {
1137 if (ct.enforcement_literal().size() != 1)
return false;
1138 if (ct.linear().vars().size() > 2)
return false;
1139 if (ct.linear().domain().size() != 2)
return false;
1140 if (ct.linear().domain(0) != 0)
return false;
1141 if (ct.linear().domain(1) != 0)
return false;
1142 for (
const int64_t coeff : ct.linear().coeffs()) {
1143 if (std::abs(coeff) != 1)
return false;
1153 std::vector<IntegerVariable>* vars,
1154 std::vector<int64_t>* coeffs,
1158 if (m->
GetOrCreate<SatParameters>()->enumerate_all_solutions()) {
1163 std::vector<IntegerVariable> bucket_sum_vars;
1164 std::vector<int64_t> bucket_sum_coeffs;
1165 std::vector<IntegerVariable> local_vars;
1166 std::vector<int64_t> local_coeffs;
1169 const int64_t num_vars = vars->size();
1170 const int64_t num_buckets =
static_cast<int>(std::round(std::sqrt(num_vars)));
1172 for (int64_t
b = 0;
b < num_buckets; ++
b) {
1174 local_coeffs.clear();
1175 int64_t bucket_lb = 0;
1176 int64_t bucket_ub = 0;
1178 const int64_t limit = num_vars * (
b + 1);
1179 for (;
i * num_buckets < limit; ++
i) {
1180 const IntegerVariable var = (*vars)[
i];
1181 const int64_t coeff = (*coeffs)[
i];
1182 gcd = std::gcd(gcd, std::abs(coeff));
1183 local_vars.push_back(var);
1184 local_coeffs.push_back(coeff);
1185 const int64_t term1 = coeff * integer_trail->LowerBound(var).value();
1186 const int64_t term2 = coeff * integer_trail->UpperBound(var).value();
1187 bucket_lb += std::min(term1, term2);
1188 bucket_ub += std::max(term1, term2);
1190 if (gcd == 0)
continue;
1193 for (int64_t& ref : local_coeffs) ref /= gcd;
1198 const IntegerVariable bucket_sum =
1199 integer_trail->AddIntegerVariable(bucket_lb, bucket_ub);
1200 bucket_sum_vars.push_back(bucket_sum);
1201 bucket_sum_coeffs.push_back(gcd);
1202 local_vars.push_back(bucket_sum);
1203 local_coeffs.push_back(-1);
1214 *vars = bucket_sum_vars;
1215 *coeffs = bucket_sum_coeffs;
1219 auto* mapping = m->GetOrCreate<CpModelMapping>();
1221 if (ct.linear().vars().empty()) {
1225 std::vector<Literal> clause;
1226 for (
const int ref : ct.enforcement_literal()) {
1227 clause.push_back(mapping->Literal(ref).Negated());
1231 VLOG(1) <<
"Trivially UNSAT constraint: " << ct;
1232 m->GetOrCreate<
SatSolver>()->NotifyThatModelIsUnsat();
1237 if (IsPartOfProductEncoding(ct)) {
1238 const Literal l = mapping->Literal(ct.enforcement_literal(0));
1239 auto* detector = m->GetOrCreate<ProductDetector>();
1240 if (ct.linear().vars().size() == 1) {
1243 detector->ProcessConditionalZero(l,
1244 mapping->Integer(ct.linear().vars(0)));
1245 }
else if (ct.linear().vars().size() == 2) {
1246 const IntegerVariable x = mapping->Integer(ct.linear().vars(0));
1247 const IntegerVariable y = mapping->Integer(ct.linear().vars(1));
1248 detector->ProcessConditionalEquality(
1250 ct.linear().coeffs(0) == ct.linear().coeffs(1) ?
NegationOf(y) : y);
1255 std::vector<IntegerVariable> vars = mapping->Integers(ct.linear().vars());
1256 std::vector<int64_t> coeffs = ValuesFromProto(ct.linear().coeffs());
1262 IntegerValue min_sum(0);
1263 IntegerValue max_sum(0);
1264 IntegerValue max_domain_size(0);
1265 bool all_booleans =
true;
1266 for (
int i = 0;
i < vars.size(); ++
i) {
1267 if (all_booleans && !mapping->IsBoolean(ct.linear().vars(
i))) {
1268 all_booleans =
false;
1270 const IntegerValue lb = integer_trail->LowerBound(vars[
i]);
1271 const IntegerValue ub = integer_trail->UpperBound(vars[
i]);
1272 max_domain_size = std::max(max_domain_size, ub - lb + 1);
1273 const IntegerValue term_a = coeffs[
i] * lb;
1274 const IntegerValue term_b = coeffs[
i] * ub;
1275 min_sum += std::min(term_a, term_b);
1276 max_sum += std::max(term_a, term_b);
1280 const SatParameters& params = *m->GetOrCreate<SatParameters>();
1281 if (params.auto_detect_greater_than_at_least_one_of() &&
1282 ct.enforcement_literal().size() == 1 && vars.size() <= 2) {
1284 int64_t rhs_min = ct.linear().domain(0);
1285 int64_t rhs_max = ct.linear().domain(ct.linear().domain().size() - 1);
1286 rhs_min = std::max(rhs_min, min_sum.value());
1287 rhs_max = std::min(rhs_max, max_sum.value());
1292 if (vars.size() == 1) {
1293 repository->Add(lit, {vars[0], coeffs[0]}, {}, rhs_min, rhs_max);
1294 }
else if (vars.size() == 2) {
1295 repository->Add(lit, {vars[0], coeffs[0]}, {vars[1], coeffs[1]}, rhs_min,
1306 int64_t rhs_min = ct.linear().domain(0);
1307 int64_t rhs_max = ct.linear().domain(ct.linear().domain().size() - 1);
1308 rhs_min = std::max(rhs_min, min_sum.value());
1309 rhs_max = std::min(rhs_max, max_sum.value());
1311 if (vars.size() == 2) {
1312 if (std::abs(coeffs[0]) == std::abs(coeffs[1])) {
1313 const int64_t magnitude = std::abs(coeffs[0]);
1314 IntegerVariable v1 = vars[0];
1315 IntegerVariable v2 = vars[1];
1325 }
else if (vars.size() == 3) {
1326 for (
int i = 0;
i < 3; ++
i) {
1327 for (
int j = 0; j < 3; ++j) {
1328 if (
i == j)
continue;
1329 if (std::abs(coeffs[
i]) != std::abs(coeffs[j]))
continue;
1330 const int other = 3 -
i - j;
1333 const int64_t magnitude = std::abs(coeffs[
i]);
1334 IntegerVariable v1 = vars[
i];
1335 IntegerVariable v2 = vars[j];
1340 const int64_t coeff = coeffs[other];
1341 const int64_t other_lb =
1343 ? coeff * integer_trail->LowerBound(vars[other]).value()
1344 : coeff * integer_trail->UpperBound(vars[other]).value();
1349 const int64_t other_ub =
1351 ? coeff * integer_trail->UpperBound(vars[other]).value()
1352 : coeff * integer_trail->LowerBound(vars[other]).value();
1360 const IntegerValue domain_size_limit(
1361 params.max_domain_size_when_encoding_eq_neq_constraints());
1362 if (ct.linear().vars_size() == 2 && !integer_trail->IsFixed(vars[0]) &&
1363 !integer_trail->IsFixed(vars[1]) &&
1364 max_domain_size <= domain_size_limit) {
1366 if (params.boolean_encoding_level() > 0 && ConstraintIsEq(ct.linear()) &&
1367 ct.linear().domain(0) != min_sum && ct.linear().domain(0) != max_sum &&
1368 encoder->VariableIsFullyEncoded(vars[0]) &&
1369 encoder->VariableIsFullyEncoded(vars[1])) {
1370 VLOG(3) <<
"Load AC version of " << ct <<
", var0 domain = "
1371 << integer_trail->InitialVariableDomain(vars[0])
1372 <<
", var1 domain = "
1373 << integer_trail->InitialVariableDomain(vars[1]);
1374 return LoadEquivalenceAC(mapping->Literals(ct.enforcement_literal()),
1375 IntegerValue(coeffs[0]), vars[0],
1376 IntegerValue(coeffs[1]), vars[1],
1377 IntegerValue(ct.linear().domain(0)), m);
1380 int64_t single_value = 0;
1381 if (params.boolean_encoding_level() > 0 &&
1382 ConstraintIsNEq(ct.linear(), mapping, integer_trail, &single_value) &&
1383 single_value != min_sum && single_value != max_sum &&
1384 encoder->VariableIsFullyEncoded(vars[0]) &&
1385 encoder->VariableIsFullyEncoded(vars[1])) {
1386 VLOG(3) <<
"Load NAC version of " << ct <<
", var0 domain = "
1387 << integer_trail->InitialVariableDomain(vars[0])
1388 <<
", var1 domain = "
1389 << integer_trail->InitialVariableDomain(vars[1])
1390 <<
", value = " << single_value;
1391 return LoadEquivalenceNeqAC(mapping->Literals(ct.enforcement_literal()),
1392 IntegerValue(coeffs[0]), vars[0],
1393 IntegerValue(coeffs[1]), vars[1],
1394 IntegerValue(single_value), m);
1402 ct.linear().domain_size() == 2 && all_booleans;
1403 if (!pseudo_boolean &&
1404 ct.linear().vars().size() > params.linear_split_size()) {
1405 const auto& domain = ct.linear().domain();
1407 domain.size() > 2 || min_sum < domain[0],
1408 domain.size() > 2 || max_sum > domain[1], &vars, &coeffs, m);
1411 if (ct.linear().domain_size() == 2) {
1412 const int64_t lb = ct.linear().domain(0);
1413 const int64_t ub = ct.linear().domain(1);
1414 const std::vector<Literal> enforcement_literals =
1415 mapping->Literals(ct.enforcement_literal());
1416 if (all_booleans && enforcement_literals.empty()) {
1419 std::vector<LiteralWithCoeff> cst;
1420 for (
int i = 0;
i < vars.size(); ++
i) {
1421 const int ref = ct.linear().vars(
i);
1422 cst.push_back({mapping->Literal(ref), coeffs[
i]});
1424 m->GetOrCreate<
SatSolver>()->AddLinearConstraint(
1426 (max_sum > ub), ub, &cst);
1442 const bool is_linear1 = vars.size() == 1 && coeffs[0] == 1;
1444 bool special_case =
false;
1445 std::vector<Literal> clause;
1446 std::vector<Literal> for_enumeration;
1448 const int domain_size = ct.linear().domain_size();
1449 for (
int i = 0;
i < domain_size;
i += 2) {
1450 const int64_t lb = ct.linear().domain(
i);
1451 const int64_t ub = ct.linear().domain(
i + 1);
1454 if (min_sum > ub)
continue;
1455 if (max_sum < lb)
continue;
1459 if (min_sum >= lb && max_sum <= ub)
return;
1464 encoding->GetOrCreateLiteralAssociatedToEquality(vars[0], lb));
1466 }
else if (min_sum >= lb) {
1467 clause.push_back(encoding->GetOrCreateAssociatedLiteral(
1470 }
else if (max_sum <= ub) {
1471 clause.push_back(encoding->GetOrCreateAssociatedLiteral(
1480 if (ct.enforcement_literal().empty() && clause.size() == 1 &&
1481 i + 1 == domain_size) {
1482 special_case =
true;
1485 const Literal subdomain_literal(
1486 special_case ? clause.back().Negated()
1488 clause.push_back(subdomain_literal);
1489 for_enumeration.push_back(subdomain_literal);
1499 const std::vector<Literal> enforcement_literals =
1500 mapping->Literals(ct.enforcement_literal());
1503 if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
1505 if (enforcement_literals.size() == 1) {
1506 linear_is_enforced = enforcement_literals[0];
1509 std::vector<Literal> maintain_linear_is_enforced;
1510 for (
const Literal e_lit : enforcement_literals) {
1511 m->Add(
Implication(e_lit.Negated(), linear_is_enforced.Negated()));
1512 maintain_linear_is_enforced.push_back(e_lit.Negated());
1514 maintain_linear_is_enforced.push_back(linear_is_enforced);
1517 for (
const Literal lit : for_enumeration) {
1518 m->Add(
Implication(linear_is_enforced.Negated(), lit.Negated()));
1519 if (special_case)
break;
1523 if (!special_case) {
1524 for (
const Literal e_lit : enforcement_literals) {
1525 clause.push_back(e_lit.Negated());
1533 const std::vector<AffineExpression> expressions =
1534 mapping->
Affines(ct.all_diff().exprs());
1539 auto* mapping = m->GetOrCreate<CpModelMapping>();
1541 std::vector<AffineExpression> terms;
1542 for (
const LinearExpressionProto& expr : ct.int_prod().exprs()) {
1543 terms.push_back(mapping->Affine(expr));
1545 switch (terms.size()) {
1547 auto* integer_trail = m->GetOrCreate<IntegerTrail>();
1548 auto* sat_solver = m->GetOrCreate<SatSolver>();
1551 sat_solver->NotifyThatModelIsUnsat();
1556 sat_solver->NotifyThatModelIsUnsat();
1563 builder.AddTerm(prod, 1);
1564 builder.AddTerm(terms[0], -1);
1573 LOG(FATAL) <<
"Loading int_prod with arity > 2, should not be here.";
1585 if (integer_trail->IsFixed(denom)) {
1588 if (VLOG_IS_ON(1)) {
1589 LinearConstraintBuilder builder(m);
1590 if (m->GetOrCreate<ProductDecomposer>()->TryToLinearize(num, denom,
1592 VLOG(1) <<
"Division " << ct <<
" can be linearized";
1606 CHECK(integer_trail->IsFixed(mod));
1607 const IntegerValue fixed_modulo = integer_trail->FixedValue(mod);
1612 if (ct.lin_max().exprs().empty()) {
1617 auto* mapping = m->GetOrCreate<CpModelMapping>();
1618 const LinearExpression max = mapping->GetExprFromProto(ct.lin_max().target());
1619 std::vector<LinearExpression> negated_exprs;
1620 negated_exprs.reserve(ct.lin_max().exprs_size());
1621 for (
int i = 0;
i < ct.lin_max().exprs_size(); ++
i) {
1622 negated_exprs.push_back(
1623 NegationOf(mapping->GetExprFromProto(ct.lin_max().exprs(
i))));
1635 if (ct.no_overlap_2d().x_intervals().empty())
return;
1637 const std::vector<IntervalVariable> x_intervals =
1638 mapping->
Intervals(ct.no_overlap_2d().x_intervals());
1639 const std::vector<IntervalVariable> y_intervals =
1640 mapping->Intervals(ct.no_overlap_2d().y_intervals());
1645 auto* mapping = m->GetOrCreate<CpModelMapping>();
1646 const std::vector<IntervalVariable> intervals =
1647 mapping->Intervals(ct.cumulative().intervals());
1648 const AffineExpression capacity = mapping->Affine(ct.cumulative().capacity());
1649 const std::vector<AffineExpression> demands =
1650 mapping->Affines(ct.cumulative().demands());
1651 m->Add(
Cumulative(intervals, demands, capacity));
1655 auto* mapping = m->GetOrCreate<CpModelMapping>();
1657 const std::vector<AffineExpression> times =
1658 mapping->Affines(ct.reservoir().time_exprs());
1659 const std::vector<AffineExpression> level_changes =
1660 mapping->Affines(ct.reservoir().level_changes());
1661 std::vector<Literal> presences;
1662 const int size = ct.reservoir().time_exprs().size();
1663 for (
int i = 0;
i < size; ++
i) {
1664 if (!ct.reservoir().active_literals().empty()) {
1665 presences.push_back(mapping->Literal(ct.reservoir().active_literals(
i)));
1667 presences.push_back(encoder->GetTrueLiteral());
1671 ct.reservoir().min_level(), ct.reservoir().max_level(),
1676 const auto& circuit = ct.circuit();
1677 if (circuit.tails().empty())
return;
1679 std::vector<int> tails(circuit.tails().begin(), circuit.tails().end());
1680 std::vector<int> heads(circuit.heads().begin(), circuit.heads().end());
1681 std::vector<Literal> literals =
1683 const int num_nodes =
ReindexArcs(&tails, &heads);
1688 const auto& routes = ct.routes();
1689 if (routes.tails().empty())
return;
1691 std::vector<int> tails(routes.tails().begin(), routes.tails().end());
1692 std::vector<int> heads(routes.heads().begin(), routes.heads().end());
1693 std::vector<Literal> literals =
1695 const int num_nodes =
ReindexArcs(&tails, &heads);
1701 switch (ct.constraint_case()) {
1702 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1704 case ConstraintProto::ConstraintCase::kBoolOr:
1707 case ConstraintProto::ConstraintCase::kBoolAnd:
1710 case ConstraintProto::ConstraintCase::kAtMostOne:
1713 case ConstraintProto::ConstraintCase::kExactlyOne:
1716 case ConstraintProto::ConstraintCase::kBoolXor:
1719 case ConstraintProto::ConstraintProto::kLinear:
1722 case ConstraintProto::ConstraintProto::kAllDiff:
1725 case ConstraintProto::ConstraintProto::kIntProd:
1728 case ConstraintProto::ConstraintProto::kIntDiv:
1731 case ConstraintProto::ConstraintProto::kIntMod:
1734 case ConstraintProto::ConstraintProto::kLinMax:
1737 case ConstraintProto::ConstraintProto::kInterval:
1740 case ConstraintProto::ConstraintProto::kNoOverlap:
1743 case ConstraintProto::ConstraintProto::kNoOverlap2D:
1746 case ConstraintProto::ConstraintProto::kCumulative:
1749 case ConstraintProto::ConstraintProto::kReservoir:
1752 case ConstraintProto::ConstraintProto::kCircuit:
1755 case ConstraintProto::ConstraintProto::kRoutes:
Domain IntersectionWith(const Domain &domain) const
bool Contains(int64_t value) const
Domain Complement() const
Domain InverseMultiplicationBy(int64_t coeff) const
static IntegralType CeilOfRatio(IntegralType numerator, IntegralType denominator)
sat::Literal Literal(int ref) const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
std::vector< AffineExpression > Affines(const List &list) const
void RegisterWith(GenericLiteralWatcher *watcher)
bool Add(Literal literal, IntegerLiteral integer_literal)
void ReserveSpaceForNumVariables(int num_vars)
LiteralIndex Index() const
BooleanVariable Variable() const
Literal(int signed_value)
T Add(std::function< T(Model *)> f)
bool AddProblemClause(absl::Span< const Literal > literals)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
std::function< std::vector< ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
void LoadBoolXorConstraint(const ConstraintProto &ct, Model *m)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
void LoadCumulativeConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> LiteralXorIs(const std::vector< Literal > &literals, bool value)
Enforces the XOR of a set of literals to be equal to the given value.
bool RefIsPositive(int ref)
void LoadLinMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadIntProdConstraint(const ConstraintProto &ct, Model *m)
void SplitAndLoadIntermediateConstraints(bool lb_required, bool ub_required, std::vector< IntegerVariable > *vars, std::vector< int64_t > *coeffs, Model *m)
std::function< void(Model *)> WeightedSumGreaterOrEqual(absl::Span< const IntegerVariable > vars, const VectorInt &coefficients, int64_t lower_bound)
Weighted sum >= constant.
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> ProductConstraint(AffineExpression a, AffineExpression b, AffineExpression p)
Adds the constraint: a * b = p.
void DetectOptionalVariables(const CpModelProto &model_proto, Model *m)
Automatically detect optional variables.
void LoadBoolOrConstraint(const ConstraintProto &ct, Model *m)
void LoadSubcircuitConstraint(int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, Model *model, bool multiple_subcircuit_through_zero)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
enforcement_literals => clause.
std::function< BooleanVariable(Model *)> NewBooleanVariable()
std::function< void(Model *)> FixedDivisionConstraint(AffineExpression a, IntegerValue b, AffineExpression c)
Adds the constraint: a / b = c where b is a constant.
bool HasEnforcementLiteral(const ConstraintProto &ct)
Small utility functions to deal with half-reified constraints.
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
void LoadVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
std::function< void(Model *)> IsEqualToMinOf(const LinearExpression &min_expr, const std::vector< LinearExpression > &exprs)
void LoadIntModConstraint(const ConstraintProto &ct, Model *m)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> Implication(absl::Span< const Literal > enforcement_literals, IntegerLiteral i)
const IntervalVariable kNoIntervalVariable(-1)
void LoadBooleanSymmetries(const CpModelProto &model_proto, Model *m)
std::function< void(Model *)> DivisionConstraint(AffineExpression num, AffineExpression denom, AffineExpression div)
Adds the constraint: num / denom = div. (denom > 0).
void LoadRoutesConstraint(const ConstraintProto &ct, Model *m)
void LoadAtMostOneConstraint(const ConstraintProto &ct, Model *m)
void AddFullEncodingFromSearchBranching(const CpModelProto &model_proto, Model *m)
std::vector< int > UsedVariables(const ConstraintProto &ct)
void LoadCircuitConstraint(const ConstraintProto &ct, Model *m)
void ExtractElementEncoding(const CpModelProto &model_proto, Model *m)
void LoadReservoirConstraint(const ConstraintProto &ct, Model *m)
void AddWeightedSumLowerOrEqual(absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const int64_t > coefficients, int64_t upper_bound, Model *model)
enforcement_literals => sum <= upper_bound
int ReindexArcs(IntContainer *tails, IntContainer *heads, absl::flat_hash_map< int, int > *mapping_output=nullptr)
void LoadNoOverlapConstraint(const ConstraintProto &ct, Model *m)
void LoadAllDiffConstraint(const ConstraintProto &ct, Model *m)
void AddDisjunctive(const std::vector< IntervalVariable > &intervals, Model *model)
std::vector< Literal > Literals(absl::Span< const int > input)
void LoadNoOverlap2dConstraint(const ConstraintProto &ct, Model *m)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void LoadBoolAndConstraint(const ConstraintProto &ct, Model *m)
void AddNonOverlappingRectangles(const std::vector< IntervalVariable > &x, const std::vector< IntervalVariable > &y, Model *model)
void LoadExactlyOneConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ExactlyOneConstraint(absl::Span< const Literal > literals)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, absl::Span< const AffineExpression > demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
void PropagateEncodingFromEquivalenceRelations(const CpModelProto &model_proto, Model *m)
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< AffineExpression > deltas, std::vector< Literal > presences, int64_t min_level, int64_t max_level, Model *model)
std::function< void(Model *)> FixedModuloConstraint(AffineExpression a, IntegerValue b, AffineExpression c)
Adds the constraint: a % b = c where b is a constant.
const BooleanVariable kNoBooleanVariable(-1)
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
void AddWeightedSumGreaterOrEqual(absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const int64_t > coefficients, int64_t lower_bound, Model *model)
enforcement_literals => sum >= lower_bound
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< AffineExpression > &expressions)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
void LoadIntDivConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> WeightedSumLowerOrEqual(absl::Span< const IntegerVariable > vars, const VectorInt &coefficients, int64_t upper_bound)
Weighted sum <= constant.
In SWIG mode, we don't want anything besides these top-level includes.
int64_t Min() const
Returns the min of the domain.
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
var * coeff + constant >= bound.
IntegerLiteral LowerOrEqual(IntegerValue bound) const
var * coeff + constant <= bound.
std::vector< int > variables
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
#define SOLVER_LOG(logger,...)