20 #include "absl/container/flat_hash_map.h"
21 #include "absl/memory/memory.h"
31 const std::vector<IntegerVariable>& vars,
32 const std::vector<IntegerValue>& coeffs,
34 : enforcement_literals_(enforcement_literals),
39 rev_integer_value_repository_(
44 CHECK(!vars_.empty());
45 max_variations_.resize(vars_.size());
48 for (
int i = 0; i < vars.size(); ++i) {
51 coeffs_[i] = -coeffs_[i];
57 literal_reason_.push_back(
literal.Negated());
61 rev_num_fixed_vars_ = 0;
62 rev_lb_fixed_vars_ = IntegerValue(0);
65 void IntegerSumLE::FillIntegerReason() {
66 integer_reason_.clear();
67 reason_coeffs_.clear();
68 const int num_vars = vars_.size();
69 for (
int i = 0; i < num_vars; ++i) {
70 const IntegerVariable
var = vars_[i];
73 reason_coeffs_.push_back(coeffs_[i]);
81 int num_unassigned_enforcement_literal = 0;
86 ++num_unassigned_enforcement_literal;
87 unique_unnasigned_literal =
literal.Index();
93 if (num_unassigned_enforcement_literal > 1)
return true;
97 rev_integer_value_repository_->
SaveState(&rev_lb_fixed_vars_);
99 rev_num_fixed_vars_ = 0;
100 rev_lb_fixed_vars_ = 0;
104 IntegerValue lb_unfixed_vars = IntegerValue(0);
105 const int num_vars = vars_.size();
106 for (
int i = rev_num_fixed_vars_; i < num_vars; ++i) {
107 const IntegerVariable
var = vars_[i];
108 const IntegerValue coeff = coeffs_[i];
112 max_variations_[i] = (ub - lb) * coeff;
113 lb_unfixed_vars += lb * coeff;
116 std::swap(vars_[i], vars_[rev_num_fixed_vars_]);
117 std::swap(coeffs_[i], coeffs_[rev_num_fixed_vars_]);
118 std::swap(max_variations_[i], max_variations_[rev_num_fixed_vars_]);
119 rev_num_fixed_vars_++;
120 rev_lb_fixed_vars_ += lb * coeff;
124 static_cast<double>(num_vars - rev_num_fixed_vars_) * 1e-9);
127 const IntegerValue slack =
128 upper_bound_ - (rev_lb_fixed_vars_ + lb_unfixed_vars);
134 if (num_unassigned_enforcement_literal == 1) {
137 std::vector<Literal> tmp = literal_reason_;
138 tmp.erase(std::find(tmp.begin(), tmp.end(), to_propagate));
139 integer_trail_->
EnqueueLiteral(to_propagate, tmp, integer_reason_);
142 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
146 if (num_unassigned_enforcement_literal > 0)
return true;
150 for (
int i = rev_num_fixed_vars_; i < num_vars; ++i) {
151 if (max_variations_[i] <= slack)
continue;
153 const IntegerVariable
var = vars_[i];
154 const IntegerValue coeff = coeffs_[i];
155 const IntegerValue div = slack / coeff;
156 const IntegerValue new_ub = integer_trail_->
LowerBound(
var) + div;
157 const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
160 [
this, propagation_slack](
162 std::vector<Literal>* literal_reason,
163 std::vector<int>* trail_indices_reason) {
164 *literal_reason = literal_reason_;
165 trail_indices_reason->clear();
166 reason_coeffs_.clear();
167 const int size = vars_.size();
168 for (int i = 0; i < size; ++i) {
169 const IntegerVariable var = vars_[i];
170 if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
174 integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
176 trail_indices_reason->push_back(index);
177 if (propagation_slack > 0) {
178 reason_coeffs_.push_back(coeffs_[i]);
182 if (propagation_slack > 0) {
184 propagation_slack, reason_coeffs_, trail_indices_reason);
194 bool IntegerSumLE::PropagateAtLevelZero() {
197 if (!enforcement_literals_.empty())
return true;
200 IntegerValue min_activity = IntegerValue(0);
201 const int num_vars =
vars_.size();
202 for (
int i = 0; i < num_vars; ++i) {
203 const IntegerVariable
var =
vars_[i];
204 const IntegerValue coeff = coeffs_[i];
205 const IntegerValue lb = integer_trail_->LevelZeroLowerBound(
var);
206 const IntegerValue ub = integer_trail_->LevelZeroUpperBound(
var);
207 max_variations_[i] = (ub - lb) * coeff;
208 min_activity += lb * coeff;
210 time_limit_->AdvanceDeterministicTime(
static_cast<double>(num_vars * 1e-9));
213 const IntegerValue slack = upper_bound_ - min_activity;
215 return integer_trail_->ReportConflict({}, {});
220 for (
int i = 0; i < num_vars; ++i) {
221 if (max_variations_[i] <= slack)
continue;
223 const IntegerVariable
var =
vars_[i];
224 const IntegerValue coeff = coeffs_[i];
225 const IntegerValue div = slack / coeff;
226 const IntegerValue new_ub = integer_trail_->LevelZeroLowerBound(
var) + div;
237 is_registered_ =
true;
238 const int id = watcher->
Register(
this);
239 for (
const IntegerVariable&
var :
vars_) {
252 LevelZeroEquality::LevelZeroEquality(IntegerVariable target,
253 const std::vector<IntegerVariable>& vars,
254 const std::vector<IntegerValue>& coeffs,
262 const int id = watcher->
Register(
this);
263 watcher->SetPropagatorPriority(
id, 2);
264 watcher->WatchIntegerVariable(target,
id);
265 for (
const IntegerVariable&
var : vars_) {
266 watcher->WatchIntegerVariable(
var,
id);
284 for (
int i = 0; i < vars_.size(); ++i) {
285 if (integer_trail_->
IsFixed(vars_[i])) {
286 sum += coeffs_[i] * integer_trail_->
LowerBound(vars_[i]);
292 if (gcd == 0)
return true;
295 VLOG(1) <<
"Objective gcd: " << gcd;
298 gcd_ = IntegerValue(gcd);
300 const IntegerValue lb = integer_trail_->
LowerBound(target_);
302 if (lb_remainder != 0) {
309 const IntegerValue ub = integer_trail_->
UpperBound(target_);
310 const IntegerValue ub_remainder =
312 if (ub_remainder != 0) {
322 IntegerVariable min_var,
324 :
vars_(vars), min_var_(min_var), integer_trail_(integer_trail) {}
327 if (vars_.empty())
return true;
333 const IntegerValue current_min_ub = integer_trail_->
UpperBound(min_var_);
334 int num_intervals_that_can_be_min = 0;
335 int last_possible_min_interval = 0;
338 for (
int i = 0; i < vars_.size(); ++i) {
339 const IntegerValue lb = integer_trail_->
LowerBound(vars_[i]);
341 if (lb <= current_min_ub) {
342 ++num_intervals_that_can_be_min;
343 last_possible_min_interval = i;
349 integer_reason_.clear();
350 for (
const IntegerVariable
var : vars_) {
354 {}, integer_reason_)) {
360 if (num_intervals_that_can_be_min == 1) {
361 const IntegerValue ub_of_only_candidate =
362 integer_trail_->
UpperBound(vars_[last_possible_min_interval]);
363 if (current_min_ub < ub_of_only_candidate) {
364 integer_reason_.clear();
368 integer_reason_.push_back(min_ub_literal);
369 for (
const IntegerVariable
var : vars_) {
370 if (
var ==
vars_[last_possible_min_interval])
continue;
371 integer_reason_.push_back(
377 {}, integer_reason_)) {
389 if (num_intervals_that_can_be_min == 0) {
390 integer_reason_.clear();
393 integer_reason_.push_back(min_ub_literal);
394 for (
const IntegerVariable
var : vars_) {
395 integer_reason_.push_back(
405 const int id = watcher->
Register(
this);
406 for (
const IntegerVariable&
var : vars_) {
419 bool LinMinPropagator::PropagateLinearUpperBound(
420 const std::vector<IntegerVariable>& vars,
421 const std::vector<IntegerValue>& coeffs,
const IntegerValue upper_bound) {
422 IntegerValue sum_lb = IntegerValue(0);
423 const int num_vars = vars.size();
424 std::vector<IntegerValue> max_variations;
425 for (
int i = 0; i < num_vars; ++i) {
426 const IntegerVariable
var = vars[i];
427 const IntegerValue coeff = coeffs[i];
432 max_variations.push_back((ub - lb) * coeff);
433 sum_lb += lb * coeff;
437 static_cast<double>(num_vars) * 1e-9);
439 const IntegerValue slack = upper_bound - sum_lb;
441 std::vector<IntegerLiteral> linear_sum_reason;
442 std::vector<IntegerValue> reason_coeffs;
443 for (
int i = 0; i < num_vars; ++i) {
444 const IntegerVariable
var = vars[i];
447 reason_coeffs.push_back(coeffs[i]);
454 std::vector<IntegerLiteral> local_reason =
455 integer_reason_for_unique_candidate_;
456 local_reason.insert(local_reason.end(), linear_sum_reason.begin(),
457 linear_sum_reason.end());
463 for (
int i = 0; i < num_vars; ++i) {
464 if (max_variations[i] <= slack)
continue;
466 const IntegerVariable
var = vars[i];
467 const IntegerValue coeff = coeffs[i];
468 const IntegerValue div = slack / coeff;
469 const IntegerValue new_ub = integer_trail_->
LowerBound(
var) + div;
471 const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
474 [
this, &vars, &coeffs, propagation_slack](
475 IntegerLiteral i_lit,
int trail_index,
476 std::vector<Literal>* literal_reason,
477 std::vector<int>* trail_indices_reason) {
478 literal_reason->clear();
479 trail_indices_reason->clear();
480 std::vector<IntegerValue> reason_coeffs;
481 const int size = vars.size();
482 for (
int i = 0; i < size; ++i) {
483 const IntegerVariable
var = vars[i];
490 trail_indices_reason->push_back(
index);
491 if (propagation_slack > 0) {
492 reason_coeffs.push_back(coeffs[i]);
496 if (propagation_slack > 0) {
498 propagation_slack, reason_coeffs, trail_indices_reason);
501 for (IntegerLiteral reason_lit :
502 integer_reason_for_unique_candidate_) {
504 reason_lit.var, trail_index);
506 trail_indices_reason->push_back(
index);
517 if (exprs_.empty())
return true;
525 const IntegerValue current_min_ub = integer_trail_->
UpperBound(min_var_);
526 int num_intervals_that_can_be_min = 0;
527 int last_possible_min_interval = 0;
530 for (
int i = 0; i < exprs_.size(); ++i) {
532 expr_lbs_.push_back(lb);
533 min_of_linear_expression_lb =
std::min(min_of_linear_expression_lb, lb);
534 if (lb <= current_min_ub) {
535 ++num_intervals_that_can_be_min;
536 last_possible_min_interval = i;
544 if (min_of_linear_expression_lb > current_min_ub) {
545 min_of_linear_expression_lb = current_min_ub + 1;
550 const bool use_slack =
false;
551 if (min_of_linear_expression_lb > integer_trail_->
LowerBound(min_var_)) {
552 std::vector<IntegerLiteral> local_reason;
553 for (
int i = 0; i < exprs_.size(); ++i) {
554 const IntegerValue slack = expr_lbs_[i] - min_of_linear_expression_lb;
556 (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
557 exprs_[i].vars, &local_reason);
560 min_var_, min_of_linear_expression_lb),
570 if (num_intervals_that_can_be_min == 1) {
571 const IntegerValue ub_of_only_candidate =
573 if (current_min_ub < ub_of_only_candidate) {
576 if (rev_unique_candidate_ == 0) {
577 integer_reason_for_unique_candidate_.clear();
581 integer_reason_for_unique_candidate_.push_back(min_ub_literal);
582 for (
int i = 0; i < exprs_.size(); ++i) {
583 if (i == last_possible_min_interval)
continue;
584 const IntegerValue slack = expr_lbs_[i] - (current_min_ub + 1);
586 (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
587 exprs_[i].vars, &integer_reason_for_unique_candidate_);
589 rev_unique_candidate_ = 1;
592 return PropagateLinearUpperBound(
593 exprs_[last_possible_min_interval].vars,
594 exprs_[last_possible_min_interval].coeffs,
595 current_min_ub - exprs_[last_possible_min_interval].offset);
603 const int id = watcher->
Register(
this);
605 for (
int i = 0; i < expr.vars.size(); ++i) {
606 const IntegerVariable&
var = expr.vars[i];
607 const IntegerValue coeff = expr.coeffs[i];
620 IntegerVariable
a, IntegerVariable
b, IntegerVariable p,
622 : a_(
a), b_(
b), p_(p), integer_trail_(integer_trail) {
633 const IntegerValue max_a = integer_trail_->
UpperBound(a_);
634 const IntegerValue max_b = integer_trail_->
UpperBound(b_);
635 const IntegerValue new_max(
CapProd(max_a.value(), max_b.value()));
636 if (new_max < integer_trail_->
UpperBound(p_)) {
638 {integer_trail_->UpperBoundAsLiteral(a_),
639 integer_trail_->UpperBoundAsLiteral(b_)})) {
644 const IntegerValue min_a = integer_trail_->
LowerBound(a_);
645 const IntegerValue min_b = integer_trail_->
LowerBound(b_);
646 const IntegerValue new_min(
CapProd(min_a.value(), min_b.value()));
647 if (new_min > integer_trail_->
LowerBound(p_)) {
650 {integer_trail_->LowerBoundAsLiteral(a_),
651 integer_trail_->LowerBoundAsLiteral(b_)})) {
656 for (
int i = 0; i < 2; ++i) {
657 const IntegerVariable
a = i == 0 ? a_ : b_;
658 const IntegerVariable
b = i == 0 ? b_ : a_;
659 const IntegerValue max_a = integer_trail_->
UpperBound(
a);
660 const IntegerValue min_b = integer_trail_->
LowerBound(
b);
661 const IntegerValue min_p = integer_trail_->
LowerBound(p_);
662 const IntegerValue max_p = integer_trail_->
UpperBound(p_);
663 const IntegerValue prod(
CapProd(max_a.value(), min_b.value()));
671 }
else if (prod < min_p) {
685 const int id = watcher->
Register(
this);
695 IntegerValue FloorSquareRoot(IntegerValue
a) {
696 IntegerValue result(
static_cast<int64>(std::floor(std::sqrt(
ToDouble(
a)))));
697 while (result * result >
a) --result;
698 while ((result + 1) * (result + 1) <=
a) ++result;
703 IntegerValue CeilSquareRoot(IntegerValue
a) {
704 IntegerValue result(
static_cast<int64>(std::ceil(std::sqrt(
ToDouble(
a)))));
705 while (result * result <
a) ++result;
706 while ((result - 1) * (result - 1) >=
a) --result;
714 : x_(x), s_(s), integer_trail_(integer_trail) {
721 const IntegerValue min_x = integer_trail_->
LowerBound(x_);
722 const IntegerValue min_s = integer_trail_->
LowerBound(s_);
723 const IntegerValue min_x_square(
CapProd(min_x.value(), min_x.value()));
724 if (min_x_square > min_s) {
727 {IntegerLiteral::GreaterOrEqual(x_, min_x)})) {
730 }
else if (min_x_square < min_s) {
731 const IntegerValue new_min = CeilSquareRoot(min_s);
734 {IntegerLiteral::GreaterOrEqual(
735 s_, (new_min - 1) * (new_min - 1) + 1)})) {
740 const IntegerValue max_x = integer_trail_->
UpperBound(x_);
741 const IntegerValue max_s = integer_trail_->
UpperBound(s_);
742 const IntegerValue max_x_square(
CapProd(max_x.value(), max_x.value()));
743 if (max_x_square < max_s) {
746 {IntegerLiteral::LowerOrEqual(x_, max_x)})) {
749 }
else if (max_x_square > max_s) {
750 const IntegerValue new_max = FloorSquareRoot(max_s);
752 {IntegerLiteral::LowerOrEqual(
753 s_, (new_max + 1) * (new_max + 1) - 1)})) {
762 const int id = watcher->
Register(
this);
771 : a_(
a), b_(
b), c_(c), integer_trail_(integer_trail) {
778 const IntegerValue min_a = integer_trail_->
LowerBound(a_);
779 const IntegerValue max_a = integer_trail_->
UpperBound(a_);
780 const IntegerValue min_b = integer_trail_->
LowerBound(b_);
781 const IntegerValue max_b = integer_trail_->
UpperBound(b_);
782 IntegerValue min_c = integer_trail_->
LowerBound(c_);
783 IntegerValue max_c = integer_trail_->
UpperBound(c_);
785 if (max_a / min_b < max_c) {
786 max_c = max_a / min_b;
788 {integer_trail_->UpperBoundAsLiteral(a_),
789 integer_trail_->LowerBoundAsLiteral(b_)})) {
793 if (min_a / max_b > min_c) {
794 min_c = min_a / max_b;
796 {integer_trail_->LowerBoundAsLiteral(a_),
797 integer_trail_->UpperBoundAsLiteral(b_)})) {
809 const int id = watcher->
Register(
this);
820 : a_(
a), b_(
b), c_(c), integer_trail_(integer_trail) {}
823 const IntegerValue min_a = integer_trail_->
LowerBound(a_);
824 const IntegerValue max_a = integer_trail_->
UpperBound(a_);
825 IntegerValue min_c = integer_trail_->
LowerBound(c_);
826 IntegerValue max_c = integer_trail_->
UpperBound(c_);
830 if (max_a / b_ < max_c) {
833 {integer_trail_->UpperBoundAsLiteral(a_)})) {
836 }
else if (max_a / b_ > max_c) {
837 const IntegerValue new_max_a =
838 max_c >= 0 ? max_c * b_ + b_ - 1
839 : IntegerValue(
CapProd(max_c.value(), b_.value()));
843 {integer_trail_->UpperBoundAsLiteral(c_)})) {
848 if (min_a / b_ > min_c) {
851 {integer_trail_->LowerBoundAsLiteral(a_)})) {
854 }
else if (min_a / b_ < min_c) {
855 const IntegerValue new_min_a =
856 min_c > 0 ? IntegerValue(
CapProd(min_c.value(), b_.value()))
857 : min_c * b_ - b_ + 1;
861 {integer_trail_->LowerBoundAsLiteral(c_)})) {
870 const int id = watcher->
Register(
this);
876 const std::vector<Literal>& selectors,
877 const std::vector<IntegerValue>& values) {
882 CHECK(!values.empty());
883 CHECK_EQ(values.size(), selectors.size());
884 std::vector<int64> unique_values;
885 absl::flat_hash_map<int64, std::vector<Literal>> value_to_selector;
886 for (
int i = 0; i < values.size(); ++i) {
887 unique_values.push_back(values[i].
value());
888 value_to_selector[values[i].value()].push_back(selectors[i]);
893 if (unique_values.size() == 1) {
900 for (
const int64 v : unique_values) {
901 const std::vector<Literal>& selectors = value_to_selector[v];
902 if (selectors.size() == 1) {
903 encoder->AssociateToIntegerEqualValue(selectors[0],
var,
908 encoder->AssociateToIntegerEqualValue(l,
var, IntegerValue(v));
const std::vector< IntVar * > vars_
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define CHECK_GT(val1, val2)
#define DCHECK_GE(val1, val2)
#define VLOG(verboselevel)
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
static int64 GCD64(int64 x, int64 y)
void SaveState(T *object)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
void RegisterWith(GenericLiteralWatcher *watcher)
DivisionPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable c, IntegerTrail *integer_trail)
FixedDivisionPropagator(IntegerVariable a, IntegerValue b, IntegerVariable c, IntegerTrail *integer_trail)
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterReversibleInt(int id, int *rev)
void WatchLiteral(Literal l, int id, int watch_index=-1)
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
int Register(PropagatorInterface *propagator)
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
IntegerSumLE(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, IntegerValue upper_bound, Model *model)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
bool IsFixed(IntegerVariable i) const
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerValue UpperBound(IntegerVariable i) const
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
IntegerValue LowerBound(IntegerVariable i) const
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
LinMinPropagator(const std::vector< LinearExpression > &exprs, IntegerVariable min_var, Model *model)
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterWith(GenericLiteralWatcher *watcher)
MinPropagator(const std::vector< IntegerVariable > &vars, IntegerVariable min_var, IntegerTrail *integer_trail)
Class that owns everything related to a particular optimization model.
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
void RegisterWith(GenericLiteralWatcher *watcher)
PositiveProductPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable p, IntegerTrail *integer_trail)
void RegisterWith(GenericLiteralWatcher *watcher)
SquarePropagator(IntegerVariable x, IntegerVariable s, IntegerTrail *integer_trail)
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
const LiteralIndex kNoLiteralIndex(-1)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
IntegerVariable PositiveVariable(IntegerVariable i)
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
double ToDouble(IntegerValue value)
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...
int64 CapProd(int64 x, int64 y)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)