OR-Tools  8.2
pb_constraint.h
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
14#ifndef OR_TOOLS_SAT_PB_CONSTRAINT_H_
15#define OR_TOOLS_SAT_PB_CONSTRAINT_H_
16
17#include <algorithm>
18#include <limits>
19#include <memory>
20#include <string>
21#include <vector>
22
23#include "absl/container/flat_hash_map.h"
24#include "absl/types/span.h"
28#include "ortools/base/macros.h"
30#include "ortools/sat/model.h"
32#include "ortools/sat/sat_parameters.pb.h"
33#include "ortools/util/bitset.h"
34#include "ortools/util/stats.h"
35
36namespace operations_research {
37namespace sat {
38
39// The type of the integer coefficients in a pseudo-Boolean constraint.
40// This is also used for the current value of a constraint or its bounds.
41DEFINE_INT_TYPE(Coefficient, int64);
42
43// IMPORTANT: We can't use numeric_limits<Coefficient>::max() which will compile
44// but just returns zero!!
45const Coefficient kCoefficientMax(
47
48// Represents a term in a pseudo-Boolean formula.
51 LiteralWithCoeff(Literal l, Coefficient c) : literal(l), coefficient(c) {}
54 Coefficient coefficient;
55 bool operator==(const LiteralWithCoeff& other) const {
56 return literal.Index() == other.literal.Index() &&
57 coefficient == other.coefficient;
58 }
59};
60inline std::ostream& operator<<(std::ostream& os, LiteralWithCoeff term) {
61 os << term.coefficient << "[" << term.literal.DebugString() << "]";
62 return os;
63}
64
65// Puts the given Boolean linear expression in canonical form:
66// - Merge all the literal corresponding to the same variable.
67// - Remove zero coefficients.
68// - Make all the coefficients positive.
69// - Sort the terms by increasing coefficient values.
70//
71// This function also computes:
72// - max_value: the maximum possible value of the formula.
73// - bound_shift: which allows to updates initial bounds. That is, if an
74// initial pseudo-Boolean constraint was
75// lhs < initial_pb_formula < rhs
76// then the new one is:
77// lhs + bound_shift < canonical_form < rhs + bound_shift
78//
79// Finally, this will return false, if some integer overflow or underflow
80// occurred during the reduction to the canonical form.
82 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
83 Coefficient* max_value);
84
85// Maps all the literals of the given constraint using the given mapping. The
86// mapping may map a literal index to kTrueLiteralIndex or kFalseLiteralIndex in
87// which case the literal will be considered fixed to the appropriate value.
88//
89// Note that this function also canonicalizes the constraint and updates
90// bound_shift and max_value like ComputeBooleanLinearExpressionCanonicalForm()
91// does.
92//
93// Finally, this will return false if some integer overflow or underflow
94// occurred during the constraint simplification.
97 std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
98 Coefficient* max_value);
99
100// From a constraint 'expr <= ub' and the result (bound_shift, max_value) of
101// calling ComputeBooleanLinearExpressionCanonicalForm() on 'expr', this returns
102// a new rhs such that 'canonical expression <= rhs' is an equivalent
103// constraint. This function deals with all the possible overflow corner cases.
104//
105// The result will be in [-1, max_value] where -1 means unsatisfiable and
106// max_value means trivialy satisfiable.
107Coefficient ComputeCanonicalRhs(Coefficient upper_bound,
108 Coefficient bound_shift, Coefficient max_value);
109
110// Same as ComputeCanonicalRhs(), but uses the initial constraint lower bound
111// instead. From a constraint 'lb <= expression', this returns a rhs such that
112// 'canonical expression with literals negated <= rhs'.
113//
114// Note that the range is also [-1, max_value] with the same meaning.
115Coefficient ComputeNegatedCanonicalRhs(Coefficient lower_bound,
116 Coefficient bound_shift,
117 Coefficient max_value);
118
119// Returns true iff the Boolean linear expression is in canonical form.
121 const std::vector<LiteralWithCoeff>& cst);
122
123// Given a Boolean linear constraint in canonical form, simplify its
124// coefficients using simple heuristics.
126 std::vector<LiteralWithCoeff>* cst, Coefficient* rhs);
127
128// Holds a set of boolean linear constraints in canonical form:
129// - The constraint is a linear sum of LiteralWithCoeff <= rhs.
130// - The linear sum satisfies the properties described in
131// ComputeBooleanLinearExpressionCanonicalForm().
132//
133// TODO(user): Simplify further the constraints.
134//
135// TODO(user): Remove the duplication between this and what the sat solver
136// is doing in AddLinearConstraint() which is basically the same.
137//
138// TODO(user): Remove duplicate constraints? some problems have them, and
139// this is not ideal for the symmetry computation since it leads to a lot of
140// symmetries of the associated graph that are not useful.
142 public:
144
145 // Adds a new constraint to the problem. The bounds are inclusive.
146 // Returns false in case of a possible overflow or if the constraint is
147 // never satisfiable.
148 //
149 // TODO(user): Use a return status to distinguish errors if needed.
150 bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound,
151 bool use_upper_bound, Coefficient upper_bound,
152 std::vector<LiteralWithCoeff>* cst);
153
154 // Getters. All the constraints are guaranteed to be in canonical form.
155 int NumConstraints() const { return constraints_.size(); }
156 const Coefficient Rhs(int i) const { return rhs_[i]; }
157 const std::vector<LiteralWithCoeff>& Constraint(int i) const {
158 return constraints_[i];
159 }
160
161 private:
162 bool AddConstraint(const std::vector<LiteralWithCoeff>& cst,
163 Coefficient max_value, Coefficient rhs);
164
165 std::vector<Coefficient> rhs_;
166 std::vector<std::vector<LiteralWithCoeff>> constraints_;
167 DISALLOW_COPY_AND_ASSIGN(CanonicalBooleanLinearProblem);
168};
169
170// Encode a constraint sum term <= rhs, where each term is a positive
171// Coefficient times a literal. This class allows efficient modification of the
172// constraint and is used during pseudo-Boolean resolution.
174 public:
175 // This must be called before any other functions is used with an higher
176 // variable index.
177 void ClearAndResize(int num_variables);
178
179 // Reset the constraint to 0 <= 0.
180 // Note that the contraint size stays the same.
181 void ClearAll();
182
183 // Returns the coefficient (>= 0) of the given variable.
184 Coefficient GetCoefficient(BooleanVariable var) const {
185 return AbsCoefficient(terms_[var]);
186 }
187
188 // Returns the literal under which the given variable appear in the
189 // constraint. Note that if GetCoefficient(var) == 0 this just returns
190 // Literal(var, true).
191 Literal GetLiteral(BooleanVariable var) const {
192 return Literal(var, terms_[var] > 0);
193 }
194
195 // If we have a lower bounded constraint sum terms >= rhs, then it is trivial
196 // to see that the coefficient of any term can be reduced to rhs if it is
197 // bigger. This does exactly this operation, but on the upper bounded
198 // representation.
199 //
200 // If we take a constraint sum ci.xi <= rhs, take its negation and add max_sum
201 // on both side, we have sum ci.(1 - xi) >= max_sum - rhs
202 // So every ci > (max_sum - rhs) can be replacend by (max_sum - rhs).
203 // Not that this operation also change the original rhs of the constraint.
204 void ReduceCoefficients();
205
206 // Same as ReduceCoefficients() but only consider the coefficient of the given
207 // variable.
208 void ReduceGivenCoefficient(BooleanVariable var) {
209 const Coefficient bound = max_sum_ - rhs_;
210 const Coefficient diff = GetCoefficient(var) - bound;
211 if (diff > 0) {
212 rhs_ -= diff;
213 max_sum_ -= diff;
214 terms_[var] = (terms_[var] > 0) ? bound : -bound;
215 }
216 }
217
218 // Compute the constraint slack assuming that only the variables with index <
219 // trail_index are assigned.
220 Coefficient ComputeSlackForTrailPrefix(const Trail& trail,
221 int trail_index) const;
222
223 // Same as ReduceCoefficients() followed by ComputeSlackForTrailPrefix(). It
224 // allows to loop only once over all the terms of the constraint instead of
225 // doing it twice. This helps since doing that can be the main bottleneck.
226 //
227 // Note that this function assumes that the returned slack will be negative.
228 // This allow to DCHECK some assumptions on what coefficients can be reduced
229 // or not.
230 //
231 // TODO(user): Ideally the slack should be maitainable incrementally.
233 const Trail& trail, int trail_index);
234
235 // Relaxes the constraint so that:
236 // - ComputeSlackForTrailPrefix(trail, trail_index) == target;
237 // - All the variables that were propagated given the assignment < trail_index
238 // are still propagated.
239 //
240 // As a precondition, ComputeSlackForTrailPrefix(trail, trail_index) >= target
241 // Note that nothing happen if the slack is already equals to target.
242 //
243 // Algorithm: Let diff = slack - target (>= 0). We will split the constraint
244 // linear expression in 3 parts:
245 // - P1: the true variables (only the one assigned < trail_index).
246 // - P2: the other variables with a coeff > diff.
247 // Note that all these variables were the propagated ones.
248 // - P3: the other variables with a coeff <= diff.
249 // We can then transform P1 + P2 + P3 <= rhs_ into P1 + P2' <= rhs_ - diff
250 // Where P2' is the same sum as P2 with all the coefficient reduced by diff.
251 //
252 // Proof: Given the old constraint, we want to show that the relaxed one is
253 // always true. If all the variable in P2' are false, then
254 // P1 <= rhs_ - slack <= rhs_ - diff is always true. If at least one of the
255 // P2' variable is true, then P2 >= P2' + diff and we have
256 // P1 + P2' + diff <= P1 + P2 <= rhs_.
257 void ReduceSlackTo(const Trail& trail, int trail_index,
258 Coefficient initial_slack, Coefficient target);
259
260 // Copies this constraint into a vector<LiteralWithCoeff> representation.
261 void CopyIntoVector(std::vector<LiteralWithCoeff>* output);
262
263 // Adds a non-negative value to this constraint Rhs().
264 void AddToRhs(Coefficient value) {
265 CHECK_GE(value, 0);
266 rhs_ += value;
267 }
268 Coefficient Rhs() const { return rhs_; }
269 Coefficient MaxSum() const { return max_sum_; }
270
271 // Adds a term to this constraint. This is in the .h for efficiency.
272 // The encoding used internally is described below in the terms_ comment.
273 void AddTerm(Literal literal, Coefficient coeff) {
274 CHECK_GT(coeff, 0);
275 const BooleanVariable var = literal.Variable();
276 const Coefficient term_encoding = literal.IsPositive() ? coeff : -coeff;
277 if (literal != GetLiteral(var)) {
278 // The two terms are of opposite sign, a "cancelation" happens.
279 // We need to change the encoding of the lower magnitude term.
280 // - If term > 0, term . x -> term . (x - 1) + term
281 // - If term < 0, term . (x - 1) -> term . x - term
282 // In both cases, rhs -= abs(term).
283 rhs_ -= std::min(coeff, AbsCoefficient(terms_[var]));
284 max_sum_ += AbsCoefficient(term_encoding + terms_[var]) -
285 AbsCoefficient(terms_[var]);
286 } else {
287 // Both terms are of the same sign (or terms_[var] is zero).
288 max_sum_ += coeff;
289 }
290 CHECK_GE(max_sum_, 0) << "Overflow";
291 terms_[var] += term_encoding;
292 non_zeros_.Set(var);
293 }
294
295 // Returns the "cancelation" amount of AddTerm(literal, coeff).
296 Coefficient CancelationAmount(Literal literal, Coefficient coeff) const {
297 DCHECK_GT(coeff, 0);
298 const BooleanVariable var = literal.Variable();
299 if (literal == GetLiteral(var)) return Coefficient(0);
300 return std::min(coeff, AbsCoefficient(terms_[var]));
301 }
302
303 // Returns a set of positions that contains all the non-zeros terms of the
304 // constraint. Note that this set can also contains some zero terms.
305 const std::vector<BooleanVariable>& PossibleNonZeros() const {
306 return non_zeros_.PositionsSetAtLeastOnce();
307 }
308
309 // Returns a string representation of the constraint.
310 std::string DebugString();
311
312 private:
313 Coefficient AbsCoefficient(Coefficient a) const { return a > 0 ? a : -a; }
314
315 // Only used for DCHECK_EQ(max_sum_, ComputeMaxSum());
316 Coefficient ComputeMaxSum() const;
317
318 // The encoding is special:
319 // - If terms_[x] > 0, then the associated term is 'terms_[x] . x'
320 // - If terms_[x] < 0, then the associated term is 'terms_[x] . (x - 1)'
322
323 // The right hand side of the constraint (sum terms <= rhs_).
324 Coefficient rhs_;
325
326 // The constraint maximum sum (i.e. sum of the absolute term coefficients).
327 // Note that checking the integer overflow on this sum is enough.
328 Coefficient max_sum_;
329
330 // Contains the possibly non-zeros terms_ value.
332};
333
334// A simple "helper" class to enqueue a propagated literal on the trail and
335// keep the information needed to explain it when requested.
336class UpperBoundedLinearConstraint;
337
339 void Enqueue(Literal l, int source_trail_index,
341 reasons[trail->Index()] = {source_trail_index, ct};
342 trail->Enqueue(l, propagator_id);
343 }
344
345 // The propagator id of PbConstraints.
347
348 // A temporary vector to store the last conflict.
349 std::vector<Literal> conflict;
350
351 // Information needed to recover the reason of an Enqueue().
352 // Indexed by trail_index.
353 struct ReasonInfo {
356 };
357 std::vector<ReasonInfo> reasons;
358};
359
360// This class contains half the propagation logic for a constraint of the form
361//
362// sum ci * li <= rhs, ci positive coefficients, li literals.
363//
364// The other half is implemented by the PbConstraints class below which takes
365// care of updating the 'threshold' value of this constraint:
366// - 'slack' is rhs minus all the ci of the variables xi assigned to
367// true. Note that it is not updated as soon as xi is assigned, but only
368// later when this assignment is "processed" by the PbConstraints class.
369// - 'threshold' is the distance from 'slack' to the largest coefficient ci
370// smaller or equal to slack. By definition, all the literals with
371// even larger coefficients that are yet 'processed' must be false for the
372// constraint to be satisfiable.
374 public:
375 // Takes a pseudo-Boolean formula in canonical form.
377 const std::vector<LiteralWithCoeff>& cst);
378
379 // Returns true if the given terms are the same as the one in this constraint.
380 bool HasIdenticalTerms(const std::vector<LiteralWithCoeff>& cst);
381 Coefficient Rhs() const { return rhs_; }
382
383 // Sets the rhs of this constraint. Compute the initial threshold value using
384 // only the literal with a trail index smaller than the given one. Enqueues on
385 // the trail any propagated literals.
386 //
387 // Returns false if the preconditions described in
388 // PbConstraints::AddConstraint() are not meet.
389 bool InitializeRhs(Coefficient rhs, int trail_index, Coefficient* threshold,
390 Trail* trail, PbConstraintsEnqueueHelper* helper);
391
392 // Tests for propagation and enqueues propagated literals on the trail.
393 // Returns false if a conflict was detected, in which case conflict is filled.
394 //
395 // Preconditions:
396 // - For each "processed" literal, the given threshold value must have been
397 // decreased by its associated coefficient in the constraint. It must now
398 // be stricly negative.
399 // - The given trail_index is the index of a true literal in the trail which
400 // just caused threshold to become stricly negative. All literals with
401 // smaller index must have been "processed". All assigned literals with
402 // greater trail index are not yet "processed".
403 //
404 // The threshold is updated to its new value.
405 bool Propagate(int trail_index, Coefficient* threshold, Trail* trail,
407
408 // Updates the given threshold and the internal state. This is the opposite of
409 // Propagate(). Each time a literal in unassigned, the threshold value must
410 // have been increased by its coefficient. This update the threshold to its
411 // new value.
412 void Untrail(Coefficient* threshold, int trail_index);
413
414 // Provided that the literal with given source_trail_index was the one that
415 // propagated the conflict or the literal we wants to explain, then this will
416 // compute the reason.
417 //
418 // Some properties of the reason:
419 // - Literals of level 0 are removed.
420 // - It will always contain the literal with given source_trail_index (except
421 // if it is of level 0).
422 // - We make the reason more compact by greedily removing terms with small
423 // coefficients that would not have changed the propagation.
424 //
425 // TODO(user): Maybe it is possible to derive a better reason by using more
426 // information. For instance one could use the mask of literals that are
427 // better to use during conflict minimization (namely the one already in the
428 // 1-UIP conflict).
429 void FillReason(const Trail& trail, int source_trail_index,
430 BooleanVariable propagated_variable,
431 std::vector<Literal>* reason);
432
433 // Same operation as SatSolver::ResolvePBConflict(), the only difference is
434 // that here the reason for var is *this.
435 void ResolvePBConflict(const Trail& trail, BooleanVariable var,
437 Coefficient* conflict_slack);
438
439 // Adds this pb constraint into the given mutable one.
440 //
441 // TODO(user): Provides instead an easy to use iterator over an
442 // UpperBoundedLinearConstraint and move this function to
443 // MutableUpperBoundedLinearConstraint.
445
446 // Compute the sum of the "cancelation" in AddTerm() if *this is added to
447 // the given conflict. The sum doesn't take into account literal assigned with
448 // a trail index smaller than the given one.
449 //
450 // Note(user): Currently, this is only used in DCHECKs.
451 Coefficient ComputeCancelation(
452 const Trail& trail, int trail_index,
454
455 // API to mark a constraint for deletion before actually deleting it.
456 void MarkForDeletion() { is_marked_for_deletion_ = true; }
457 bool is_marked_for_deletion() const { return is_marked_for_deletion_; }
458
459 // Only learned constraints are considered for deletion during the constraint
460 // cleanup phase. We also can't delete variables used as a reason.
461 void set_is_learned(bool is_learned) { is_learned_ = is_learned; }
462 bool is_learned() const { return is_learned_; }
463 bool is_used_as_a_reason() const { return first_reason_trail_index_ != -1; }
464
465 // Activity of the constraint. Only low activity constraint will be deleted
466 // during the constraint cleanup phase.
467 void set_activity(double activity) { activity_ = activity; }
468 double activity() const { return activity_; }
469
470 // Returns a fingerprint of the constraint linear expression (without rhs).
471 // This is used for duplicate detection.
472 int64 hash() const { return hash_; }
473
474 // This is used to get statistics of the number of literals inspected by
475 // a Propagate() call.
476 int already_propagated_end() const { return already_propagated_end_; }
477
478 private:
479 Coefficient GetSlackFromThreshold(Coefficient threshold) {
480 return (index_ < 0) ? threshold : coeffs_[index_] + threshold;
481 }
482 void Update(Coefficient slack, Coefficient* threshold) {
483 *threshold = (index_ < 0) ? slack : slack - coeffs_[index_];
484 already_propagated_end_ = starts_[index_ + 1];
485 }
486
487 // Constraint management fields.
488 // TODO(user): Rearrange and specify bit size to minimize memory usage.
489 bool is_marked_for_deletion_;
490 bool is_learned_;
491 int first_reason_trail_index_;
492 double activity_;
493
494 // Constraint propagation fields.
495 int index_;
496 int already_propagated_end_;
497
498 // In the internal representation, we merge the terms with the same
499 // coefficient.
500 // - literals_ contains all the literal of the constraint sorted by
501 // increasing coefficients.
502 // - coeffs_ contains unique increasing coefficients.
503 // - starts_[i] is the index in literals_ of the first literal with
504 // coefficient coeffs_[i].
505 std::vector<Coefficient> coeffs_;
506 std::vector<int> starts_;
507 std::vector<Literal> literals_;
508 Coefficient rhs_;
509
510 int64 hash_;
511};
512
513// Class responsible for managing a set of pseudo-Boolean constraints and their
514// propagation.
516 public:
518 : SatPropagator("PbConstraints"),
519 conflicting_constraint_index_(-1),
520 num_learned_constraint_before_cleanup_(0),
521 constraint_activity_increment_(1.0),
522 parameters_(model->GetOrCreate<SatParameters>()),
523 stats_("PbConstraints"),
524 num_constraint_lookups_(0),
525 num_inspected_constraint_literals_(0),
526 num_threshold_updates_(0) {
527 model->GetOrCreate<Trail>()->RegisterPropagator(this);
528 }
529 ~PbConstraints() override {
531 LOG(INFO) << stats_.StatString();
532 LOG(INFO) << "num_constraint_lookups_: " << num_constraint_lookups_;
533 LOG(INFO) << "num_threshold_updates_: " << num_threshold_updates_;
534 });
535 }
536
537 bool Propagate(Trail* trail) final;
538 void Untrail(const Trail& trail, int trail_index) final;
539 absl::Span<const Literal> Reason(const Trail& trail,
540 int trail_index) const final;
541
542 // Changes the number of variables.
543 void Resize(int num_variables) {
544 // Note that we avoid using up memory in the common case where there are no
545 // pb constraints at all. If there is 10 million variables, this vector
546 // alone will take 480 MB!
547 if (!constraints_.empty()) {
548 to_update_.resize(num_variables << 1);
549 enqueue_helper_.reasons.resize(num_variables);
550 }
551 }
552
553 // Adds a constraint in canonical form to the set of managed constraints. Note
554 // that this detects constraints with exactly the same terms. In this case,
555 // the constraint rhs is updated if the new one is lower or nothing is done
556 // otherwise.
557 //
558 // There are some preconditions, and the function will return false if they
559 // are not met. The constraint can be added when the trail is not empty,
560 // however given the current propagated assignment:
561 // - The constraint cannot be conflicting.
562 // - The constraint cannot have propagated at an earlier decision level.
563 bool AddConstraint(const std::vector<LiteralWithCoeff>& cst, Coefficient rhs,
564 Trail* trail);
565
566 // Same as AddConstraint(), but also marks the added constraint as learned
567 // so that it can be deleted during the constraint cleanup phase.
568 bool AddLearnedConstraint(const std::vector<LiteralWithCoeff>& cst,
569 Coefficient rhs, Trail* trail);
570
571 // Returns the number of constraints managed by this class.
572 int NumberOfConstraints() const { return constraints_.size(); }
573
574 // ConflictingConstraint() returns the last PB constraint that caused a
575 // conflict. Calling ClearConflictingConstraint() reset this to nullptr.
576 //
577 // TODO(user): This is a hack to get the PB conflict, because the rest of
578 // the solver API assume only clause conflict. Find a cleaner way?
579 void ClearConflictingConstraint() { conflicting_constraint_index_ = -1; }
581 if (conflicting_constraint_index_ == -1) return nullptr;
582 return constraints_[conflicting_constraint_index_.value()].get();
583 }
584
585 // Returns the underlying UpperBoundedLinearConstraint responsible for
586 // assigning the literal at given trail index.
587 UpperBoundedLinearConstraint* ReasonPbConstraint(int trail_index) const;
588
589 // Activity update functions.
590 // TODO(user): Remove duplication with other activity update functions.
592 void RescaleActivities(double scaling_factor);
594
595 // Only used for testing.
597 constraints_[index]->MarkForDeletion();
598 DeleteConstraintMarkedForDeletion();
599 }
600
601 // Some statistics.
602 int64 num_constraint_lookups() const { return num_constraint_lookups_; }
604 return num_inspected_constraint_literals_;
605 }
606 int64 num_threshold_updates() const { return num_threshold_updates_; }
607
608 private:
609 bool PropagateNext(Trail* trail);
610
611 // Same function as the clause related one is SatSolver().
612 // TODO(user): Remove duplication.
613 void ComputeNewLearnedConstraintLimit();
614 void DeleteSomeLearnedConstraintIfNeeded();
615
616 // Deletes all the UpperBoundedLinearConstraint for which
617 // is_marked_for_deletion() is true. This is relatively slow in O(number of
618 // terms in all constraints).
619 void DeleteConstraintMarkedForDeletion();
620
621 // Each constraint managed by this class is associated with an index.
622 // The set of indices is always [0, num_constraints_).
623 //
624 // Note(user): this complicate things during deletion, but the propagation is
625 // about two times faster with this implementation than one with direct
626 // pointer to an UpperBoundedLinearConstraint. The main reason for this is
627 // probably that the thresholds_ vector is a lot more efficient cache-wise.
628 DEFINE_INT_TYPE(ConstraintIndex, int32);
629 struct ConstraintIndexWithCoeff {
630 ConstraintIndexWithCoeff() {} // Needed for vector.resize()
631 ConstraintIndexWithCoeff(bool n, ConstraintIndex i, Coefficient c)
632 : need_untrail_inspection(n), index(i), coefficient(c) {}
633 bool need_untrail_inspection;
634 ConstraintIndex index;
635 Coefficient coefficient;
636 };
637
638 // The set of all pseudo-boolean constraint managed by this class.
639 std::vector<std::unique_ptr<UpperBoundedLinearConstraint>> constraints_;
640
641 // The current value of the threshold for each constraints.
643
644 // For each literal, the list of all the constraints that contains it together
645 // with the literal coefficient in these constraints.
647 to_update_;
648
649 // Bitset used to optimize the Untrail() function.
650 SparseBitset<ConstraintIndex> to_untrail_;
651
652 // Pointers to the constraints grouped by their hash.
653 // This is used to find duplicate constraints by AddConstraint().
654 absl::flat_hash_map<int64, std::vector<UpperBoundedLinearConstraint*>>
655 possible_duplicates_;
656
657 // Helper to enqueue propagated literals on the trail and store their reasons.
658 PbConstraintsEnqueueHelper enqueue_helper_;
659
660 // Last conflicting PB constraint index. This is reset to -1 when
661 // ClearConflictingConstraint() is called.
662 ConstraintIndex conflicting_constraint_index_;
663
664 // Used for the constraint cleaning policy.
665 int target_number_of_learned_constraint_;
666 int num_learned_constraint_before_cleanup_;
667 double constraint_activity_increment_;
668
669 // Algorithm parameters.
670 SatParameters* parameters_;
671
672 // Some statistics.
673 mutable StatsGroup stats_;
674 int64 num_constraint_lookups_;
675 int64 num_inspected_constraint_literals_;
676 int64 num_threshold_updates_;
677 DISALLOW_COPY_AND_ASSIGN(PbConstraints);
678};
679
680// Boolean linear constraints can propagate a lot of literals at the same time.
681// As a result, all these literals will have exactly the same reason. It is
682// important to take advantage of that during the conflict
683// computation/minimization. On some problem, this can have a huge impact.
684//
685// TODO(user): With the new SAME_REASON_AS mechanism, this is more general so
686// move out of pb_constraint.
688 public:
690 : trail_(trail) {}
691
692 void Resize(int num_variables) {
693 first_variable_.resize(num_variables);
694 seen_.ClearAndResize(BooleanVariable(num_variables));
695 }
696
697 // Clears the cache. Call this before each conflict analysis.
698 void Clear() { seen_.ClearAll(); }
699
700 // Returns the first variable with exactly the same reason as 'var' on which
701 // this function was called since the last Clear(). Note that if no variable
702 // had the same reason, then var is returned.
703 BooleanVariable FirstVariableWithSameReason(BooleanVariable var) {
704 if (seen_[var]) return first_variable_[var];
705 const BooleanVariable reference_var =
707 if (reference_var == var) return var;
708 if (seen_[reference_var]) return first_variable_[reference_var];
709 seen_.Set(reference_var);
710 first_variable_[reference_var] = var;
711 return var;
712 }
713
714 private:
715 const Trail& trail_;
718
719 DISALLOW_COPY_AND_ASSIGN(VariableWithSameReasonIdentifier);
720};
721
722} // namespace sat
723} // namespace operations_research
724
725#endif // OR_TOOLS_SAT_PB_CONSTRAINT_H_
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define LOG(severity)
Definition: base/logging.h:420
void resize(size_type new_size)
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
std::string StatString() const
Definition: stats.cc:71
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
const std::vector< LiteralWithCoeff > & Constraint(int i) const
LiteralIndex Index() const
Definition: sat_base.h:84
std::string DebugString() const
Definition: sat_base.h:93
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
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 * ConflictingConstraint()
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)
void Enqueue(Literal true_literal, int propagator_id)
Definition: sat_base.h:250
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const
Definition: sat_base.h:560
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)
BooleanVariable FirstVariableWithSameReason(BooleanVariable var)
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
int64_t int64
const int INFO
Definition: log_severity.h:31
Coefficient ComputeCanonicalRhs(Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
Definition: cp_model.cc:65
DEFINE_INT_TYPE(ClauseIndex, int)
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)
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
bool BooleanLinearExpressionIsCanonical(const std::vector< LiteralWithCoeff > &cst)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 bound
int64 coefficient
#define IF_STATS_ENABLED(instructions)
Definition: stats.h:437
bool operator==(const LiteralWithCoeff &other) const
Definition: pb_constraint.h:55
LiteralWithCoeff(Literal l, Coefficient c)
Definition: pb_constraint.h:51
void Enqueue(Literal l, int source_trail_index, UpperBoundedLinearConstraint *ct, Trail *trail)