OR-Tools  8.2
pb_constraint.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <utility>
17
18#include "absl/strings/str_format.h"
22
23namespace operations_research {
24namespace sat {
25
26namespace {
27
28bool LiteralComparator(const LiteralWithCoeff& a, const LiteralWithCoeff& b) {
29 return a.literal.Index() < b.literal.Index();
30}
31
32bool CoeffComparator(const LiteralWithCoeff& a, const LiteralWithCoeff& b) {
33 if (a.coefficient == b.coefficient) {
34 return a.literal.Index() < b.literal.Index();
35 }
36 return a.coefficient < b.coefficient;
37}
38
39} // namespace
40
42 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
43 Coefficient* max_value) {
44 // Note(user): For some reason, the IntType checking doesn't work here ?! that
45 // is a bit worrying, but the code seems to behave correctly.
46 *bound_shift = 0;
47 *max_value = 0;
48
49 // First, sort by literal to remove duplicate literals.
50 // This also remove term with a zero coefficient.
51 std::sort(cst->begin(), cst->end(), LiteralComparator);
52 int index = 0;
54 for (int i = 0; i < cst->size(); ++i) {
55 const LiteralWithCoeff current = (*cst)[i];
56 if (current.coefficient == 0) continue;
57 if (representative != nullptr &&
58 current.literal.Variable() == representative->literal.Variable()) {
59 if (current.literal == representative->literal) {
60 if (!SafeAddInto(current.coefficient, &(representative->coefficient))) {
61 return false;
62 }
63 } else {
64 // Here current_literal is equal to (1 - representative).
65 if (!SafeAddInto(-current.coefficient,
66 &(representative->coefficient))) {
67 return false;
68 }
69 if (!SafeAddInto(-current.coefficient, bound_shift)) return false;
70 }
71 } else {
72 if (representative != nullptr && representative->coefficient == 0) {
73 --index;
74 }
75 (*cst)[index] = current;
76 representative = &((*cst)[index]);
77 ++index;
78 }
79 }
80 if (representative != nullptr && representative->coefficient == 0) {
81 --index;
82 }
83 cst->resize(index);
84
85 // Then, make all coefficients positive by replacing a term "-c x" into
86 // "c(1-x) - c" which is the same as "c(not x) - c".
87 for (int i = 0; i < cst->size(); ++i) {
88 const LiteralWithCoeff current = (*cst)[i];
89 if (current.coefficient < 0) {
90 if (!SafeAddInto(-current.coefficient, bound_shift)) return false;
91 (*cst)[i].coefficient = -current.coefficient;
92 (*cst)[i].literal = current.literal.Negated();
93 }
94 if (!SafeAddInto((*cst)[i].coefficient, max_value)) return false;
95 }
96
97 // Finally sort by increasing coefficients.
98 std::sort(cst->begin(), cst->end(), CoeffComparator);
99 DCHECK_GE(*max_value, 0);
100 return true;
101}
102
105 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
106 Coefficient* max_value) {
107 int index = 0;
108 Coefficient shift_due_to_fixed_variables(0);
109 for (const LiteralWithCoeff& entry : *cst) {
110 if (mapping[entry.literal.Index()] >= 0) {
111 (*cst)[index] = LiteralWithCoeff(Literal(mapping[entry.literal.Index()]),
112 entry.coefficient);
113 ++index;
114 } else if (mapping[entry.literal.Index()] == kTrueLiteralIndex) {
115 if (!SafeAddInto(-entry.coefficient, &shift_due_to_fixed_variables)) {
116 return false;
117 }
118 } else {
119 // Nothing to do if the literal is false.
120 DCHECK_EQ(mapping[entry.literal.Index()], kFalseLiteralIndex);
121 }
122 }
123 cst->resize(index);
124 if (cst->empty()) {
125 *bound_shift = shift_due_to_fixed_variables;
126 *max_value = 0;
127 return true;
128 }
129 const bool result =
130 ComputeBooleanLinearExpressionCanonicalForm(cst, bound_shift, max_value);
131 if (!SafeAddInto(shift_due_to_fixed_variables, bound_shift)) return false;
132 return result;
133}
134
135// TODO(user): Also check for no duplicates literals + unit tests.
137 const std::vector<LiteralWithCoeff>& cst) {
138 Coefficient previous(1);
139 for (LiteralWithCoeff term : cst) {
140 if (term.coefficient < previous) return false;
141 previous = term.coefficient;
142 }
143 return true;
144}
145
146// TODO(user): Use more complex simplification like dividing by the gcd of
147// everyone and using less different coefficients if possible.
149 std::vector<LiteralWithCoeff>* cst, Coefficient* rhs) {
150 // Replace all coefficient >= rhs by rhs + 1 (these literal must actually be
151 // false). Note that the linear sum of literals remains canonical.
152 //
153 // TODO(user): It is probably better to remove these literals and have other
154 // constraint setting them to false from the symmetry finder perspective.
155 for (LiteralWithCoeff& x : *cst) {
156 if (x.coefficient > *rhs) x.coefficient = *rhs + 1;
157 }
158}
159
160Coefficient ComputeCanonicalRhs(Coefficient upper_bound,
161 Coefficient bound_shift,
162 Coefficient max_value) {
163 Coefficient rhs = upper_bound;
164 if (!SafeAddInto(bound_shift, &rhs)) {
165 if (bound_shift > 0) {
166 // Positive overflow. The constraint is trivially true.
167 // This is because the canonical linear expression is in [0, max_value].
168 return max_value;
169 } else {
170 // Negative overflow. The constraint is infeasible.
171 return Coefficient(-1);
172 }
173 }
174 if (rhs < 0) return Coefficient(-1);
175 return std::min(max_value, rhs);
176}
177
178Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound,
179 Coefficient bound_shift,
180 Coefficient max_value) {
181 // The new bound is "max_value - (lower_bound + bound_shift)", but we must
182 // pay attention to possible overflows.
183 Coefficient shifted_lb = lower_bound;
184 if (!SafeAddInto(bound_shift, &shifted_lb)) {
185 if (bound_shift > 0) {
186 // Positive overflow. The constraint is infeasible.
187 return Coefficient(-1);
188 } else {
189 // Negative overflow. The constraint is trivialy satisfiable.
190 return max_value;
191 }
192 }
193 if (shifted_lb <= 0) {
194 // If shifted_lb <= 0 then the constraint is trivialy satisfiable. We test
195 // this so we are sure that max_value - shifted_lb doesn't overflow below.
196 return max_value;
197 }
198 return max_value - shifted_lb;
199}
200
202 bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound,
203 Coefficient upper_bound, std::vector<LiteralWithCoeff>* cst) {
204 // Canonicalize the linear expression of the constraint.
205 Coefficient bound_shift;
206 Coefficient max_value;
207 if (!ComputeBooleanLinearExpressionCanonicalForm(cst, &bound_shift,
208 &max_value)) {
209 return false;
210 }
211 if (use_upper_bound) {
212 const Coefficient rhs =
213 ComputeCanonicalRhs(upper_bound, bound_shift, max_value);
214 if (!AddConstraint(*cst, max_value, rhs)) return false;
215 }
216 if (use_lower_bound) {
217 // We transform the constraint into an upper-bounded one.
218 for (int i = 0; i < cst->size(); ++i) {
219 (*cst)[i].literal = (*cst)[i].literal.Negated();
220 }
221 const Coefficient rhs =
222 ComputeNegatedCanonicalRhs(lower_bound, bound_shift, max_value);
223 if (!AddConstraint(*cst, max_value, rhs)) return false;
224 }
225 return true;
226}
227
228bool CanonicalBooleanLinearProblem::AddConstraint(
229 const std::vector<LiteralWithCoeff>& cst, Coefficient max_value,
230 Coefficient rhs) {
231 if (rhs < 0) return false; // Trivially unsatisfiable.
232 if (rhs >= max_value) return true; // Trivially satisfiable.
233 constraints_.emplace_back(cst.begin(), cst.end());
234 rhs_.push_back(rhs);
235 SimplifyCanonicalBooleanLinearConstraint(&constraints_.back(), &rhs_.back());
236 return true;
237}
238
240 if (terms_.size() != num_variables) {
241 terms_.assign(num_variables, Coefficient(0));
242 non_zeros_.ClearAndResize(BooleanVariable(num_variables));
243 rhs_ = 0;
244 max_sum_ = 0;
245 } else {
246 ClearAll();
247 }
248}
249
251 // TODO(user): We could be more efficient and have only one loop here.
252 for (BooleanVariable var : non_zeros_.PositionsSetAtLeastOnce()) {
253 terms_[var] = Coefficient(0);
254 }
255 non_zeros_.ClearAll();
256 rhs_ = 0;
257 max_sum_ = 0;
258}
259
260// TODO(user): Also reduce the trivially false literal when coeff > rhs_ ?
262 CHECK_LT(rhs_, max_sum_) << "Trivially sat.";
263 Coefficient removed_sum(0);
264 const Coefficient bound = max_sum_ - rhs_;
265 for (BooleanVariable var : PossibleNonZeros()) {
266 const Coefficient diff = GetCoefficient(var) - bound;
267 if (diff > 0) {
268 removed_sum += diff;
269 terms_[var] = (terms_[var] > 0) ? bound : -bound;
270 }
271 }
272 rhs_ -= removed_sum;
273 max_sum_ -= removed_sum;
274 DCHECK_EQ(max_sum_, ComputeMaxSum());
275}
276
278 std::string result;
279 for (BooleanVariable var : PossibleNonZeros()) {
280 if (!result.empty()) result += " + ";
281 result += absl::StrFormat("%d[%s]", GetCoefficient(var).value(),
283 }
284 result += absl::StrFormat(" <= %d", rhs_.value());
285 return result;
286}
287
288// TODO(user): Keep this for DCHECK(), but maintain the slack incrementally
289// instead of recomputing it.
291 const Trail& trail, int trail_index) const {
292 Coefficient activity(0);
293 for (BooleanVariable var : PossibleNonZeros()) {
294 if (GetCoefficient(var) == 0) continue;
295 if (trail.Assignment().LiteralIsTrue(GetLiteral(var)) &&
296 trail.Info(var).trail_index < trail_index) {
297 activity += GetCoefficient(var);
298 }
299 }
300 return rhs_ - activity;
301}
302
305 int trail_index) {
306 Coefficient activity(0);
307 Coefficient removed_sum(0);
308 const Coefficient bound = max_sum_ - rhs_;
309 for (BooleanVariable var : PossibleNonZeros()) {
310 if (GetCoefficient(var) == 0) continue;
311 const Coefficient diff = GetCoefficient(var) - bound;
312 if (trail.Assignment().LiteralIsTrue(GetLiteral(var)) &&
313 trail.Info(var).trail_index < trail_index) {
314 if (diff > 0) {
315 removed_sum += diff;
316 terms_[var] = (terms_[var] > 0) ? bound : -bound;
317 }
318 activity += GetCoefficient(var);
319 } else {
320 // Because we assume the slack (rhs - activity) to be negative, we have
321 // coeff + rhs - max_sum_ <= coeff + rhs - (activity + coeff)
322 // <= slack
323 // < 0
324 CHECK_LE(diff, 0);
325 }
326 }
327 rhs_ -= removed_sum;
328 max_sum_ -= removed_sum;
329 DCHECK_EQ(max_sum_, ComputeMaxSum());
330 return rhs_ - activity;
331}
332
334 const Trail& trail, int trail_index, Coefficient initial_slack,
335 Coefficient target) {
336 // Positive slack.
337 const Coefficient slack = initial_slack;
338 DCHECK_EQ(slack, ComputeSlackForTrailPrefix(trail, trail_index));
339 CHECK_LE(target, slack);
340 CHECK_GE(target, 0);
341
342 // This is not stricly needed, but true in our use case:
343 // The variable assigned at trail_index was causing a conflict.
344 const Coefficient coeff = GetCoefficient(trail[trail_index].Variable());
345 CHECK_LT(slack, coeff);
346
347 // Nothing to do if the slack is already target.
348 if (slack == target) return;
349
350 // Applies the algorithm described in the .h
351 const Coefficient diff = slack - target;
352 rhs_ -= diff;
353 for (BooleanVariable var : PossibleNonZeros()) {
354 if (GetCoefficient(var) == 0) continue;
355 if (trail.Assignment().LiteralIsTrue(GetLiteral(var)) &&
356 trail.Info(var).trail_index < trail_index) {
357 continue;
358 }
359 if (GetCoefficient(var) > diff) {
360 terms_[var] = (terms_[var] > 0) ? terms_[var] - diff : terms_[var] + diff;
361 max_sum_ -= diff;
362 } else {
363 max_sum_ -= GetCoefficient(var);
364 terms_[var] = 0;
365 }
366 }
367 DCHECK_EQ(max_sum_, ComputeMaxSum());
368}
369
371 std::vector<LiteralWithCoeff>* output) {
372 output->clear();
373 for (BooleanVariable var : non_zeros_.PositionsSetAtLeastOnce()) {
374 const Coefficient coeff = GetCoefficient(var);
375 if (coeff != 0) {
376 output->push_back(LiteralWithCoeff(GetLiteral(var), GetCoefficient(var)));
377 }
378 }
379 std::sort(output->begin(), output->end(), CoeffComparator);
380}
381
382Coefficient MutableUpperBoundedLinearConstraint::ComputeMaxSum() const {
383 Coefficient result(0);
384 for (BooleanVariable var : non_zeros_.PositionsSetAtLeastOnce()) {
385 result += GetCoefficient(var);
386 }
387 return result;
388}
389
391 const std::vector<LiteralWithCoeff>& cst)
392 : is_marked_for_deletion_(false),
393 is_learned_(false),
394 first_reason_trail_index_(-1),
395 activity_(0.0) {
396 DCHECK(!cst.empty());
397 DCHECK(std::is_sorted(cst.begin(), cst.end(), CoeffComparator));
398 literals_.reserve(cst.size());
399
400 // Reserve the space for coeffs_ and starts_ (it is slightly more efficient).
401 {
402 int size = 0;
403 Coefficient prev(0); // Ignore initial zeros.
404 for (LiteralWithCoeff term : cst) {
405 if (term.coefficient != prev) {
406 prev = term.coefficient;
407 ++size;
408 }
409 }
410 coeffs_.reserve(size);
411 starts_.reserve(size + 1);
412 }
413
414 Coefficient prev(0);
415 for (LiteralWithCoeff term : cst) {
416 if (term.coefficient != prev) {
417 prev = term.coefficient;
418 coeffs_.push_back(term.coefficient);
419 starts_.push_back(literals_.size());
420 }
421 literals_.push_back(term.literal);
422 }
423
424 // Sentinel.
425 starts_.push_back(literals_.size());
426
427 hash_ = ThoroughHash(reinterpret_cast<const char*>(cst.data()),
428 cst.size() * sizeof(LiteralWithCoeff));
429}
430
433 int literal_index = 0;
434 int coeff_index = 0;
435 for (Literal literal : literals_) {
436 conflict->AddTerm(literal, coeffs_[coeff_index]);
437 ++literal_index;
438 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
439 }
440 conflict->AddToRhs(rhs_);
441}
442
444 const std::vector<LiteralWithCoeff>& cst) {
445 if (cst.size() != literals_.size()) return false;
446 int literal_index = 0;
447 int coeff_index = 0;
448 for (LiteralWithCoeff term : cst) {
449 if (literals_[literal_index] != term.literal) return false;
450 if (coeffs_[coeff_index] != term.coefficient) return false;
451 ++literal_index;
452 if (literal_index == starts_[coeff_index + 1]) {
453 ++coeff_index;
454 }
455 }
456 return true;
457}
458
460 Coefficient rhs, int trail_index, Coefficient* threshold, Trail* trail,
462 // Compute the slack from the assigned variables with a trail index
463 // smaller than the given trail_index. The variable at trail_index has not
464 // yet been propagated.
465 rhs_ = rhs;
466 Coefficient slack = rhs;
467
468 // sum_at_previous_level[i] is the sum of assigned literals with a level <
469 // i. Since we want the sums up to sum_at_previous_level[last_level + 1],
470 // the size of the vector must be last_level + 2.
471 const int last_level = trail->CurrentDecisionLevel();
472 std::vector<Coefficient> sum_at_previous_level(last_level + 2,
473 Coefficient(0));
474
475 int max_relevant_trail_index = 0;
476 if (trail_index > 0) {
477 int literal_index = 0;
478 int coeff_index = 0;
479 for (Literal literal : literals_) {
480 const BooleanVariable var = literal.Variable();
481 const Coefficient coeff = coeffs_[coeff_index];
482 if (trail->Assignment().LiteralIsTrue(literal) &&
483 trail->Info(var).trail_index < trail_index) {
484 max_relevant_trail_index =
485 std::max(max_relevant_trail_index, trail->Info(var).trail_index);
486 slack -= coeff;
487 sum_at_previous_level[trail->Info(var).level + 1] += coeff;
488 }
489 ++literal_index;
490 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
491 }
492
493 // The constraint is infeasible provided the current propagated trail.
494 if (slack < 0) return false;
495
496 // Cummulative sum.
497 for (int i = 1; i < sum_at_previous_level.size(); ++i) {
498 sum_at_previous_level[i] += sum_at_previous_level[i - 1];
499 }
500 }
501
502 // Check the no-propagation at earlier level precondition.
503 int literal_index = 0;
504 int coeff_index = 0;
505 for (Literal literal : literals_) {
506 const BooleanVariable var = literal.Variable();
507 const int level = trail->Assignment().VariableIsAssigned(var)
508 ? trail->Info(var).level
509 : last_level;
510 if (level > 0) {
511 CHECK_LE(coeffs_[coeff_index], rhs_ - sum_at_previous_level[level])
512 << "var should have been propagated at an earlier level !";
513 }
514 ++literal_index;
515 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
516 }
517
518 // Initial propagation.
519 //
520 // TODO(user): The source trail index for the propagation reason (i.e.
521 // max_relevant_trail_index) may be higher than necessary (for some of the
522 // propagated literals). Currently this works with FillReason(), but it was a
523 // source of a really nasty bug (see CL 68906167) because of the (rhs == 1)
524 // optim. Find a good way to test the logic.
525 index_ = coeffs_.size() - 1;
526 already_propagated_end_ = literals_.size();
527 Update(slack, threshold);
528 return *threshold < 0
529 ? Propagate(max_relevant_trail_index, threshold, trail, helper)
530 : true;
531}
532
534 int trail_index, Coefficient* threshold, Trail* trail,
536 DCHECK_LT(*threshold, 0);
537 const Coefficient slack = GetSlackFromThreshold(*threshold);
538 DCHECK_GE(slack, 0) << "The constraint is already a conflict!";
539 while (index_ >= 0 && coeffs_[index_] > slack) --index_;
540
541 // Check propagation.
542 BooleanVariable first_propagated_variable(-1);
543 for (int i = starts_[index_ + 1]; i < already_propagated_end_; ++i) {
544 if (trail->Assignment().LiteralIsFalse(literals_[i])) continue;
545 if (trail->Assignment().LiteralIsTrue(literals_[i])) {
546 if (trail->Info(literals_[i].Variable()).trail_index > trail_index) {
547 // Conflict.
548 FillReason(*trail, trail_index, literals_[i].Variable(),
549 &helper->conflict);
550 helper->conflict.push_back(literals_[i].Negated());
551 Update(slack, threshold);
552 return false;
553 }
554 } else {
555 // Propagation.
556 if (first_propagated_variable < 0) {
557 if (first_reason_trail_index_ == -1) {
558 first_reason_trail_index_ = trail->Index();
559 }
560 helper->Enqueue(literals_[i].Negated(), trail_index, this, trail);
561 first_propagated_variable = literals_[i].Variable();
562 } else {
563 // Note that the reason for first_propagated_variable is always a
564 // valid reason for literals_[i].Variable() because we process the
565 // variable in increasing coefficient order.
566 trail->EnqueueWithSameReasonAs(literals_[i].Negated(),
567 first_propagated_variable);
568 }
569 }
570 }
571 Update(slack, threshold);
572 DCHECK_GE(*threshold, 0);
573 return true;
574}
575
577 const Trail& trail, int source_trail_index,
578 BooleanVariable propagated_variable, std::vector<Literal>* reason) {
579 reason->clear();
580
581 // Optimization for an "at most one" constraint.
582 // Note that the source_trail_index set by InitializeRhs() is ok in this case.
583 if (rhs_ == 1) {
584 reason->push_back(trail[source_trail_index].Negated());
585 return;
586 }
587
588 // Optimization: This will be set to the index of the last literal in the
589 // reason.
590 int last_i = 0;
591 int last_coeff_index = 0;
592
593 // Compute the initial reason which is formed by all the literals of the
594 // constraint that were assigned to true at the time of the propagation.
595 // We remove literals with a level of 0 since they are not needed.
596 // We also compute the slack at the time.
597 Coefficient slack = rhs_;
598 Coefficient propagated_variable_coefficient(0);
599 int coeff_index = coeffs_.size() - 1;
600 for (int i = literals_.size() - 1; i >= 0; --i) {
601 const Literal literal = literals_[i];
602 if (literal.Variable() == propagated_variable) {
603 propagated_variable_coefficient = coeffs_[coeff_index];
604 } else {
605 if (trail.Assignment().LiteralIsTrue(literal) &&
606 trail.Info(literal.Variable()).trail_index <= source_trail_index) {
607 if (trail.Info(literal.Variable()).level > 0) {
608 reason->push_back(literal.Negated());
609 last_i = i;
610 last_coeff_index = coeff_index;
611 }
612 slack -= coeffs_[coeff_index];
613 }
614 }
615 if (i == starts_[coeff_index]) {
616 --coeff_index;
617 }
618 }
619 DCHECK_GT(propagated_variable_coefficient, slack);
620 DCHECK_GE(propagated_variable_coefficient, 0);
621
622 // In both cases, we can't minimize the reason further.
623 if (reason->size() <= 1 || coeffs_.size() == 1) return;
624
625 Coefficient limit = propagated_variable_coefficient - slack;
626 DCHECK_GE(limit, 1);
627
628 // Remove literals with small coefficients from the reason as long as the
629 // limit is still stricly positive.
630 coeff_index = last_coeff_index;
631 if (coeffs_[coeff_index] >= limit) return;
632 for (int i = last_i; i < literals_.size(); ++i) {
633 const Literal literal = literals_[i];
634 if (i == starts_[coeff_index + 1]) {
635 ++coeff_index;
636 if (coeffs_[coeff_index] >= limit) break;
637 }
638 if (literal.Negated() != reason->back()) continue;
639 limit -= coeffs_[coeff_index];
640 reason->pop_back();
641 if (coeffs_[coeff_index] >= limit) break;
642 }
643 DCHECK(!reason->empty());
644 DCHECK_GE(limit, 1);
645}
646
648 const Trail& trail, int trail_index,
649 const MutableUpperBoundedLinearConstraint& conflict) {
650 Coefficient result(0);
651 int literal_index = 0;
652 int coeff_index = 0;
653 for (Literal literal : literals_) {
654 if (!trail.Assignment().VariableIsAssigned(literal.Variable()) ||
655 trail.Info(literal.Variable()).trail_index >= trail_index) {
656 result += conflict.CancelationAmount(literal, coeffs_[coeff_index]);
657 }
658 ++literal_index;
659 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
660 }
661 return result;
662}
663
665 const Trail& trail, BooleanVariable var,
667 Coefficient* conflict_slack) {
668 const int limit_trail_index = trail.Info(var).trail_index;
669
670 // Compute the constraint activity at the time and the coefficient of the
671 // variable var.
672 Coefficient activity(0);
673 Coefficient var_coeff(0);
674 int literal_index = 0;
675 int coeff_index = 0;
676 for (Literal literal : literals_) {
677 if (literal.Variable() == var) {
678 // The variable must be of the opposite sign in the current conflict.
679 CHECK_NE(literal, conflict->GetLiteral(var));
680 var_coeff = coeffs_[coeff_index];
681 } else if (trail.Assignment().LiteralIsTrue(literal) &&
682 trail.Info(literal.Variable()).trail_index < limit_trail_index) {
683 activity += coeffs_[coeff_index];
684 }
685 ++literal_index;
686 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
687 }
688
689 // Special case.
690 if (activity > rhs_) {
691 // This constraint is already a conflict.
692 // Use this one instead to start the resolution.
693 //
694 // TODO(user): Investigate if this is a good idea. It doesn't happen often,
695 // but does happend. Maybe we can detect this before in Propagate()? The
696 // setup is:
697 // - At a given trail_index, var is propagated and added on the trail.
698 // - There is some constraint literals assigned to true with a trail index
699 // in (trail_index, var.trail_index).
700 // - Their sum is high enough to cause a conflict.
701 // - But individually, their coefficients are too small to be propagated, so
702 // the conflict is not yet detected. It will be when these variables are
703 // processed by PropagateNext().
704 conflict->ClearAll();
705 AddToConflict(conflict);
706 *conflict_slack = rhs_ - activity;
707 DCHECK_EQ(*conflict_slack,
708 conflict->ComputeSlackForTrailPrefix(trail, limit_trail_index));
709 return;
710 }
711
712 // This is the slack of *this for the trail prefix < limit_trail_index.
713 const Coefficient slack = rhs_ - activity;
714 CHECK_GE(slack, 0);
715
716 // This is the slack of the conflict at the same level.
717 DCHECK_EQ(*conflict_slack,
718 conflict->ComputeSlackForTrailPrefix(trail, limit_trail_index));
719
720 // TODO(user): If there is more "cancelation" than the min_coeffs below when
721 // we add the two constraints, the resulting slack may be even lower. Taking
722 // that into account is probably good.
723 const Coefficient cancelation =
724 DEBUG_MODE ? ComputeCancelation(trail, limit_trail_index, *conflict)
725 : Coefficient(0);
726
727 // When we add the two constraints together, the slack of the result for the
728 // trail < limit_trail_index - 1 must be negative. We know that its value is
729 // <= slack1 + slack2 - min(coeffs), so we have nothing to do if this bound is
730 // already negative.
731 const Coefficient conflict_var_coeff = conflict->GetCoefficient(var);
732 const Coefficient min_coeffs = std::min(var_coeff, conflict_var_coeff);
733 const Coefficient new_slack_ub = slack + *conflict_slack - min_coeffs;
734 CHECK_LT(*conflict_slack, conflict_var_coeff);
735 CHECK_LT(slack, var_coeff);
736 if (new_slack_ub < 0) {
737 AddToConflict(conflict);
738 DCHECK_EQ(*conflict_slack + slack - cancelation,
739 conflict->ComputeSlackForTrailPrefix(trail, limit_trail_index));
740 return;
741 }
742
743 // We need to relax one or both of the constraints so the new slack is < 0.
744 // Using the relaxation described in ReduceSlackTo(), we can have this new
745 // slack bound:
746 //
747 // (slack - diff) + (conflict_slack - conflict_diff)
748 // - min(var_coeff - diff, conflict_var_coeff - conflict_diff).
749 //
750 // For all diff in [0, slack)
751 // For all conflict_diff in [0, conflict_slack)
752 Coefficient diff(0);
753 Coefficient conflict_diff(0);
754
755 // Is relaxing the constraint with the highest coeff enough?
756 if (new_slack_ub < std::max(var_coeff, conflict_var_coeff) - min_coeffs) {
757 const Coefficient reduc = new_slack_ub + 1;
758 if (var_coeff < conflict_var_coeff) {
759 conflict_diff += reduc;
760 } else {
761 diff += reduc;
762 }
763 } else {
764 // Just reduce the slack of both constraints to zero.
765 //
766 // TODO(user): The best will be to relax as little as possible.
767 diff = slack;
768 conflict_diff = *conflict_slack;
769 }
770
771 // Relax the conflict.
772 CHECK_GE(conflict_diff, 0);
773 CHECK_LE(conflict_diff, *conflict_slack);
774 if (conflict_diff > 0) {
775 conflict->ReduceSlackTo(trail, limit_trail_index, *conflict_slack,
776 *conflict_slack - conflict_diff);
777 *conflict_slack -= conflict_diff;
778 }
779
780 // We apply the same algorithm as the one in ReduceSlackTo() but on
781 // the non-mutable representation and add it on the fly into conflict.
782 CHECK_GE(diff, 0);
783 CHECK_LE(diff, slack);
784 if (diff == 0) {
785 // Special case if there if no relaxation is needed.
786 AddToConflict(conflict);
787 return;
788 }
789
790 literal_index = 0;
791 coeff_index = 0;
792 for (Literal literal : literals_) {
793 if (trail.Assignment().LiteralIsTrue(literal) &&
794 trail.Info(literal.Variable()).trail_index < limit_trail_index) {
795 conflict->AddTerm(literal, coeffs_[coeff_index]);
796 } else {
797 const Coefficient new_coeff = coeffs_[coeff_index] - diff;
798 if (new_coeff > 0) {
799 // TODO(user): track the cancelation here so we can update
800 // *conflict_slack properly.
801 conflict->AddTerm(literal, new_coeff);
802 }
803 }
804 ++literal_index;
805 if (literal_index == starts_[coeff_index + 1]) ++coeff_index;
806 }
807
808 // And the rhs.
809 conflict->AddToRhs(rhs_ - diff);
810}
811
812void UpperBoundedLinearConstraint::Untrail(Coefficient* threshold,
813 int trail_index) {
814 const Coefficient slack = GetSlackFromThreshold(*threshold);
815 while (index_ + 1 < coeffs_.size() && coeffs_[index_ + 1] <= slack) ++index_;
816 Update(slack, threshold);
817 if (first_reason_trail_index_ >= trail_index) {
818 first_reason_trail_index_ = -1;
819 }
820}
821
822// TODO(user): This is relatively slow. Take the "transpose" all at once, and
823// maybe put small constraints first on the to_update_ lists.
824bool PbConstraints::AddConstraint(const std::vector<LiteralWithCoeff>& cst,
825 Coefficient rhs, Trail* trail) {
826 SCOPED_TIME_STAT(&stats_);
827 DCHECK(!cst.empty());
828 DCHECK(std::is_sorted(cst.begin(), cst.end(), CoeffComparator));
829
830 // Special case if this is the first constraint.
831 if (constraints_.empty()) {
832 to_update_.resize(trail->NumVariables() << 1);
833 enqueue_helper_.propagator_id = propagator_id_;
834 enqueue_helper_.reasons.resize(trail->NumVariables());
836 }
837
838 std::unique_ptr<UpperBoundedLinearConstraint> c(
840 std::vector<UpperBoundedLinearConstraint*>& duplicate_candidates =
841 possible_duplicates_[c->hash()];
842
843 // Optimization if the constraint terms are duplicates.
844 for (UpperBoundedLinearConstraint* candidate : duplicate_candidates) {
845 if (candidate->HasIdenticalTerms(cst)) {
846 if (rhs < candidate->Rhs()) {
847 // TODO(user): the index is needed to give the correct thresholds_ entry
848 // to InitializeRhs() below, but this linear scan is not super
849 // efficient.
850 ConstraintIndex i(0);
851 while (i < constraints_.size() &&
852 constraints_[i.value()].get() != candidate) {
853 ++i;
854 }
855 CHECK_LT(i, constraints_.size());
856 return candidate->InitializeRhs(rhs, propagation_trail_index_,
857 &thresholds_[i], trail,
858 &enqueue_helper_);
859 } else {
860 // The constraint is redundant, so there is nothing to do.
861 return true;
862 }
863 }
864 }
865
866 thresholds_.push_back(Coefficient(0));
867 if (!c->InitializeRhs(rhs, propagation_trail_index_, &thresholds_.back(),
868 trail, &enqueue_helper_)) {
869 thresholds_.pop_back();
870 return false;
871 }
872
873 const ConstraintIndex cst_index(constraints_.size());
874 duplicate_candidates.push_back(c.get());
875 constraints_.emplace_back(c.release());
876 for (LiteralWithCoeff term : cst) {
877 DCHECK_LT(term.literal.Index(), to_update_.size());
878 to_update_[term.literal.Index()].push_back(ConstraintIndexWithCoeff(
879 trail->Assignment().VariableIsAssigned(term.literal.Variable()),
880 cst_index, term.coefficient));
881 }
882 return true;
883}
884
886 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs, Trail* trail) {
887 DeleteSomeLearnedConstraintIfNeeded();
888 const int old_num_constraints = constraints_.size();
889 const bool result = AddConstraint(cst, rhs, trail);
890
891 // The second test is to avoid marking a problem constraint as learned because
892 // of the "reuse last constraint" optimization.
893 if (result && constraints_.size() > old_num_constraints) {
894 constraints_.back()->set_is_learned(true);
895 }
896 return result;
897}
898
899bool PbConstraints::PropagateNext(Trail* trail) {
900 SCOPED_TIME_STAT(&stats_);
901 const int source_trail_index = propagation_trail_index_;
902 const Literal true_literal = (*trail)[propagation_trail_index_];
904
905 // We need to upate ALL threshold, otherwise the Untrail() will not be
906 // synchronized.
907 bool conflict = false;
908 num_threshold_updates_ += to_update_[true_literal.Index()].size();
909 for (ConstraintIndexWithCoeff& update : to_update_[true_literal.Index()]) {
910 const Coefficient threshold =
911 thresholds_[update.index] - update.coefficient;
912 thresholds_[update.index] = threshold;
913 if (threshold < 0 && !conflict) {
915 constraints_[update.index.value()].get();
916 update.need_untrail_inspection = true;
917 ++num_constraint_lookups_;
918 const int old_value = cst->already_propagated_end();
919 if (!cst->Propagate(source_trail_index, &thresholds_[update.index], trail,
920 &enqueue_helper_)) {
921 trail->MutableConflict()->swap(enqueue_helper_.conflict);
922 conflicting_constraint_index_ = update.index;
923 conflict = true;
924
925 // We bump the activity of the conflict.
926 BumpActivity(constraints_[update.index.value()].get());
927 }
928 num_inspected_constraint_literals_ +=
929 old_value - cst->already_propagated_end();
930 }
931 }
932 return !conflict;
933}
934
936 const int old_index = trail->Index();
937 while (trail->Index() == old_index && propagation_trail_index_ < old_index) {
938 if (!PropagateNext(trail)) return false;
939 }
940 return true;
941}
942
943void PbConstraints::Untrail(const Trail& trail, int trail_index) {
944 SCOPED_TIME_STAT(&stats_);
945 to_untrail_.ClearAndResize(ConstraintIndex(constraints_.size()));
946 while (propagation_trail_index_ > trail_index) {
949 for (ConstraintIndexWithCoeff& update : to_update_[literal.Index()]) {
950 thresholds_[update.index] += update.coefficient;
951
952 // Only the constraints which were inspected during Propagate() need
953 // inspection during Untrail().
954 if (update.need_untrail_inspection) {
955 update.need_untrail_inspection = false;
956 to_untrail_.Set(update.index);
957 }
958 }
959 }
960 for (ConstraintIndex cst_index : to_untrail_.PositionsSetAtLeastOnce()) {
961 constraints_[cst_index.value()]->Untrail(&(thresholds_[cst_index]),
962 trail_index);
963 }
964}
965
966absl::Span<const Literal> PbConstraints::Reason(const Trail& trail,
967 int trail_index) const {
968 SCOPED_TIME_STAT(&stats_);
969 const PbConstraintsEnqueueHelper::ReasonInfo& reason_info =
970 enqueue_helper_.reasons[trail_index];
971 std::vector<Literal>* reason = trail.GetEmptyVectorToStoreReason(trail_index);
972 reason_info.pb_constraint->FillReason(trail, reason_info.source_trail_index,
973 trail[trail_index].Variable(), reason);
974 return *reason;
975}
976
978 int trail_index) const {
979 const PbConstraintsEnqueueHelper::ReasonInfo& reason_info =
980 enqueue_helper_.reasons[trail_index];
981 return reason_info.pb_constraint;
982}
983
984// TODO(user): Because num_constraints also include problem constraints, the
985// policy may not be what we want if there is a big number of problem
986// constraints. Fix this.
987void PbConstraints::ComputeNewLearnedConstraintLimit() {
988 const int num_constraints = constraints_.size();
989 target_number_of_learned_constraint_ =
990 num_constraints + parameters_->pb_cleanup_increment();
991 num_learned_constraint_before_cleanup_ =
992 static_cast<int>(target_number_of_learned_constraint_ /
993 parameters_->pb_cleanup_ratio()) -
994 num_constraints;
995}
996
997void PbConstraints::DeleteSomeLearnedConstraintIfNeeded() {
998 if (num_learned_constraint_before_cleanup_ == 0) {
999 // First time.
1000 ComputeNewLearnedConstraintLimit();
1001 return;
1002 }
1003 --num_learned_constraint_before_cleanup_;
1004 if (num_learned_constraint_before_cleanup_ > 0) return;
1005 SCOPED_TIME_STAT(&stats_);
1006
1007 // Mark the constraint that needs to be deleted.
1008 // We do that in two pass, first we extract the activities.
1009 std::vector<double> activities;
1010 for (int i = 0; i < constraints_.size(); ++i) {
1011 const UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1012 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1013 activities.push_back(constraint.activity());
1014 }
1015 }
1016
1017 // Then we compute the cutoff threshold.
1018 // Note that we can't delete constraint used as a reason!!
1019 std::sort(activities.begin(), activities.end());
1020 const int num_constraints_to_delete =
1021 constraints_.size() - target_number_of_learned_constraint_;
1022 CHECK_GT(num_constraints_to_delete, 0);
1023 if (num_constraints_to_delete >= activities.size()) {
1024 // Unlikely, but may happen, so in this case, we just delete all the
1025 // constraint that can possibly be deleted
1026 for (int i = 0; i < constraints_.size(); ++i) {
1027 UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1028 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1029 constraint.MarkForDeletion();
1030 }
1031 }
1032 } else {
1033 const double limit_activity = activities[num_constraints_to_delete];
1034 int num_constraint_at_limit_activity = 0;
1035 for (int i = num_constraints_to_delete; i >= 0; --i) {
1036 if (activities[i] == limit_activity) {
1037 ++num_constraint_at_limit_activity;
1038 } else {
1039 break;
1040 }
1041 }
1042
1043 // Mark for deletion all the constraints under this threshold.
1044 // We only keep the most recent constraint amongst the one with the activity
1045 // exactly equal ot limit_activity, it is why the loop is in the reverse
1046 // order.
1047 for (int i = constraints_.size() - 1; i >= 0; --i) {
1048 UpperBoundedLinearConstraint& constraint = *(constraints_[i].get());
1049 if (constraint.is_learned() && !constraint.is_used_as_a_reason()) {
1050 if (constraint.activity() <= limit_activity) {
1051 if (constraint.activity() == limit_activity &&
1052 num_constraint_at_limit_activity > 0) {
1053 --num_constraint_at_limit_activity;
1054 } else {
1055 constraint.MarkForDeletion();
1056 }
1057 }
1058 }
1059 }
1060 }
1061
1062 // Finally we delete the marked constraint and compute the next limit.
1063 DeleteConstraintMarkedForDeletion();
1064 ComputeNewLearnedConstraintLimit();
1065}
1066
1068 if (!constraint->is_learned()) return;
1069 const double max_activity = parameters_->max_clause_activity_value();
1070 constraint->set_activity(constraint->activity() +
1071 constraint_activity_increment_);
1072 if (constraint->activity() > max_activity) {
1073 RescaleActivities(1.0 / max_activity);
1074 }
1075}
1076
1077void PbConstraints::RescaleActivities(double scaling_factor) {
1078 constraint_activity_increment_ *= scaling_factor;
1079 for (int i = 0; i < constraints_.size(); ++i) {
1080 constraints_[i]->set_activity(constraints_[i]->activity() * scaling_factor);
1081 }
1082}
1083
1085 const double decay = parameters_->clause_activity_decay();
1086 constraint_activity_increment_ *= 1.0 / decay;
1087}
1088
1089void PbConstraints::DeleteConstraintMarkedForDeletion() {
1091 constraints_.size(), ConstraintIndex(-1));
1092 ConstraintIndex new_index(0);
1093 for (ConstraintIndex i(0); i < constraints_.size(); ++i) {
1094 if (!constraints_[i.value()]->is_marked_for_deletion()) {
1095 index_mapping[i] = new_index;
1096 if (new_index < i) {
1097 constraints_[new_index.value()] = std::move(constraints_[i.value()]);
1098 thresholds_[new_index] = thresholds_[i];
1099 }
1100 ++new_index;
1101 } else {
1102 // Remove it from possible_duplicates_.
1103 UpperBoundedLinearConstraint* c = constraints_[i.value()].get();
1104 std::vector<UpperBoundedLinearConstraint*>& ref =
1105 possible_duplicates_[c->hash()];
1106 for (int i = 0; i < ref.size(); ++i) {
1107 if (ref[i] == c) {
1108 std::swap(ref[i], ref.back());
1109 ref.pop_back();
1110 break;
1111 }
1112 }
1113 }
1114 }
1115 constraints_.resize(new_index.value());
1116 thresholds_.resize(new_index.value());
1117
1118 // This is the slow part, we need to remap all the ConstraintIndex to the
1119 // new ones.
1120 for (LiteralIndex lit(0); lit < to_update_.size(); ++lit) {
1121 std::vector<ConstraintIndexWithCoeff>& updates = to_update_[lit];
1122 int new_index = 0;
1123 for (int i = 0; i < updates.size(); ++i) {
1124 const ConstraintIndex m = index_mapping[updates[i].index];
1125 if (m != -1) {
1126 updates[new_index] = updates[i];
1127 updates[new_index].index = m;
1128 ++new_index;
1129 }
1130 }
1131 updates.resize(new_index);
1132 }
1133}
1134
1135} // namespace sat
1136} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define DCHECK(condition)
Definition: base/logging.h:884
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
size_type size() const
void push_back(const value_type &x)
void Set(IntegerType index)
Definition: bitset.h:803
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
void ClearAndResize(IntegerType size)
Definition: bitset.h:778
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
LiteralIndex Index() const
Definition: sat_base.h:84
BooleanVariable Variable() const
Definition: sat_base.h:80
const std::vector< BooleanVariable > & PossibleNonZeros() const
Coefficient ComputeSlackForTrailPrefix(const Trail &trail, int trail_index) const
Coefficient ReduceCoefficientsAndComputeSlackForTrailPrefix(const Trail &trail, int trail_index)
void ReduceSlackTo(const Trail &trail, int trail_index, Coefficient initial_slack, Coefficient target)
Coefficient CancelationAmount(Literal literal, Coefficient coeff) const
void AddTerm(Literal literal, Coefficient coeff)
void CopyIntoVector(std::vector< LiteralWithCoeff > *output)
Coefficient GetCoefficient(BooleanVariable var) const
void RescaleActivities(double scaling_factor)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
bool AddConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
UpperBoundedLinearConstraint * ReasonPbConstraint(int trail_index) const
void BumpActivity(UpperBoundedLinearConstraint *constraint)
void Untrail(const Trail &trail, int trail_index) final
bool AddLearnedConstraint(const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
Definition: sat_base.h:272
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
Coefficient ComputeCancelation(const Trail &trail, int trail_index, const MutableUpperBoundedLinearConstraint &conflict)
bool Propagate(int trail_index, Coefficient *threshold, Trail *trail, PbConstraintsEnqueueHelper *helper)
void FillReason(const Trail &trail, int source_trail_index, BooleanVariable propagated_variable, std::vector< Literal > *reason)
bool HasIdenticalTerms(const std::vector< LiteralWithCoeff > &cst)
void ResolvePBConflict(const Trail &trail, BooleanVariable var, MutableUpperBoundedLinearConstraint *conflict, Coefficient *conflict_slack)
bool InitializeRhs(Coefficient rhs, int trail_index, Coefficient *threshold, Trail *trail, PbConstraintsEnqueueHelper *helper)
void Untrail(Coefficient *threshold, int trail_index)
void AddToConflict(MutableUpperBoundedLinearConstraint *conflict)
UpperBoundedLinearConstraint(const std::vector< LiteralWithCoeff > &cst)
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
int64 value
IntVar * var
Definition: expr_array.cc:1858
const bool DEBUG_MODE
Definition: macros.h:24
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
const LiteralIndex kFalseLiteralIndex(-3)
bool ApplyLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound, Coefficient bound_shift, Coefficient max_value)
void SimplifyCanonicalBooleanLinearConstraint(std::vector< LiteralWithCoeff > *cst, Coefficient *rhs)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
bool BooleanLinearExpressionIsCanonical(const std::vector< LiteralWithCoeff > &cst)
const LiteralIndex kTrueLiteralIndex(-2)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
uint64 ThoroughHash(const char *bytes, size_t len)
Definition: thorough_hash.h:33
bool SafeAddInto(IntegerType a, IntegerType *b)
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
ColIndex representative
int64 bound
int64 coefficient
#define SCOPED_TIME_STAT(stats)
Definition: stats.h:438
void Enqueue(Literal l, int source_trail_index, UpperBoundedLinearConstraint *ct, Trail *trail)