24 #include "absl/container/flat_hash_map.h"
25 #include "absl/container/flat_hash_set.h"
34 #include "ortools/sat/cp_model.pb.h"
46 #include "ortools/sat/sat_parameters.pb.h"
59 template <
typename Values>
60 std::vector<int64> ValuesFromProto(
const Values& values) {
61 return std::vector<int64>(values.begin(), values.end());
64 void ComputeLinearBounds(
const LinearConstraintProto&
proto,
65 CpModelMapping* mapping, IntegerTrail* integer_trail,
70 for (
int i = 0; i <
proto.vars_size(); ++i) {
72 const IntegerVariable
var = mapping->Integer(
proto.vars(i));
73 const int64 lb = integer_trail->LowerBound(
var).value();
74 const int64 ub = integer_trail->UpperBound(
var).value();
76 (*sum_min) += coeff * lb;
77 (*sum_max) += coeff * ub;
79 (*sum_min) += coeff * ub;
80 (*sum_max) += coeff * lb;
86 bool ConstraintIsEq(
const LinearConstraintProto&
proto) {
91 bool ConstraintIsNEq(
const LinearConstraintProto&
proto,
92 CpModelMapping* mapping, IntegerTrail* integer_trail,
93 int64* single_value) {
96 ComputeLinearBounds(
proto, mapping, integer_trail, &sum_min, &sum_max);
98 const Domain complement =
99 Domain(sum_min, sum_max)
101 if (complement.IsEmpty())
return false;
104 if (complement.Size() == 1) {
105 if (single_value !=
nullptr) {
106 *single_value =
value;
116 bool view_all_booleans_as_integers,
118 const int num_proto_variables =
model_proto.variables_size();
124 CHECK_EQ(sat_solver->NumVariables(), 0);
126 BooleanVariable new_var(0);
127 std::vector<BooleanVariable> false_variables;
128 std::vector<BooleanVariable> true_variables;
131 reverse_boolean_map_.
resize(num_proto_variables, -1);
132 for (
int i = 0; i < num_proto_variables; ++i) {
133 const auto& domain =
model_proto.variables(i).domain();
134 if (domain.size() != 2)
continue;
135 if (domain[0] >= 0 && domain[1] <= 1) {
136 booleans_[i] = new_var;
137 reverse_boolean_map_[new_var] = i;
138 if (domain[1] == 0) {
140 }
else if (domain[0] == 1) {
141 true_variables.push_back(new_var);
147 sat_solver->SetNumVariables(new_var.value());
148 for (
const BooleanVariable
var : true_variables) {
151 for (
const BooleanVariable
var : false_variables) {
158 std::vector<int> var_to_instantiate_as_integer;
159 if (view_all_booleans_as_integers) {
160 var_to_instantiate_as_integer.resize(num_proto_variables);
161 for (
int i = 0; i < num_proto_variables; ++i) {
162 var_to_instantiate_as_integer[i] = i;
166 absl::flat_hash_set<int> used_variables;
169 for (
int c = 0; c <
model_proto.constraints_size(); ++c) {
180 for (
const int obj_var :
model_proto.objective().vars()) {
184 for (
const DecisionStrategyProto& strategy :
186 for (
const int var : strategy.variables()) {
193 for (
int i = 0; i < num_proto_variables; ++i) {
195 used_variables.insert(i);
200 var_to_instantiate_as_integer.assign(used_variables.begin(),
201 used_variables.end());
208 var_to_instantiate_as_integer.size());
209 reverse_integer_map_.
resize(2 * var_to_instantiate_as_integer.size(), -1);
210 for (
const int i : var_to_instantiate_as_integer) {
215 reverse_integer_map_[integers_[i]] = i;
222 for (
int i = 0; i < num_proto_variables; ++i) {
227 encoder->AssociateToIntegerEqualValue(
sat::Literal(booleans_[i],
true),
228 integers_[i], IntegerValue(1));
233 for (
int c = 0; c <
model_proto.constraints_size(); ++c) {
235 if (
ct.constraint_case() != ConstraintProto::ConstraintCase::kInterval) {
244 if (
ct.interval().has_start_view()) {
245 intervals_[c] = intervals_repository->CreateInterval(
249 enforcement_literal.
Index(),
254 Integer(
ct.interval().size()), enforcement_literal));
257 if (
ct.interval().has_start_view()) {
258 intervals_[c] = intervals_repository->CreateInterval(
269 already_loaded_ct_.insert(&
ct);
275 const SatParameters& params = *m->
GetOrCreate<SatParameters>();
276 const SymmetryProto symmetry =
model_proto.symmetry();
277 if (symmetry.permutations().empty())
return;
281 sat_solver->AddPropagator(symmetry_handler);
282 const int num_literals = 2 * sat_solver->NumVariables();
284 for (
const SparsePermutationProto& perm : symmetry.permutations()) {
285 bool all_bool =
true;
286 for (
const int var : perm.support()) {
292 if (!all_bool)
continue;
295 auto literal_permutation =
296 absl::make_unique<SparsePermutation>(num_literals);
297 int support_index = 0;
298 const int num_cycle = perm.cycle_sizes().size();
299 for (
int i = 0; i < num_cycle; ++i) {
300 const int size = perm.cycle_sizes(i);
301 const int saved_support_index = support_index;
302 for (
int j = 0; j < size; ++j) {
303 const int var = perm.support(support_index++);
306 literal_permutation->CloseCurrentCycle();
310 support_index = saved_support_index;
311 for (
int j = 0; j < size; ++j) {
312 const int var = perm.support(support_index++);
313 literal_permutation->AddToCurrentCycle(
316 literal_permutation->CloseCurrentCycle();
318 symmetry_handler->AddSymmetry(std::move(literal_permutation));
321 const bool log_info =
VLOG_IS_ON(1) || params.log_search_progress();
323 LOG(
INFO) <<
"Added " << symmetry_handler->num_permutations()
324 <<
" symmetry to the SAT solver.";
341 if (sat_solver->IsModelUnsat())
return;
346 struct EqualityDetectionHelper {
347 const ConstraintProto*
ct;
352 bool operator<(
const EqualityDetectionHelper& o)
const {
353 if (
literal.Variable() == o.literal.Variable()) {
354 if (
value == o.value)
return is_equality && !o.is_equality;
355 return value < o.value;
357 return literal.Variable() < o.literal.Variable();
360 std::vector<std::vector<EqualityDetectionHelper>> var_to_equalities(
372 struct InequalityDetectionHelper {
373 const ConstraintProto*
ct;
377 bool operator<(
const InequalityDetectionHelper& o)
const {
378 if (
literal.Variable() == o.literal.Variable()) {
379 return i_lit.
var < o.i_lit.var;
381 return literal.Variable() < o.literal.Variable();
384 std::vector<InequalityDetectionHelper> inequalities;
387 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
388 if (
ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
391 if (
ct.enforcement_literal().size() != 1)
continue;
392 if (
ct.linear().vars_size() != 1)
continue;
396 const int ref =
ct.linear().vars(0);
400 const Domain domain_if_enforced =
407 if (domain_if_enforced.
Max() >= domain.
Max() &&
408 domain_if_enforced.
Min() > domain.
Min()) {
409 inequalities.push_back(
410 {&
ct, enforcement_literal,
413 implied_bounds->Add(enforcement_literal, inequalities.back().i_lit);
414 }
else if (domain_if_enforced.
Min() <= domain.
Min() &&
415 domain_if_enforced.
Max() < domain.
Max()) {
416 inequalities.push_back(
417 {&
ct, enforcement_literal,
420 implied_bounds->Add(enforcement_literal, inequalities.back().i_lit);
432 var_to_equalities[
var].push_back(
433 {&
ct, enforcement_literal, inter.
Min(),
true});
435 variables_to_encoded_values_[
var].insert(inter.
Min());
443 var_to_equalities[
var].push_back(
444 {&
ct, enforcement_literal, inter.
Min(),
false});
446 variables_to_encoded_values_[
var].insert(inter.
Min());
453 int num_inequalities = 0;
454 std::sort(inequalities.begin(), inequalities.end());
455 for (
int i = 0; i + 1 < inequalities.size(); i++) {
456 if (inequalities[i].
literal != inequalities[i + 1].
literal.Negated()) {
463 if (integer_trail->IntegerLiteralIsTrue(inequalities[i].i_lit) ||
464 integer_trail->IntegerLiteralIsFalse(inequalities[i].i_lit)) {
467 if (integer_trail->IntegerLiteralIsTrue(inequalities[i + 1].i_lit) ||
468 integer_trail->IntegerLiteralIsFalse(inequalities[i + 1].i_lit)) {
472 const auto pair_a = encoder->Canonicalize(inequalities[i].i_lit);
473 const auto pair_b = encoder->Canonicalize(inequalities[i + 1].i_lit);
474 if (pair_a.first == pair_b.second) {
476 encoder->AssociateToIntegerLiteral(inequalities[i].
literal,
477 inequalities[i].i_lit);
478 already_loaded_ct_.insert(inequalities[i].
ct);
479 already_loaded_ct_.insert(inequalities[i + 1].
ct);
484 int num_half_inequalities = 0;
485 for (
const auto inequality : inequalities) {
489 encoder->GetOrCreateAssociatedLiteral(inequality.i_lit)));
490 if (sat_solver->IsModelUnsat())
return;
492 ++num_half_inequalities;
493 already_loaded_ct_.insert(inequality.ct);
494 is_half_encoding_ct_.insert(inequality.ct);
497 if (!inequalities.empty()) {
498 VLOG(1) << num_inequalities <<
" literals associated to VAR >= value, and "
499 << num_half_inequalities <<
" half-associations.";
505 int num_constraints = 0;
506 int num_equalities = 0;
507 int num_half_equalities = 0;
508 int num_fully_encoded = 0;
509 int num_partially_encoded = 0;
510 for (
int i = 0; i < var_to_equalities.size(); ++i) {
511 std::vector<EqualityDetectionHelper>& encoding = var_to_equalities[i];
512 std::sort(encoding.begin(), encoding.end());
513 if (encoding.empty())
continue;
514 num_constraints += encoding.size();
516 absl::flat_hash_set<int64> values;
517 for (
int j = 0; j + 1 < encoding.size(); j++) {
518 if ((encoding[j].
value != encoding[j + 1].
value) ||
520 (encoding[j].is_equality !=
true) ||
521 (encoding[j + 1].is_equality !=
false)) {
526 encoder->AssociateToIntegerEqualValue(encoding[j].
literal, integers_[i],
527 IntegerValue(encoding[j].
value));
528 already_loaded_ct_.insert(encoding[j].
ct);
529 already_loaded_ct_.insert(encoding[j + 1].
ct);
530 values.insert(encoding[j].
value);
536 if (sat_solver->IsModelUnsat())
return;
544 for (
const auto equality : encoding) {
546 const class Literal eq = encoder->GetOrCreateLiteralAssociatedToEquality(
547 integers_[i], IntegerValue(equality.value));
548 if (equality.is_equality) {
554 ++num_half_equalities;
555 already_loaded_ct_.insert(equality.ct);
556 is_half_encoding_ct_.insert(equality.ct);
561 if (encoder->VariableIsFullyEncoded(integers_[i])) {
564 ++num_partially_encoded;
569 if (num_constraints > 0) {
570 VLOG(1) << num_equalities <<
" literals associated to VAR == value, and "
571 << num_half_equalities <<
" half-associations.";
573 if (num_fully_encoded > 0) {
574 VLOG(1) <<
"num_fully_encoded_variables: " << num_fully_encoded;
576 if (num_partially_encoded > 0) {
577 VLOG(1) <<
"num_partially_encoded_variables: " << num_partially_encoded;
587 int64 num_associations = 0;
588 int64 num_set_to_false = 0;
589 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
590 if (!
ct.enforcement_literal().empty())
continue;
591 if (
ct.constraint_case() != ConstraintProto::kLinear)
continue;
592 if (
ct.linear().vars_size() != 2)
continue;
593 if (!ConstraintIsEq(
ct.linear()))
continue;
595 const IntegerValue rhs(
ct.linear().domain(0));
598 IntegerVariable var1 =
Integer(
ct.linear().vars(0));
599 IntegerVariable var2 =
Integer(
ct.linear().vars(1));
600 IntegerValue coeff1(
ct.linear().coeffs(0));
601 IntegerValue coeff2(
ct.linear().coeffs(1));
613 if (coeff1 == 0 || coeff2 == 0)
continue;
618 for (
int i = 0; i < 2; ++i) {
619 for (
const auto value_literal :
620 encoder->PartialGreaterThanEncoding(var1)) {
621 const IntegerValue value1 = value_literal.first;
622 const IntegerValue bound2 =
FloorRatio(rhs - value1 * coeff1, coeff2);
624 encoder->AssociateToIntegerLiteral(
627 std::swap(var1, var2);
628 std::swap(coeff1, coeff2);
636 for (
int i = 0; i < 2; ++i) {
637 for (
const auto value_literal : encoder->PartialDomainEncoding(var1)) {
638 const IntegerValue value1 = value_literal.value;
639 const IntegerValue intermediate = rhs - value1 * coeff1;
640 if (intermediate % coeff2 != 0) {
643 sat_solver->AddUnitClause(value_literal.literal.Negated());
648 intermediate / coeff2);
650 std::swap(var1, var2);
651 std::swap(coeff1, coeff2);
655 if (num_associations > 0) {
656 VLOG(1) <<
"Num associations from equivalences = " << num_associations;
658 if (num_set_to_false > 0) {
659 VLOG(1) <<
"Num literals set to false from equivalences = "
667 if (!
parameters.use_optional_variables())
return;
668 if (
parameters.enumerate_all_solutions())
return;
671 const int num_proto_variables =
model_proto.variables_size();
672 std::vector<bool> already_seen(num_proto_variables,
false);
674 for (
const int ref :
model_proto.objective().vars()) {
687 std::vector<std::vector<int>> enforcement_intersection(num_proto_variables);
688 std::set<int> literals_set;
689 for (
int c = 0; c <
model_proto.constraints_size(); ++c) {
691 if (
ct.enforcement_literal().empty()) {
693 already_seen[
var] =
true;
694 enforcement_intersection[
var].clear();
697 literals_set.clear();
698 literals_set.insert(
ct.enforcement_literal().begin(),
699 ct.enforcement_literal().end());
701 if (!already_seen[
var]) {
702 enforcement_intersection[
var].assign(
ct.enforcement_literal().begin(),
703 ct.enforcement_literal().end());
706 std::vector<int>& vector_ref = enforcement_intersection[
var];
708 for (
const int literal : vector_ref) {
710 vector_ref[new_size++] =
literal;
713 vector_ref.resize(new_size);
715 already_seen[
var] =
true;
721 int num_optionals = 0;
723 for (
int var = 0;
var < num_proto_variables; ++
var) {
724 const IntegerVariableProto& var_proto =
model_proto.variables(
var);
725 const int64 min = var_proto.domain(0);
726 const int64 max = var_proto.domain(var_proto.domain().size() - 1);
728 if (
min == 0 &&
max == 1)
continue;
729 if (enforcement_intersection[
var].empty())
continue;
732 integer_trail->MarkIntegerVariableAsOptional(
735 VLOG(2) <<
"Auto-detected " << num_optionals <<
" optional variables.";
747 parameters_(*(
model->GetOrCreate<SatParameters>())),
756 DEFINE_INT_TYPE(ConstraintIndex,
int32);
759 void Register(ConstraintIndex ct_index,
int variable) {
761 constraint_is_registered_[ct_index] =
true;
762 if (variable_watchers_.size() <= variable) {
763 variable_watchers_.resize(variable + 1);
764 variable_was_added_in_to_propagate_.resize(variable + 1);
766 variable_watchers_[variable].push_back(ct_index);
769 void AddVariableToPropagationQueue(
int variable) {
771 if (variable_was_added_in_to_propagate_.size() <= variable) {
772 variable_watchers_.resize(variable + 1);
773 variable_was_added_in_to_propagate_.resize(variable + 1);
775 if (!variable_was_added_in_to_propagate_[variable]) {
776 variable_was_added_in_to_propagate_[variable] =
true;
777 variables_to_propagate_.push_back(variable);
782 const bool IsFullyEncoded(
int v) {
783 const IntegerVariable variable = mapping_->
Integer(v);
785 return integer_trail_->
IsFixed(variable) ||
789 const bool VariableIsFixed(
int v) {
790 const IntegerVariable variable = mapping_->
Integer(v);
792 return integer_trail_->
IsFixed(variable);
795 void FullyEncode(
int v) {
797 const IntegerVariable variable = mapping_->
Integer(v);
799 if (!integer_trail_->
IsFixed(variable)) {
802 AddVariableToPropagationQueue(v);
805 bool ProcessConstraint(ConstraintIndex ct_index);
806 bool ProcessElement(ConstraintIndex ct_index);
807 bool ProcessTable(ConstraintIndex ct_index);
808 bool ProcessAutomaton(ConstraintIndex ct_index);
809 bool ProcessLinear(ConstraintIndex ct_index);
811 const CpModelProto& model_proto_;
812 const SatParameters& parameters_;
815 CpModelMapping* mapping_;
816 IntegerEncoder* integer_encoder_;
817 IntegerTrail* integer_trail_;
819 std::vector<bool> variable_was_added_in_to_propagate_;
820 std::vector<int> variables_to_propagate_;
821 std::vector<std::vector<ConstraintIndex>> variable_watchers_;
826 absl::flat_hash_map<int, absl::flat_hash_set<int>>
827 variables_to_equal_or_diff_variables_;
833 const int num_constraints = model_proto_.constraints_size();
834 const int num_vars = model_proto_.variables_size();
835 constraint_is_finished_.
assign(num_constraints,
false);
836 constraint_is_registered_.
assign(num_constraints,
false);
839 for (ConstraintIndex ct_index(0); ct_index < num_constraints; ++ct_index) {
840 constraint_is_finished_[ct_index] = ProcessConstraint(ct_index);
850 int num_variables_fully_encoded_by_heuristics = 0;
851 for (
int var = 0;
var < num_vars; ++
var) {
853 const IntegerVariableProto& int_var_proto = model_proto_.variables(
var);
856 int64 num_diff_or_equal_var_constraints = 0;
857 int64 num_potential_encoded_values_without_bounds = 0;
859 if (domain_size <= 2)
continue;
861 const absl::flat_hash_set<int64>& value_set =
863 for (
const int value : value_set) {
866 num_potential_encoded_values_without_bounds++;
870 const auto& it = variables_to_equal_or_diff_variables_.find(
var);
871 if (it != variables_to_equal_or_diff_variables_.end()) {
872 num_diff_or_equal_var_constraints = it->second.size();
875 if (num_potential_encoded_values_without_bounds >= domain_size / 2 ||
876 (num_diff_or_equal_var_constraints >= domain_size / 2 &&
878 VLOG(3) << model_proto_.variables(
var).ShortDebugString()
879 <<
" is encoded with "
880 << num_potential_encoded_values_without_bounds
881 <<
" unary constraints, and " << num_diff_or_equal_var_constraints
882 <<
" binary constraints on a domain of size " << domain_size;
884 num_variables_fully_encoded_by_heuristics++;
887 if (num_variables_fully_encoded_by_heuristics > 0) {
888 VLOG(2) << num_variables_fully_encoded_by_heuristics
889 <<
" variables fully encoded after model introspection.";
893 for (
int v = 0; v < variable_watchers_.size(); v++) {
894 if (!variable_watchers_[v].empty() && IsFullyEncoded(v)) {
895 AddVariableToPropagationQueue(v);
900 while (!variables_to_propagate_.empty()) {
901 const int variable = variables_to_propagate_.back();
902 variables_to_propagate_.pop_back();
903 for (
const ConstraintIndex ct_index : variable_watchers_[variable]) {
904 if (constraint_is_finished_[ct_index])
continue;
905 constraint_is_finished_[ct_index] = ProcessConstraint(ct_index);
911 bool FullEncodingFixedPointComputer::ProcessConstraint(
912 ConstraintIndex ct_index) {
913 const ConstraintProto&
ct = model_proto_.constraints(ct_index.value());
914 switch (
ct.constraint_case()) {
915 case ConstraintProto::ConstraintProto::kElement:
916 return ProcessElement(ct_index);
917 case ConstraintProto::ConstraintProto::kTable:
918 return ProcessTable(ct_index);
919 case ConstraintProto::ConstraintProto::kAutomaton:
920 return ProcessAutomaton(ct_index);
921 case ConstraintProto::ConstraintProto::kLinear:
922 return ProcessLinear(ct_index);
928 bool FullEncodingFixedPointComputer::ProcessElement(ConstraintIndex ct_index) {
929 const ConstraintProto&
ct = model_proto_.constraints(ct_index.value());
932 FullyEncode(
ct.element().index());
934 const int target =
ct.element().target();
937 if (VariableIsFixed(target))
return true;
940 if (IsFullyEncoded(target)) {
941 for (
const int v :
ct.element().vars()) FullyEncode(v);
945 bool all_variables_are_fully_encoded =
true;
946 for (
const int v :
ct.element().vars()) {
947 if (v == target)
continue;
948 if (!IsFullyEncoded(v)) {
949 all_variables_are_fully_encoded =
false;
953 if (all_variables_are_fully_encoded) {
954 if (!IsFullyEncoded(target)) FullyEncode(target);
959 if (constraint_is_registered_[ct_index]) {
960 for (
const int v :
ct.element().vars()) Register(ct_index, v);
961 Register(ct_index, target);
966 bool FullEncodingFixedPointComputer::ProcessTable(ConstraintIndex ct_index) {
967 const ConstraintProto&
ct = model_proto_.constraints(ct_index.value());
969 if (
ct.table().negated())
return true;
971 for (
const int variable :
ct.table().vars()) {
972 FullyEncode(variable);
978 bool FullEncodingFixedPointComputer::ProcessAutomaton(
979 ConstraintIndex ct_index) {
980 const ConstraintProto&
ct = model_proto_.constraints(ct_index.value());
981 for (
const int variable :
ct.automaton().vars()) {
982 FullyEncode(variable);
987 bool FullEncodingFixedPointComputer::ProcessLinear(ConstraintIndex ct_index) {
990 const ConstraintProto&
ct = model_proto_.constraints(ct_index.value());
991 if (parameters_.boolean_encoding_level() == 0 ||
992 ct.linear().vars_size() != 2) {
996 if (!ConstraintIsEq(
ct.linear()) &&
997 !ConstraintIsNEq(
ct.linear(), mapping_, integer_trail_,
nullptr)) {
1001 const int var0 =
ct.linear().vars(0);
1002 const int var1 =
ct.linear().vars(1);
1003 if (!IsFullyEncoded(var0)) {
1004 variables_to_equal_or_diff_variables_[var0].insert(var1);
1006 if (!IsFullyEncoded(var1)) {
1007 variables_to_equal_or_diff_variables_[var1].insert(var0);
1023 std::vector<Literal> literals = mapping->
Literals(
ct.bool_or().literals());
1024 for (
const int ref :
ct.enforcement_literal()) {
1025 literals.push_back(mapping->Literal(ref).Negated());
1032 std::vector<Literal> literals;
1033 for (
const int ref :
ct.enforcement_literal()) {
1034 literals.push_back(mapping->Literal(ref).Negated());
1037 for (
const Literal literal : mapping->Literals(
ct.bool_and().literals())) {
1040 literals.pop_back();
1066 void 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 for (
const auto value_literal : encoder->FullDomainEncoding(var2)) {
1079 const IntegerValue target = rhs - value_literal.value * coeff2;
1082 {value_literal.literal.Negated()}));
1084 const Literal target_literal = term1_value_to_literal[target];
1086 {value_literal.literal.Negated(), target_literal}));
1088 {value_literal.literal, target_literal.Negated()}));
1092 term1_value_to_literal.erase(target);
1098 std::vector<Literal> implied_false;
1099 for (
const auto entry : term1_value_to_literal) {
1100 implied_false.push_back(entry.second);
1102 std::sort(implied_false.begin(), implied_false.end());
1103 for (
const Literal l : implied_false) {
1110 void LoadEquivalenceNeqAC(
const std::vector<Literal> enforcement_literal,
1111 IntegerValue coeff1, IntegerVariable var1,
1112 IntegerValue coeff2, IntegerVariable var2,
1113 const IntegerValue rhs, Model* m) {
1114 auto* encoder = m->GetOrCreate<IntegerEncoder>();
1115 CHECK(encoder->VariableIsFullyEncoded(var1));
1116 CHECK(encoder->VariableIsFullyEncoded(var2));
1117 absl::flat_hash_map<IntegerValue, Literal> term1_value_to_literal;
1118 for (
const auto value_literal : encoder->FullDomainEncoding(var1)) {
1119 term1_value_to_literal[coeff1 * value_literal.value] =
1120 value_literal.literal;
1122 for (
const auto value_literal : encoder->FullDomainEncoding(var2)) {
1123 const IntegerValue target_value = rhs - value_literal.value * coeff2;
1124 const auto& it = term1_value_to_literal.find(target_value);
1125 if (it != term1_value_to_literal.end()) {
1126 const Literal target_literal = it->second;
1128 enforcement_literal,
1129 {value_literal.literal.Negated(), target_literal.Negated()}));
1138 if (
ct.linear().vars().empty()) {
1142 std::vector<Literal> clause;
1143 for (
const int ref :
ct.enforcement_literal()) {
1144 clause.push_back(mapping->Literal(ref).Negated());
1148 VLOG(1) <<
"Trivially UNSAT constraint: " <<
ct.DebugString();
1155 const std::vector<IntegerVariable> vars =
1156 mapping->Integers(
ct.linear().vars());
1157 const std::vector<int64> coeffs = ValuesFromProto(
ct.linear().coeffs());
1163 IntegerValue min_sum(0);
1164 IntegerValue max_sum(0);
1165 IntegerValue max_domain_size(0);
1166 bool all_booleans =
true;
1167 for (
int i = 0; i < vars.size(); ++i) {
1168 if (all_booleans && !mapping->IsBoolean(
ct.linear().vars(i))) {
1169 all_booleans =
false;
1171 const IntegerValue lb = integer_trail->LowerBound(vars[i]);
1172 const IntegerValue ub = integer_trail->UpperBound(vars[i]);
1173 max_domain_size =
std::max(max_domain_size, ub - lb + 1);
1174 const IntegerValue term_a = coeffs[i] * lb;
1175 const IntegerValue term_b = coeffs[i] * ub;
1176 min_sum +=
std::min(term_a, term_b);
1177 max_sum +=
std::max(term_a, term_b);
1180 if (
ct.linear().vars_size() == 2 && !integer_trail->IsFixed(vars[0]) &&
1181 !integer_trail->IsFixed(vars[1]) && max_domain_size < 16) {
1182 const SatParameters& params = *m->
GetOrCreate<SatParameters>();
1184 if (params.boolean_encoding_level() > 0 && ConstraintIsEq(
ct.linear()) &&
1185 ct.linear().domain(0) != min_sum &&
ct.linear().domain(0) != max_sum &&
1186 encoder->VariableIsFullyEncoded(vars[0]) &&
1187 encoder->VariableIsFullyEncoded(vars[1])) {
1188 VLOG(3) <<
"Load AC version of " <<
ct.DebugString() <<
", var0 domain = "
1189 << integer_trail->InitialVariableDomain(vars[0])
1190 <<
", var1 domain = "
1191 << integer_trail->InitialVariableDomain(vars[1]);
1192 return LoadEquivalenceAC(mapping->Literals(
ct.enforcement_literal()),
1193 IntegerValue(coeffs[0]), vars[0],
1194 IntegerValue(coeffs[1]), vars[1],
1195 IntegerValue(
ct.linear().domain(0)), m);
1198 int64 single_value = 0;
1199 if (params.boolean_encoding_level() > 0 &&
1200 ConstraintIsNEq(
ct.linear(), mapping, integer_trail, &single_value) &&
1201 single_value != min_sum && single_value != max_sum &&
1202 encoder->VariableIsFullyEncoded(vars[0]) &&
1203 encoder->VariableIsFullyEncoded(vars[1])) {
1204 VLOG(3) <<
"Load NAC version of " <<
ct.DebugString()
1205 <<
", var0 domain = "
1206 << integer_trail->InitialVariableDomain(vars[0])
1207 <<
", var1 domain = "
1208 << integer_trail->InitialVariableDomain(vars[1])
1209 <<
", value = " << single_value;
1210 return LoadEquivalenceNeqAC(mapping->Literals(
ct.enforcement_literal()),
1211 IntegerValue(coeffs[0]), vars[0],
1212 IntegerValue(coeffs[1]), vars[1],
1213 IntegerValue(single_value), m);
1217 if (
ct.linear().domain_size() == 2) {
1218 int64 lb =
ct.linear().domain(0);
1219 int64 ub =
ct.linear().domain(1);
1227 std::vector<LiteralWithCoeff> cst;
1228 for (
int i = 0; i < vars.size(); ++i) {
1229 const int ref =
ct.linear().vars(i);
1230 cst.push_back({mapping->Literal(ref), coeffs[i]});
1242 const std::vector<Literal> enforcement_literals =
1243 mapping->Literals(
ct.enforcement_literal());
1256 const bool special_case =
1257 ct.enforcement_literal().empty() &&
ct.linear().domain_size() == 4;
1259 std::vector<Literal> clause;
1260 for (
int i = 0; i <
ct.linear().domain_size(); i += 2) {
1261 int64 lb =
ct.linear().domain(i);
1262 int64 ub =
ct.linear().domain(i + 1);
1266 const Literal subdomain_literal(
1267 special_case && i > 0 ? clause.back().Negated()
1269 clause.push_back(subdomain_literal);
1280 for (
const int ref :
ct.enforcement_literal()) {
1281 clause.push_back(mapping->Literal(ref).Negated());
1289 const std::vector<IntegerVariable> vars =
1295 int num_fully_encoded = 0;
1296 int64 max_domain_size = 0;
1297 for (
const IntegerVariable variable : vars) {
1298 if (encoder->VariableIsFullyEncoded(variable)) num_fully_encoded++;
1300 IntegerValue lb = integer_trail->
LowerBound(variable);
1301 IntegerValue ub = integer_trail->
UpperBound(variable);
1302 const int64 domain_size = ub.value() - lb.value() + 1;
1303 max_domain_size =
std::max(max_domain_size, domain_size);
1306 if (num_fully_encoded == vars.size() && max_domain_size < 1024) {
1316 const IntegerVariable prod = mapping->
Integer(
ct.int_prod().target());
1317 const std::vector<IntegerVariable> vars =
1318 mapping->Integers(
ct.int_prod().vars());
1319 CHECK_EQ(vars.size(), 2) <<
"General int_prod not supported yet.";
1325 const IntegerVariable div = mapping->
Integer(
ct.int_div().target());
1326 const std::vector<IntegerVariable> vars =
1327 mapping->Integers(
ct.int_div().vars());
1329 const IntegerValue denom(m->
Get(
Value(vars[1])));
1342 const IntegerVariable
min = mapping->Integer(
ct.int_min().target());
1343 const std::vector<IntegerVariable> vars =
1344 mapping->Integers(
ct.int_min().vars());
1352 for (
int j = 0; j < expr_proto.coeffs_size(); ++j) {
1353 expr.
coeffs.push_back(IntegerValue(expr_proto.coeffs(j)));
1355 expr.
offset = IntegerValue(expr_proto.offset());
1363 std::vector<LinearExpression> negated_exprs;
1364 negated_exprs.reserve(
ct.lin_max().exprs_size());
1365 for (
int i = 0; i <
ct.lin_max().exprs_size(); ++i) {
1366 negated_exprs.push_back(
1375 const IntegerVariable
max = mapping->Integer(
ct.int_max().target());
1376 const std::vector<IntegerVariable> vars =
1377 mapping->Integers(
ct.int_max().vars());
1387 if (
ct.no_overlap_2d().x_intervals().empty())
return;
1389 const std::vector<IntervalVariable> x_intervals =
1390 mapping->
Intervals(
ct.no_overlap_2d().x_intervals());
1391 const std::vector<IntervalVariable> y_intervals =
1392 mapping->Intervals(
ct.no_overlap_2d().y_intervals());
1394 x_intervals, y_intervals,
1395 !
ct.no_overlap_2d().boxes_with_null_area_can_overlap()));
1400 const std::vector<IntervalVariable> intervals =
1403 std::vector<AffineExpression> demands;
1404 for (
const IntegerVariable
var :
1405 mapping->Integers(
ct.cumulative().demands())) {
1414 std::vector<AffineExpression> times;
1415 std::vector<IntegerValue> deltas;
1416 std::vector<Literal> presences;
1417 const int size =
ct.reservoir().times().size();
1418 for (
int i = 0; i < size; ++i) {
1419 times.push_back(mapping->Integer(
ct.reservoir().times(i)));
1420 deltas.push_back(IntegerValue(
ct.reservoir().demands(i)));
1421 if (!
ct.reservoir().actives().empty()) {
1422 presences.push_back(mapping->Literal(
ct.reservoir().actives(i)));
1424 presences.push_back(encoder->GetTrueLiteral());
1428 ct.reservoir().max_level(), m);
1440 const IntegerVariable
index = mapping->Integer(
ct.element().index());
1441 const IntegerVariable target = mapping->Integer(
ct.element().target());
1442 const std::vector<IntegerVariable> vars =
1443 mapping->Integers(
ct.element().vars());
1447 Domain union_of_non_constant_domains;
1448 std::map<IntegerValue, int> constant_to_num;
1450 const int i = literal_value.value.value();
1453 constant_to_num[
value]++;
1455 union_of_non_constant_domains = union_of_non_constant_domains.
UnionWith(
1456 integer_trail->InitialVariableDomain(vars[i]));
1461 for (
const auto entry : constant_to_num) {
1462 if (union_of_non_constant_domains.
Contains(entry.first.value())) {
1463 constant_to_num[entry.first]++;
1469 bool is_one_to_one_mapping =
true;
1471 const int i = literal_value.value.value();
1473 is_one_to_one_mapping =
false;
1478 if (constant_to_num[
value] == 1) {
1479 const Literal r = literal_value.literal;
1480 encoder->AssociateToIntegerEqualValue(r, target,
value);
1482 is_one_to_one_mapping =
false;
1486 return is_one_to_one_mapping;
1494 const IntegerVariable
index = mapping->Integer(
ct.element().index());
1495 const IntegerVariable target = mapping->Integer(
ct.element().target());
1496 const std::vector<IntegerVariable> vars =
1497 mapping->Integers(
ct.element().vars());
1502 std::vector<Literal> selectors;
1503 std::vector<IntegerVariable> possible_vars;
1504 for (
const auto literal_value : encoding) {
1505 const int i = literal_value.value.value();
1508 possible_vars.push_back(vars[i]);
1509 selectors.push_back(literal_value.literal);
1510 const Literal r = literal_value.literal;
1512 if (vars[i] == target)
continue;
1546 const IntegerVariable
index = mapping->Integer(
ct.element().index());
1547 const IntegerVariable target = mapping->Integer(
ct.element().target());
1548 const std::vector<IntegerVariable> vars =
1549 mapping->Integers(
ct.element().vars());
1553 absl::flat_hash_map<IntegerValue, Literal> target_map;
1555 for (
const auto literal_value : target_encoding) {
1556 target_map[literal_value.value] = literal_value.literal;
1561 absl::flat_hash_map<IntegerValue, std::vector<Literal>> value_to_literals;
1564 for (
const auto literal_value : index_encoding) {
1565 const int i = literal_value.value.value();
1566 const Literal i_lit = literal_value.literal;
1570 value_to_literals[integer_trail->
LowerBound(vars[i])].push_back(i_lit);
1575 std::vector<Literal> var_selected_literals;
1576 for (
const auto var_literal_value : var_encoding) {
1577 const IntegerValue
value = var_literal_value.value;
1578 const Literal var_is_value = var_literal_value.literal;
1587 const Literal var_is_value_and_selected =
1590 value_to_literals[
value].push_back(var_is_value_and_selected);
1591 var_selected_literals.push_back(var_is_value_and_selected);
1598 for (
const auto& entry : target_map) {
1599 const IntegerValue
value = entry.first;
1600 const Literal target_is_value = entry.second;
1618 void LoadElementConstraintHalfAC(
const ConstraintProto&
ct, Model* m) {
1619 auto* mapping = m->GetOrCreate<CpModelMapping>();
1620 const IntegerVariable
index = mapping->Integer(
ct.element().index());
1621 const IntegerVariable target = mapping->Integer(
ct.element().target());
1622 const std::vector<IntegerVariable> vars =
1623 mapping->Integers(
ct.element().vars());
1629 const int i = value_literal.value.value();
1631 LoadEquivalenceAC({value_literal.literal}, IntegerValue(1), vars[i],
1632 IntegerValue(-1), target, IntegerValue(0), m);
1636 void LoadBooleanElement(
const ConstraintProto&
ct, Model* m) {
1637 auto* mapping = m->GetOrCreate<CpModelMapping>();
1638 const IntegerVariable
index = mapping->Integer(
ct.element().index());
1639 const std::vector<Literal> literals = mapping->Literals(
ct.element().vars());
1640 const Literal target = mapping->Literal(
ct.element().target());
1647 std::vector<Literal> all_true;
1648 std::vector<Literal> all_false;
1650 const Literal a_lit = literals[value_literal.value.value()];
1651 const Literal i_lit = value_literal.literal;
1654 all_true.push_back(a_lit.Negated());
1655 all_false.push_back(a_lit);
1657 all_true.push_back(target);
1658 all_false.push_back(target.Negated());
1668 const IntegerVariable
index = mapping->Integer(
ct.element().index());
1670 bool boolean_array =
true;
1671 for (
const int ref :
ct.element().vars()) {
1672 if (!mapping->IsBoolean(ref)) {
1673 boolean_array =
false;
1677 if (boolean_array && !mapping->IsBoolean(
ct.element().target())) {
1679 VLOG(1) <<
"Fix boolean_element not propagated on target";
1680 boolean_array =
false;
1685 if (boolean_array) {
1686 LoadBooleanElement(
ct, m);
1690 const IntegerVariable target = mapping->Integer(
ct.element().target());
1691 const std::vector<IntegerVariable> vars =
1692 mapping->Integers(
ct.element().vars());
1721 int num_AC_variables = 0;
1722 const int num_vars =
ct.element().vars().size();
1723 for (
const int v :
ct.element().vars()) {
1724 IntegerVariable variable = mapping->Integer(v);
1725 const bool is_full =
1727 if (is_full) num_AC_variables++;
1730 const SatParameters& params = *m->
GetOrCreate<SatParameters>();
1731 if (params.boolean_encoding_level() > 0 &&
1732 (target_is_AC || num_AC_variables >= num_vars - 1)) {
1733 if (params.boolean_encoding_level() > 1) {
1736 LoadElementConstraintHalfAC(
ct, m);
1745 const std::vector<IntegerVariable> vars =
1747 const std::vector<int64> values = ValuesFromProto(
ct.table().values());
1748 const int num_vars = vars.size();
1749 const int num_tuples = values.size() / num_vars;
1750 std::vector<std::vector<int64>> tuples(num_tuples);
1752 for (
int i = 0; i < num_tuples; ++i) {
1753 for (
int j = 0; j < num_vars; ++j) {
1754 tuples[i].push_back(values[count++]);
1757 if (
ct.table().negated()) {
1766 const std::vector<IntegerVariable> vars =
1769 const int num_transitions =
ct.automaton().transition_tail_size();
1770 std::vector<std::vector<int64>> transitions;
1771 transitions.reserve(num_transitions);
1772 for (
int i = 0; i < num_transitions; ++i) {
1773 transitions.push_back({
ct.automaton().transition_tail(i),
1774 ct.automaton().transition_label(i),
1775 ct.automaton().transition_head(i)});
1778 const int64 starting_state =
ct.automaton().starting_state();
1779 const std::vector<int64> final_states =
1780 ValuesFromProto(
ct.automaton().final_states());
1787 const std::vector<IntegerVariable>& vars,
Model* m) {
1788 const int n = vars.size();
1793 std::vector<std::vector<Literal>> matrix(
1794 n, std::vector<Literal>(n, kFalseLiteral));
1795 for (
int i = 0; i < n; i++) {
1796 for (
int j = 0; j < n; j++) {
1801 matrix[i][
value] = kTrueLiteral;
1804 for (
const auto& entry : encoding) {
1805 const int value = entry.value.value();
1808 matrix[i][
value] = entry.literal;
1817 const auto& circuit =
ct.circuit();
1818 if (circuit.tails().empty())
return;
1820 std::vector<int> tails(circuit.tails().begin(), circuit.tails().end());
1821 std::vector<int> heads(circuit.heads().begin(), circuit.heads().end());
1822 std::vector<Literal> literals =
1824 const int num_nodes =
ReindexArcs(&tails, &heads);
1829 const auto& routes =
ct.routes();
1830 if (routes.tails().empty())
return;
1832 std::vector<int> tails(routes.tails().begin(), routes.tails().end());
1833 std::vector<int> heads(routes.heads().begin(), routes.heads().end());
1834 std::vector<Literal> literals =
1836 const int num_nodes =
ReindexArcs(&tails, &heads);
1842 switch (
ct.constraint_case()) {
1843 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1845 case ConstraintProto::ConstraintCase::kBoolOr:
1848 case ConstraintProto::ConstraintCase::kBoolAnd:
1851 case ConstraintProto::ConstraintCase::kAtMostOne:
1854 case ConstraintProto::ConstraintCase::kExactlyOne:
1857 case ConstraintProto::ConstraintCase::kBoolXor:
1860 case ConstraintProto::ConstraintProto::kLinear:
1863 case ConstraintProto::ConstraintProto::kAllDiff:
1866 case ConstraintProto::ConstraintProto::kIntProd:
1869 case ConstraintProto::ConstraintProto::kIntDiv:
1872 case ConstraintProto::ConstraintProto::kIntMin:
1875 case ConstraintProto::ConstraintProto::kLinMax:
1878 case ConstraintProto::ConstraintProto::kIntMax:
1881 case ConstraintProto::ConstraintProto::kInterval:
1884 case ConstraintProto::ConstraintProto::kNoOverlap:
1887 case ConstraintProto::ConstraintProto::kNoOverlap2D:
1890 case ConstraintProto::ConstraintProto::kCumulative:
1893 case ConstraintProto::ConstraintProto::kReservoir:
1896 case ConstraintProto::ConstraintProto::kElement:
1899 case ConstraintProto::ConstraintProto::kTable:
1902 case ConstraintProto::ConstraintProto::kAutomaton:
1905 case ConstraintProto::ConstraintProto::kCircuit:
1908 case ConstraintProto::ConstraintProto::kRoutes:
#define DCHECK_LE(val1, val2)
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define DCHECK_LT(val1, val2)
#define VLOG(verboselevel)
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
Domain Complement() const
Returns the set Int64 ∖ D.
int64 Size() const
Returns the number of elements in the domain.
int NumIntervals() const
Basic read-only std::vector<> wrapping to view a Domain as a sorted list of non-adjacent intervals.
Domain InverseMultiplicationBy(const int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
int64 Min() const
Returns the min value of the domain.
Domain UnionWith(const Domain &domain) const
Returns the union of D and domain.
int64 Max() const
Returns the max value of the domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
bool IsEmpty() const
Returns true if this is the empty set.
bool Contains(int64 value) const
Returns true iff value is in Domain.
std::vector< sat::Literal > Literals(const ProtoIndices &indices) const
AffineExpression LoadAffineView(const LinearExpressionProto &exp) const
std::vector< IntegerVariable > Integers(const List &list) const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
bool IsBoolean(int ref) const
void LoadBooleanSymmetries(const CpModelProto &model_proto, Model *m)
bool IsInteger(int ref) const
bool ConstraintIsAlreadyLoaded(const ConstraintProto *ct) const
IntegerVariable Integer(int ref) const
sat::Literal Literal(int ref) const
void DetectOptionalVariables(const CpModelProto &model_proto, Model *m)
const absl::flat_hash_set< int64 > & PotentialEncodedValues(int var)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
void PropagateEncodingFromEquivalenceRelations(const CpModelProto &model_proto, Model *m)
void CreateVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
FullEncodingFixedPointComputer(const CpModelProto &model_proto, Model *model)
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
bool VariableIsFullyEncoded(IntegerVariable var) const
void ReserveSpaceForNumVariables(int num_vars)
bool IsFixed(IntegerVariable i) const
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue LowerBound(IntegerVariable i) const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
T Add(std::function< T(Model *)> f)
This makes it possible to have a nicer API on the client side, and it allows both of these forms:
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
bool AddProblemClause(absl::Span< const Literal > literals)
CpModelProto const * model_proto
static const int64 kint64max
static const int64 kint64min
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
bool ContainsKey(const Collection &collection, const Key &key)
void LoadTableConstraint(const ConstraintProto &ct, Model *m)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::function< void(Model *)> ConditionalWeightedSumLowerOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
std::function< void(Model *)> AllDifferentAC(const std::vector< IntegerVariable > &variables)
std::function< void(Model *)> NonOverlappingRectangles(const std::vector< IntervalVariable > &x, const std::vector< IntervalVariable > &y, bool is_strict)
std::function< void(Model *)> IsEqualToMaxOf(IntegerVariable max_var, const std::vector< IntegerVariable > &vars)
void LoadExactlyOneConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
void LoadIntProdConstraint(const ConstraintProto &ct, Model *m)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
std::vector< int > UsedVariables(const ConstraintProto &ct)
void LoadBoolOrConstraint(const ConstraintProto &ct, Model *m)
bool RefIsPositive(int ref)
std::function< void(Model *)> DivisionConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable c)
void MaybeFullyEncodeMoreVariables(const CpModelProto &model_proto, Model *m)
const LiteralIndex kNoLiteralIndex(-1)
std::function< void(Model *)> TransitionConstraint(const std::vector< IntegerVariable > &vars, const std::vector< std::vector< int64 >> &automaton, int64 initial_state, const std::vector< int64 > &final_states)
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
std::function< void(Model *)> PartialIsOneOfVar(IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
std::function< void(Model *)> LiteralXorIs(const std::vector< Literal > &literals, bool value)
std::function< void(Model *)> ConditionalLowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
std::function< void(Model *)> SubcircuitConstraint(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, bool multiple_subcircuit_through_zero)
std::function< int64(const Model &)> Value(IntegerVariable v)
bool HasEnforcementLiteral(const ConstraintProto &ct)
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< IntegerVariable > &vars)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >Model *)> FullyEncodeVariable(IntegerVariable var)
bool DetectEquivalencesInElementConstraint(const ConstraintProto &ct, Model *m)
void LoadCumulativeConstraint(const ConstraintProto &ct, Model *m)
void LoadRoutesConstraint(const ConstraintProto &ct, Model *m)
void LoadReservoirConstraint(const ConstraintProto &ct, Model *m)
void AddTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 >> tuples, Model *model)
void LoadBoolAndConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
void LoadLinMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadBoolXorConstraint(const ConstraintProto &ct, Model *m)
LinearExpression GetExprFromProto(const LinearExpressionProto &expr_proto, const CpModelMapping &mapping)
const IntegerVariable kNoIntegerVariable(-1)
const IntervalVariable kNoIntervalVariable(-1)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
LinearExpression CanonicalizeExpr(const LinearExpression &expr)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
std::function< void(Model *)> ImpliesInInterval(Literal in_interval, IntegerVariable v, int64 lb, int64 ub)
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
std::vector< std::vector< Literal > > GetSquareMatrixFromIntegerVariables(const std::vector< IntegerVariable > &vars, Model *m)
void LoadIntDivConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ConditionalWeightedSumGreaterOrEqual(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
std::function< void(Model *)> FixedDivisionConstraint(IntegerVariable a, IntegerValue b, IntegerVariable c)
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< IntegerValue > deltas, std::vector< Literal > presences, int64 min_level, int64 max_level, Model *model)
int ReindexArcs(IntContainer *tails, IntContainer *heads)
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
void LoadAtMostOneConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> AllDifferentBinary(const std::vector< IntegerVariable > &vars)
void LoadCircuitConstraint(const ConstraintProto &ct, Model *m)
void LoadIntMaxConstraint(const ConstraintProto &ct, Model *m)
void LoadNoOverlapConstraint(const ConstraintProto &ct, Model *m)
void LoadAllDiffConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
void AddNegatedTableConstraint(absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 >> tuples, Model *model)
void LoadElementConstraint(const ConstraintProto &ct, Model *m)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
void LoadAutomatonConstraint(const ConstraintProto &ct, Model *m)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
std::function< void(Model *)> IsEqualToMinOf(IntegerVariable min_var, const std::vector< IntegerVariable > &vars)
void LoadNoOverlap2dConstraint(const ConstraintProto &ct, Model *m)
void LoadIntMinConstraint(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> AtMostOneConstraint(const std::vector< Literal > &literals)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
const BooleanVariable kNoBooleanVariable(-1)
std::function< void(Model *)> ProductConstraint(IntegerVariable a, IntegerVariable b, IntegerVariable p)
void LoadElementConstraintAC(const ConstraintProto &ct, Model *m)
void LoadElementConstraintBounds(const ConstraintProto &ct, Model *m)
std::function< void(Model *)> ReifiedBoolOr(const std::vector< Literal > &literals, Literal r)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::vector< int > variables
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars
#define VLOG_IS_ON(verboselevel)