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 
23 namespace operations_research {
24 namespace sat {
25 
26 namespace {
27 
28 bool LiteralComparator(const LiteralWithCoeff& a, const LiteralWithCoeff& b) {
29  return a.literal.Index() < b.literal.Index();
30 }
31 
32 bool 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 
160 Coefficient 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 
178 Coefficient 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 
228 bool 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 
382 Coefficient 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,
461  PbConstraintsEnqueueHelper* helper) {
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,
535  PbConstraintsEnqueueHelper* helper) {
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 
812 void 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.
824 bool 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());
835  propagation_trail_index_ = trail->Index();
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 
899 bool 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) {
914  UpperBoundedLinearConstraint* const cst =
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 
943 void 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 
966 absl::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.
987 void 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 
997 void 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 
1077 void 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 
1089 void 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)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:813
void Set(IntegerType index)
Definition: bitset.h:803
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
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)
const std::vector< BooleanVariable > & PossibleNonZeros() const
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)
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
Definition: sat_base.h:272
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
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)
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)
const LiteralIndex kTrueLiteralIndex(-2)
bool ComputeBooleanLinearExpressionCanonicalForm(std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
const LiteralIndex kFalseLiteralIndex(-3)
bool BooleanLinearExpressionIsCanonical(const std::vector< LiteralWithCoeff > &cst)
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)