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