26 const std::vector<AffineExpression>& exprs,
27 const std::vector<Literal>& selectors,
29 : enforcement_literal_(enforcement_literal),
32 selectors_(selectors),
41 const
Literal enforcement_literal_;
44 const std::vector<
Literal> selectors_;
50 std::vector<
Literal> literal_reason_;
60 const auto add_var_non_selection_to_reason = [&](
int i) {
62 literal_reason_.push_back(selectors_[i]);
64 const auto add_var_selection_to_reason = [&](
int i) {
66 literal_reason_.push_back(selectors_[i].Negated());
76 enforcement_lit.
Index()) {
83 if (i_lit.bound > integer_trail_->
UpperBound(i_lit.var)) {
84 integer_reason_.push_back(
88 literal_reason_, integer_reason_);
94 if (!integer_trail_->
Enqueue(i_lit, literal_reason_, integer_reason_)) {
102 const int num_vars = exprs_.size();
103 const IntegerValue target_min = integer_trail_->
LowerBound(target_);
104 const IntegerValue target_max = integer_trail_->
UpperBound(target_);
111 int num_possible_vars = 0;
112 int num_selected_vars = 0;
113 int min_of_selected_maxes_index = -1;
114 int first_selected = -1;
115 for (
int i = 0; i < num_vars; ++i) {
118 const IntegerValue var_min = integer_trail_->
LowerBound(exprs_[i]);
119 const IntegerValue var_max = integer_trail_->
UpperBound(exprs_[i]);
121 min_of_mins =
std::min(min_of_mins, var_min);
126 if (var_max < min_of_selected_maxes) {
127 min_of_selected_maxes = var_max;
128 min_of_selected_maxes_index = i;
130 if (first_selected == -1) {
136 max_of_possible_maxes =
std::max(max_of_possible_maxes, var_max);
140 if (min_of_mins > target_min) {
141 literal_reason_.clear();
142 integer_reason_.clear();
143 for (
int i = 0; i < num_vars; ++i) {
145 add_var_non_selection_to_reason(i);
150 if (!push_bound(enforcement_literal_,
151 target_.GreaterOrEqual(min_of_mins))) {
156 if (num_selected_vars > 0 && min_of_selected_maxes < target_max) {
158 DCHECK_NE(min_of_selected_maxes_index, -1);
160 literal_reason_.clear();
161 integer_reason_.clear();
162 add_var_selection_to_reason(min_of_selected_maxes_index);
164 integer_reason_.push_back(
166 min_of_selected_maxes));
168 if (!integer_trail_->
Enqueue(target_.LowerOrEqual(min_of_selected_maxes),
169 literal_reason_, integer_reason_)) {
175 if (num_possible_vars > 0 && num_selected_vars == 0) {
176 if (target_max > max_of_possible_maxes) {
177 literal_reason_.clear();
178 integer_reason_.clear();
180 for (
int i = 0; i < num_vars; ++i) {
182 add_var_non_selection_to_reason(i);
184 integer_reason_.push_back(
188 if (!push_bound(enforcement_literal_,
189 target_.LowerOrEqual(max_of_possible_maxes))) {
196 if (!assignment.
LiteralIsTrue(enforcement_literal_))
return true;
203 if (num_possible_vars > 0) {
204 DCHECK_GT(num_possible_vars + num_selected_vars, 1);
207 if (num_selected_vars != 1)
return true;
214 if (target_min > integer_trail_->
LowerBound(unique_selected_var)) {
215 literal_reason_.clear();
216 integer_reason_.clear();
217 for (
int i = 0; i < num_vars; ++i) {
218 if (i != first_selected) {
219 add_var_non_selection_to_reason(i);
221 add_var_selection_to_reason(i);
225 integer_reason_.push_back(target_.GreaterOrEqual(target_min));
228 literal_reason_, integer_reason_)) {
233 if (target_max < integer_trail_->
UpperBound(unique_selected_var)) {
234 literal_reason_.clear();
235 integer_reason_.clear();
236 for (
int i = 0; i < num_vars; ++i) {
237 if (i != first_selected) {
238 add_var_non_selection_to_reason(i);
240 add_var_selection_to_reason(i);
244 integer_reason_.push_back(target_.LowerOrEqual(target_max));
247 literal_reason_, integer_reason_)) {
256 const int id = watcher->
Register(
this);
257 for (
int t = 0; t < exprs_.size(); ++t) {
268 const std::vector<AffineExpression>& exprs,
269 const std::vector<Literal>& selectors) {
270 CHECK_EQ(exprs.size(), selectors.size());
274 for (
int i = 0; i < exprs.size(); ++i) {
276 builder.
AddTerm(target, IntegerValue(1));
277 builder.
AddTerm(exprs[i], IntegerValue(-1));
284 enforcement_literal, target, exprs, selectors,
model);
286 model->TakeOwnership(constraint);
292 const std::vector<AffineExpression>& exprs,
293 const std::vector<Literal>& selectors) {
294 CHECK_EQ(exprs.size(), selectors.size());
296 std::vector<AffineExpression> negations;
298 negations.push_back(expr.Negated());
301 enforcement_literal, target.
Negated(), negations, selectors));
306 IntervalVariable span,
const std::vector<IntervalVariable>& intervals) {
312 if (repository->IsAbsent(span)) {
313 for (
const IntervalVariable
interval : intervals) {
314 if (repository->IsOptional(
interval)) {
315 sat_solver->AddBinaryClause(
316 repository->PresenceLiteral(span).Negated(),
317 repository->PresenceLiteral(
interval));
318 }
else if (repository->IsPresent(
interval)) {
319 sat_solver->NotifyThatModelIsUnsat();
328 std::vector<Literal> presence_literals;
329 std::vector<AffineExpression> starts;
330 std::vector<AffineExpression> ends;
331 std::vector<Literal> clause;
332 bool at_least_one_interval_is_present =
false;
336 for (
const IntervalVariable
interval : intervals) {
337 if (repository->IsAbsent(
interval))
continue;
339 if (repository->IsOptional(
interval)) {
341 presence_literals.push_back(task_lit);
342 clause.push_back(task_lit);
344 if (repository->IsOptional(span)) {
347 repository->PresenceLiteral(span));
351 presence_literals.push_back(true_literal);
352 at_least_one_interval_is_present =
true;
354 starts.push_back(repository->Start(
interval));
355 ends.push_back(repository->End(
interval));
358 if (!at_least_one_interval_is_present) {
360 if (repository->IsOptional(span)) {
361 clause.push_back(repository->PresenceLiteral(span).Negated());
363 sat_solver->AddProblemClause(clause);
367 const Literal enforcement_literal =
368 repository->IsOptional(span)
369 ? repository->PresenceLiteral(span)
372 repository->Start(span), starts,
375 enforcement_literal, repository->End(span), ends, presence_literals));
#define DCHECK_NE(val1, val2)
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK(condition)
void WatchLiteral(Literal l, int id, int watch_index=-1)
void WatchAffineExpression(AffineExpression e, int id)
int Register(PropagatorInterface *propagator)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
LiteralIndex OptionalLiteralIndex(IntegerVariable i) const
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue LowerBound(IntegerVariable i) const
void AddTerm(IntegerVariable var, IntegerValue coeff)
LiteralIndex Index() const
Class that owns everything related to a particular optimization model.
bool AddBinaryClause(Literal a, Literal b)
int RegisterWith(GenericLiteralWatcher *watcher)
SelectedMinPropagator(Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors, Model *model)
const VariablesAssignment & Assignment() const
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> EqualMaxOfSelectedVariables(Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
std::function< void(Model *)> SpanOfIntervals(IntervalVariable span, const std::vector< IntervalVariable > &intervals)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< void(Model *)> EqualMinOfSelectedVariables(Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
AffineExpression Negated() const
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
IntegerLiteral LowerOrEqual(IntegerValue bound) const
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)