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)) {
346 sat_solver->AddBinaryClause(task_lit.
Negated(),
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));