Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
precedences.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <stdint.h>
17
18#include <algorithm>
19#include <deque>
20#include <string>
21#include <utility>
22#include <vector>
23
24#include "absl/cleanup/cleanup.h"
25#include "absl/container/btree_set.h"
26#include "absl/container/flat_hash_map.h"
27#include "absl/container/flat_hash_set.h"
28#include "absl/container/inlined_vector.h"
29#include "absl/log/check.h"
30#include "absl/log/log.h"
31#include "absl/log/vlog_is_on.h"
32#include "absl/types/span.h"
37#include "ortools/graph/graph.h"
39#include "ortools/sat/clause.h"
41#include "ortools/sat/integer.h"
43#include "ortools/sat/model.h"
47#include "ortools/sat/util.h"
48#include "ortools/util/bitset.h"
52
53namespace operations_research {
54namespace sat {
55
57 IntegerValue ub) {
58 expr.CanonicalizeAndUpdateBounds(lb, ub);
59
60 if (expr.coeffs[0] == 0 || expr.coeffs[1] == 0) {
61 // This class handles only binary relationships, let something else handle
62 // the case where there is actually a single variable.
63 return false;
64 }
65
66 // Add to root_relations_.
67 //
68 // TODO(user): AddInternal() only returns true if this is the first relation
69 // between head and tail. But we can still avoid an extra lookup.
70 const bool add_ub = ub < LevelZeroUpperBound(expr);
71 LinearExpression2 expr_for_lb = expr;
72 expr_for_lb.Negate();
73 const bool add_lb = lb > -LevelZeroUpperBound(expr_for_lb);
74 if (!add_ub && !add_lb) {
75 return false;
76 }
77
78 if (add_ub) {
79 AddInternal(expr, ub);
80 }
81 if (add_lb) {
82 AddInternal(expr_for_lb, -lb);
83 }
84
85 // If we are not built, make sure there is enough room in the graph.
86 // TODO(user): Alternatively, force caller to do a Resize().
87 const int max_node =
88 std::max(PositiveVariable(expr.vars[0]), PositiveVariable(expr.vars[1]))
89 .value() +
90 1;
91 if (!is_built_ && max_node >= graph_.num_nodes()) {
92 graph_.AddNode(max_node);
93 }
94 return true;
95}
96
98 IntegerValue ub) {
99 return AddBounds(expr, kMinIntegerValue, ub);
100}
101
103 absl::Span<const Literal> enforcements, LinearExpression2 expr,
104 IntegerValue rhs) {
106 if (expr.coeffs[0] == 0 || expr.coeffs[1] == 0) {
107 return;
108 }
109
110 // This must be currently true.
111 if (DEBUG_MODE) {
112 for (const Literal l : enforcements) {
113 CHECK(trail_->Assignment().LiteralIsTrue(l));
114 }
115 }
116
117 if (enforcements.empty() || trail_->CurrentDecisionLevel() == 0) {
118 AddUpperBound(expr, rhs);
119 return;
120 }
121
122 const IntegerValue gcd = expr.DivideByGcd();
123 rhs = FloorRatio(rhs, gcd);
124
125 // Ignore if no better than best_relations, otherwise increase it.
126 {
127 const auto [it, inserted] = best_relations_.insert({expr, rhs});
128 if (!inserted) {
129 if (rhs >= it->second) return; // Ignore.
130 it->second = rhs;
131 }
132 }
133
134 const int new_index = conditional_stack_.size();
135 const auto [it, inserted] = conditional_relations_.insert({expr, new_index});
136 if (inserted) {
137 CreateLevelEntryIfNeeded();
138 conditional_stack_.emplace_back(/*prev_entry=*/-1, rhs, expr, enforcements);
139
140 if (expr.coeffs[0] == 1 && expr.coeffs[1] == 1) {
141 const int new_size =
142 std::max(expr.vars[0].value(), expr.vars[1].value()) + 1;
143 if (new_size > conditional_after_.size()) {
144 conditional_after_.resize(new_size);
145 }
146 conditional_after_[expr.vars[0]].push_back(NegationOf(expr.vars[1]));
147 conditional_after_[expr.vars[1]].push_back(NegationOf(expr.vars[0]));
148 }
149 } else {
150 // We should only decrease because we ignored entry worse than the one in
151 // best_relations_.
152 const int prev_entry = it->second;
153 DCHECK_LT(rhs, conditional_stack_[prev_entry].rhs);
154
155 // Update.
156 it->second = new_index;
157 CreateLevelEntryIfNeeded();
158 conditional_stack_.emplace_back(prev_entry, rhs, expr, enforcements);
159 }
160}
161
162void PrecedenceRelations::CreateLevelEntryIfNeeded() {
163 const int current = trail_->CurrentDecisionLevel();
164 if (!level_to_stack_size_.empty() &&
165 level_to_stack_size_.back().first == current)
166 return;
167 level_to_stack_size_.push_back({current, conditional_stack_.size()});
168}
169
170// We only pop what is needed.
172 while (!level_to_stack_size_.empty() &&
173 level_to_stack_size_.back().first > level) {
174 const int target = level_to_stack_size_.back().second;
175 DCHECK_GE(conditional_stack_.size(), target);
176 while (conditional_stack_.size() > target) {
177 const ConditionalEntry& back = conditional_stack_.back();
178 if (back.prev_entry != -1) {
179 conditional_relations_[back.key] = back.prev_entry;
180 UpdateBestRelation(back.key, conditional_stack_[back.prev_entry].rhs);
181 } else {
182 UpdateBestRelation(back.key, kMaxIntegerValue);
183 conditional_relations_.erase(back.key);
184
185 if (back.key.coeffs[0] == 1 && back.key.coeffs[1] == 1) {
186 DCHECK_EQ(conditional_after_[back.key.vars[0]].back(),
187 NegationOf(back.key.vars[1]));
188 DCHECK_EQ(conditional_after_[back.key.vars[1]].back(),
189 NegationOf(back.key.vars[0]));
190 conditional_after_[back.key.vars[0]].pop_back();
191 conditional_after_[back.key.vars[1]].pop_back();
192 }
193 }
194 conditional_stack_.pop_back();
195 }
196 level_to_stack_size_.pop_back();
197 }
198}
199
201 LinearExpression2 expr) const {
203 const IntegerValue gcd = expr.DivideByGcd();
204 const auto it = root_relations_.find(expr);
205 if (it != root_relations_.end()) {
206 return CapProdI(it->second, gcd);
207 }
208 return kMaxIntegerValue;
209}
210
212 LinearExpression2 expr, IntegerValue ub,
213 std::vector<Literal>* literal_reason,
214 std::vector<IntegerLiteral>* /*unused*/) const {
216 if (ub >= LevelZeroUpperBound(expr)) return;
217 const IntegerValue gcd = expr.DivideByGcd();
218 const auto it = conditional_relations_.find(expr);
219 DCHECK(it != conditional_relations_.end());
220
221 const ConditionalEntry& entry = conditional_stack_[it->second];
222 if (DEBUG_MODE) {
223 for (const Literal l : entry.enforcements) {
224 CHECK(trail_->Assignment().LiteralIsTrue(l));
225 }
226 }
227 DCHECK_EQ(CapProdI(gcd, entry.rhs), UpperBound(expr));
228 DCHECK_LE(CapProdI(gcd, entry.rhs), ub);
229 for (const Literal l : entry.enforcements) {
230 literal_reason->push_back(l.Negated());
231 }
232}
233
236 const IntegerValue gcd = expr.DivideByGcd();
237 const auto it = best_relations_.find(expr);
238 if (it != best_relations_.end()) {
239 return CapProdI(gcd, it->second);
240 }
241 DCHECK(!root_relations_.contains(expr));
242 DCHECK(!conditional_relations_.contains(expr));
243 return kMaxIntegerValue;
244}
245
247 if (is_built_) return;
248 is_built_ = true;
249
250 const int num_nodes = graph_.num_nodes();
252 before(num_nodes);
253
254 // We will construct a graph with the current relation from all_relations_.
255 // And use this to compute the "closure".
256 CHECK(arc_offsets_.empty());
257 graph_.ReserveArcs(2 * root_relations_.size());
258 std::vector<std::pair<LinearExpression2, IntegerValue>> root_relations_sorted(
259 root_relations_.begin(), root_relations_.end());
260 std::sort(root_relations_sorted.begin(), root_relations_sorted.end());
261 for (const auto [var_pair, negated_offset] : root_relations_sorted) {
262 // TODO(user): Support negative offset?
263 //
264 // Note that if we only have >= 0 ones, if we do have a cycle, we could
265 // make sure all variales are the same, and otherwise, we have a DAG or a
266 // conflict.
267 const IntegerValue offset = -negated_offset;
268 if (offset < 0) continue;
269
270 if (var_pair.coeffs[0] != 1 || var_pair.coeffs[1] != 1) {
271 // TODO(user): Support non-1 coefficients.
272 continue;
273 }
274
275 // We have two arcs.
276 {
277 const IntegerVariable tail = var_pair.vars[0];
278 const IntegerVariable head = NegationOf(var_pair.vars[1]);
279 graph_.AddArc(tail.value(), head.value());
280 arc_offsets_.push_back(offset);
281 CHECK_LT(var_pair.vars[1], before.size());
282 before[head].push_back(tail);
283 }
284 {
285 const IntegerVariable tail = var_pair.vars[1];
286 const IntegerVariable head = NegationOf(var_pair.vars[0]);
287 graph_.AddArc(tail.value(), head.value());
288 arc_offsets_.push_back(offset);
289 CHECK_LT(var_pair.vars[1], before.size());
290 before[head].push_back(tail);
291 }
292 }
293
294 std::vector<int> permutation;
295 graph_.Build(&permutation);
296 util::Permute(permutation, &arc_offsets_);
297
298 // Is it a DAG?
299 // Get a topological order of the DAG formed by all the arcs that are present.
300 //
301 // TODO(user): This can fail if we don't have a DAG. We could just skip Bad
302 // edges instead, and have a sub-DAG as an heuristic. Or analyze the arc
303 // weight and make sure cycle are not an issue. We can also start with arcs
304 // with strictly positive weight.
305 //
306 // TODO(user): Only explore the sub-graph reachable from "vars".
307 DenseIntStableTopologicalSorter sorter(num_nodes);
308 for (int arc = 0; arc < graph_.num_arcs(); ++arc) {
309 sorter.AddEdge(graph_.Tail(arc), graph_.Head(arc));
310 }
311 int next;
312 bool graph_has_cycle = false;
313 topological_order_.clear();
314 while (sorter.GetNext(&next, &graph_has_cycle, nullptr)) {
315 topological_order_.push_back(IntegerVariable(next));
316 if (graph_has_cycle) {
317 is_dag_ = false;
318 return;
319 }
320 }
321 is_dag_ = !graph_has_cycle;
322
323 // Lets build full precedences if we don't have too many of them.
324 // TODO(user): Also do that if we don't have a DAG?
325 if (!is_dag_) return;
326
327 int work = 0;
328 const int kWorkLimit = 1e6;
329 for (const IntegerVariable tail_var : topological_order_) {
330 if (++work > kWorkLimit) break;
331 for (const int arc : graph_.OutgoingArcs(tail_var.value())) {
332 DCHECK_EQ(tail_var.value(), graph_.Tail(arc));
333 const IntegerVariable head_var = IntegerVariable(graph_.Head(arc));
334 const IntegerValue arc_offset = arc_offsets_[arc];
335
336 if (++work > kWorkLimit) break;
337 if (AddInternal(LinearExpression2::Difference(tail_var, head_var),
338 -arc_offset)) {
339 before[head_var].push_back(tail_var);
340 }
341
342 for (const IntegerVariable before_var : before[tail_var]) {
343 if (++work > kWorkLimit) break;
344 LinearExpression2 expr_for_key(before_var, tail_var, 1, -1);
345 expr_for_key.SimpleCanonicalization();
346 const IntegerValue offset =
347 -root_relations_.at(expr_for_key) + arc_offset;
348 if (AddInternal(LinearExpression2::Difference(before_var, head_var),
349 -offset)) {
350 before[head_var].push_back(before_var);
351 }
352 }
353 }
354 }
355
356 VLOG(2) << "Full precedences. Work=" << work
357 << " Relations=" << root_relations_.size();
358}
359
361 absl::Span<const IntegerVariable> vars,
362 std::vector<FullIntegerPrecedence>* output) {
363 output->clear();
364 if (!is_built_) Build();
365 if (!is_dag_) return;
366
367 VLOG(2) << "num_nodes: " << graph_.num_nodes()
368 << " num_arcs: " << graph_.num_arcs() << " is_dag: " << is_dag_;
369
370 // Compute all precedences.
371 // We loop over the node in topological order, and we maintain for all
372 // variable we encounter, the list of "to_consider" variables that are before.
373 //
374 // TODO(user): use vector of fixed size.
375 absl::flat_hash_set<IntegerVariable> is_interesting;
376 absl::flat_hash_set<IntegerVariable> to_consider(vars.begin(), vars.end());
377 absl::flat_hash_map<IntegerVariable,
378 absl::flat_hash_map<IntegerVariable, IntegerValue>>
379 vars_before_with_offset;
380 absl::flat_hash_map<IntegerVariable, IntegerValue> tail_map;
381 for (const IntegerVariable tail_var : topological_order_) {
382 if (!to_consider.contains(tail_var) &&
383 !vars_before_with_offset.contains(tail_var)) {
384 continue;
385 }
386
387 // We copy the data for tail_var here, because the pointer is not stable.
388 // TODO(user): optimize when needed.
389 tail_map.clear();
390 {
391 const auto it = vars_before_with_offset.find(tail_var);
392 if (it != vars_before_with_offset.end()) {
393 tail_map = it->second;
394 }
395 }
396
397 for (const int arc : graph_.OutgoingArcs(tail_var.value())) {
398 CHECK_EQ(tail_var.value(), graph_.Tail(arc));
399 const IntegerVariable head_var = IntegerVariable(graph_.Head(arc));
400 const IntegerValue arc_offset = arc_offsets_[arc];
401
402 // No need to create an empty entry in this case.
403 if (tail_map.empty() && !to_consider.contains(tail_var)) continue;
404
405 auto& to_update = vars_before_with_offset[head_var];
406 for (const auto& [var_before, offset] : tail_map) {
407 if (!to_update.contains(var_before)) {
408 to_update[var_before] = arc_offset + offset;
409 } else {
410 to_update[var_before] =
411 std::max(arc_offset + offset, to_update[var_before]);
412 }
413 }
414 if (to_consider.contains(tail_var)) {
415 if (!to_update.contains(tail_var)) {
416 to_update[tail_var] = arc_offset;
417 } else {
418 to_update[tail_var] = std::max(arc_offset, to_update[tail_var]);
419 }
420 }
421
422 // Small filtering heuristic: if we have (before) < tail, and tail < head,
423 // we really do not need to list (before, tail) < head. We only need that
424 // if the list of variable before head contains some variable that are not
425 // already before tail.
426 if (to_update.size() > tail_map.size() + 1) {
427 is_interesting.insert(head_var);
428 } else {
429 is_interesting.erase(head_var);
430 }
431 }
432
433 // Extract the output for tail_var. Because of the topological ordering, the
434 // data for tail_var is already final now.
435 //
436 // TODO(user): Release the memory right away.
437 if (!is_interesting.contains(tail_var)) continue;
438 if (tail_map.size() == 1) continue;
439
441 data.var = tail_var;
442 IntegerValue min_offset = kMaxIntegerValue;
443 for (int i = 0; i < vars.size(); ++i) {
444 const auto offset_it = tail_map.find(vars[i]);
445 if (offset_it == tail_map.end()) continue;
446 data.indices.push_back(i);
447 data.offsets.push_back(offset_it->second);
448 min_offset = std::min(data.offsets.back(), min_offset);
449 }
450 output->push_back(std::move(data));
451 }
452}
453
455 absl::Span<const IntegerVariable> vars,
456 std::vector<PrecedenceData>* output) {
457 // +1 for the negation.
458 const int needed_size =
459 std::max(after_.size(), conditional_after_.size()) + 1;
460 var_to_degree_.resize(needed_size);
461 var_to_last_index_.resize(needed_size);
462 var_with_positive_degree_.resize(needed_size);
463 tmp_precedences_.clear();
464
465 // We first compute the degree/size in order to perform the transposition.
466 // Note that we also remove duplicates.
467 int num_relevants = 0;
468 IntegerVariable* var_with_positive_degree = var_with_positive_degree_.data();
469 int* var_to_degree = var_to_degree_.data();
470 int* var_to_last_index = var_to_last_index_.data();
471 const auto process = [&](int index, absl::Span<const IntegerVariable> v) {
472 for (const IntegerVariable after : v) {
473 DCHECK_LT(after, needed_size);
474 if (var_to_degree[after.value()] == 0) {
475 var_with_positive_degree[num_relevants++] = after;
476 } else {
477 // We do not want duplicates.
478 if (var_to_last_index[after.value()] == index) continue;
479 }
480
481 tmp_precedences_.push_back({after, index});
482 var_to_degree[after.value()]++;
483 var_to_last_index[after.value()] = index;
484 }
485 };
486
487 for (int index = 0; index < vars.size(); ++index) {
488 const IntegerVariable var = vars[index];
489 if (var < after_.size()) {
490 process(index, after_[var]);
491 }
492 if (var < conditional_after_.size()) {
493 process(index, conditional_after_[var]);
494 }
495 }
496
497 // Permute tmp_precedences_ into the output to put it in the correct order.
498 // For that we transform var_to_degree to point to the first position of
499 // each lbvar in the output vector.
500 int start = 0;
501 for (int i = 0; i < num_relevants; ++i) {
502 const IntegerVariable var = var_with_positive_degree[i];
503 const int degree = var_to_degree[var.value()];
504 if (degree > 1) {
505 var_to_degree[var.value()] = start;
506 start += degree;
507 } else {
508 // Optimization: we remove degree one relations.
509 var_to_degree[var.value()] = -1;
510 }
511 }
512
513 output->resize(start);
514 for (const auto& precedence : tmp_precedences_) {
515 // Note that it is okay to increase the -1 pos since they appear only once.
516 const int pos = var_to_degree[precedence.var.value()]++;
517 if (pos < 0) continue;
518 (*output)[pos] = precedence;
519 }
520
521 // Cleanup var_to_degree, note that we don't need to clean
522 // var_to_last_index_.
523 for (int i = 0; i < num_relevants; ++i) {
524 const IntegerVariable var = var_with_positive_degree[i];
525 var_to_degree[var.value()] = 0;
526 }
527}
528
529namespace {
530
531void AppendLowerBoundReasonIfValid(IntegerVariable var,
532 const IntegerTrail& i_trail,
533 std::vector<IntegerLiteral>* reason) {
534 if (var != kNoIntegerVariable) {
535 reason->push_back(i_trail.LowerBoundAsLiteral(var));
536 }
537}
538
539} // namespace
540
542 if (!VLOG_IS_ON(1)) return;
543 if (shared_stats_ == nullptr) return;
544 std::vector<std::pair<std::string, int64_t>> stats;
545 stats.push_back({"precedences/num_cycles", num_cycles_});
546 stats.push_back({"precedences/num_pushes", num_pushes_});
547 stats.push_back(
548 {"precedences/num_enforcement_pushes", num_enforcement_pushes_});
549 shared_stats_->AddStats(stats);
550}
551
553
556 const Literal literal = (*trail_)[propagation_trail_index_++];
557 if (literal.Index() >= literal_to_new_impacted_arcs_.size()) continue;
558
559 // IMPORTANT: Because of the way Untrail() work, we need to add all the
560 // potential arcs before we can abort. It is why we iterate twice here.
561 for (const ArcIndex arc_index :
562 literal_to_new_impacted_arcs_[literal.Index()]) {
563 if (--arc_counts_[arc_index] == 0) {
564 const ArcInfo& arc = arcs_[arc_index];
565 PushConditionalRelations(arc);
566 impacted_arcs_[arc.tail_var].push_back(arc_index);
567 }
568 }
569
570 // Iterate again to check for a propagation and indirectly update
571 // modified_vars_.
572 for (const ArcIndex arc_index :
573 literal_to_new_impacted_arcs_[literal.Index()]) {
574 if (arc_counts_[arc_index] > 0) continue;
575 const ArcInfo& arc = arcs_[arc_index];
576 const IntegerValue new_head_lb =
577 integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
578 if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
579 if (!EnqueueAndCheck(arc, new_head_lb, trail_)) return false;
580 }
581 }
582 }
583
584 // Do the actual propagation of the IntegerVariable bounds.
585 InitializeBFQueueWithModifiedNodes();
586 if (!BellmanFordTarjan(trail_)) return false;
587
588 // We can only test that no propagation is left if we didn't enqueue new
589 // literal in the presence of optional variables.
590 //
591 // TODO(user): Because of our code to deal with InPropagationLoop(), this is
592 // not always true. Find a cleaner way to DCHECK() while not failing in this
593 // corner case.
594 if (/*DISABLES CODE*/ (false) &&
595 propagation_trail_index_ == trail_->Index()) {
596 DCHECK(NoPropagationLeft(*trail_));
597 }
598
599 // Propagate the presence literals of the arcs that can't be added.
600 PropagateOptionalArcs(trail_);
601
602 // Clean-up modified_vars_ to do as little as possible on the next call.
603 modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
604 return true;
605}
606
608 CHECK_NE(var, kNoIntegerVariable);
609 if (var >= impacted_arcs_.size()) return true;
610 for (const ArcIndex arc_index : impacted_arcs_[var]) {
611 const ArcInfo& arc = arcs_[arc_index];
612 const IntegerValue new_head_lb =
613 integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
614 if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
615 if (!EnqueueAndCheck(arc, new_head_lb, trail_)) return false;
616 }
617 }
618 return true;
619}
620
621// TODO(user): Remove literal fixed at level zero from there.
622void PrecedencesPropagator::PushConditionalRelations(const ArcInfo& arc) {
623 // We currently do not handle variable size in the reasons.
624 // TODO(user): we could easily take a level zero ArcOffset() instead, or
625 // add this to the reason though.
626 if (arc.offset_var != kNoIntegerVariable) return;
627 const IntegerValue offset = ArcOffset(arc);
628 relations_->PushConditionalRelation(
629 arc.presence_literals,
630 LinearExpression2::Difference(arc.tail_var, arc.head_var), -offset);
631}
632
633void PrecedencesPropagator::Untrail(const Trail& trail, int trail_index) {
634 if (propagation_trail_index_ > trail_index) {
635 // This means that we already propagated all there is to propagate
636 // at the level trail_index, so we can safely clear modified_vars_ in case
637 // it wasn't already done.
638 modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
639 }
640 while (propagation_trail_index_ > trail_index) {
641 const Literal literal = trail[--propagation_trail_index_];
642 if (literal.Index() >= literal_to_new_impacted_arcs_.size()) continue;
643 for (const ArcIndex arc_index :
644 literal_to_new_impacted_arcs_[literal.Index()]) {
645 if (arc_counts_[arc_index]++ == 0) {
646 const ArcInfo& arc = arcs_[arc_index];
647 impacted_arcs_[arc.tail_var].pop_back();
648 }
649 }
650 }
651}
652
653void PrecedencesPropagator::AdjustSizeFor(IntegerVariable i) {
654 const int index = std::max(i.value(), NegationOf(i).value());
655 if (index >= impacted_arcs_.size()) {
656 // TODO(user): only watch lower bound of the relevant variable instead
657 // of watching everything in [0, max_index_of_variable_used_in_this_class).
658 for (IntegerVariable var(impacted_arcs_.size()); var <= index; ++var) {
659 watcher_->WatchLowerBound(var, watcher_id_);
660 }
661 impacted_arcs_.resize(index + 1);
662 impacted_potential_arcs_.resize(index + 1);
663 }
664}
665
666void PrecedencesPropagator::AddArc(
667 IntegerVariable tail, IntegerVariable head, IntegerValue offset,
668 IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
669 AdjustSizeFor(tail);
670 AdjustSizeFor(head);
671 if (offset_var != kNoIntegerVariable) AdjustSizeFor(offset_var);
672
673 // This arc is present iff all the literals here are true.
674 absl::InlinedVector<Literal, 6> enforcement_literals;
675 {
676 for (const Literal l : presence_literals) {
677 enforcement_literals.push_back(l);
678 }
679 gtl::STLSortAndRemoveDuplicates(&enforcement_literals);
680
681 if (trail_->CurrentDecisionLevel() == 0) {
682 int new_size = 0;
683 for (const Literal l : enforcement_literals) {
684 if (trail_->Assignment().LiteralIsTrue(Literal(l))) {
685 continue; // At true, ignore this literal.
686 } else if (trail_->Assignment().LiteralIsFalse(Literal(l))) {
687 return; // At false, ignore completely this arc.
688 }
689 enforcement_literals[new_size++] = l;
690 }
691 enforcement_literals.resize(new_size);
692 }
693 }
694
695 if (head == tail) {
696 // A self-arc is either plain SAT or plain UNSAT or it forces something on
697 // the given offset_var or presence_literal_index. In any case it could be
698 // presolved in something more efficient.
699 VLOG(1) << "Self arc! This could be presolved. "
700 << "var:" << tail << " offset:" << offset
701 << " offset_var:" << offset_var
702 << " conditioned_by:" << presence_literals;
703 }
704
705 // Remove the offset_var if it is fixed.
706 // TODO(user): We should also handle the case where tail or head is fixed.
707 if (offset_var != kNoIntegerVariable) {
708 const IntegerValue lb = integer_trail_->LevelZeroLowerBound(offset_var);
709 if (lb == integer_trail_->LevelZeroUpperBound(offset_var)) {
710 offset += lb;
711 offset_var = kNoIntegerVariable;
712 }
713 }
714
715 // Deal first with impacted_potential_arcs_/potential_arcs_.
716 if (!enforcement_literals.empty()) {
717 const OptionalArcIndex arc_index(potential_arcs_.size());
718 potential_arcs_.push_back(
719 {tail, head, offset, offset_var, enforcement_literals});
720 impacted_potential_arcs_[tail].push_back(arc_index);
721 impacted_potential_arcs_[NegationOf(head)].push_back(arc_index);
722 if (offset_var != kNoIntegerVariable) {
723 impacted_potential_arcs_[offset_var].push_back(arc_index);
724 }
725 }
726
727 // Now deal with impacted_arcs_/arcs_.
728 struct InternalArc {
729 IntegerVariable tail_var;
730 IntegerVariable head_var;
731 IntegerVariable offset_var;
732 };
733 std::vector<InternalArc> to_add;
734 if (offset_var == kNoIntegerVariable) {
735 // a + offset <= b and -b + offset <= -a
736 to_add.push_back({tail, head, kNoIntegerVariable});
737 to_add.push_back({NegationOf(head), NegationOf(tail), kNoIntegerVariable});
738 } else {
739 // tail (a) and offset_var (b) are symmetric, so we add:
740 // - a + b + offset <= c
741 to_add.push_back({tail, head, offset_var});
742 to_add.push_back({offset_var, head, tail});
743 // - a - c + offset <= -b
744 to_add.push_back({tail, NegationOf(offset_var), NegationOf(head)});
745 to_add.push_back({NegationOf(head), NegationOf(offset_var), tail});
746 // - b - c + offset <= -a
747 to_add.push_back({offset_var, NegationOf(tail), NegationOf(head)});
748 to_add.push_back({NegationOf(head), NegationOf(tail), offset_var});
749 }
750 for (const InternalArc a : to_add) {
751 // Since we add a new arc, we will need to consider its tail during the next
752 // propagation. Note that the size of modified_vars_ will be automatically
753 // updated when new integer variables are created since we register it with
754 // IntegerTrail in this class constructor.
755 //
756 // TODO(user): Adding arcs and then calling Untrail() before Propagate()
757 // will cause this mecanism to break. Find a more robust implementation.
758 //
759 // TODO(user): In some rare corner case, rescanning the whole list of arc
760 // leaving tail_var can make AddVar() have a quadratic complexity where it
761 // shouldn't. A better solution would be to see if this new arc currently
762 // propagate something, and if it does, just update the lower bound of
763 // a.head_var and let the normal "is modified" mecanism handle any eventual
764 // follow up propagations.
765 modified_vars_.Set(a.tail_var);
766
767 // If a.head_var is optional, we can potentially remove some literal from
768 // enforcement_literals.
769 const ArcIndex arc_index(arcs_.size());
770 arcs_.push_back(
771 {a.tail_var, a.head_var, offset, a.offset_var, enforcement_literals});
772 auto& presence_literals = arcs_.back().presence_literals;
773
774 if (presence_literals.empty()) {
775 impacted_arcs_[a.tail_var].push_back(arc_index);
776 } else {
777 for (const Literal l : presence_literals) {
778 if (l.Index() >= literal_to_new_impacted_arcs_.size()) {
779 literal_to_new_impacted_arcs_.resize(l.Index().value() + 1);
780 }
781 literal_to_new_impacted_arcs_[l.Index()].push_back(arc_index);
782 }
783 }
784
785 if (trail_->CurrentDecisionLevel() == 0) {
786 arc_counts_.push_back(presence_literals.size());
787 } else {
788 arc_counts_.push_back(0);
789 for (const Literal l : presence_literals) {
790 if (!trail_->Assignment().LiteralIsTrue(l)) {
791 ++arc_counts_.back();
792 }
793 }
794 CHECK(presence_literals.empty() || arc_counts_.back() > 0);
795 }
796 }
797}
798
800 IntegerVariable i2,
801 IntegerValue offset) {
802 DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
803 if (i1 < impacted_arcs_.size() && i2 < impacted_arcs_.size()) {
804 for (const ArcIndex index : impacted_arcs_[i1]) {
805 const ArcInfo& arc = arcs_[index];
806 if (arc.head_var == i2) {
807 const IntegerValue current = ArcOffset(arc);
808 if (offset <= current) {
809 return false;
810 } else {
811 // TODO(user): Modify arc in place!
812 }
813 break;
814 }
815 }
816 }
817
818 AddPrecedenceWithOffset(i1, i2, offset);
819 return true;
820}
821
822// TODO(user): On jobshop problems with a lot of tasks per machine (500), this
823// takes up a big chunk of the running time even before we find a solution.
824// This is because, for each lower bound changed, we inspect 500 arcs even
825// though they will never be propagated because the other bound is still at the
826// horizon. Find an even sparser algorithm?
827void PrecedencesPropagator::PropagateOptionalArcs(Trail* trail) {
828 for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
829 // The variables are not in increasing order, so we need to continue.
830 if (var >= impacted_potential_arcs_.size()) continue;
831
832 // Note that we can currently check the same ArcInfo up to 3 times, one for
833 // each of the arc variables: tail, NegationOf(head) and offset_var.
834 for (const OptionalArcIndex arc_index : impacted_potential_arcs_[var]) {
835 const ArcInfo& arc = potential_arcs_[arc_index];
836 int num_not_true = 0;
837 Literal to_propagate;
838 for (const Literal l : arc.presence_literals) {
839 if (!trail->Assignment().LiteralIsTrue(l)) {
840 ++num_not_true;
841 to_propagate = l;
842 }
843 }
844 if (num_not_true != 1) continue;
845 if (trail->Assignment().LiteralIsFalse(to_propagate)) continue;
846
847 // Test if this arc can be present or not.
848 // Important arc.tail_var can be different from var here.
849 const IntegerValue tail_lb = integer_trail_->LowerBound(arc.tail_var);
850 const IntegerValue head_ub = integer_trail_->UpperBound(arc.head_var);
851 if (tail_lb + ArcOffset(arc) > head_ub) {
852 integer_reason_.clear();
853 integer_reason_.push_back(
854 integer_trail_->LowerBoundAsLiteral(arc.tail_var));
855 integer_reason_.push_back(
856 integer_trail_->UpperBoundAsLiteral(arc.head_var));
857 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
858 &integer_reason_);
859 literal_reason_.clear();
860 for (const Literal l : arc.presence_literals) {
861 if (l != to_propagate) literal_reason_.push_back(l.Negated());
862 }
863 ++num_enforcement_pushes_;
864 integer_trail_->EnqueueLiteral(to_propagate.Negated(), literal_reason_,
865 integer_reason_);
866 }
867 }
868 }
869}
870
871IntegerValue PrecedencesPropagator::ArcOffset(const ArcInfo& arc) const {
872 return arc.offset + (arc.offset_var == kNoIntegerVariable
873 ? IntegerValue(0)
874 : integer_trail_->LowerBound(arc.offset_var));
875}
876
877bool PrecedencesPropagator::EnqueueAndCheck(const ArcInfo& arc,
878 IntegerValue new_head_lb,
879 Trail* trail) {
880 ++num_pushes_;
881 DCHECK_GT(new_head_lb, integer_trail_->LowerBound(arc.head_var));
882
883 // Compute the reason for new_head_lb.
884 //
885 // TODO(user): do like for clause and keep the negation of
886 // arc.presence_literals? I think we could change the integer.h API to accept
887 // true literal like for IntegerVariable, it is really confusing currently.
888 literal_reason_.clear();
889 for (const Literal l : arc.presence_literals) {
890 literal_reason_.push_back(l.Negated());
891 }
892
893 integer_reason_.clear();
894 integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(arc.tail_var));
895 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
896 &integer_reason_);
897
898 // The code works without this block since Enqueue() below can already take
899 // care of conflicts. However, it is better to deal with the conflict
900 // ourselves because we can be smarter about the reason this way.
901 //
902 // The reason for a "precedence" conflict is always a linear reason
903 // involving the tail lower_bound, the head upper bound and eventually the
904 // size lower bound. Because of that, we can use the RelaxLinearReason()
905 // code.
906 if (new_head_lb > integer_trail_->UpperBound(arc.head_var)) {
907 const IntegerValue slack =
908 new_head_lb - integer_trail_->UpperBound(arc.head_var) - 1;
909 integer_reason_.push_back(
910 integer_trail_->UpperBoundAsLiteral(arc.head_var));
911 std::vector<IntegerValue> coeffs(integer_reason_.size(), IntegerValue(1));
912 integer_trail_->RelaxLinearReason(slack, coeffs, &integer_reason_);
913 return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
914 }
915
916 return integer_trail_->Enqueue(
917 IntegerLiteral::GreaterOrEqual(arc.head_var, new_head_lb),
918 literal_reason_, integer_reason_);
919}
920
921bool PrecedencesPropagator::NoPropagationLeft(const Trail& trail) const {
922 const int num_nodes = impacted_arcs_.size();
923 for (IntegerVariable var(0); var < num_nodes; ++var) {
924 for (const ArcIndex arc_index : impacted_arcs_[var]) {
925 const ArcInfo& arc = arcs_[arc_index];
926 if (integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc) >
927 integer_trail_->LowerBound(arc.head_var)) {
928 return false;
929 }
930 }
931 }
932 return true;
933}
934
935void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
936 // Sparse clear of the queue. TODO(user): only use the sparse version if
937 // queue.size() is small or use SparseBitset.
938 const int num_nodes = impacted_arcs_.size();
939 bf_in_queue_.resize(num_nodes, false);
940 for (const int node : bf_queue_) bf_in_queue_[node] = false;
941 bf_queue_.clear();
942 DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
943 [](bool v) { return v; }));
944 for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
945 if (var >= num_nodes) continue;
946 bf_queue_.push_back(var.value());
947 bf_in_queue_[var.value()] = true;
948 }
949}
950
951void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
952 // To be sparse, we use the fact that each node with a parent must be in
953 // modified_vars_.
954 const int num_nodes = impacted_arcs_.size();
955 for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
956 if (var >= num_nodes) continue;
957 const ArcIndex parent_arc_index = bf_parent_arc_of_[var.value()];
958 if (parent_arc_index != -1) {
959 arcs_[parent_arc_index].is_marked = false;
960 bf_parent_arc_of_[var.value()] = -1;
961 bf_can_be_skipped_[var.value()] = false;
962 }
963 }
964 DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
965 [](ArcIndex v) { return v != -1; }));
966 DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
967 [](bool v) { return v; }));
968}
969
970bool PrecedencesPropagator::DisassembleSubtree(
971 int source, int target, std::vector<bool>* can_be_skipped) {
972 // Note that we explore a tree, so we can do it in any order, and the one
973 // below seems to be the fastest.
974 tmp_vector_.clear();
975 tmp_vector_.push_back(source);
976 while (!tmp_vector_.empty()) {
977 const int tail = tmp_vector_.back();
978 tmp_vector_.pop_back();
979 for (const ArcIndex arc_index : impacted_arcs_[IntegerVariable(tail)]) {
980 const ArcInfo& arc = arcs_[arc_index];
981 if (arc.is_marked) {
982 arc.is_marked = false; // mutable.
983 if (arc.head_var.value() == target) return true;
984 DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
985 (*can_be_skipped)[arc.head_var.value()] = true;
986 tmp_vector_.push_back(arc.head_var.value());
987 }
988 }
989 }
990 return false;
991}
992
993void PrecedencesPropagator::AnalyzePositiveCycle(
994 ArcIndex first_arc, Trail* trail, std::vector<Literal>* must_be_all_true,
995 std::vector<Literal>* literal_reason,
996 std::vector<IntegerLiteral>* integer_reason) {
997 must_be_all_true->clear();
998 literal_reason->clear();
999 integer_reason->clear();
1000
1001 // Follow bf_parent_arc_of_[] to find the cycle containing first_arc.
1002 const IntegerVariable first_arc_head = arcs_[first_arc].head_var;
1003 ArcIndex arc_index = first_arc;
1004 std::vector<ArcIndex> arc_on_cycle;
1005
1006 // Just to be safe and avoid an infinite loop we use the fact that the maximum
1007 // cycle size on a graph with n nodes is of size n. If we have more in the
1008 // code below, it means first_arc is not part of a cycle according to
1009 // bf_parent_arc_of_[], which should never happen.
1010 const int num_nodes = impacted_arcs_.size();
1011 while (arc_on_cycle.size() <= num_nodes) {
1012 arc_on_cycle.push_back(arc_index);
1013 const ArcInfo& arc = arcs_[arc_index];
1014 if (arc.tail_var == first_arc_head) break;
1015 arc_index = bf_parent_arc_of_[arc.tail_var.value()];
1016 CHECK_NE(arc_index, ArcIndex(-1));
1017 }
1018 CHECK_NE(arc_on_cycle.size(), num_nodes + 1) << "Infinite loop.";
1019
1020 // Compute the reason for this cycle.
1021 IntegerValue sum(0);
1022 for (const ArcIndex arc_index : arc_on_cycle) {
1023 const ArcInfo& arc = arcs_[arc_index];
1024 sum += ArcOffset(arc);
1025 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
1026 integer_reason);
1027 for (const Literal l : arc.presence_literals) {
1028 literal_reason->push_back(l.Negated());
1029 }
1030 }
1031
1032 // TODO(user): what if the sum overflow? this is just a check so I guess
1033 // we don't really care, but fix the issue.
1034 CHECK_GT(sum, 0);
1035}
1036
1037// Note that in our settings it is important to use an algorithm that tries to
1038// minimize the number of integer_trail_->Enqueue() as much as possible.
1039//
1040// TODO(user): The current algorithm is quite efficient, but there is probably
1041// still room for improvements.
1042bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) {
1043 const int num_nodes = impacted_arcs_.size();
1044
1045 // These vector are reset by CleanUpMarkedArcsAndParents() so resize is ok.
1046 bf_can_be_skipped_.resize(num_nodes, false);
1047 bf_parent_arc_of_.resize(num_nodes, ArcIndex(-1));
1048 const auto cleanup =
1049 ::absl::MakeCleanup([this]() { CleanUpMarkedArcsAndParents(); });
1050
1051 // The queue initialization is done by InitializeBFQueueWithModifiedNodes().
1052 while (!bf_queue_.empty()) {
1053 const int node = bf_queue_.front();
1054 bf_queue_.pop_front();
1055 bf_in_queue_[node] = false;
1056
1057 // TODO(user): we don't need bf_can_be_skipped_ since we can detect this
1058 // if this node has a parent arc which is not marked. Investigate if it is
1059 // faster without the vector<bool>.
1060 //
1061 // TODO(user): An alternative algorithm is to remove all these nodes from
1062 // the queue instead of simply marking them. This should also lead to a
1063 // better "relaxation" order of the arcs. It is however a bit more work to
1064 // remove them since we need to track their position.
1065 if (bf_can_be_skipped_[node]) {
1066 DCHECK_NE(bf_parent_arc_of_[node], -1);
1067 DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
1068 continue;
1069 }
1070
1071 const IntegerValue tail_lb =
1072 integer_trail_->LowerBound(IntegerVariable(node));
1073 for (const ArcIndex arc_index : impacted_arcs_[IntegerVariable(node)]) {
1074 const ArcInfo& arc = arcs_[arc_index];
1075 DCHECK_EQ(arc.tail_var, node);
1076 const IntegerValue candidate = tail_lb + ArcOffset(arc);
1077 if (candidate > integer_trail_->LowerBound(arc.head_var)) {
1078 if (!EnqueueAndCheck(arc, candidate, trail)) return false;
1079
1080 // This is the Tarjan contribution to Bellman-Ford. This code detect
1081 // positive cycle, and because it disassemble the subtree while doing
1082 // so, the cost is amortized during the algorithm execution. Another
1083 // advantages is that it will mark the node explored here as skippable
1084 // which will avoid to propagate them too early (knowing that they will
1085 // need to be propagated again later).
1086 if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
1087 &bf_can_be_skipped_)) {
1088 std::vector<Literal> must_be_all_true;
1089 AnalyzePositiveCycle(arc_index, trail, &must_be_all_true,
1090 &literal_reason_, &integer_reason_);
1091 if (must_be_all_true.empty()) {
1092 ++num_cycles_;
1093 return integer_trail_->ReportConflict(literal_reason_,
1094 integer_reason_);
1095 } else {
1096 gtl::STLSortAndRemoveDuplicates(&must_be_all_true);
1097 for (const Literal l : must_be_all_true) {
1098 if (trail_->Assignment().LiteralIsFalse(l)) {
1099 literal_reason_.push_back(l);
1100 return integer_trail_->ReportConflict(literal_reason_,
1101 integer_reason_);
1102 }
1103 }
1104 for (const Literal l : must_be_all_true) {
1105 if (trail_->Assignment().LiteralIsTrue(l)) continue;
1106 integer_trail_->EnqueueLiteral(l, literal_reason_,
1107 integer_reason_);
1108 }
1109
1110 // We just marked some optional variable as ignored, no need
1111 // to update bf_parent_arc_of_[].
1112 continue;
1113 }
1114 }
1115
1116 // We need to enforce the invariant that only the arc_index in
1117 // bf_parent_arc_of_[] are marked (but not necessarily all of them
1118 // since we unmark some in DisassembleSubtree()).
1119 if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
1120 arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked = false;
1121 }
1122
1123 // Tricky: We just enqueued the fact that the lower-bound of head is
1124 // candidate. However, because the domain of head may be discrete, it is
1125 // possible that the lower-bound of head is now higher than candidate!
1126 // If this is the case, we don't update bf_parent_arc_of_[] so that we
1127 // don't wrongly detect a positive weight cycle because of this "extra
1128 // push".
1129 const IntegerValue new_bound = integer_trail_->LowerBound(arc.head_var);
1130 if (new_bound == candidate) {
1131 bf_parent_arc_of_[arc.head_var.value()] = arc_index;
1132 arcs_[arc_index].is_marked = true;
1133 } else {
1134 // We still unmark any previous dependency, since we have pushed the
1135 // value of arc.head_var further.
1136 bf_parent_arc_of_[arc.head_var.value()] = -1;
1137 }
1138
1139 // We do not re-enqueue if we are in a propagation loop and new_bound
1140 // was not pushed to candidate or higher.
1141 bf_can_be_skipped_[arc.head_var.value()] = false;
1142 if (!bf_in_queue_[arc.head_var.value()] && new_bound >= candidate) {
1143 bf_queue_.push_back(arc.head_var.value());
1144 bf_in_queue_[arc.head_var.value()] = true;
1145 }
1146 }
1147 }
1148 }
1149 return true;
1150}
1151
1153 IntegerValue lhs, IntegerValue rhs) {
1154 if (lit.Index() != kNoLiteralIndex) {
1155 num_enforced_relations_++;
1156 DCHECK(a.coeff == 0 || a.var != kNoIntegerVariable);
1157 DCHECK(b.coeff == 0 || b.var != kNoIntegerVariable);
1158 } else {
1159 DCHECK_NE(a.coeff, 0);
1160 DCHECK_NE(b.coeff, 0);
1161 DCHECK_NE(a.var, kNoIntegerVariable);
1162 DCHECK_NE(b.var, kNoIntegerVariable);
1163 }
1164
1165 Relation r;
1166 r.enforcement = lit;
1167 r.a = a;
1168 r.b = b;
1169 r.lhs = lhs;
1170 r.rhs = rhs;
1171
1172 // We shall only consider positive variable here.
1173 if (r.a.var != kNoIntegerVariable && !VariableIsPositive(r.a.var)) {
1174 r.a.var = NegationOf(r.a.var);
1175 r.a.coeff = -r.a.coeff;
1176 }
1177 if (r.b.var != kNoIntegerVariable && !VariableIsPositive(r.b.var)) {
1178 r.b.var = NegationOf(r.b.var);
1179 r.b.coeff = -r.b.coeff;
1180 }
1181
1182 relations_.push_back(std::move(r));
1183}
1184
1186 IntegerVariable a,
1187 IntegerVariable b) {
1188 DCHECK_NE(a, kNoIntegerVariable);
1189 DCHECK_NE(b, kNoIntegerVariable);
1190 DCHECK_NE(a, b);
1191 Add(lit, LinearTerm(a, 1), LinearTerm(b, 1), 0, 0);
1192}
1193
1195 DCHECK(!is_built_);
1196 is_built_ = true;
1197 std::vector<std::pair<LiteralIndex, int>> literal_key_values;
1198 std::vector<std::pair<IntegerVariable, int>> var_key_values;
1199 const int num_relations = relations_.size();
1200 literal_key_values.reserve(num_enforced_relations_);
1201 var_key_values.reserve(num_relations - num_enforced_relations_);
1202 for (int i = 0; i < num_relations; ++i) {
1203 const Relation& r = relations_[i];
1204 if (r.enforcement.Index() == kNoLiteralIndex) {
1205 var_key_values.emplace_back(r.a.var, i);
1206 var_key_values.emplace_back(r.b.var, i);
1207 std::pair<IntegerVariable, IntegerVariable> key(r.a.var, r.b.var);
1208 if (relations_[i].a.var > relations_[i].b.var) {
1209 std::swap(key.first, key.second);
1210 }
1211 var_pair_to_relations_[key].push_back(i);
1212 } else {
1213 literal_key_values.emplace_back(r.enforcement.Index(), i);
1214 }
1215 }
1216 lit_to_relations_.ResetFromPairs(literal_key_values);
1217 var_to_relations_.ResetFromPairs(var_key_values);
1218}
1219
1221 const IntegerTrail& integer_trail, Literal lit,
1222 const absl::flat_hash_map<IntegerVariable, IntegerValue>& input,
1223 absl::flat_hash_map<IntegerVariable, IntegerValue>* output) const {
1224 DCHECK_NE(lit.Index(), kNoLiteralIndex);
1225
1226 auto get_lower_bound = [&](IntegerVariable var) {
1227 const auto it = input.find(var);
1228 if (it != input.end()) return it->second;
1229 return integer_trail.LevelZeroLowerBound(var);
1230 };
1231 auto get_upper_bound = [&](IntegerVariable var) {
1232 return -get_lower_bound(NegationOf(var));
1233 };
1234 auto update_lower_bound_by_var = [&](IntegerVariable var, IntegerValue lb) {
1235 if (lb <= integer_trail.LevelZeroLowerBound(var)) return;
1236 const auto [it, inserted] = output->insert({var, lb});
1237 if (!inserted) {
1238 it->second = std::max(it->second, lb);
1239 }
1240 };
1241 auto update_upper_bound_by_var = [&](IntegerVariable var, IntegerValue ub) {
1242 update_lower_bound_by_var(NegationOf(var), -ub);
1243 };
1244 auto update_var_bounds = [&](const LinearTerm& a, const LinearTerm& b,
1245 IntegerValue lhs, IntegerValue rhs) {
1246 if (a.coeff == 0) return;
1247
1248 // lb(b.y) <= b.y <= ub(b.y) and lhs <= a.x + b.y <= rhs imply
1249 // ceil((lhs - ub(b.y)) / a) <= x <= floor((rhs - lb(b.y)) / a)
1250 if (b.coeff != 0) {
1251 lhs = lhs - b.coeff * get_upper_bound(b.var);
1252 rhs = rhs - b.coeff * get_lower_bound(b.var);
1253 }
1254 update_lower_bound_by_var(a.var, MathUtil::CeilOfRatio(lhs, a.coeff));
1255 update_upper_bound_by_var(a.var, MathUtil::FloorOfRatio(rhs, a.coeff));
1256 };
1257 auto update_var_bounds_from_relation = [&](Relation r) {
1258 r.a.MakeCoeffPositive();
1259 r.b.MakeCoeffPositive();
1260 update_var_bounds(r.a, r.b, r.lhs, r.rhs);
1261 update_var_bounds(r.b, r.a, r.lhs, r.rhs);
1262 };
1263 if (lit.Index() < lit_to_relations_.size()) {
1264 for (const int relation_index : lit_to_relations_[lit]) {
1265 update_var_bounds_from_relation(relations_[relation_index]);
1266 }
1267 }
1268 for (const auto& [var, _] : input) {
1269 if (var >= var_to_relations_.size()) continue;
1270 for (const int relation_index : var_to_relations_[var]) {
1271 update_var_bounds_from_relation(relations_[relation_index]);
1272 }
1273 }
1274
1275 // Check feasibility.
1276 // TODO(user): we might do that earlier?
1277 for (const auto [var, lb] : *output) {
1278 if (lb > integer_trail.LevelZeroUpperBound(var)) return false;
1279 }
1280 return true;
1281}
1282
1283bool GreaterThanAtLeastOneOfDetector::AddRelationFromIndices(
1284 IntegerVariable var, absl::Span<const Literal> clause,
1285 absl::Span<const int> indices, Model* model) {
1286 std::vector<AffineExpression> exprs;
1287 std::vector<Literal> selectors;
1288 absl::flat_hash_set<LiteralIndex> used;
1289 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1290
1291 const IntegerValue var_lb = integer_trail->LevelZeroLowerBound(var);
1292 for (const int index : indices) {
1293 Relation r = repository_.relation(index);
1294 if (r.a.var != PositiveVariable(var)) std::swap(r.a, r.b);
1295 CHECK_EQ(r.a.var, PositiveVariable(var));
1296
1297 if ((r.a.coeff == 1) == VariableIsPositive(var)) {
1298 // a + b >= lhs
1299 if (r.lhs <= kMinIntegerValue) continue;
1300 exprs.push_back(AffineExpression(r.b.var, -r.b.coeff, r.lhs));
1301 } else {
1302 // -a + b <= rhs.
1303 if (r.rhs >= kMaxIntegerValue) continue;
1304 exprs.push_back(AffineExpression(r.b.var, r.b.coeff, -r.rhs));
1305 }
1306
1307 // Ignore this entry if it is always true.
1308 if (var_lb >= integer_trail->LevelZeroUpperBound(exprs.back())) {
1309 exprs.pop_back();
1310 continue;
1311 }
1312
1313 // Note that duplicate selector are supported.
1314 selectors.push_back(r.enforcement);
1315 used.insert(r.enforcement);
1316 }
1317
1318 // The enforcement of the new constraint are simply the literal not used
1319 // above.
1320 std::vector<Literal> enforcements;
1321 for (const Literal l : clause) {
1322 if (!used.contains(l.Index())) {
1323 enforcements.push_back(l.Negated());
1324 }
1325 }
1326
1327 // No point adding a constraint if there is not at least two different
1328 // literals in selectors.
1329 if (used.size() <= 1) return false;
1330
1331 // Add the constraint.
1332 GreaterThanAtLeastOneOfPropagator* constraint =
1333 new GreaterThanAtLeastOneOfPropagator(var, exprs, selectors, enforcements,
1334 model);
1335 constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
1336 model->TakeOwnership(constraint);
1337 return true;
1338}
1339
1340int GreaterThanAtLeastOneOfDetector::
1341 AddGreaterThanAtLeastOneOfConstraintsFromClause(
1342 const absl::Span<const Literal> clause, Model* model) {
1343 CHECK_EQ(model->GetOrCreate<Trail>()->CurrentDecisionLevel(), 0);
1344 if (clause.size() < 2) return 0;
1345
1346 // Collect all relations impacted by this clause.
1347 std::vector<std::pair<IntegerVariable, int>> infos;
1348 for (const Literal l : clause) {
1349 for (const int index :
1350 repository_.IndicesOfRelationsEnforcedBy(l.Index())) {
1351 const Relation& r = repository_.relation(index);
1352 if (r.a.var != kNoIntegerVariable && IntTypeAbs(r.a.coeff) == 1) {
1353 infos.push_back({r.a.var, index});
1354 }
1355 if (r.b.var != kNoIntegerVariable && IntTypeAbs(r.b.coeff) == 1) {
1356 infos.push_back({r.b.var, index});
1357 }
1358 }
1359 }
1360 if (infos.size() <= 1) return 0;
1361
1362 // Stable sort to regroup by var.
1363 std::stable_sort(infos.begin(), infos.end());
1364
1365 // We process the info with same variable together.
1366 int num_added_constraints = 0;
1367 std::vector<int> indices;
1368 for (int i = 0; i < infos.size();) {
1369 const int start = i;
1370 const IntegerVariable var = infos[start].first;
1371
1372 indices.clear();
1373 for (; i < infos.size() && infos[i].first == var; ++i) {
1374 indices.push_back(infos[i].second);
1375 }
1376
1377 // Skip single relations, we are not interested in these.
1378 if (indices.size() < 2) continue;
1379
1380 // Heuristic. Look for full or almost full clauses.
1381 //
1382 // TODO(user): We could add GreaterThanAtLeastOneOf() with more enforcement
1383 // literals. Experiment.
1384 if (indices.size() + 1 < clause.size()) continue;
1385
1386 if (AddRelationFromIndices(var, clause, indices, model)) {
1387 ++num_added_constraints;
1388 }
1389 if (AddRelationFromIndices(NegationOf(var), clause, indices, model)) {
1390 ++num_added_constraints;
1391 }
1392 }
1393 return num_added_constraints;
1394}
1395
1396int GreaterThanAtLeastOneOfDetector::
1397 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(Model* model) {
1398 auto* time_limit = model->GetOrCreate<TimeLimit>();
1399 auto* solver = model->GetOrCreate<SatSolver>();
1400
1401 // Fill the set of interesting relations for each variables.
1402 util_intops::StrongVector<IntegerVariable, std::vector<int>> var_to_relations;
1403 for (int index = 0; index < repository_.size(); ++index) {
1404 const Relation& r = repository_.relation(index);
1405 if (r.enforcement.Index() == kNoLiteralIndex) continue;
1406 if (r.a.var != kNoIntegerVariable && IntTypeAbs(r.a.coeff) == 1) {
1407 if (r.a.var >= var_to_relations.size()) {
1408 var_to_relations.resize(r.a.var + 1);
1409 }
1410 var_to_relations[r.a.var].push_back(index);
1411 }
1412 if (r.b.var != kNoIntegerVariable && IntTypeAbs(r.b.coeff) == 1) {
1413 if (r.b.var >= var_to_relations.size()) {
1414 var_to_relations.resize(r.b.var + 1);
1415 }
1416 var_to_relations[r.b.var].push_back(index);
1417 }
1418 }
1419
1420 int num_added_constraints = 0;
1421 for (IntegerVariable target(0); target < var_to_relations.size(); ++target) {
1422 if (var_to_relations[target].size() <= 1) continue;
1423 if (time_limit->LimitReached()) return num_added_constraints;
1424
1425 // Detect set of incoming arcs for which at least one must be present.
1426 // TODO(user): Find more than one disjoint set of incoming arcs.
1427 // TODO(user): call MinimizeCoreWithPropagation() on the clause.
1428 solver->Backtrack(0);
1429 if (solver->ModelIsUnsat()) return num_added_constraints;
1430 std::vector<Literal> clause;
1431 for (const int index : var_to_relations[target]) {
1432 const Literal literal = repository_.relation(index).enforcement;
1433 if (solver->Assignment().LiteralIsFalse(literal)) continue;
1434 const SatSolver::Status status =
1435 solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated());
1436 if (status == SatSolver::INFEASIBLE) return num_added_constraints;
1437 if (status == SatSolver::ASSUMPTIONS_UNSAT) {
1438 // We need to invert it, since a clause is not all false.
1439 clause = solver->GetLastIncompatibleDecisions();
1440 for (Literal& ref : clause) ref = ref.Negated();
1441 break;
1442 }
1443 }
1444 solver->Backtrack(0);
1445 if (clause.size() <= 1) continue;
1446
1447 // Recover the indices corresponding to this clause.
1448 const absl::btree_set<Literal> clause_set(clause.begin(), clause.end());
1449
1450 std::vector<int> indices;
1451 for (const int index : var_to_relations[target]) {
1452 const Literal literal = repository_.relation(index).enforcement;
1453 if (clause_set.contains(literal)) {
1454 indices.push_back(index);
1455 }
1456 }
1457
1458 // Try both direction.
1459 if (AddRelationFromIndices(target, clause, indices, model)) {
1460 ++num_added_constraints;
1461 }
1462 if (AddRelationFromIndices(NegationOf(target), clause, indices, model)) {
1463 ++num_added_constraints;
1464 }
1465 }
1466
1467 solver->Backtrack(0);
1468 return num_added_constraints;
1469}
1470
1472 Model* model, bool auto_detect_clauses) {
1473 auto* time_limit = model->GetOrCreate<TimeLimit>();
1474 auto* solver = model->GetOrCreate<SatSolver>();
1475 auto* clauses = model->GetOrCreate<ClauseManager>();
1476 auto* logger = model->GetOrCreate<SolverLogger>();
1477
1478 int num_added_constraints = 0;
1479 SOLVER_LOG(logger, "[Precedences] num_relations=", repository_.size(),
1480 " num_clauses=", clauses->AllClausesInCreationOrder().size());
1481
1482 // We have two possible approaches. For now, we prefer the first one except if
1483 // there is too many clauses in the problem.
1484 //
1485 // TODO(user): Do more extensive experiment. Remove the second approach as
1486 // it is more time consuming? or identify when it make sense. Note that the
1487 // first approach also allows to use "incomplete" at least one between arcs.
1488 if (!auto_detect_clauses &&
1489 clauses->AllClausesInCreationOrder().size() < 1e6) {
1490 // TODO(user): This does not take into account clause of size 2 since they
1491 // are stored in the BinaryImplicationGraph instead. Some ideas specific
1492 // to size 2:
1493 // - There can be a lot of such clauses, but it might be nice to consider
1494 // them. we need to experiments.
1495 // - The automatic clause detection might be a better approach and it
1496 // could be combined with probing.
1497 for (const SatClause* clause : clauses->AllClausesInCreationOrder()) {
1498 if (time_limit->LimitReached()) return num_added_constraints;
1499 if (solver->ModelIsUnsat()) return num_added_constraints;
1500 num_added_constraints += AddGreaterThanAtLeastOneOfConstraintsFromClause(
1501 clause->AsSpan(), model);
1502 }
1503
1504 // It is common that there is only two alternatives to push a variable.
1505 // In this case, our presolve most likely made sure that the two are
1506 // controlled by a single Boolean. This allows to detect this and add the
1507 // appropriate greater than at least one of.
1508 const int num_booleans = solver->NumVariables();
1509 if (num_booleans < 1e6) {
1510 for (int i = 0; i < num_booleans; ++i) {
1511 if (time_limit->LimitReached()) return num_added_constraints;
1512 if (solver->ModelIsUnsat()) return num_added_constraints;
1513 num_added_constraints +=
1514 AddGreaterThanAtLeastOneOfConstraintsFromClause(
1515 {Literal(BooleanVariable(i), true),
1516 Literal(BooleanVariable(i), false)},
1517 model);
1518 }
1519 }
1520
1521 } else {
1522 num_added_constraints +=
1523 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(model);
1524 }
1525
1526 if (num_added_constraints > 0) {
1527 SOLVER_LOG(logger, "[Precedences] Added ", num_added_constraints,
1528 " GreaterThanAtLeastOneOf() constraints.");
1529 }
1530
1531 return num_added_constraints;
1532}
1533
1535 : integer_trail_(model->GetOrCreate<IntegerTrail>()),
1536 integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
1537 watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
1538 shared_stats_(model->GetOrCreate<SharedStatistics>()) {
1539 int index = 0;
1540 model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
1541 [index = index, trail = model->GetOrCreate<Trail>(), this]() mutable {
1542 DCHECK_EQ(trail->CurrentDecisionLevel(), 0);
1543 absl::flat_hash_set<Literal> relevant_true_literals;
1544 for (; index < trail->Index(); ++index) {
1545 const Literal l = (*trail)[index];
1546 if (variable_appearing_in_reified_relations_.contains(l.Variable())) {
1547 relevant_true_literals.insert(l);
1548 }
1549 }
1550 if (relevant_true_literals.empty()) return true;
1551
1552 // Linear scan.
1553 for (const auto [l, expr, ub] : all_reified_relations_) {
1554 if (relevant_true_literals.contains(l)) {
1556 VLOG(2) << "New fixed precedence: " << expr << " <= " << ub
1557 << " (was reified by " << l << ")";
1558 } else if (relevant_true_literals.contains(l.Negated())) {
1559 AddRelationBounds(expr, ub + 1, kMaxIntegerValue);
1560 VLOG(2) << "New fixed precedence: " << expr << " > " << ub
1561 << " (was reified by not(" << l << "))";
1562 }
1563 }
1564 return true;
1565 });
1566}
1567
1569 if (!VLOG_IS_ON(1)) return;
1570 std::vector<std::pair<std::string, int64_t>> stats;
1571 stats.push_back({"BinaryRelationsMaps/num_relations", num_updates_});
1572 stats.push_back(
1573 {"BinaryRelationsMaps/num_affine_updates", num_affine_updates_});
1574 shared_stats_->AddStats(stats);
1575}
1576
1577IntegerValue BinaryRelationsMaps::GetImpliedUpperBound(
1578 const LinearExpression2& expr) const {
1579 DCHECK_GE(expr.coeffs[0], 0);
1580 DCHECK_GE(expr.coeffs[1], 0);
1581 IntegerValue implied_ub = 0;
1582 for (const int i : {0, 1}) {
1583 if (expr.coeffs[i] > 0) {
1584 implied_ub += expr.coeffs[i] * integer_trail_->UpperBound(expr.vars[i]);
1585 }
1586 }
1587 return implied_ub;
1588}
1589
1590std::pair<IntegerValue, IntegerValue>
1591BinaryRelationsMaps::GetImpliedLevelZeroBounds(
1592 const LinearExpression2& expr) const {
1593 // Compute the implied bounds on the expression.
1594 IntegerValue implied_lb = 0;
1595 IntegerValue implied_ub = 0;
1596 if (expr.coeffs[0] != 0) {
1597 CHECK_GE(expr.vars[0], 0);
1598 implied_lb +=
1599 expr.coeffs[0] * integer_trail_->LevelZeroLowerBound(expr.vars[0]);
1600 implied_ub +=
1601 expr.coeffs[0] * integer_trail_->LevelZeroUpperBound(expr.vars[0]);
1602 }
1603 if (expr.coeffs[1] != 0) {
1604 CHECK_GE(expr.vars[1], 0);
1605 implied_lb +=
1606 expr.coeffs[1] * integer_trail_->LevelZeroLowerBound(expr.vars[1]);
1607 implied_ub +=
1608 expr.coeffs[1] * integer_trail_->LevelZeroUpperBound(expr.vars[1]);
1609 }
1610
1611 return {implied_lb, implied_ub};
1612}
1613
1615 IntegerValue lb, IntegerValue ub) {
1616 expr.CanonicalizeAndUpdateBounds(lb, ub);
1617 const auto [implied_lb, implied_ub] = GetImpliedLevelZeroBounds(expr);
1618 lb = std::max(lb, implied_lb);
1619 ub = std::min(ub, implied_ub);
1620
1621 if (lb > ub) return; // unsat ??
1622 if (lb == implied_lb && ub == implied_ub) return; // trivially true.
1623
1624 if (best_root_level_bounds_.Add(expr, lb, ub)) {
1625 // TODO(user): Also push them to a global shared repository after
1626 // remapping IntegerVariable to proto indices.
1627 ++num_updates_;
1628 }
1629}
1630
1632 IntegerValue lb,
1633 IntegerValue ub) const {
1634 expr.CanonicalizeAndUpdateBounds(lb, ub);
1635 const auto [implied_lb, implied_ub] = GetImpliedLevelZeroBounds(expr);
1636 lb = std::max(lb, implied_lb);
1637 ub = std::min(ub, implied_ub);
1638
1639 // Returns directly if the status can be derived from the implied bounds.
1640 if (lb > ub) return RelationStatus::IS_FALSE;
1641 if (lb == implied_lb && ub == implied_ub) return RelationStatus::IS_TRUE;
1642
1643 // Relax as best_root_level_bounds_.GetStatus() might have older bounds.
1644 if (lb == implied_lb) lb = kMinIntegerValue;
1645 if (ub == implied_ub) ub = kMaxIntegerValue;
1646
1647 return best_root_level_bounds_.GetStatus(expr, lb, ub);
1648}
1649
1650std::pair<LinearExpression2, IntegerValue> BinaryRelationsMaps::FromDifference(
1651 const AffineExpression& a, const AffineExpression& b) const {
1652 LinearExpression2 expr;
1653 expr.vars[0] = a.var;
1654 expr.vars[1] = b.var;
1655 expr.coeffs[0] = a.coeff;
1656 expr.coeffs[1] = -b.coeff;
1657 IntegerValue lb = kMinIntegerValue; // unused.
1658 IntegerValue ub = b.constant - a.constant;
1659 expr.CanonicalizeAndUpdateBounds(lb, ub, /*allow_negation=*/false);
1660 return {std::move(expr), ub};
1661}
1662
1665 const auto [expr, ub] = FromDifference(a, b);
1666 return GetLevelZeroStatus(expr, kMinIntegerValue, ub);
1667}
1668
1672 const auto [expr, ub] = FromDifference(a, b);
1673 const RelationStatus status = GetLevelZeroStatus(expr, kMinIntegerValue, ub);
1674 if (status != RelationStatus::IS_UNKNOWN) return;
1675
1676 relation_to_lit_.insert({{expr, ub}, l});
1677
1678 variable_appearing_in_reified_relations_.insert(l.Variable());
1679 all_reified_relations_.push_back({l, expr, ub});
1680}
1681
1684 const auto [expr, ub] = FromDifference(a, b);
1685 const RelationStatus status = GetLevelZeroStatus(expr, kMinIntegerValue, ub);
1686 if (status == RelationStatus::IS_TRUE) {
1687 return integer_encoder_->GetTrueLiteral().Index();
1688 }
1689 if (status == RelationStatus::IS_FALSE) {
1690 return integer_encoder_->GetFalseLiteral().Index();
1691 }
1692
1693 const auto it = relation_to_lit_.find({expr, ub});
1694 if (it == relation_to_lit_.end()) return kNoLiteralIndex;
1695 return it->second;
1696}
1697
1699 AffineExpression affine_ub) {
1700 const IntegerValue new_ub = integer_trail_->UpperBound(affine_ub);
1702
1703 // Not better than trivial upper bound.
1704 if (GetImpliedUpperBound(expr) <= new_ub) return false;
1705
1706 // Not better than the root level upper bound.
1707 if (best_root_level_bounds_.GetUpperBound(expr) <= new_ub) return false;
1708
1709 const IntegerValue gcd = expr.DivideByGcd();
1710
1711 const auto it = best_affine_ub_.find(expr);
1712 if (it != best_affine_ub_.end()) {
1713 const auto [old_affine_ub, old_gcd] = it->second;
1714 // We have an affine bound for this expr in the map. Can be exactly the
1715 // same, a better one or a worse one.
1716 if (old_affine_ub == affine_ub && old_gcd == gcd) {
1717 // The affine bound is already in the map.
1718 NotifyWatchingPropagators(); // The affine bound was updated.
1719 return false;
1720 }
1721 const IntegerValue old_ub =
1722 FloorRatio(integer_trail_->UpperBound(old_affine_ub), old_gcd);
1723 if (old_ub <= new_ub) return false; // old bound is better.
1724 }
1725
1726 // We have gcd * canonical_expr <= affine_ub, so we do need to store a
1727 // "divisor".
1728 ++num_affine_updates_;
1729 best_affine_ub_[expr] = {affine_ub, gcd};
1730 NotifyWatchingPropagators();
1731 return true;
1732}
1733
1734void BinaryRelationsMaps::NotifyWatchingPropagators() const {
1735 for (const int id : propagator_ids_) {
1736 watcher_->CallOnNextPropagate(id);
1737 }
1738}
1739
1742
1743 const IntegerValue trivial_ub = GetImpliedUpperBound(expr);
1744 const IntegerValue root_level_ub =
1745 best_root_level_bounds_.GetUpperBound(expr);
1746 const IntegerValue best_ub = std::min(root_level_ub, trivial_ub);
1747
1748 const IntegerValue gcd = expr.DivideByGcd();
1749 const auto it = best_affine_ub_.find(expr);
1750 if (it == best_affine_ub_.end()) {
1751 return best_ub;
1752 } else {
1753 const auto [affine, divisor] = it->second;
1754 const IntegerValue canonical_ub =
1755 FloorRatio(integer_trail_->UpperBound(affine), divisor);
1756 return std::min(best_ub, CapProdI(gcd, canonical_ub));
1757 }
1758}
1759
1760// TODO(user): If the trivial bound is better, its explanation is different...
1762 LinearExpression2 expr, IntegerValue ub,
1763 std::vector<Literal>* /*literal_reason*/,
1764 std::vector<IntegerLiteral>* integer_reason) const {
1766
1767 if (expr.coeffs[0] == 0 && expr.coeffs[1] == 0) return; // trivially zero
1768
1769 // Starts by simple bounds.
1770 if (best_root_level_bounds_.GetUpperBound(expr) <= ub) return;
1771
1772 // Add explanation if it is a trivial bound.
1773 const IntegerValue implied_ub = GetImpliedUpperBound(expr);
1774 if (implied_ub <= ub) {
1775 const IntegerValue slack = ub - implied_ub;
1776 expr.Negate(); // AppendRelaxedLinearReason() explains a lower bound.
1777 absl::Span<const IntegerVariable> vars = expr.non_zero_vars();
1778 absl::Span<const IntegerValue> coeffs = expr.non_zero_coeffs();
1779 integer_trail_->AppendRelaxedLinearReason(slack, coeffs, vars,
1780 integer_reason);
1781 return;
1782 }
1783
1784 // None of the bound above are enough, try the affine one. Note that gcd *
1785 // expr <= ub, is the same as asking why expr <= FloorRatio(ub, gcd).
1786 const IntegerValue gcd = expr.DivideByGcd();
1787 const auto it = best_affine_ub_.find(expr);
1788 if (it == best_affine_ub_.end()) return;
1789
1790 // We want the reason for "expr <= ub", that is the reason for
1791 // - "gcd * canonical_expr <= ub"
1792 // - "canonical_expr <= FloorRatio(ub, gcd);
1793 //
1794 // knowing that canonical_expr <= affine_ub / divisor.
1795 const auto [affine, divisor] = it->second;
1796 integer_reason->push_back(
1797 affine.LowerOrEqual(CapProdI(FloorRatio(ub, gcd) + 1, divisor) - 1));
1798}
1799
1800std::vector<LinearExpression2>
1802 std::vector<LinearExpression2> result;
1803 for (const auto [expr, info] : best_affine_ub_) {
1804 result.push_back(expr);
1805 }
1806 return result;
1807}
1808
1809} // namespace sat
1810} // namespace operations_research
static IntegralType CeilOfRatio(IntegralType numerator, IntegralType denominator)
Definition mathutil.h:39
static IntegralType FloorOfRatio(IntegralType numerator, IntegralType denominator)
Definition mathutil.h:53
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
Definition bitset.h:899
bool PropagateLocalBounds(const IntegerTrail &integer_trail, Literal lit, const absl::flat_hash_map< IntegerVariable, IntegerValue > &input, absl::flat_hash_map< IntegerVariable, IntegerValue > *output) const
const Relation & relation(int index) const
The returned relation is guaranteed to only have positive variables.
void AddPartialRelation(Literal lit, IntegerVariable a, IntegerVariable b)
void Add(Literal lit, LinearTerm a, LinearTerm b, IntegerValue lhs, IntegerValue rhs)
void AddReifiedPrecedenceIfNonTrivial(Literal l, AffineExpression a, AffineExpression b)
IntegerValue UpperBound(LinearExpression2 expr) const
std::vector< LinearExpression2 > GetAllExpressionsWithAffineBounds() const
Warning, the order will not be deterministic.
RelationStatus GetLevelZeroPrecedenceStatus(AffineExpression a, AffineExpression b) const
Return the status of a <= b;.
LiteralIndex GetReifiedPrecedence(AffineExpression a, AffineExpression b)
void AddReasonForUpperBoundLowerThan(LinearExpression2 expr, IntegerValue ub, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
RelationStatus GetLevelZeroStatus(LinearExpression2 expr, IntegerValue lb, IntegerValue ub) const
bool AddAffineUpperBound(LinearExpression2 expr, AffineExpression affine_ub)
void AddRelationBounds(LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
Definition integer.h:1478
int AddGreaterThanAtLeastOneOfConstraints(Model *model, bool auto_detect_clauses=false)
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
Definition integer.h:1317
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Definition integer.h:1365
IntegerValue UpperBound(IntegerVariable i) const
Definition integer.h:1321
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
Definition integer.h:1360
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
Definition integer.h:1419
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
Definition integer.h:1412
LiteralIndex Index() const
Definition sat_base.h:91
BooleanVariable Variable() const
Definition sat_base.h:87
void CollectPrecedences(absl::Span< const IntegerVariable > vars, std::vector< PrecedenceData > *output)
bool AddBounds(LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
IntegerValue UpperBound(LinearExpression2 expr) const
void PushConditionalRelation(absl::Span< const Literal > enforcements, LinearExpression2 expr, IntegerValue rhs)
IntegerValue LevelZeroUpperBound(LinearExpression2 expr) const
void ComputeFullPrecedences(absl::Span< const IntegerVariable > vars, std::vector< FullIntegerPrecedence > *output)
bool AddUpperBound(LinearExpression2 expr, IntegerValue ub)
Same as above, but only for the upper bound.
void SetLevel(int level) final
Called each time we change decision level.
void AddReasonForUpperBoundLowerThan(LinearExpression2 expr, IntegerValue ub, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
bool AddPrecedenceWithOffsetIfNew(IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
This version check current precedence. It is however "slow".
void AddPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
void Untrail(const Trail &trail, int trail_index) final
Simple class to add statistics by name and print them at the end.
const VariablesAssignment & Assignment() const
Definition sat_base.h:462
bool LiteralIsFalse(Literal literal) const
Definition sat_base.h:185
bool LiteralIsTrue(Literal literal) const
Definition sat_base.h:188
bool GetNext(int *next_node_index, bool *cyclic, std::vector< int > *output_cycle_nodes=nullptr)
void push_back(const value_type &val)
void resize(size_type new_size)
time_limit
Definition solve.cc:22
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:55
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntType IntTypeAbs(IntType t)
const LiteralIndex kNoLiteralIndex(-1)
std::function< int64_t(const Model &)> LowerBound(IntegerVariable v)
Definition integer.h:1581
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
bool VariableIsPositive(IntegerVariable i)
IntegerValue CapProdI(IntegerValue a, IntegerValue b)
Overflows and saturated arithmetic.
In SWIG mode, we don't want anything besides these top-level includes.
int64_t FloorRatio(int64_t value, int64_t positive_coeff)
const bool DEBUG_MODE
Definition radix_sort.h:266
void Permute(const IntVector &permutation, Array *array_to_permute)
Definition graph.h:1105
if(!yyg->yy_init)
Definition parser.yy.cc:966
static int input(yyscan_t yyscanner)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::vector< std::function< bool()> > callbacks
absl::Span< const IntegerValue > non_zero_coeffs() const
absl::Span< const IntegerVariable > non_zero_vars() const
void CanonicalizeAndUpdateBounds(IntegerValue &lb, IntegerValue &ub, bool allow_negation=false)
static LinearExpression2 Difference(IntegerVariable v1, IntegerVariable v2)
Build (v1 - v2)
void Negate()
Take the negation of this expression.
::util::DenseIntStableTopologicalSorter DenseIntStableTopologicalSorter
#define SOLVER_LOG(logger,...)
Definition logging.h:110