OR-Tools  8.1
integer_expr.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 <algorithm>
17 #include <memory>
18 #include <vector>
19 
20 #include "absl/container/flat_hash_map.h"
21 #include "absl/memory/memory.h"
22 #include "ortools/base/stl_util.h"
23 #include "ortools/sat/integer.h"
26 
27 namespace operations_research {
28 namespace sat {
29 
30 IntegerSumLE::IntegerSumLE(const std::vector<Literal>& enforcement_literals,
31  const std::vector<IntegerVariable>& vars,
32  const std::vector<IntegerValue>& coeffs,
33  IntegerValue upper, Model* model)
34  : enforcement_literals_(enforcement_literals),
35  upper_bound_(upper),
36  trail_(model->GetOrCreate<Trail>()),
37  integer_trail_(model->GetOrCreate<IntegerTrail>()),
38  time_limit_(model->GetOrCreate<TimeLimit>()),
39  rev_integer_value_repository_(
40  model->GetOrCreate<RevIntegerValueRepository>()),
41  vars_(vars),
42  coeffs_(coeffs) {
43  // TODO(user): deal with this corner case.
44  CHECK(!vars_.empty());
45  max_variations_.resize(vars_.size());
46 
47  // Handle negative coefficients.
48  for (int i = 0; i < vars.size(); ++i) {
49  if (coeffs_[i] < 0) {
50  vars_[i] = NegationOf(vars_[i]);
51  coeffs_[i] = -coeffs_[i];
52  }
53  }
54 
55  // Literal reason will only be used with the negation of enforcement_literals.
56  for (const Literal literal : enforcement_literals) {
57  literal_reason_.push_back(literal.Negated());
58  }
59 
60  // Initialize the reversible numbers.
61  rev_num_fixed_vars_ = 0;
62  rev_lb_fixed_vars_ = IntegerValue(0);
63 }
64 
65 void IntegerSumLE::FillIntegerReason() {
66  integer_reason_.clear();
67  reason_coeffs_.clear();
68  const int num_vars = vars_.size();
69  for (int i = 0; i < num_vars; ++i) {
70  const IntegerVariable var = vars_[i];
71  if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
72  integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
73  reason_coeffs_.push_back(coeffs_[i]);
74  }
75  }
76 }
77 
79  // Reified case: If any of the enforcement_literals are false, we ignore the
80  // constraint.
81  int num_unassigned_enforcement_literal = 0;
82  LiteralIndex unique_unnasigned_literal = kNoLiteralIndex;
83  for (const Literal literal : enforcement_literals_) {
84  if (trail_->Assignment().LiteralIsFalse(literal)) return true;
85  if (!trail_->Assignment().LiteralIsTrue(literal)) {
86  ++num_unassigned_enforcement_literal;
87  unique_unnasigned_literal = literal.Index();
88  }
89  }
90 
91  // Unfortunately, we can't propagate anything if we have more than one
92  // unassigned enforcement literal.
93  if (num_unassigned_enforcement_literal > 1) return true;
94 
95  // Save the current sum of fixed variables.
96  if (is_registered_) {
97  rev_integer_value_repository_->SaveState(&rev_lb_fixed_vars_);
98  } else {
99  rev_num_fixed_vars_ = 0;
100  rev_lb_fixed_vars_ = 0;
101  }
102 
103  // Compute the new lower bound and update the reversible structures.
104  IntegerValue lb_unfixed_vars = IntegerValue(0);
105  const int num_vars = vars_.size();
106  for (int i = rev_num_fixed_vars_; i < num_vars; ++i) {
107  const IntegerVariable var = vars_[i];
108  const IntegerValue coeff = coeffs_[i];
109  const IntegerValue lb = integer_trail_->LowerBound(var);
110  const IntegerValue ub = integer_trail_->UpperBound(var);
111  if (lb != ub) {
112  max_variations_[i] = (ub - lb) * coeff;
113  lb_unfixed_vars += lb * coeff;
114  } else {
115  // Update the set of fixed variables.
116  std::swap(vars_[i], vars_[rev_num_fixed_vars_]);
117  std::swap(coeffs_[i], coeffs_[rev_num_fixed_vars_]);
118  std::swap(max_variations_[i], max_variations_[rev_num_fixed_vars_]);
119  rev_num_fixed_vars_++;
120  rev_lb_fixed_vars_ += lb * coeff;
121  }
122  }
123  time_limit_->AdvanceDeterministicTime(
124  static_cast<double>(num_vars - rev_num_fixed_vars_) * 1e-9);
125 
126  // Conflict?
127  const IntegerValue slack =
128  upper_bound_ - (rev_lb_fixed_vars_ + lb_unfixed_vars);
129  if (slack < 0) {
130  FillIntegerReason();
131  integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs_,
132  &integer_reason_);
133 
134  if (num_unassigned_enforcement_literal == 1) {
135  // Propagate the only non-true literal to false.
136  const Literal to_propagate = Literal(unique_unnasigned_literal).Negated();
137  std::vector<Literal> tmp = literal_reason_;
138  tmp.erase(std::find(tmp.begin(), tmp.end(), to_propagate));
139  integer_trail_->EnqueueLiteral(to_propagate, tmp, integer_reason_);
140  return true;
141  }
142  return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
143  }
144 
145  // We can only propagate more if all the enforcement literals are true.
146  if (num_unassigned_enforcement_literal > 0) return true;
147 
148  // The lower bound of all the variables except one can be used to update the
149  // upper bound of the last one.
150  for (int i = rev_num_fixed_vars_; i < num_vars; ++i) {
151  if (max_variations_[i] <= slack) continue;
152 
153  const IntegerVariable var = vars_[i];
154  const IntegerValue coeff = coeffs_[i];
155  const IntegerValue div = slack / coeff;
156  const IntegerValue new_ub = integer_trail_->LowerBound(var) + div;
157  const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
158  if (!integer_trail_->Enqueue(
160  /*lazy_reason=*/[this, propagation_slack](
161  IntegerLiteral i_lit, int trail_index,
162  std::vector<Literal>* literal_reason,
163  std::vector<int>* trail_indices_reason) {
164  *literal_reason = literal_reason_;
165  trail_indices_reason->clear();
166  reason_coeffs_.clear();
167  const int size = vars_.size();
168  for (int i = 0; i < size; ++i) {
169  const IntegerVariable var = vars_[i];
170  if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
171  continue;
172  }
173  const int index =
174  integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
175  if (index >= 0) {
176  trail_indices_reason->push_back(index);
177  if (propagation_slack > 0) {
178  reason_coeffs_.push_back(coeffs_[i]);
179  }
180  }
181  }
182  if (propagation_slack > 0) {
183  integer_trail_->RelaxLinearReason(
184  propagation_slack, reason_coeffs_, trail_indices_reason);
185  }
186  })) {
187  return false;
188  }
189  }
190 
191  return true;
192 }
193 
194 bool IntegerSumLE::PropagateAtLevelZero() {
195  // TODO(user): Deal with enforcements. It is just a bit of code to read the
196  // value of the literals at level zero.
197  if (!enforcement_literals_.empty()) return true;
198 
199  // Compute the new lower bound and update the reversible structures.
200  IntegerValue min_activity = IntegerValue(0);
201  const int num_vars = vars_.size();
202  for (int i = 0; i < num_vars; ++i) {
203  const IntegerVariable var = vars_[i];
204  const IntegerValue coeff = coeffs_[i];
205  const IntegerValue lb = integer_trail_->LevelZeroLowerBound(var);
206  const IntegerValue ub = integer_trail_->LevelZeroUpperBound(var);
207  max_variations_[i] = (ub - lb) * coeff;
208  min_activity += lb * coeff;
209  }
210  time_limit_->AdvanceDeterministicTime(static_cast<double>(num_vars * 1e-9));
211 
212  // Conflict?
213  const IntegerValue slack = upper_bound_ - min_activity;
214  if (slack < 0) {
215  return integer_trail_->ReportConflict({}, {});
216  }
217 
218  // The lower bound of all the variables except one can be used to update the
219  // upper bound of the last one.
220  for (int i = 0; i < num_vars; ++i) {
221  if (max_variations_[i] <= slack) continue;
222 
223  const IntegerVariable var = vars_[i];
224  const IntegerValue coeff = coeffs_[i];
225  const IntegerValue div = slack / coeff;
226  const IntegerValue new_ub = integer_trail_->LevelZeroLowerBound(var) + div;
227  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(var, new_ub), {},
228  {})) {
229  return false;
230  }
231  }
232 
233  return true;
234 }
235 
236 void IntegerSumLE::RegisterWith(GenericLiteralWatcher* watcher) {
237  is_registered_ = true;
238  const int id = watcher->Register(this);
239  for (const IntegerVariable& var : vars_) {
240  watcher->WatchLowerBound(var, id);
241  }
242  for (const Literal literal : enforcement_literals_) {
243  // We only watch the true direction.
244  //
245  // TODO(user): if there is more than one, maybe we should watch more to
246  // propagate a "conflict" as soon as only one is unassigned?
247  watcher->WatchLiteral(Literal(literal), id);
248  }
249  watcher->RegisterReversibleInt(id, &rev_num_fixed_vars_);
250 }
251 
252 LevelZeroEquality::LevelZeroEquality(IntegerVariable target,
253  const std::vector<IntegerVariable>& vars,
254  const std::vector<IntegerValue>& coeffs,
255  Model* model)
256  : target_(target),
257  vars_(vars),
258  coeffs_(coeffs),
259  trail_(model->GetOrCreate<Trail>()),
260  integer_trail_(model->GetOrCreate<IntegerTrail>()) {
261  auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
262  const int id = watcher->Register(this);
263  watcher->SetPropagatorPriority(id, 2);
264  watcher->WatchIntegerVariable(target, id);
265  for (const IntegerVariable& var : vars_) {
266  watcher->WatchIntegerVariable(var, id);
267  }
268 }
269 
270 // TODO(user): We could go even further than just the GCD, and do more
271 // arithmetic to tighten the target bounds. See for instance a problem like
272 // ej.mps.gz that we don't solve easily, but has just 3 variables! the goal is
273 // to minimize X, given 31013 X - 41014 Y - 51015 Z = -31013 (all >=0, Y and Z
274 // bounded with high values). I know some MIP solvers have a basic linear
275 // diophantine equation support.
277  // TODO(user): Once the GCD is not 1, we could at any level make sure the
278  // objective is of the correct form. For now, this only happen in a few
279  // miplib problem that we close quickly, so I didn't add the extra code yet.
280  if (trail_->CurrentDecisionLevel() != 0) return true;
281 
282  int64 gcd = 0;
283  IntegerValue sum(0);
284  for (int i = 0; i < vars_.size(); ++i) {
285  if (integer_trail_->IsFixed(vars_[i])) {
286  sum += coeffs_[i] * integer_trail_->LowerBound(vars_[i]);
287  continue;
288  }
289  gcd = MathUtil::GCD64(gcd, std::abs(coeffs_[i].value()));
290  if (gcd == 1) break;
291  }
292  if (gcd == 0) return true; // All fixed.
293 
294  if (gcd > gcd_) {
295  VLOG(1) << "Objective gcd: " << gcd;
296  }
297  CHECK_GE(gcd, gcd_);
298  gcd_ = IntegerValue(gcd);
299 
300  const IntegerValue lb = integer_trail_->LowerBound(target_);
301  const IntegerValue lb_remainder = PositiveRemainder(lb - sum, gcd_);
302  if (lb_remainder != 0) {
303  if (!integer_trail_->Enqueue(
304  IntegerLiteral::GreaterOrEqual(target_, lb + gcd_ - lb_remainder),
305  {}, {}))
306  return false;
307  }
308 
309  const IntegerValue ub = integer_trail_->UpperBound(target_);
310  const IntegerValue ub_remainder =
311  PositiveRemainder(ub - sum, IntegerValue(gcd));
312  if (ub_remainder != 0) {
313  if (!integer_trail_->Enqueue(
314  IntegerLiteral::LowerOrEqual(target_, ub - ub_remainder), {}, {}))
315  return false;
316  }
317 
318  return true;
319 }
320 
321 MinPropagator::MinPropagator(const std::vector<IntegerVariable>& vars,
322  IntegerVariable min_var,
323  IntegerTrail* integer_trail)
324  : vars_(vars), min_var_(min_var), integer_trail_(integer_trail) {}
325 
327  if (vars_.empty()) return true;
328 
329  // Count the number of interval that are possible candidate for the min.
330  // Only the intervals for which lb > current_min_ub cannot.
331  const IntegerLiteral min_ub_literal =
332  integer_trail_->UpperBoundAsLiteral(min_var_);
333  const IntegerValue current_min_ub = integer_trail_->UpperBound(min_var_);
334  int num_intervals_that_can_be_min = 0;
335  int last_possible_min_interval = 0;
336 
337  IntegerValue min = kMaxIntegerValue;
338  for (int i = 0; i < vars_.size(); ++i) {
339  const IntegerValue lb = integer_trail_->LowerBound(vars_[i]);
340  min = std::min(min, lb);
341  if (lb <= current_min_ub) {
342  ++num_intervals_that_can_be_min;
343  last_possible_min_interval = i;
344  }
345  }
346 
347  // Propagation a)
348  if (min > integer_trail_->LowerBound(min_var_)) {
349  integer_reason_.clear();
350  for (const IntegerVariable var : vars_) {
351  integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(var, min));
352  }
353  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(min_var_, min),
354  {}, integer_reason_)) {
355  return false;
356  }
357  }
358 
359  // Propagation b)
360  if (num_intervals_that_can_be_min == 1) {
361  const IntegerValue ub_of_only_candidate =
362  integer_trail_->UpperBound(vars_[last_possible_min_interval]);
363  if (current_min_ub < ub_of_only_candidate) {
364  integer_reason_.clear();
365 
366  // The reason is that all the other interval start after current_min_ub.
367  // And that min_ub has its current value.
368  integer_reason_.push_back(min_ub_literal);
369  for (const IntegerVariable var : vars_) {
370  if (var == vars_[last_possible_min_interval]) continue;
371  integer_reason_.push_back(
372  IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
373  }
374  if (!integer_trail_->Enqueue(
375  IntegerLiteral::LowerOrEqual(vars_[last_possible_min_interval],
376  current_min_ub),
377  {}, integer_reason_)) {
378  return false;
379  }
380  }
381  }
382 
383  // Conflict.
384  //
385  // TODO(user): Not sure this code is useful since this will be detected
386  // by the fact that the [lb, ub] of the min is empty. It depends on the
387  // propagation order though, but probably the precedences propagator would
388  // propagate before this one. So change this to a CHECK?
389  if (num_intervals_that_can_be_min == 0) {
390  integer_reason_.clear();
391 
392  // Almost the same as propagation b).
393  integer_reason_.push_back(min_ub_literal);
394  for (const IntegerVariable var : vars_) {
395  integer_reason_.push_back(
396  IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
397  }
398  return integer_trail_->ReportConflict(integer_reason_);
399  }
400 
401  return true;
402 }
403 
405  const int id = watcher->Register(this);
406  for (const IntegerVariable& var : vars_) {
407  watcher->WatchLowerBound(var, id);
408  }
409  watcher->WatchUpperBound(min_var_, id);
410 }
411 
412 LinMinPropagator::LinMinPropagator(const std::vector<LinearExpression>& exprs,
413  IntegerVariable min_var, Model* model)
414  : exprs_(exprs),
415  min_var_(min_var),
416  model_(model),
417  integer_trail_(model_->GetOrCreate<IntegerTrail>()) {}
418 
419 bool LinMinPropagator::PropagateLinearUpperBound(
420  const std::vector<IntegerVariable>& vars,
421  const std::vector<IntegerValue>& coeffs, const IntegerValue upper_bound) {
422  IntegerValue sum_lb = IntegerValue(0);
423  const int num_vars = vars.size();
424  std::vector<IntegerValue> max_variations;
425  for (int i = 0; i < num_vars; ++i) {
426  const IntegerVariable var = vars[i];
427  const IntegerValue coeff = coeffs[i];
428  // The coefficients are assumed to be positive for this to work properly.
429  DCHECK_GE(coeff, 0);
430  const IntegerValue lb = integer_trail_->LowerBound(var);
431  const IntegerValue ub = integer_trail_->UpperBound(var);
432  max_variations.push_back((ub - lb) * coeff);
433  sum_lb += lb * coeff;
434  }
435 
436  model_->GetOrCreate<TimeLimit>()->AdvanceDeterministicTime(
437  static_cast<double>(num_vars) * 1e-9);
438 
439  const IntegerValue slack = upper_bound - sum_lb;
440 
441  std::vector<IntegerLiteral> linear_sum_reason;
442  std::vector<IntegerValue> reason_coeffs;
443  for (int i = 0; i < num_vars; ++i) {
444  const IntegerVariable var = vars[i];
445  if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
446  linear_sum_reason.push_back(integer_trail_->LowerBoundAsLiteral(var));
447  reason_coeffs.push_back(coeffs[i]);
448  }
449  }
450  if (slack < 0) {
451  // Conflict.
452  integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs,
453  &linear_sum_reason);
454  std::vector<IntegerLiteral> local_reason =
455  integer_reason_for_unique_candidate_;
456  local_reason.insert(local_reason.end(), linear_sum_reason.begin(),
457  linear_sum_reason.end());
458  return integer_trail_->ReportConflict({}, local_reason);
459  }
460 
461  // The lower bound of all the variables except one can be used to update the
462  // upper bound of the last one.
463  for (int i = 0; i < num_vars; ++i) {
464  if (max_variations[i] <= slack) continue;
465 
466  const IntegerVariable var = vars[i];
467  const IntegerValue coeff = coeffs[i];
468  const IntegerValue div = slack / coeff;
469  const IntegerValue new_ub = integer_trail_->LowerBound(var) + div;
470 
471  const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
472  if (!integer_trail_->Enqueue(
474  /*lazy_reason=*/[this, &vars, &coeffs, propagation_slack](
475  IntegerLiteral i_lit, int trail_index,
476  std::vector<Literal>* literal_reason,
477  std::vector<int>* trail_indices_reason) {
478  literal_reason->clear();
479  trail_indices_reason->clear();
480  std::vector<IntegerValue> reason_coeffs;
481  const int size = vars.size();
482  for (int i = 0; i < size; ++i) {
483  const IntegerVariable var = vars[i];
484  if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
485  continue;
486  }
487  const int index =
488  integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
489  if (index >= 0) {
490  trail_indices_reason->push_back(index);
491  if (propagation_slack > 0) {
492  reason_coeffs.push_back(coeffs[i]);
493  }
494  }
495  }
496  if (propagation_slack > 0) {
497  integer_trail_->RelaxLinearReason(
498  propagation_slack, reason_coeffs, trail_indices_reason);
499  }
500  // Now add the old integer_reason that triggered this propatation.
501  for (IntegerLiteral reason_lit :
502  integer_reason_for_unique_candidate_) {
503  const int index = integer_trail_->FindTrailIndexOfVarBefore(
504  reason_lit.var, trail_index);
505  if (index >= 0) {
506  trail_indices_reason->push_back(index);
507  }
508  }
509  })) {
510  return false;
511  }
512  }
513  return true;
514 }
515 
517  if (exprs_.empty()) return true;
518 
519  expr_lbs_.clear();
520 
521  // Count the number of interval that are possible candidate for the min.
522  // Only the intervals for which lb > current_min_ub cannot.
523  const IntegerLiteral min_ub_literal =
524  integer_trail_->UpperBoundAsLiteral(min_var_);
525  const IntegerValue current_min_ub = integer_trail_->UpperBound(min_var_);
526  int num_intervals_that_can_be_min = 0;
527  int last_possible_min_interval = 0;
528 
529  IntegerValue min_of_linear_expression_lb = kMaxIntegerValue;
530  for (int i = 0; i < exprs_.size(); ++i) {
531  const IntegerValue lb = LinExprLowerBound(exprs_[i], *integer_trail_);
532  expr_lbs_.push_back(lb);
533  min_of_linear_expression_lb = std::min(min_of_linear_expression_lb, lb);
534  if (lb <= current_min_ub) {
535  ++num_intervals_that_can_be_min;
536  last_possible_min_interval = i;
537  }
538  }
539 
540  // Propagation a) lb(min) >= lb(MIN(exprs)) = MIN(lb(exprs));
541 
542  // Conflict will be detected by the fact that the [lb, ub] of the min is
543  // empty. In case of conflict, we just need the reason for pushing UB + 1.
544  if (min_of_linear_expression_lb > current_min_ub) {
545  min_of_linear_expression_lb = current_min_ub + 1;
546  }
547 
548  // Early experiments seems to show that the code if faster without relaxing
549  // the linear reason. But that might change in the future.
550  const bool use_slack = false;
551  if (min_of_linear_expression_lb > integer_trail_->LowerBound(min_var_)) {
552  std::vector<IntegerLiteral> local_reason;
553  for (int i = 0; i < exprs_.size(); ++i) {
554  const IntegerValue slack = expr_lbs_[i] - min_of_linear_expression_lb;
555  integer_trail_->AppendRelaxedLinearReason(
556  (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
557  exprs_[i].vars, &local_reason);
558  }
559  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(
560  min_var_, min_of_linear_expression_lb),
561  {}, local_reason)) {
562  return false;
563  }
564  }
565 
566  // Propagation b) ub(min) >= ub(MIN(exprs)) and we can't propagate anything
567  // here unless there is just one possible expression 'e' that can be the min:
568  // for all u != e, lb(u) > ub(min);
569  // In this case, ub(min) >= ub(e).
570  if (num_intervals_that_can_be_min == 1) {
571  const IntegerValue ub_of_only_candidate =
572  LinExprUpperBound(exprs_[last_possible_min_interval], *integer_trail_);
573  if (current_min_ub < ub_of_only_candidate) {
574  // For this propagation, we only need to fill the integer reason once at
575  // the lowest level. At higher levels this reason still remains valid.
576  if (rev_unique_candidate_ == 0) {
577  integer_reason_for_unique_candidate_.clear();
578 
579  // The reason is that all the other interval start after current_min_ub.
580  // And that min_ub has its current value.
581  integer_reason_for_unique_candidate_.push_back(min_ub_literal);
582  for (int i = 0; i < exprs_.size(); ++i) {
583  if (i == last_possible_min_interval) continue;
584  const IntegerValue slack = expr_lbs_[i] - (current_min_ub + 1);
585  integer_trail_->AppendRelaxedLinearReason(
586  (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
587  exprs_[i].vars, &integer_reason_for_unique_candidate_);
588  }
589  rev_unique_candidate_ = 1;
590  }
591 
592  return PropagateLinearUpperBound(
593  exprs_[last_possible_min_interval].vars,
594  exprs_[last_possible_min_interval].coeffs,
595  current_min_ub - exprs_[last_possible_min_interval].offset);
596  }
597  }
598 
599  return true;
600 }
601 
603  const int id = watcher->Register(this);
604  for (const LinearExpression& expr : exprs_) {
605  for (int i = 0; i < expr.vars.size(); ++i) {
606  const IntegerVariable& var = expr.vars[i];
607  const IntegerValue coeff = expr.coeffs[i];
608  if (coeff > 0) {
609  watcher->WatchLowerBound(var, id);
610  } else {
611  watcher->WatchUpperBound(var, id);
612  }
613  }
614  }
615  watcher->WatchUpperBound(min_var_, id);
616  watcher->RegisterReversibleInt(id, &rev_unique_candidate_);
617 }
618 
620  IntegerVariable a, IntegerVariable b, IntegerVariable p,
621  IntegerTrail* integer_trail)
622  : a_(a), b_(b), p_(p), integer_trail_(integer_trail) {
623  // Note that we assume this is true at level zero, and so we never include
624  // that fact in the reasons we compute.
625  CHECK_GE(integer_trail_->LevelZeroLowerBound(a_), 0);
626  CHECK_GE(integer_trail_->LevelZeroLowerBound(b_), 0);
627 }
628 
629 // TODO(user): We can tighten the bounds on p by removing extreme value that
630 // do not contains divisor in the domains of a or b. There is an algo in O(
631 // smallest domain size between a or b).
633  const IntegerValue max_a = integer_trail_->UpperBound(a_);
634  const IntegerValue max_b = integer_trail_->UpperBound(b_);
635  const IntegerValue new_max(CapProd(max_a.value(), max_b.value()));
636  if (new_max < integer_trail_->UpperBound(p_)) {
637  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(p_, new_max), {},
638  {integer_trail_->UpperBoundAsLiteral(a_),
639  integer_trail_->UpperBoundAsLiteral(b_)})) {
640  return false;
641  }
642  }
643 
644  const IntegerValue min_a = integer_trail_->LowerBound(a_);
645  const IntegerValue min_b = integer_trail_->LowerBound(b_);
646  const IntegerValue new_min(CapProd(min_a.value(), min_b.value()));
647  if (new_min > integer_trail_->LowerBound(p_)) {
648  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(p_, new_min),
649  {},
650  {integer_trail_->LowerBoundAsLiteral(a_),
651  integer_trail_->LowerBoundAsLiteral(b_)})) {
652  return false;
653  }
654  }
655 
656  for (int i = 0; i < 2; ++i) {
657  const IntegerVariable a = i == 0 ? a_ : b_;
658  const IntegerVariable b = i == 0 ? b_ : a_;
659  const IntegerValue max_a = integer_trail_->UpperBound(a);
660  const IntegerValue min_b = integer_trail_->LowerBound(b);
661  const IntegerValue min_p = integer_trail_->LowerBound(p_);
662  const IntegerValue max_p = integer_trail_->UpperBound(p_);
663  const IntegerValue prod(CapProd(max_a.value(), min_b.value()));
664  if (prod > max_p) {
665  if (!integer_trail_->Enqueue(
666  IntegerLiteral::LowerOrEqual(a, FloorRatio(max_p, min_b)), {},
667  {integer_trail_->LowerBoundAsLiteral(b),
668  integer_trail_->UpperBoundAsLiteral(p_)})) {
669  return false;
670  }
671  } else if (prod < min_p) {
672  if (!integer_trail_->Enqueue(
673  IntegerLiteral::GreaterOrEqual(b, CeilRatio(min_p, max_a)), {},
674  {integer_trail_->UpperBoundAsLiteral(a),
675  integer_trail_->LowerBoundAsLiteral(p_)})) {
676  return false;
677  }
678  }
679  }
680 
681  return true;
682 }
683 
685  const int id = watcher->Register(this);
686  watcher->WatchIntegerVariable(a_, id);
687  watcher->WatchIntegerVariable(b_, id);
688  watcher->WatchIntegerVariable(p_, id);
690 }
691 
692 namespace {
693 
694 // TODO(user): Find better implementation?
695 IntegerValue FloorSquareRoot(IntegerValue a) {
696  IntegerValue result(static_cast<int64>(std::floor(std::sqrt(ToDouble(a)))));
697  while (result * result > a) --result;
698  while ((result + 1) * (result + 1) <= a) ++result;
699  return result;
700 }
701 
702 // TODO(user): Find better implementation?
703 IntegerValue CeilSquareRoot(IntegerValue a) {
704  IntegerValue result(static_cast<int64>(std::ceil(std::sqrt(ToDouble(a)))));
705  while (result * result < a) ++result;
706  while ((result - 1) * (result - 1) >= a) --result;
707  return result;
708 }
709 
710 } // namespace
711 
712 SquarePropagator::SquarePropagator(IntegerVariable x, IntegerVariable s,
713  IntegerTrail* integer_trail)
714  : x_(x), s_(s), integer_trail_(integer_trail) {
715  CHECK_GE(integer_trail->LevelZeroLowerBound(x), 0);
716 }
717 
718 // Propagation from x to s: s in [min_x * min_x, max_x * max_x].
719 // Propagation from s to x: x in [ceil(sqrt(min_s)), floor(sqrt(max_s))].
721  const IntegerValue min_x = integer_trail_->LowerBound(x_);
722  const IntegerValue min_s = integer_trail_->LowerBound(s_);
723  const IntegerValue min_x_square(CapProd(min_x.value(), min_x.value()));
724  if (min_x_square > min_s) {
725  if (!integer_trail_->Enqueue(
726  IntegerLiteral::GreaterOrEqual(s_, min_x_square), {},
727  {IntegerLiteral::GreaterOrEqual(x_, min_x)})) {
728  return false;
729  }
730  } else if (min_x_square < min_s) {
731  const IntegerValue new_min = CeilSquareRoot(min_s);
732  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(x_, new_min),
733  {},
734  {IntegerLiteral::GreaterOrEqual(
735  s_, (new_min - 1) * (new_min - 1) + 1)})) {
736  return false;
737  }
738  }
739 
740  const IntegerValue max_x = integer_trail_->UpperBound(x_);
741  const IntegerValue max_s = integer_trail_->UpperBound(s_);
742  const IntegerValue max_x_square(CapProd(max_x.value(), max_x.value()));
743  if (max_x_square < max_s) {
744  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(s_, max_x_square),
745  {},
746  {IntegerLiteral::LowerOrEqual(x_, max_x)})) {
747  return false;
748  }
749  } else if (max_x_square > max_s) {
750  const IntegerValue new_max = FloorSquareRoot(max_s);
751  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(x_, new_max), {},
752  {IntegerLiteral::LowerOrEqual(
753  s_, (new_max + 1) * (new_max + 1) - 1)})) {
754  return false;
755  }
756  }
757 
758  return true;
759 }
760 
762  const int id = watcher->Register(this);
763  watcher->WatchIntegerVariable(x_, id);
764  watcher->WatchIntegerVariable(s_, id);
766 }
767 
768 DivisionPropagator::DivisionPropagator(IntegerVariable a, IntegerVariable b,
769  IntegerVariable c,
770  IntegerTrail* integer_trail)
771  : a_(a), b_(b), c_(c), integer_trail_(integer_trail) {
772  // TODO(user): support these cases.
773  CHECK_GE(integer_trail->LevelZeroLowerBound(a), 0);
774  CHECK_GT(integer_trail->LevelZeroLowerBound(b), 0); // b can never be zero.
775 }
776 
778  const IntegerValue min_a = integer_trail_->LowerBound(a_);
779  const IntegerValue max_a = integer_trail_->UpperBound(a_);
780  const IntegerValue min_b = integer_trail_->LowerBound(b_);
781  const IntegerValue max_b = integer_trail_->UpperBound(b_);
782  IntegerValue min_c = integer_trail_->LowerBound(c_);
783  IntegerValue max_c = integer_trail_->UpperBound(c_);
784 
785  if (max_a / min_b < max_c) {
786  max_c = max_a / min_b;
787  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(c_, max_c), {},
788  {integer_trail_->UpperBoundAsLiteral(a_),
789  integer_trail_->LowerBoundAsLiteral(b_)})) {
790  return false;
791  }
792  }
793  if (min_a / max_b > min_c) {
794  min_c = min_a / max_b;
795  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(c_, min_c), {},
796  {integer_trail_->LowerBoundAsLiteral(a_),
797  integer_trail_->UpperBoundAsLiteral(b_)})) {
798  return false;
799  }
800  }
801 
802  // TODO(user): propagate the bounds on a and b from the ones of c.
803  // Note however that what we did is enough to enforce the constraint when
804  // all the values are fixed.
805  return true;
806 }
807 
809  const int id = watcher->Register(this);
810  watcher->WatchIntegerVariable(a_, id);
811  watcher->WatchIntegerVariable(b_, id);
812  watcher->WatchIntegerVariable(c_, id);
814 }
815 
817  IntegerValue b,
818  IntegerVariable c,
819  IntegerTrail* integer_trail)
820  : a_(a), b_(b), c_(c), integer_trail_(integer_trail) {}
821 
823  const IntegerValue min_a = integer_trail_->LowerBound(a_);
824  const IntegerValue max_a = integer_trail_->UpperBound(a_);
825  IntegerValue min_c = integer_trail_->LowerBound(c_);
826  IntegerValue max_c = integer_trail_->UpperBound(c_);
827 
828  CHECK_GT(b_, 0);
829 
830  if (max_a / b_ < max_c) {
831  max_c = max_a / b_;
832  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(c_, max_c), {},
833  {integer_trail_->UpperBoundAsLiteral(a_)})) {
834  return false;
835  }
836  } else if (max_a / b_ > max_c) {
837  const IntegerValue new_max_a =
838  max_c >= 0 ? max_c * b_ + b_ - 1
839  : IntegerValue(CapProd(max_c.value(), b_.value()));
840  CHECK_LT(new_max_a, max_a);
841  if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(a_, new_max_a),
842  {},
843  {integer_trail_->UpperBoundAsLiteral(c_)})) {
844  return false;
845  }
846  }
847 
848  if (min_a / b_ > min_c) {
849  min_c = min_a / b_;
850  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(c_, min_c), {},
851  {integer_trail_->LowerBoundAsLiteral(a_)})) {
852  return false;
853  }
854  } else if (min_a / b_ < min_c) {
855  const IntegerValue new_min_a =
856  min_c > 0 ? IntegerValue(CapProd(min_c.value(), b_.value()))
857  : min_c * b_ - b_ + 1;
858  CHECK_GT(new_min_a, min_a);
859  if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(a_, new_min_a),
860  {},
861  {integer_trail_->LowerBoundAsLiteral(c_)})) {
862  return false;
863  }
864  }
865 
866  return true;
867 }
868 
870  const int id = watcher->Register(this);
871  watcher->WatchIntegerVariable(a_, id);
872  watcher->WatchIntegerVariable(c_, id);
873 }
874 
875 std::function<void(Model*)> IsOneOf(IntegerVariable var,
876  const std::vector<Literal>& selectors,
877  const std::vector<IntegerValue>& values) {
878  return [=](Model* model) {
879  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
880  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
881 
882  CHECK(!values.empty());
883  CHECK_EQ(values.size(), selectors.size());
884  std::vector<int64> unique_values;
885  absl::flat_hash_map<int64, std::vector<Literal>> value_to_selector;
886  for (int i = 0; i < values.size(); ++i) {
887  unique_values.push_back(values[i].value());
888  value_to_selector[values[i].value()].push_back(selectors[i]);
889  }
890  gtl::STLSortAndRemoveDuplicates(&unique_values);
891 
892  integer_trail->UpdateInitialDomain(var, Domain::FromValues(unique_values));
893  if (unique_values.size() == 1) {
894  model->Add(ClauseConstraint(selectors));
895  return;
896  }
897 
898  // Note that it is more efficient to call AssociateToIntegerEqualValue()
899  // with the values ordered, like we do here.
900  for (const int64 v : unique_values) {
901  const std::vector<Literal>& selectors = value_to_selector[v];
902  if (selectors.size() == 1) {
903  encoder->AssociateToIntegerEqualValue(selectors[0], var,
904  IntegerValue(v));
905  } else {
906  const Literal l(model->Add(NewBooleanVariable()), true);
907  model->Add(ReifiedBoolOr(selectors, l));
908  encoder->AssociateToIntegerEqualValue(l, var, IntegerValue(v));
909  }
910  }
911  };
912 }
913 
914 } // namespace sat
915 } // namespace operations_research
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::GenericLiteralWatcher::Register
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1910
if
if(!yyg->yy_init)
Definition: parser.yy.cc:965
min
int64 min
Definition: alldiff_cst.cc:138
operations_research::sat::IntegerTrail
Definition: integer.h:533
VLOG
#define VLOG(verboselevel)
Definition: base/logging.h:978
operations_research::sat::FixedDivisionPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: integer_expr.cc:869
operations_research::sat::FloorRatio
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:90
time_limit.h
operations_research::sat::GenericLiteralWatcher::WatchLowerBound
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1356
operations_research::CapProd
int64 CapProd(int64 x, int64 y)
Definition: saturated_arithmetic.h:231
operations_research::sat::kNoLiteralIndex
const LiteralIndex kNoLiteralIndex(-1)
operations_research::sat::CeilRatio
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
operations_research::sat::ReifiedBoolOr
std::function< void(Model *)> ReifiedBoolOr(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:935
operations_research::sat::IntegerTrail::LevelZeroLowerBound
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Definition: integer.h:1333
operations_research::sat::PositiveProductPropagator::Propagate
bool Propagate() final
Definition: integer_expr.cc:632
CHECK_GE
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
operations_research::sat::IntegerTrail::VariableLowerBoundIsFromLevelZero
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const
Definition: integer.h:810
operations_research::sat::GenericLiteralWatcher::RegisterReversibleInt
void RegisterReversibleInt(int id, int *rev)
Definition: integer.cc:1954
value
int64 value
Definition: demon_profiler.cc:43
CHECK_GT
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
operations_research::Domain::FromValues
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
Definition: sorted_interval_list.cc:137
operations_research::sat::SquarePropagator::Propagate
bool Propagate() final
Definition: integer_expr.cc:720
operations_research::sat::LinExprUpperBound
IntegerValue LinExprUpperBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
Definition: linear_constraint.cc:302
CHECK_LT
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
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::MathUtil::GCD64
static int64 GCD64(int64 x, int64 y)
Definition: mathutil.h:107
operations_research::sat::IntegerTrail::EnqueueLiteral
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:1058
operations_research::sat::NegationOf
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
operations_research::sat::FixedDivisionPropagator::FixedDivisionPropagator
FixedDivisionPropagator(IntegerVariable a, IntegerValue b, IntegerVariable c, IntegerTrail *integer_trail)
Definition: integer_expr.cc:816
operations_research::sat::VariablesAssignment::LiteralIsTrue
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
operations_research::sat::IntegerLiteral::GreaterOrEqual
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1247
operations_research::sat::DivisionPropagator::DivisionPropagator
DivisionPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable c, IntegerTrail *integer_trail)
Definition: integer_expr.cc:768
operations_research::sat::PositiveVariable
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
int64
int64_t int64
Definition: integral_types.h:34
operations_research::sat::Literal::Negated
Literal Negated() const
Definition: sat_base.h:91
operations_research::TimeLimit
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
index
int index
Definition: pack.cc:508
operations_research::sat::IntegerTrail::UpdateInitialDomain
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::PositiveRemainder
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:102
a
int64 a
Definition: constraint_solver/table.cc:42
operations_research::sat::LevelZeroEquality::Propagate
bool Propagate() final
Definition: integer_expr.cc:276
operations_research::sat::IntegerTrail::UpperBoundAsLiteral
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1318
operations_research::sat::IntegerTrail::AppendRelaxedLinearReason
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:807
operations_research::sat::NewBooleanVariable
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1395
operations_research::sat::IntegerTrail::UpperBound
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1287
operations_research::sat::IntegerTrail::Enqueue
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.cc:989
operations_research::sat::DivisionPropagator::Propagate
bool Propagate() final
Definition: integer_expr.cc:777
operations_research::sat::MinPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: integer_expr.cc:404
operations_research::sat::PositiveProductPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: integer_expr.cc:684
operations_research::sat::GenericLiteralWatcher::NotifyThatPropagatorMayNotReachFixedPointInOnePass
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
Definition: integer.cc:1940
gtl::STLSortAndRemoveDuplicates
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
operations_research::sat::IsOneOf
std::function< void(Model *)> IsOneOf(IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
Definition: integer_expr.cc:875
operations_research::sat::kMaxIntegerValue
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
integer_expr.h
operations_research::sat::Trail::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
operations_research::sat::LinMinPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: integer_expr.cc:602
operations_research::sat::DivisionPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: integer_expr.cc:808
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::LinearExpression
Definition: linear_constraint.h:173
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::IntegerTrail::LowerBoundAsLiteral
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1313
operations_research::sat::IntegerLiteral
Definition: integer.h:153
operations_research::sat::LowerOrEqual
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1492
operations_research::sat::MinPropagator::MinPropagator
MinPropagator(const std::vector< IntegerVariable > &vars, IntegerVariable min_var, IntegerTrail *integer_trail)
Definition: integer_expr.cc:321
operations_research::sat::LinMinPropagator::Propagate
bool Propagate() final
Definition: integer_expr.cc:516
operations_research::sat::GenericLiteralWatcher::WatchIntegerVariable
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
Definition: integer.h:1380
operations_research::sat::LinExprLowerBound
IntegerValue LinExprLowerBound(const LinearExpression &expr, const IntegerTrail &integer_trail)
Definition: linear_constraint.cc:292
operations_research::sat::IntegerLiteral::LowerOrEqual
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1253
operations_research::sat::FixedDivisionPropagator::Propagate
bool Propagate() final
Definition: integer_expr.cc:822
sorted_interval_list.h
operations_research::sat::Model::GetOrCreate
T * GetOrCreate()
Returns an object of type T that is unique to this model (like a "local" singleton).
Definition: sat/model.h:106
operations_research::sat::ClauseConstraint
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:905
DCHECK_GE
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::TimeLimit::AdvanceDeterministicTime
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
Definition: time_limit.h:226
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::RevIntegerValueRepository
Definition: integer.h:1080
operations_research::sat::ToDouble
double ToDouble(IntegerValue value)
Definition: integer.h:69
operations_research::sat::PositiveProductPropagator::PositiveProductPropagator
PositiveProductPropagator(IntegerVariable a, IntegerVariable b, IntegerVariable p, IntegerTrail *integer_trail)
Definition: integer_expr.cc:619
operations_research::sat::MinPropagator::Propagate
bool Propagate() final
Definition: integer_expr.cc:326
operations_research::sat::GenericLiteralWatcher::WatchLiteral
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1348
operations_research::sat::IntegerTrail::ReportConflict
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
Definition: integer.h:793
stl_util.h
vars_
const std::vector< IntVar * > vars_
Definition: alldiff_cst.cc:43
operations_research::sat::IntegerSumLE::IntegerSumLE
IntegerSumLE(const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const std::vector< IntegerValue > &coeffs, IntegerValue upper_bound, Model *model)
Definition: integer_expr.cc:30
operations_research::sat::IntegerTrail::RelaxLinearReason
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:785
operations_research::sat::UpperBound
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1456
operations_research::sat::SquarePropagator::SquarePropagator
SquarePropagator(IntegerVariable x, IntegerVariable s, IntegerTrail *integer_trail)
Definition: integer_expr.cc:712
operations_research::sat::IntegerTrail::FindTrailIndexOfVarBefore
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
Definition: integer.cc:716
operations_research::sat::IntegerTrail::IsFixed
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1291
b
int64 b
Definition: constraint_solver/table.cc:43
operations_research::sat::IntegerSumLE::Propagate
bool Propagate() final
Definition: integer_expr.cc:78
operations_research::sat::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::sat::SquarePropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: integer_expr.cc:761
operations_research::sat::LinMinPropagator::LinMinPropagator
LinMinPropagator(const std::vector< LinearExpression > &exprs, IntegerVariable min_var, Model *model)
Definition: integer_expr.cc:412
literal
Literal literal
Definition: optimization.cc:84
operations_research::RevRepository::SaveState
void SaveState(T *object)
Definition: rev.h:61
CHECK
#define CHECK(condition)
Definition: base/logging.h:495
operations_research::sat::IntegerEncoder
Definition: integer.h:276
integer.h
operations_research::sat::VariablesAssignment::LiteralIsFalse
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
operations_research::sat::GenericLiteralWatcher::WatchUpperBound
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1374
operations_research::sat::Trail
Definition: sat_base.h:233