OR-Tools  8.1
precedences.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 
19 #include "ortools/base/cleanup.h"
20 #include "ortools/base/logging.h"
21 #include "ortools/base/stl_util.h"
22 #include "ortools/sat/clause.h"
24 
25 namespace operations_research {
26 namespace sat {
27 
28 namespace {
29 
30 void AppendLowerBoundReasonIfValid(IntegerVariable var,
31  const IntegerTrail& i_trail,
32  std::vector<IntegerLiteral>* reason) {
33  if (var != kNoIntegerVariable) {
34  reason->push_back(i_trail.LowerBoundAsLiteral(var));
35  }
36 }
37 
38 } // namespace
39 
41 
43  while (propagation_trail_index_ < trail_->Index()) {
44  const Literal literal = (*trail_)[propagation_trail_index_++];
45  if (literal.Index() >= literal_to_new_impacted_arcs_.size()) continue;
46 
47  // IMPORTANT: Because of the way Untrail() work, we need to add all the
48  // potential arcs before we can abort. It is why we iterate twice here.
49  for (const ArcIndex arc_index :
50  literal_to_new_impacted_arcs_[literal.Index()]) {
51  if (--arc_counts_[arc_index] == 0) {
52  const ArcInfo& arc = arcs_[arc_index];
53  impacted_arcs_[arc.tail_var].push_back(arc_index);
54  }
55  }
56 
57  // Iterate again to check for a propagation and indirectly update
58  // modified_vars_.
59  for (const ArcIndex arc_index :
60  literal_to_new_impacted_arcs_[literal.Index()]) {
61  if (arc_counts_[arc_index] > 0) continue;
62  const ArcInfo& arc = arcs_[arc_index];
63  if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue;
64  const IntegerValue new_head_lb =
65  integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
66  if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
67  if (!EnqueueAndCheck(arc, new_head_lb, trail_)) return false;
68  }
69  }
70  }
71 
72  // Do the actual propagation of the IntegerVariable bounds.
73  InitializeBFQueueWithModifiedNodes();
74  if (!BellmanFordTarjan(trail_)) return false;
75 
76  // We can only test that no propagation is left if we didn't enqueue new
77  // literal in the presence of optional variables.
78  //
79  // TODO(user): Because of our code to deal with InPropagationLoop(), this is
80  // not always true. Find a cleaner way to DCHECK() while not failing in this
81  // corner case.
82  if (/*DISABLES CODE*/ (false) &&
83  propagation_trail_index_ == trail_->Index()) {
84  DCHECK(NoPropagationLeft(*trail_));
85  }
86 
87  // Propagate the presence literals of the arcs that can't be added.
88  PropagateOptionalArcs(trail_);
89 
90  // Clean-up modified_vars_ to do as little as possible on the next call.
91  modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
92  return true;
93 }
94 
96  for (const ArcIndex arc_index : impacted_arcs_[var]) {
97  const ArcInfo& arc = arcs_[arc_index];
98  if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue;
99  const IntegerValue new_head_lb =
100  integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
101  if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
102  if (!EnqueueAndCheck(arc, new_head_lb, trail_)) return false;
103  }
104  }
105  return true;
106 }
107 
108 void PrecedencesPropagator::Untrail(const Trail& trail, int trail_index) {
109  if (propagation_trail_index_ > trail_index) {
110  // This means that we already propagated all there is to propagate
111  // at the level trail_index, so we can safely clear modified_vars_ in case
112  // it wasn't already done.
113  modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
114  }
115  while (propagation_trail_index_ > trail_index) {
116  const Literal literal = trail[--propagation_trail_index_];
117  if (literal.Index() >= literal_to_new_impacted_arcs_.size()) continue;
118  for (const ArcIndex arc_index :
119  literal_to_new_impacted_arcs_[literal.Index()]) {
120  if (arc_counts_[arc_index]++ == 0) {
121  const ArcInfo& arc = arcs_[arc_index];
122  impacted_arcs_[arc.tail_var].pop_back();
123  }
124  }
125  }
126 }
127 
128 // Instead of simply sorting the IntegerPrecedences returned by .var,
129 // experiments showed that it is faster to regroup all the same .var "by hand"
130 // by first computing how many times they appear and then apply the sorting
131 // permutation.
133  const std::vector<IntegerVariable>& vars,
134  std::vector<IntegerPrecedences>* output) {
135  tmp_sorted_vars_.clear();
136  tmp_precedences_.clear();
137  for (int index = 0; index < vars.size(); ++index) {
138  const IntegerVariable var = vars[index];
140  if (var >= impacted_arcs_.size()) continue;
141  for (const ArcIndex arc_index : impacted_arcs_[var]) {
142  const ArcInfo& arc = arcs_[arc_index];
143  if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue;
144 
145  IntegerValue offset = arc.offset;
146  if (arc.offset_var != kNoIntegerVariable) {
147  offset += integer_trail_->LowerBound(arc.offset_var);
148  }
149 
150  // TODO(user): it seems better to ignore negative min offset as we will
151  // often have relation of the form interval_start >= interval_end -
152  // offset, and such relation are usually not useful. Revisit this in case
153  // we see problems where we can propagate more without this test.
154  if (offset < 0) continue;
155 
156  if (var_to_degree_[arc.head_var] == 0) {
157  tmp_sorted_vars_.push_back(
158  {arc.head_var, integer_trail_->LowerBound(arc.head_var)});
159  } else {
160  // This "seen" mechanism is needed because we may have multi-arc and we
161  // don't want any duplicates in the "is_before" relation. Note that it
162  // works because var_to_last_index_ is reset by the var_to_degree_ == 0
163  // case.
164  if (var_to_last_index_[arc.head_var] == index) continue;
165  }
166  var_to_last_index_[arc.head_var] = index;
167  var_to_degree_[arc.head_var]++;
168  tmp_precedences_.push_back(
169  {index, arc.head_var, arc_index.value(), offset});
170  }
171  }
172 
173  // This order is a topological order for the precedences relation order
174  // provided that all the offset between the involved IntegerVariable are
175  // positive.
176  //
177  // TODO(user): use an order that is always topological? This is not clear
178  // since it may be slower to compute and not worth it because the order below
179  // is more natural and may work better.
180  std::sort(tmp_sorted_vars_.begin(), tmp_sorted_vars_.end());
181 
182  // Permute tmp_precedences_ into the output to put it in the correct order.
183  // For that we transform var_to_degree_ to point to the first position of
184  // each lbvar in the output vector.
185  int start = 0;
186  for (const SortedVar pair : tmp_sorted_vars_) {
187  const int degree = var_to_degree_[pair.var];
188  if (degree > 1) {
189  var_to_degree_[pair.var] = start;
190  start += degree;
191  } else {
192  // Optimization: we remove degree one relations.
193  var_to_degree_[pair.var] = -1;
194  }
195  }
196  output->resize(start);
197  for (const IntegerPrecedences& precedence : tmp_precedences_) {
198  if (var_to_degree_[precedence.var] < 0) continue;
199  (*output)[var_to_degree_[precedence.var]++] = precedence;
200  }
201 
202  // Cleanup var_to_degree_, note that we don't need to clean
203  // var_to_last_index_.
204  for (const SortedVar pair : tmp_sorted_vars_) {
205  var_to_degree_[pair.var] = 0;
206  }
207 }
208 
210  int arc_index, IntegerValue min_offset,
211  std::vector<Literal>* literal_reason,
212  std::vector<IntegerLiteral>* integer_reason) const {
213  const ArcInfo& arc = arcs_[ArcIndex(arc_index)];
214  for (const Literal l : arc.presence_literals) {
215  literal_reason->push_back(l.Negated());
216  }
217  if (arc.offset_var != kNoIntegerVariable) {
218  // Reason for ArcOffset(arc) to be >= min_offset.
219  integer_reason->push_back(IntegerLiteral::GreaterOrEqual(
220  arc.offset_var, min_offset - arc.offset));
221  }
222 }
223 
224 void PrecedencesPropagator::AdjustSizeFor(IntegerVariable i) {
225  const int index = std::max(i.value(), NegationOf(i).value());
226  if (index >= impacted_arcs_.size()) {
227  // TODO(user): only watch lower bound of the relevant variable instead
228  // of watching everything in [0, max_index_of_variable_used_in_this_class).
229  for (IntegerVariable var(impacted_arcs_.size()); var <= index; ++var) {
230  watcher_->WatchLowerBound(var, watcher_id_);
231  }
232  impacted_arcs_.resize(index + 1);
233  impacted_potential_arcs_.resize(index + 1);
234  var_to_degree_.resize(index + 1);
235  var_to_last_index_.resize(index + 1);
236  }
237 }
238 
239 void PrecedencesPropagator::AddArc(
240  IntegerVariable tail, IntegerVariable head, IntegerValue offset,
241  IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
242  DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
243  AdjustSizeFor(tail);
244  AdjustSizeFor(head);
245  if (offset_var != kNoIntegerVariable) AdjustSizeFor(offset_var);
246 
247  // This arc is present iff all the literals here are true.
248  absl::InlinedVector<Literal, 6> enforcement_literals;
249  {
250  for (const Literal l : presence_literals) {
251  enforcement_literals.push_back(l);
252  }
253  if (integer_trail_->IsOptional(tail)) {
254  enforcement_literals.push_back(
255  integer_trail_->IsIgnoredLiteral(tail).Negated());
256  }
257  if (integer_trail_->IsOptional(head)) {
258  enforcement_literals.push_back(
259  integer_trail_->IsIgnoredLiteral(head).Negated());
260  }
261  if (offset_var != kNoIntegerVariable &&
262  integer_trail_->IsOptional(offset_var)) {
263  enforcement_literals.push_back(
264  integer_trail_->IsIgnoredLiteral(offset_var).Negated());
265  }
266  gtl::STLSortAndRemoveDuplicates(&enforcement_literals);
267  int new_size = 0;
268  for (const Literal l : enforcement_literals) {
269  if (trail_->Assignment().LiteralIsTrue(Literal(l))) {
270  continue; // At true, ignore this literal.
271  } else if (trail_->Assignment().LiteralIsFalse(Literal(l))) {
272  return; // At false, ignore completely this arc.
273  }
274  enforcement_literals[new_size++] = l;
275  }
276  enforcement_literals.resize(new_size);
277  }
278 
279  if (head == tail) {
280  // A self-arc is either plain SAT or plain UNSAT or it forces something on
281  // the given offset_var or presence_literal_index. In any case it could be
282  // presolved in something more efficent.
283  VLOG(1) << "Self arc! This could be presolved. "
284  << "var:" << tail << " offset:" << offset
285  << " offset_var:" << offset_var
286  << " conditioned_by:" << presence_literals;
287  }
288 
289  // Remove the offset_var if it is fixed.
290  // TODO(user): We should also handle the case where tail or head is fixed.
291  if (offset_var != kNoIntegerVariable) {
292  const IntegerValue lb = integer_trail_->LowerBound(offset_var);
293  if (lb == integer_trail_->UpperBound(offset_var)) {
294  offset += lb;
295  offset_var = kNoIntegerVariable;
296  }
297  }
298 
299  // Deal first with impacted_potential_arcs_/potential_arcs_.
300  if (!enforcement_literals.empty()) {
301  const OptionalArcIndex arc_index(potential_arcs_.size());
302  potential_arcs_.push_back(
303  {tail, head, offset, offset_var, enforcement_literals});
304  impacted_potential_arcs_[tail].push_back(arc_index);
305  impacted_potential_arcs_[NegationOf(head)].push_back(arc_index);
306  if (offset_var != kNoIntegerVariable) {
307  impacted_potential_arcs_[offset_var].push_back(arc_index);
308  }
309  }
310 
311  // Now deal with impacted_arcs_/arcs_.
312  struct InternalArc {
313  IntegerVariable tail_var;
314  IntegerVariable head_var;
315  IntegerVariable offset_var;
316  };
317  std::vector<InternalArc> to_add;
318  if (offset_var == kNoIntegerVariable) {
319  // a + offset <= b and -b + offset <= -a
320  to_add.push_back({tail, head, kNoIntegerVariable});
321  to_add.push_back({NegationOf(head), NegationOf(tail), kNoIntegerVariable});
322  } else {
323  // tail (a) and offset_var (b) are symmetric, so we add:
324  // - a + b + offset <= c
325  to_add.push_back({tail, head, offset_var});
326  to_add.push_back({offset_var, head, tail});
327  // - a - c + offset <= -b
328  to_add.push_back({tail, NegationOf(offset_var), NegationOf(head)});
329  to_add.push_back({NegationOf(head), NegationOf(offset_var), tail});
330  // - b - c + offset <= -a
331  to_add.push_back({offset_var, NegationOf(tail), NegationOf(head)});
332  to_add.push_back({NegationOf(head), NegationOf(tail), offset_var});
333  }
334  for (const InternalArc a : to_add) {
335  // Since we add a new arc, we will need to consider its tail during the next
336  // propagation. Note that the size of modified_vars_ will be automatically
337  // updated when new integer variables are created since we register it with
338  // IntegerTrail in this class contructor.
339  //
340  // TODO(user): Adding arcs and then calling Untrail() before Propagate()
341  // will cause this mecanism to break. Find a more robust implementation.
342  //
343  // TODO(user): In some rare corner case, rescanning the whole list of arc
344  // leaving tail_var can make AddVar() have a quadratic complexity where it
345  // shouldn't. A better solution would be to see if this new arc currently
346  // propagate something, and if it does, just update the lower bound of
347  // a.head_var and let the normal "is modified" mecanism handle any eventual
348  // follow up propagations.
349  modified_vars_.Set(a.tail_var);
350 
351  // If a.head_var is optional, we can potentially remove some literal from
352  // enforcement_literals.
353  const ArcIndex arc_index(arcs_.size());
354  arcs_.push_back(
355  {a.tail_var, a.head_var, offset, a.offset_var, enforcement_literals});
356  auto& presence_literals = arcs_.back().presence_literals;
357  if (integer_trail_->IsOptional(a.head_var)) {
358  // TODO(user): More generally, we can remove any literal that is implied
359  // by to_remove.
360  const Literal to_remove =
361  integer_trail_->IsIgnoredLiteral(a.head_var).Negated();
362  const auto it = std::find(presence_literals.begin(),
363  presence_literals.end(), to_remove);
364  if (it != presence_literals.end()) presence_literals.erase(it);
365  }
366 
367  if (presence_literals.empty()) {
368  impacted_arcs_[a.tail_var].push_back(arc_index);
369  } else {
370  for (const Literal l : presence_literals) {
371  if (l.Index() >= literal_to_new_impacted_arcs_.size()) {
372  literal_to_new_impacted_arcs_.resize(l.Index().value() + 1);
373  }
374  literal_to_new_impacted_arcs_[l.Index()].push_back(arc_index);
375  }
376  }
377  arc_counts_.push_back(presence_literals.size());
378  }
379 }
380 
381 // TODO(user): On jobshop problems with a lot of tasks per machine (500), this
382 // takes up a big chunck of the running time even before we find a solution.
383 // This is because, for each lower bound changed, we inspect 500 arcs even
384 // though they will never be propagated because the other bound is still at the
385 // horizon. Find an even sparser algorithm?
386 void PrecedencesPropagator::PropagateOptionalArcs(Trail* trail) {
387  for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
388  // The variables are not in increasing order, so we need to continue.
389  if (var >= impacted_potential_arcs_.size()) continue;
390 
391  // Note that we can currently check the same ArcInfo up to 3 times, one for
392  // each of the arc variables: tail, NegationOf(head) and offset_var.
393  for (const OptionalArcIndex arc_index : impacted_potential_arcs_[var]) {
394  const ArcInfo& arc = potential_arcs_[arc_index];
395  int num_not_true = 0;
396  Literal to_propagate;
397  for (const Literal l : arc.presence_literals) {
398  if (!trail->Assignment().LiteralIsTrue(l)) {
399  ++num_not_true;
400  to_propagate = l;
401  }
402  }
403  if (num_not_true != 1) continue;
404  if (trail->Assignment().LiteralIsFalse(to_propagate)) continue;
405 
406  // Test if this arc can be present or not.
407  // Important arc.tail_var can be different from var here.
408  const IntegerValue tail_lb = integer_trail_->LowerBound(arc.tail_var);
409  const IntegerValue head_ub = integer_trail_->UpperBound(arc.head_var);
410  if (tail_lb + ArcOffset(arc) > head_ub) {
411  integer_reason_.clear();
412  integer_reason_.push_back(
413  integer_trail_->LowerBoundAsLiteral(arc.tail_var));
414  integer_reason_.push_back(
415  integer_trail_->UpperBoundAsLiteral(arc.head_var));
416  AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
417  &integer_reason_);
418  literal_reason_.clear();
419  for (const Literal l : arc.presence_literals) {
420  if (l != to_propagate) literal_reason_.push_back(l.Negated());
421  }
422  integer_trail_->EnqueueLiteral(to_propagate.Negated(), literal_reason_,
423  integer_reason_);
424  }
425  }
426  }
427 }
428 
429 IntegerValue PrecedencesPropagator::ArcOffset(const ArcInfo& arc) const {
430  return arc.offset + (arc.offset_var == kNoIntegerVariable
431  ? IntegerValue(0)
432  : integer_trail_->LowerBound(arc.offset_var));
433 }
434 
435 bool PrecedencesPropagator::EnqueueAndCheck(const ArcInfo& arc,
436  IntegerValue new_head_lb,
437  Trail* trail) {
438  DCHECK_GT(new_head_lb, integer_trail_->LowerBound(arc.head_var));
439 
440  // Compute the reason for new_head_lb.
441  //
442  // TODO(user): do like for clause and keep the negation of
443  // arc.presence_literals? I think we could change the integer.h API to accept
444  // true literal like for IntegerVariable, it is really confusing currently.
445  literal_reason_.clear();
446  for (const Literal l : arc.presence_literals) {
447  literal_reason_.push_back(l.Negated());
448  }
449 
450  integer_reason_.clear();
451  integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(arc.tail_var));
452  AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
453  &integer_reason_);
454 
455  // The code works without this block since Enqueue() below can already take
456  // care of conflicts. However, it is better to deal with the conflict
457  // ourselves because we can be smarter about the reason this way.
458  //
459  // The reason for a "precedence" conflict is always a linear reason
460  // involving the tail lower_bound, the head upper bound and eventually the
461  // size lower bound. Because of that, we can use the RelaxLinearReason()
462  // code.
463  if (new_head_lb > integer_trail_->UpperBound(arc.head_var)) {
464  const IntegerValue slack =
465  new_head_lb - integer_trail_->UpperBound(arc.head_var) - 1;
466  integer_reason_.push_back(
467  integer_trail_->UpperBoundAsLiteral(arc.head_var));
468  std::vector<IntegerValue> coeffs(integer_reason_.size(), IntegerValue(1));
469  integer_trail_->RelaxLinearReason(slack, coeffs, &integer_reason_);
470 
471  if (!integer_trail_->IsOptional(arc.head_var)) {
472  return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
473  } else {
474  CHECK(!integer_trail_->IsCurrentlyIgnored(arc.head_var));
475  const Literal l = integer_trail_->IsIgnoredLiteral(arc.head_var);
476  if (trail->Assignment().LiteralIsFalse(l)) {
477  literal_reason_.push_back(l);
478  return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
479  } else {
480  integer_trail_->EnqueueLiteral(l, literal_reason_, integer_reason_);
481  return true;
482  }
483  }
484  }
485 
486  return integer_trail_->Enqueue(
487  IntegerLiteral::GreaterOrEqual(arc.head_var, new_head_lb),
488  literal_reason_, integer_reason_);
489 }
490 
491 bool PrecedencesPropagator::NoPropagationLeft(const Trail& trail) const {
492  const int num_nodes = impacted_arcs_.size();
493  for (IntegerVariable var(0); var < num_nodes; ++var) {
494  for (const ArcIndex arc_index : impacted_arcs_[var]) {
495  const ArcInfo& arc = arcs_[arc_index];
496  if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue;
497  if (integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc) >
498  integer_trail_->LowerBound(arc.head_var)) {
499  return false;
500  }
501  }
502  }
503  return true;
504 }
505 
506 void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
507  // Sparse clear of the queue. TODO(user): only use the sparse version if
508  // queue.size() is small or use SparseBitset.
509  const int num_nodes = impacted_arcs_.size();
510  bf_in_queue_.resize(num_nodes, false);
511  for (const int node : bf_queue_) bf_in_queue_[node] = false;
512  bf_queue_.clear();
513  DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
514  [](bool v) { return v; }));
515  for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
516  if (var >= num_nodes) continue;
517  bf_queue_.push_back(var.value());
518  bf_in_queue_[var.value()] = true;
519  }
520 }
521 
522 void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
523  // To be sparse, we use the fact that each node with a parent must be in
524  // modified_vars_.
525  const int num_nodes = impacted_arcs_.size();
526  for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
527  if (var >= num_nodes) continue;
528  const ArcIndex parent_arc_index = bf_parent_arc_of_[var.value()];
529  if (parent_arc_index != -1) {
530  arcs_[parent_arc_index].is_marked = false;
531  bf_parent_arc_of_[var.value()] = -1;
532  bf_can_be_skipped_[var.value()] = false;
533  }
534  }
535  DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
536  [](ArcIndex v) { return v != -1; }));
537  DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
538  [](bool v) { return v; }));
539 }
540 
541 bool PrecedencesPropagator::DisassembleSubtree(
542  int source, int target, std::vector<bool>* can_be_skipped) {
543  // Note that we explore a tree, so we can do it in any order, and the one
544  // below seems to be the fastest.
545  tmp_vector_.clear();
546  tmp_vector_.push_back(source);
547  while (!tmp_vector_.empty()) {
548  const int tail = tmp_vector_.back();
549  tmp_vector_.pop_back();
550  for (const ArcIndex arc_index : impacted_arcs_[IntegerVariable(tail)]) {
551  const ArcInfo& arc = arcs_[arc_index];
552  if (arc.is_marked) {
553  arc.is_marked = false; // mutable.
554  if (arc.head_var.value() == target) return true;
555  DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
556  (*can_be_skipped)[arc.head_var.value()] = true;
557  tmp_vector_.push_back(arc.head_var.value());
558  }
559  }
560  }
561  return false;
562 }
563 
564 void PrecedencesPropagator::AnalyzePositiveCycle(
565  ArcIndex first_arc, Trail* trail, std::vector<Literal>* must_be_all_true,
566  std::vector<Literal>* literal_reason,
567  std::vector<IntegerLiteral>* integer_reason) {
568  must_be_all_true->clear();
569  literal_reason->clear();
570  integer_reason->clear();
571 
572  // Follow bf_parent_arc_of_[] to find the cycle containing first_arc.
573  const IntegerVariable first_arc_head = arcs_[first_arc].head_var;
574  ArcIndex arc_index = first_arc;
575  std::vector<ArcIndex> arc_on_cycle;
576 
577  // Just to be safe and avoid an infinite loop we use the fact that the maximum
578  // cycle size on a graph with n nodes is of size n. If we have more in the
579  // code below, it means first_arc is not part of a cycle according to
580  // bf_parent_arc_of_[], which should never happen.
581  const int num_nodes = impacted_arcs_.size();
582  while (arc_on_cycle.size() <= num_nodes) {
583  arc_on_cycle.push_back(arc_index);
584  const ArcInfo& arc = arcs_[arc_index];
585  if (arc.tail_var == first_arc_head) break;
586  arc_index = bf_parent_arc_of_[arc.tail_var.value()];
587  CHECK_NE(arc_index, ArcIndex(-1));
588  }
589  CHECK_NE(arc_on_cycle.size(), num_nodes + 1) << "Infinite loop.";
590 
591  // Compute the reason for this cycle.
592  IntegerValue sum(0);
593  for (const ArcIndex arc_index : arc_on_cycle) {
594  const ArcInfo& arc = arcs_[arc_index];
595  sum += ArcOffset(arc);
596  AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
597  integer_reason);
598  for (const Literal l : arc.presence_literals) {
599  literal_reason->push_back(l.Negated());
600  }
601 
602  // If the cycle happens to contain optional variable not yet ignored, then
603  // it is not a conflict anymore, but we can infer that these variable must
604  // all be ignored. This is because since we propagated them even if they
605  // where not present for sure, their presence literal must form a cycle
606  // together (i.e. they are all absent or present at the same time).
607  if (integer_trail_->IsOptional(arc.head_var)) {
608  must_be_all_true->push_back(
609  integer_trail_->IsIgnoredLiteral(arc.head_var));
610  }
611  }
612 
613  // TODO(user): what if the sum overflow? this is just a check so I guess
614  // we don't really care, but fix the issue.
615  CHECK_GT(sum, 0);
616 }
617 
618 // Note that in our settings it is important to use an algorithm that tries to
619 // minimize the number of integer_trail_->Enqueue() as much as possible.
620 //
621 // TODO(user): The current algorithm is quite efficient, but there is probably
622 // still room for improvments.
623 bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) {
624  const int num_nodes = impacted_arcs_.size();
625 
626  // These vector are reset by CleanUpMarkedArcsAndParents() so resize is ok.
627  bf_can_be_skipped_.resize(num_nodes, false);
628  bf_parent_arc_of_.resize(num_nodes, ArcIndex(-1));
629  const auto cleanup =
630  ::absl::MakeCleanup([this]() { CleanUpMarkedArcsAndParents(); });
631 
632  // The queue initialization is done by InitializeBFQueueWithModifiedNodes().
633  while (!bf_queue_.empty()) {
634  const int node = bf_queue_.front();
635  bf_queue_.pop_front();
636  bf_in_queue_[node] = false;
637 
638  // TODO(user): we don't need bf_can_be_skipped_ since we can detect this
639  // if this node has a parent arc which is not marked. Investigate if it is
640  // faster without the vector<bool>.
641  //
642  // TODO(user): An alternative algorithm is to remove all these nodes from
643  // the queue instead of simply marking them. This should also lead to a
644  // better "relaxation" order of the arcs. It is however a bit more work to
645  // remove them since we need to track their position.
646  if (bf_can_be_skipped_[node]) {
647  DCHECK_NE(bf_parent_arc_of_[node], -1);
648  DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
649  continue;
650  }
651 
652  const IntegerValue tail_lb =
653  integer_trail_->LowerBound(IntegerVariable(node));
654  for (const ArcIndex arc_index : impacted_arcs_[IntegerVariable(node)]) {
655  const ArcInfo& arc = arcs_[arc_index];
656  DCHECK_EQ(arc.tail_var, node);
657  const IntegerValue candidate = tail_lb + ArcOffset(arc);
658  if (candidate > integer_trail_->LowerBound(arc.head_var)) {
659  if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue;
660  if (!EnqueueAndCheck(arc, candidate, trail)) return false;
661 
662  // This is the Tarjan contribution to Bellman-Ford. This code detect
663  // positive cycle, and because it disassemble the subtree while doing
664  // so, the cost is amortized during the algorithm execution. Another
665  // advantages is that it will mark the node explored here as skippable
666  // which will avoid to propagate them too early (knowing that they will
667  // need to be propagated again later).
668  if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
669  &bf_can_be_skipped_)) {
670  std::vector<Literal> must_be_all_true;
671  AnalyzePositiveCycle(arc_index, trail, &must_be_all_true,
672  &literal_reason_, &integer_reason_);
673  if (must_be_all_true.empty()) {
674  return integer_trail_->ReportConflict(literal_reason_,
675  integer_reason_);
676  } else {
677  gtl::STLSortAndRemoveDuplicates(&must_be_all_true);
678  for (const Literal l : must_be_all_true) {
679  if (trail_->Assignment().LiteralIsFalse(l)) {
680  literal_reason_.push_back(l);
681  return integer_trail_->ReportConflict(literal_reason_,
682  integer_reason_);
683  }
684  }
685  for (const Literal l : must_be_all_true) {
686  if (trail_->Assignment().LiteralIsTrue(l)) continue;
687  integer_trail_->EnqueueLiteral(l, literal_reason_,
688  integer_reason_);
689  }
690 
691  // We just marked some optional variable as ignored, no need
692  // to update bf_parent_arc_of_[].
693  continue;
694  }
695  }
696 
697  // We need to enforce the invariant that only the arc_index in
698  // bf_parent_arc_of_[] are marked (but not necessarily all of them
699  // since we unmark some in DisassembleSubtree()).
700  if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
701  arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked = false;
702  }
703 
704  // Tricky: We just enqueued the fact that the lower-bound of head is
705  // candidate. However, because the domain of head may be discrete, it is
706  // possible that the lower-bound of head is now higher than candidate!
707  // If this is the case, we don't update bf_parent_arc_of_[] so that we
708  // don't wrongly detect a positive weight cycle because of this "extra
709  // push".
710  const IntegerValue new_bound = integer_trail_->LowerBound(arc.head_var);
711  if (new_bound == candidate) {
712  bf_parent_arc_of_[arc.head_var.value()] = arc_index;
713  arcs_[arc_index].is_marked = true;
714  } else {
715  // We still unmark any previous dependency, since we have pushed the
716  // value of arc.head_var further.
717  bf_parent_arc_of_[arc.head_var.value()] = -1;
718  }
719 
720  // We do not re-enqueue if we are in a propagation loop and new_bound
721  // was not pushed to candidate or higher.
722  bf_can_be_skipped_[arc.head_var.value()] = false;
723  if (!bf_in_queue_[arc.head_var.value()] && new_bound >= candidate) {
724  bf_queue_.push_back(arc.head_var.value());
725  bf_in_queue_[arc.head_var.value()] = true;
726  }
727  }
728  }
729  }
730  return true;
731 }
732 
733 int PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraintsFromClause(
734  const absl::Span<const Literal> clause, Model* model) {
735  CHECK_EQ(model->GetOrCreate<Trail>()->CurrentDecisionLevel(), 0);
736  if (clause.size() < 2) return 0;
737 
738  // Collect all arcs impacted by this clause.
739  std::vector<ArcInfo> infos;
740  for (const Literal l : clause) {
741  if (l.Index() >= literal_to_new_impacted_arcs_.size()) continue;
742  for (const ArcIndex arc_index : literal_to_new_impacted_arcs_[l.Index()]) {
743  const ArcInfo& arc = arcs_[arc_index];
744  if (arc.presence_literals.size() != 1) continue;
745 
746  // TODO(user): Support variable offset.
747  if (arc.offset_var != kNoIntegerVariable) continue;
748  infos.push_back(arc);
749  }
750  }
751  if (infos.size() <= 1) return 0;
752 
753  // Stable sort by head_var so that for a same head_var, the entry are sorted
754  // by Literal as they appear in clause.
755  std::stable_sort(infos.begin(), infos.end(),
756  [](const ArcInfo& a, const ArcInfo& b) {
757  return a.head_var < b.head_var;
758  });
759 
760  // We process ArcInfo with the same head_var toghether.
761  int num_added_constraints = 0;
762  auto* solver = model->GetOrCreate<SatSolver>();
763  for (int i = 0; i < infos.size();) {
764  const int start = i;
765  const IntegerVariable head_var = infos[start].head_var;
766  for (i++; i < infos.size() && infos[i].head_var == head_var; ++i) {
767  }
768  const absl::Span<ArcInfo> arcs(&infos[start], i - start);
769 
770  // Skip single arcs since it will already be fully propagated.
771  if (arcs.size() < 2) continue;
772 
773  // Heuristic. Look for full or almost full clauses. We could add
774  // GreaterThanAtLeastOneOf() with more enforcement literals. TODO(user):
775  // experiments.
776  if (arcs.size() + 1 < clause.size()) continue;
777 
778  std::vector<IntegerVariable> vars;
779  std::vector<IntegerValue> offsets;
780  std::vector<Literal> selectors;
781  std::vector<Literal> enforcements;
782 
783  int j = 0;
784  for (const Literal l : clause) {
785  bool added = false;
786  for (; j < arcs.size() && l == arcs[j].presence_literals.front(); ++j) {
787  added = true;
788  vars.push_back(arcs[j].tail_var);
789  offsets.push_back(arcs[j].offset);
790 
791  // Note that duplicate selector are supported.
792  //
793  // TODO(user): If we support variable offset, we should regroup the arcs
794  // into one (tail + offset <= head) though, instead of having too
795  // identical entries.
796  selectors.push_back(l);
797  }
798  if (!added) {
799  enforcements.push_back(l.Negated());
800  }
801  }
802 
803  // No point adding a constraint if there is not at least two different
804  // literals in selectors.
805  if (enforcements.size() + 1 == clause.size()) continue;
806 
807  ++num_added_constraints;
808  model->Add(GreaterThanAtLeastOneOf(head_var, vars, offsets, selectors,
809  enforcements));
810  if (!solver->FinishPropagation()) return num_added_constraints;
811  }
812  return num_added_constraints;
813 }
814 
815 int PrecedencesPropagator::
816  AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(Model* model) {
817  auto* time_limit = model->GetOrCreate<TimeLimit>();
818  auto* solver = model->GetOrCreate<SatSolver>();
819 
820  // Fill the set of incoming conditional arcs for each variables.
822  for (ArcIndex arc_index(0); arc_index < arcs_.size(); ++arc_index) {
823  const ArcInfo& arc = arcs_[arc_index];
824 
825  // Only keep arc that have a fixed offset and a single presence_literals.
826  if (arc.offset_var != kNoIntegerVariable) continue;
827  if (arc.tail_var == arc.head_var) continue;
828  if (arc.presence_literals.size() != 1) continue;
829 
830  if (arc.head_var >= incoming_arcs_.size()) {
831  incoming_arcs_.resize(arc.head_var.value() + 1);
832  }
833  incoming_arcs_[arc.head_var].push_back(arc_index);
834  }
835 
836  int num_added_constraints = 0;
837  for (IntegerVariable target(0); target < incoming_arcs_.size(); ++target) {
838  if (incoming_arcs_[target].size() <= 1) continue;
839  if (time_limit->LimitReached()) return num_added_constraints;
840 
841  // Detect set of incoming arcs for which at least one must be present.
842  // TODO(user): Find more than one disjoint set of incoming arcs.
843  // TODO(user): call MinimizeCoreWithPropagation() on the clause.
844  solver->Backtrack(0);
845  if (solver->IsModelUnsat()) return num_added_constraints;
846  std::vector<Literal> clause;
847  for (const ArcIndex arc_index : incoming_arcs_[target]) {
848  const Literal literal = arcs_[arc_index].presence_literals.front();
849  if (solver->Assignment().LiteralIsFalse(literal)) continue;
850 
851  const int old_level = solver->CurrentDecisionLevel();
852  solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated());
853  if (solver->IsModelUnsat()) return num_added_constraints;
854  const int new_level = solver->CurrentDecisionLevel();
855  if (new_level <= old_level) {
856  clause = solver->GetLastIncompatibleDecisions();
857  break;
858  }
859  }
860  solver->Backtrack(0);
861 
862  if (clause.size() > 1) {
863  // Extract the set of arc for which at least one must be present.
864  const std::set<Literal> clause_set(clause.begin(), clause.end());
865  std::vector<ArcIndex> arcs_in_clause;
866  for (const ArcIndex arc_index : incoming_arcs_[target]) {
867  const Literal literal(arcs_[arc_index].presence_literals.front());
868  if (gtl::ContainsKey(clause_set, literal.Negated())) {
869  arcs_in_clause.push_back(arc_index);
870  }
871  }
872 
873  VLOG(2) << arcs_in_clause.size() << "/" << incoming_arcs_[target].size();
874 
875  ++num_added_constraints;
876  std::vector<IntegerVariable> vars;
877  std::vector<IntegerValue> offsets;
878  std::vector<Literal> selectors;
879  for (const ArcIndex a : arcs_in_clause) {
880  vars.push_back(arcs_[a].tail_var);
881  offsets.push_back(arcs_[a].offset);
882  selectors.push_back(Literal(arcs_[a].presence_literals.front()));
883  }
884  model->Add(GreaterThanAtLeastOneOf(target, vars, offsets, selectors));
885  if (!solver->FinishPropagation()) return num_added_constraints;
886  }
887  }
888 
889  return num_added_constraints;
890 }
891 
893  VLOG(1) << "Detecting GreaterThanAtLeastOneOf() constraints...";
894  auto* time_limit = model->GetOrCreate<TimeLimit>();
895  auto* solver = model->GetOrCreate<SatSolver>();
896  auto* clauses = model->GetOrCreate<LiteralWatchers>();
897  int num_added_constraints = 0;
898 
899  // We have two possible approaches. For now, we prefer the first one except if
900  // there is too many clauses in the problem.
901  //
902  // TODO(user): Do more extensive experiment. Remove the second approach as
903  // it is more time consuming? or identify when it make sense. Note that the
904  // first approach also allows to use "incomplete" at least one between arcs.
905  if (clauses->AllClausesInCreationOrder().size() < 1e6) {
906  // TODO(user): This does not take into account clause of size 2 since they
907  // are stored in the BinaryImplicationGraph instead. Some ideas specific
908  // to size 2:
909  // - There can be a lot of such clauses, but it might be nice to consider
910  // them. we need to experiments.
911  // - The automatic clause detection might be a better approach and it
912  // could be combined with probing.
913  for (const SatClause* clause : clauses->AllClausesInCreationOrder()) {
914  if (time_limit->LimitReached()) return num_added_constraints;
915  if (solver->IsModelUnsat()) return num_added_constraints;
916  num_added_constraints += AddGreaterThanAtLeastOneOfConstraintsFromClause(
917  clause->AsSpan(), model);
918  }
919  } else {
920  num_added_constraints +=
921  AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(model);
922  }
923 
924  VLOG(1) << "Added " << num_added_constraints
925  << " GreaterThanAtLeastOneOf() constraints.";
926  return num_added_constraints;
927 }
928 
929 } // namespace sat
930 } // namespace operations_research
var
IntVar * var
Definition: expr_array.cc:1858
tail
int64 tail
Definition: routing_flow.cc:127
operations_research::sat::LowerBound
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1450
VLOG
#define VLOG(verboselevel)
Definition: base/logging.h:978
absl::StrongVector::push_back
void push_back(const value_type &x)
Definition: strong_vector.h:158
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
max
int64 max
Definition: alldiff_cst.cc:139
operations_research::sat::GenericLiteralWatcher::WatchLowerBound
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition: integer.h:1356
operations_research::SparseBitset::ClearAndResize
void ClearAndResize(IntegerType size)
Definition: bitset.h:780
absl::StrongVector::size
size_type size() const
Definition: strong_vector.h:147
logging.h
operations_research::sat::SatSolver
Definition: sat_solver.h:58
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
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
cleanup.h
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::PrecedencesPropagator::Untrail
void Untrail(const Trail &trail, int trail_index) final
Definition: precedences.cc:108
operations_research::sat::NegationOf
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
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::SatPropagator::propagation_trail_index_
int propagation_trail_index_
Definition: sat_base.h:507
operations_research::sat::Literal::Negated
Literal Negated() const
Definition: sat_base.h:91
absl::MakeCleanup
absl::Cleanup< absl::decay_t< Callback > > MakeCleanup(Callback &&callback)
Definition: cleanup.h:120
operations_research::sat::PrecedencesPropagator::AddPrecedenceReason
void AddPrecedenceReason(int arc_index, IntegerValue min_offset, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
Definition: precedences.cc:209
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
clause.h
operations_research::sat::Trail::Index
int Index() const
Definition: sat_base.h:378
operations_research::sat::IntegerTrail::NumIntegerVariables
IntegerVariable NumIntegerVariables() const
Definition: integer.h:558
operations_research::SparseBitset::Set
void Set(IntegerType index)
Definition: bitset.h:805
DCHECK_NE
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
a
int64 a
Definition: constraint_solver/table.cc:42
operations_research::sat::IntegerTrail::UpperBoundAsLiteral
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1318
operations_research::sat::PrecedencesPropagator::ComputePrecedences
void ComputePrecedences(const std::vector< IntegerVariable > &vars, std::vector< IntegerPrecedences > *output)
Definition: precedences.cc:132
time_limit
SharedTimeLimit * time_limit
Definition: cp_model_solver.cc:2103
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
precedences.h
gtl::STLSortAndRemoveDuplicates
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
operations_research::sat::LiteralWatchers
Definition: clause.h:160
absl::StrongVector::pop_back
void pop_back()
Definition: strong_vector.h:168
operations_research::sat::Trail::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
operations_research::sat::IntegerTrail::IsIgnoredLiteral
Literal IsIgnoredLiteral(IntegerVariable i) const
Definition: integer.h:623
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::SparseBitset::PositionsSetAtLeastOnce
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition: bitset.h:815
operations_research::sat::PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints
int AddGreaterThanAtLeastOneOfConstraints(Model *model)
Definition: precedences.cc:892
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
cp_constraints.h
DCHECK
#define DCHECK(condition)
Definition: base/logging.h:884
operations_research::ArcIndex
int32 ArcIndex
Definition: ebert_graph.h:201
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Trail::CurrentDecisionLevel
int CurrentDecisionLevel() const
Definition: sat_base.h:355
operations_research::sat::Literal
Definition: sat_base.h:64
absl::StrongVector
Definition: strong_vector.h:76
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
operations_research::sat::IntegerTrail::RelaxLinearReason
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
Definition: integer.cc:785
absl::StrongVector::back
reference back()
Definition: strong_vector.h:174
DCHECK_EQ
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
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::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::glop::Index
int32 Index
Definition: lp_types.h:37
operations_research::sat::PrecedencesPropagator::IntegerPrecedences
Definition: precedences.h:111
CHECK_NE
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
operations_research::sat::IntegerTrail::IsCurrentlyIgnored
bool IsCurrentlyIgnored(IntegerVariable i) const
Definition: integer.h:618
operations_research::sat::PrecedencesPropagator::Propagate
bool Propagate() final
Definition: precedences.cc:42
operations_research::sat::SatClause
Definition: clause.h:51
head
int64 head
Definition: routing_flow.cc:128
literal
Literal literal
Definition: optimization.cc:84
operations_research::sat::IntegerTrail::IsOptional
bool IsOptional(IntegerVariable i) const
Definition: integer.h:615
operations_research::sat::PrecedencesPropagator::PropagateOutgoingArcs
bool PropagateOutgoingArcs(IntegerVariable var)
Definition: precedences.cc:95
absl::StrongVector::front
reference front()
Definition: strong_vector.h:172
CHECK
#define CHECK(condition)
Definition: base/logging.h:495
operations_research::sat::GreaterThanAtLeastOneOf
std::function< void(Model *)> GreaterThanAtLeastOneOf(IntegerVariable target_var, const absl::Span< const IntegerVariable > vars, const absl::Span< const IntegerValue > offsets, const absl::Span< const Literal > selectors)
Definition: cp_constraints.h:123
operations_research::sat::VariablesAssignment::LiteralIsFalse
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
operations_research::sat::Trail
Definition: sat_base.h:233
gtl::ContainsKey
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170