18 #include "absl/container/flat_hash_set.h"
21 #include "ortools/sat/cp_model.pb.h"
36 if (encoder ==
nullptr)
return false;
37 if (!encoder->VariableIsFullyEncoded(
var))
return false;
48 std::vector<Literal> at_most_one;
50 for (
const auto value_literal : encoding) {
51 const Literal lit = value_literal.literal;
52 const IntegerValue
delta = value_literal.value - var_min;
54 at_most_one.push_back(lit);
55 if (!at_least_one.
AddLiteralTerm(lit, IntegerValue(1)))
return false;
56 if (
delta != IntegerValue(0)) {
70 std::pair<IntegerValue, IntegerValue> GetMinAndMaxNotEncoded(
72 const absl::flat_hash_set<IntegerValue>& encoded_values,
74 const auto* domains =
model.Get<IntegerDomains>();
75 if (domains ==
nullptr ||
var >= domains->size()) {
82 for (
const ClosedInterval
interval : (*domains)[
var]) {
93 const auto& domain = (*domains)[
var];
94 for (
int i = domain.NumIntervals() - 1; i >= 0; --i) {
95 const ClosedInterval
interval = domain[i];
114 if (encoder ==
nullptr || integer_trail ==
nullptr)
return;
116 const std::vector<IntegerEncoder::ValueLiteralPair>& encoding =
117 encoder->PartialDomainEncoding(
var);
118 if (encoding.empty())
return;
120 std::vector<Literal> at_most_one_ct;
121 absl::flat_hash_set<IntegerValue> encoded_values;
122 for (
const auto value_literal : encoding) {
131 at_most_one_ct.push_back(
literal);
132 encoded_values.insert(value_literal.value);
134 if (encoded_values.empty())
return;
140 const auto pair = GetMinAndMaxNotEncoded(
var, encoded_values,
model);
150 for (
const auto value_literal : encoding) {
151 const Literal lit = value_literal.literal;
154 encoding_ct.
AddLiteralTerm(lit, IntegerValue(-value_literal.value)));
162 const IntegerValue d_min = pair.first;
165 for (
const auto value_literal : encoding) {
167 d_min - value_literal.value));
171 const IntegerValue d_max = pair.second;
174 for (
const auto value_literal : encoding) {
176 d_max - value_literal.value));
190 if (integer_trail ==
nullptr || encoder ==
nullptr)
return;
192 const std::map<IntegerValue, Literal>& greater_than_encoding =
193 encoder->PartialGreaterThanEncoding(
var);
194 if (greater_than_encoding.empty())
return;
199 IntegerValue prev_used_bound = integer_trail->
LowerBound(
var);
204 for (
const auto entry : greater_than_encoding) {
205 if (entry.first <= prev_used_bound)
continue;
207 const LiteralIndex literal_index = entry.second.Index();
208 const IntegerValue diff = prev_used_bound - entry.first;
217 prev_used_bound = entry.first;
218 prev_literal_index = literal_index;
226 IntegerValue prev_used_bound = integer_trail->LowerBound(
NegationOf(
var));
230 for (
const auto entry :
232 if (entry.first <= prev_used_bound)
continue;
233 const IntegerValue diff = prev_used_bound - entry.first;
237 prev_used_bound = entry.first;
245 void AppendEnforcedUpperBound(
const Literal enforcing_lit,
246 const IntegerVariable target,
247 const IntegerVariable bounding_var, Model*
model,
248 LinearRelaxation* relaxation) {
249 IntegerTrail* integer_trail =
model->GetOrCreate<IntegerTrail>();
250 const IntegerValue max_target_value = integer_trail->UpperBound(target);
251 const IntegerValue min_var_value = integer_trail->LowerBound(bounding_var);
252 const IntegerValue max_term_value = max_target_value - min_var_value;
254 lc.AddTerm(target, IntegerValue(1));
255 lc.AddTerm(bounding_var, IntegerValue(-1));
256 CHECK(lc.AddLiteralTerm(enforcing_lit, max_term_value));
257 relaxation->linear_constraints.push_back(lc.Build());
262 void AppendEnforcedLinearExpression(
263 const std::vector<Literal>& enforcing_literals,
264 const LinearExpression& expr,
const IntegerValue rhs_domain_min,
265 const IntegerValue rhs_domain_max,
const Model&
model,
266 LinearRelaxation* relaxation) {
267 CHECK_EQ(expr.offset, IntegerValue(0));
269 const IntegerTrail* integer_trail =
model.Get<IntegerTrail>();
270 const IntegerValue min_expr_value =
273 if (rhs_domain_min > min_expr_value) {
278 for (
const Literal&
literal : enforcing_literals) {
280 rhs_domain_min - min_expr_value));
282 for (
int i = 0; i < canonical_expr.vars.size(); i++) {
283 lc.AddTerm(canonical_expr.vars[i], canonical_expr.coeffs[i]);
285 relaxation->linear_constraints.push_back(lc.Build());
287 const IntegerValue max_expr_value =
289 if (rhs_domain_max < max_expr_value) {
294 for (
const Literal&
literal : enforcing_literals) {
296 rhs_domain_max - max_expr_value));
298 for (
int i = 0; i < canonical_expr.vars.size(); i++) {
299 lc.AddTerm(canonical_expr.vars[i], canonical_expr.coeffs[i]);
301 relaxation->linear_constraints.push_back(lc.Build());
305 bool AllLiteralsHaveViews(
const IntegerEncoder& encoder,
306 const std::vector<Literal>& literals) {
307 for (
const Literal lit : literals) {
308 if (!encoder.LiteralOrNegationHasView(lit))
return false;
325 int linearization_level,
331 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
332 if (linearization_level < 2)
return;
334 for (
const int enforcement_ref :
ct.enforcement_literal()) {
338 for (
const int ref :
ct.bool_or().literals()) {
342 }
else if (
ct.constraint_case() ==
343 ConstraintProto::ConstraintCase::kBoolAnd) {
347 if (linearization_level < 2)
return;
349 if (
ct.enforcement_literal().size() == 1) {
351 for (
const int ref :
ct.bool_and().literals()) {
353 {enforcement, mapping->
Literal(ref).Negated()});
360 int num_literals =
ct.bool_and().literals_size();
363 for (
const int ref :
ct.bool_and().literals()) {
366 for (
const int enforcement_ref :
ct.enforcement_literal()) {
368 IntegerValue(num_literals)));
371 }
else if (
ct.constraint_case() ==
372 ConstraintProto::ConstraintCase::kAtMostOne) {
375 mapping->Literals(
ct.at_most_one().literals()));
376 }
else if (
ct.constraint_case() ==
377 ConstraintProto::ConstraintCase::kExactlyOne) {
379 const std::vector<Literal> literals =
380 mapping->Literals(
ct.exactly_one().literals());
381 if (linearization_level >= 2 || AllLiteralsHaveViews(encoder, literals)) {
383 for (
const Literal lit : literals) {
387 }
else if (linearization_level == 1) {
392 }
else if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMax) {
394 const IntegerVariable target = mapping->Integer(
ct.int_max().target());
395 const std::vector<IntegerVariable> vars =
396 mapping->Integers(
ct.int_max().vars());
399 }
else if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kIntMin) {
401 const IntegerVariable negative_target =
403 const std::vector<IntegerVariable> negative_vars =
407 }
else if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
410 }
else if (
ct.constraint_case() ==
411 ConstraintProto::ConstraintCase::kCircuit) {
413 const int num_arcs =
ct.circuit().literals_size();
414 CHECK_EQ(num_arcs,
ct.circuit().tails_size());
415 CHECK_EQ(num_arcs,
ct.circuit().heads_size());
419 std::map<int, std::vector<Literal>> incoming_arc_constraints;
420 std::map<int, std::vector<Literal>> outgoing_arc_constraints;
421 for (
int i = 0; i < num_arcs; i++) {
423 const int tail =
ct.circuit().tails(i);
424 const int head =
ct.circuit().heads(i);
428 outgoing_arc_constraints[
tail].push_back(arc);
429 incoming_arc_constraints[
head].push_back(arc);
431 for (
const auto* node_map :
432 {&outgoing_arc_constraints, &incoming_arc_constraints}) {
433 for (
const auto& entry : *node_map) {
434 const std::vector<Literal>& exactly_one = entry.second;
435 if (exactly_one.size() > 1) {
438 for (
const Literal l : exactly_one) {
448 }
else if (
ct.constraint_case() ==
449 ConstraintProto::ConstraintCase::kElement) {
450 const IntegerVariable
index = mapping->Integer(
ct.element().index());
451 const IntegerVariable target = mapping->Integer(
ct.element().target());
452 const std::vector<IntegerVariable> vars =
453 mapping->Integers(
ct.element().vars());
458 constraint.
AddTerm(target, IntegerValue(-1));
461 const IntegerVariable
var = vars[literal_value.value.value()];
471 }
else if (
ct.constraint_case() ==
472 ConstraintProto::ConstraintCase::kInterval) {
475 if (linearization_level < 2)
return;
476 if (
ct.interval().has_start_view())
return;
477 const IntegerVariable start = mapping->Integer(
ct.interval().start());
478 const IntegerVariable size = mapping->Integer(
ct.interval().size());
479 const IntegerVariable end = mapping->Integer(
ct.interval().end());
481 const bool size_is_fixed = integer_trail->
IsFixed(size);
482 const IntegerValue rhs =
483 size_is_fixed ? -integer_trail->
LowerBound(size) : IntegerValue(0);
485 lc.
AddTerm(start, IntegerValue(1));
486 if (!size_is_fixed) {
487 lc.
AddTerm(size, IntegerValue(1));
489 lc.
AddTerm(end, IntegerValue(-1));
495 AppendEnforcedLinearExpression(
496 mapping->Literals(
ct.enforcement_literal()), expr, tmp_lc.
ub,
497 tmp_lc.
ub, *
model, relaxation);
501 }
else if (
ct.constraint_case() ==
502 ConstraintProto::ConstraintCase::kNoOverlap) {
505 }
else if (
ct.constraint_case() ==
506 ConstraintProto::ConstraintCase::kCumulative) {
514 const std::vector<IntegerVariable>& demands,
515 IntegerValue capacity_upper_bound,
Model*
model,
520 model->TakeOwnership(helper);
521 const int num_intervals = helper->NumTasks();
528 int num_variable_sizes = 0;
529 int num_optionals = 0;
532 min_of_starts =
std::min(min_of_starts, helper->StartMin(
index));
535 if (helper->IsOptional(
index)) {
539 if (!helper->SizeIsFixed(
index) ||
540 (!demands.empty() && !integer_trail->
IsFixed(demands[
index]))) {
541 num_variable_sizes++;
545 VLOG(2) <<
"Span [" << min_of_starts <<
".." << max_of_ends <<
"] with "
546 << num_optionals <<
" optional intervals, and " << num_variable_sizes
547 <<
" variable size intervals out of " << num_intervals
550 if (num_variable_sizes + num_optionals == 0)
return;
552 const IntegerVariable span_start =
555 IntegerValue(0), max_of_ends - min_of_starts);
556 const IntegerVariable span_end =
559 IntervalVariable span_var;
560 if (num_optionals < num_intervals) {
564 span_var =
model->Add(
571 lc.
AddTerm(span_size, -capacity_upper_bound);
572 for (
int i = 0; i < num_intervals; ++i) {
573 const IntegerValue demand_lower_bound =
574 demands.empty() ? IntegerValue(1)
576 const bool demand_is_fixed =
577 demands.empty() || integer_trail->
IsFixed(demands[i]);
578 if (!helper->IsOptional(i)) {
579 if (helper->SizeIsFixed(i) && !demands.empty()) {
580 lc.
AddTerm(demands[i], helper->SizeMin(i));
581 }
else if (demand_is_fixed) {
582 lc.
AddTerm(helper->Sizes()[i], demand_lower_bound);
591 lc.
AddTerm(helper->Sizes()[i], demand_lower_bound);
592 lc.
AddTerm(demands[i], helper->SizeMin(i));
593 lc.
AddConstant(-helper->SizeMin(i) * demand_lower_bound);
597 helper->SizeMin(i) * demand_lower_bound)) {
606 const ConstraintProto&
ct,
610 if (linearization_level < 2)
return;
614 const std::vector<IntegerVariable> demands =
616 std::vector<IntervalVariable> intervals =
617 mapping->Intervals(
ct.cumulative().intervals());
618 const IntegerValue capacity_upper_bound =
620 mapping->Integer(
ct.cumulative().capacity()));
625 const ConstraintProto&
ct,
629 if (linearization_level < 2)
return;
633 std::vector<IntervalVariable> intervals =
636 IntegerValue(1),
model, relaxation);
640 const std::vector<IntegerVariable>& vars,
645 for (
const IntegerVariable
var : vars) {
648 if (target ==
var)
continue;
651 lc.
AddTerm(target, IntegerValue(-1));
656 if (linearization_level < 2)
return;
660 if (vars.size() == 2) {
663 encoder->GetOrCreateLiteralAssociatedToEquality(y, IntegerValue(1));
664 AppendEnforcedUpperBound(y_lit, target, vars[0],
model, relaxation);
669 {y_lit}, {target, vars[0]}, {IntegerValue(1), IntegerValue(-1)},
670 IntegerValue(0),
model);
672 model->TakeOwnership(upper_bound1);
673 AppendEnforcedUpperBound(y_lit.
Negated(), target, vars[1],
model,
676 {y_lit.
Negated()}, {target, vars[1]},
677 {IntegerValue(1), IntegerValue(-1)}, IntegerValue(0),
model);
679 model->TakeOwnership(upper_bound2);
688 std::vector<Literal> exactly_one_literals;
689 exactly_one_literals.reserve(vars.size());
690 for (
const IntegerVariable
var : vars) {
691 if (target ==
var)
continue;
697 encoder->GetOrCreateLiteralAssociatedToEquality(y, IntegerValue(1));
699 AppendEnforcedUpperBound(y_lit, target,
var,
model, relaxation);
701 {y_lit}, {target,
var}, {IntegerValue(1), IntegerValue(-1)},
702 IntegerValue(0),
model);
704 model->TakeOwnership(upper_bound_constraint);
705 exactly_one_literals.push_back(y_lit);
714 IntegerVariable target,
const std::vector<LinearExpression>& exprs,
720 for (
int i = 0; i < expr.vars.size(); ++i) {
721 lc.
AddTerm(expr.vars[i], expr.coeffs[i]);
723 lc.
AddTerm(target, IntegerValue(-1));
731 const int num_exprs = exprs.size();
736 std::vector<IntegerVariable> z_vars;
737 std::vector<Literal> z_lits;
738 z_vars.reserve(num_exprs);
739 z_lits.reserve(num_exprs);
742 std::vector<Literal> exactly_one_literals;
743 for (
int i = 0; i < num_exprs; ++i) {
748 z_lits.push_back(z_lit);
751 local_expr.
vars.push_back(target);
752 local_expr.
coeffs = exprs[i].coeffs;
753 local_expr.
coeffs.push_back(IntegerValue(1));
757 model->TakeOwnership(upper_bound);
767 std::vector<IntegerVariable> x_vars;
768 for (
int i = 0; i < num_exprs; ++i) {
769 x_vars.insert(x_vars.end(), exprs[i].vars.begin(), exprs[i].vars.end());
773 DCHECK(std::all_of(x_vars.begin(), x_vars.end(), [](IntegerVariable
var) {
774 return VariableIsPositive(var);
777 std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
778 num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
781 for (
int i = 0; i < num_exprs; ++i) {
782 for (
int j = 0; j < num_exprs; ++j) {
783 if (i == j)
continue;
784 for (
const IntegerVariable x_var : x_vars) {
787 const IntegerValue diff =
789 sum_of_max_corner_diff[i][j] +=
std::max(diff * lb, diff * ub);
793 for (
int i = 0; i < num_exprs; ++i) {
795 lc.
AddTerm(target, IntegerValue(1));
796 for (
int j = 0; j < exprs[i].vars.size(); ++j) {
797 lc.
AddTerm(exprs[i].vars[j], -exprs[i].coeffs[j]);
799 for (
int j = 0; j < num_exprs; ++j) {
801 -exprs[j].offset - sum_of_max_corner_diff[i][j]));
811 const int linearization_level,
823 const IntegerValue rhs_domain_min =
824 IntegerValue(constraint_proto.linear().domain(0));
825 const IntegerValue rhs_domain_max =
826 IntegerValue(constraint_proto.linear().domain(
827 constraint_proto.linear().domain_size() - 1));
832 for (
int i = 0; i < constraint_proto.linear().vars_size(); i++) {
833 const int ref = constraint_proto.linear().vars(i);
834 const int64 coeff = constraint_proto.linear().coeffs(i);
835 lc.
AddTerm(mapping->Integer(ref), IntegerValue(coeff));
842 if (linearization_level < 2)
return;
846 if (!mapping->IsHalfEncodingConstraint(&constraint_proto) &&
847 constraint_proto.linear().vars_size() <= 1) {
851 std::vector<Literal> enforcing_literals;
852 enforcing_literals.reserve(constraint_proto.enforcement_literal_size());
853 for (
const int enforcement_ref : constraint_proto.enforcement_literal()) {
854 enforcing_literals.push_back(mapping->Literal(enforcement_ref));
857 expr.
vars.reserve(constraint_proto.linear().vars_size());
858 expr.
coeffs.reserve(constraint_proto.linear().vars_size());
859 for (
int i = 0; i < constraint_proto.linear().vars_size(); i++) {
860 int ref = constraint_proto.linear().vars(i);
861 IntegerValue coeff(constraint_proto.linear().coeffs(i));
866 const IntegerVariable int_var = mapping->Integer(ref);
867 expr.
vars.push_back(int_var);
868 expr.
coeffs.push_back(coeff);
870 AppendEnforcedLinearExpression(enforcing_literals, expr, rhs_domain_min,
871 rhs_domain_max,
model, relaxation);
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK(condition)
#define VLOG(verboselevel)
std::vector< IntegerVariable > Integers(const List &list) const
std::vector< IntervalVariable > Intervals(const ProtoIndices &indices) const
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
std::vector< ValueLiteralPair > FullDomainEncoding(IntegerVariable var) const
void RegisterWith(GenericLiteralWatcher *watcher)
bool IsFixed(IntegerVariable i) const
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
IntegerVariable AddIntegerVariable(IntegerValue lower_bound, IntegerValue upper_bound)
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
IntegerValue LowerBound(IntegerVariable i) const
ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff)
void AddConstant(IntegerValue value)
void AddTerm(IntegerVariable var, IntegerValue coeff)
Literal(int signed_value)
Class that owns everything related to a particular optimization model.
int CurrentDecisionLevel() const
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)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::vector< IntegerVariable > AppendLinMaxRelaxation(IntegerVariable target, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
void AppendLinearConstraintRelaxation(const ConstraintProto &constraint_proto, const int linearization_level, const Model &model, LinearRelaxation *relaxation)
bool RefIsPositive(int ref)
const LiteralIndex kNoLiteralIndex(-1)
std::function< IntervalVariable(Model *)> NewOptionalInterval(int64 min_start, int64 max_end, int64 size, Literal is_present)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
bool HasEnforcementLiteral(const ConstraintProto &ct)
std::function< std::vector< IntegerEncoder::ValueLiteralPair >Model *)> FullyEncodeVariable(IntegerVariable var)
bool AppendFullEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
const IntegerVariable kNoIntegerVariable(-1)
std::function< IntervalVariable(Model *)> NewInterval(int64 min_start, int64 max_end, int64 size)
LinearExpression CanonicalizeExpr(const LinearExpression &expr)
void AppendMaxRelaxation(IntegerVariable target, const std::vector< IntegerVariable > &vars, int linearization_level, Model *model, LinearRelaxation *relaxation)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
IntegerValue GetCoefficient(const IntegerVariable var, const LinearExpression &expr)
void TryToLinearizeConstraint(const CpModelProto &model_proto, const ConstraintProto &ct, Model *model, int linearization_level, LinearRelaxation *relaxation)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
void AppendPartialEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> SpanOfIntervals(IntervalVariable span, const std::vector< IntervalVariable > &intervals)
void AddCumulativeCut(const std::vector< IntervalVariable > &intervals, const std::vector< IntegerVariable > &demands, IntegerValue capacity_upper_bound, Model *model, LinearRelaxation *relaxation)
void AppendNoOverlapRelaxation(const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
void AppendCumulativeRelaxation(const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars
std::vector< std::vector< Literal > > at_most_ones
std::vector< LinearConstraint > linear_constraints