OR-Tools  8.2
precedences.h
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
14#ifndef OR_TOOLS_SAT_PRECEDENCES_H_
15#define OR_TOOLS_SAT_PRECEDENCES_H_
16
17#include <deque>
18#include <functional>
19#include <vector>
20
21#include "absl/container/inlined_vector.h"
24#include "ortools/base/macros.h"
26#include "ortools/sat/integer.h"
27#include "ortools/sat/model.h"
30#include "ortools/util/bitset.h"
31
32namespace operations_research {
33namespace sat {
34
35// This class implement a propagator on simple inequalities between integer
36// variables of the form (i1 + offset <= i2). The offset can be constant or
37// given by the value of a third integer variable. Offsets can also be negative.
38//
39// The algorithm works by mapping the problem onto a graph where the edges carry
40// the offset and the nodes correspond to one of the two bounds of an integer
41// variable (lower_bound or -upper_bound). It then find the fixed point using an
42// incremental variant of the Bellman-Ford(-Tarjan) algorithm.
43//
44// This is also known as an "integer difference logic theory" in the SMT world.
45// Another word is "separation logic".
46//
47// TODO(user): We could easily generalize the code to support any relation of
48// the form a*X + b*Y + c*Z >= rhs (or <=). Do that since this class should be
49// a lot faster at propagating small linear inequality than the generic
50// propagator and the overhead of supporting coefficient should not be too bad.
52 public:
54 : SatPropagator("PrecedencesPropagator"),
55 trail_(model->GetOrCreate<Trail>()),
56 integer_trail_(model->GetOrCreate<IntegerTrail>()),
57 watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
58 watcher_id_(watcher_->Register(this)) {
59 model->GetOrCreate<SatSolver>()->AddPropagator(this);
60 integer_trail_->RegisterWatcher(&modified_vars_);
61 watcher_->SetPropagatorPriority(watcher_id_, 0);
62 }
63
64 bool Propagate() final;
65 bool Propagate(Trail* trail) final;
66 void Untrail(const Trail& trail, int trail_index) final;
67
68 // Propagates all the outgoing arcs of the given variable (and only those). It
69 // is more efficient to do all these propagation in one go by calling
70 // Propagate(), but for scheduling problem, we wants to propagate right away
71 // the end of an interval when its start moved.
72 bool PropagateOutgoingArcs(IntegerVariable var);
73
74 // Add a precedence relation (i1 + offset <= i2) between integer variables.
75 //
76 // Important: The optionality of the variable should be marked BEFORE this
77 // is called.
78 void AddPrecedence(IntegerVariable i1, IntegerVariable i2);
79 void AddPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2,
80 IntegerValue offset);
81 void AddPrecedenceWithVariableOffset(IntegerVariable i1, IntegerVariable i2,
82 IntegerVariable offset_var);
83
84 // Same as above, but the relation is only true when the given literal is.
85 void AddConditionalPrecedence(IntegerVariable i1, IntegerVariable i2,
86 Literal l);
87 void AddConditionalPrecedenceWithOffset(IntegerVariable i1,
88 IntegerVariable i2,
89 IntegerValue offset, Literal l);
90
91 // Generic function that cover all of the above case and more.
92 void AddPrecedenceWithAllOptions(IntegerVariable i1, IntegerVariable i2,
93 IntegerValue offset,
94 IntegerVariable offset_var,
95 absl::Span<const Literal> presence_literals);
96
97 // Finds all the IntegerVariable that are "after" at least two of the
98 // IntegerVariable in vars. Returns a vector of these precedences relation
99 // sorted by IntegerPrecedences.var so that it is efficient to find all the
100 // IntegerVariable "before" another one.
101 //
102 // Note that we only consider direct precedences here. Given our usage, it may
103 // be better to compute the full reachability in the precedence graph, but in
104 // pratice that may be too slow.
105 //
106 // Note that the IntegerVariable in the vector are also returned in
107 // topological order for a more efficient propagation in
108 // DisjunctivePrecedences::Propagate() where this is used.
109 //
110 // Important: For identical vars, the entry are sorted by index.
112 int index; // position in vars.
113 IntegerVariable var; // An IntegerVariable that is >= to vars[index].
114 int arc_index; // Used by AddPrecedenceReason().
115 IntegerValue offset; // we have: vars[index] + offset <= var
116 };
117 void ComputePrecedences(const std::vector<IntegerVariable>& vars,
118 std::vector<IntegerPrecedences>* output);
119 void AddPrecedenceReason(int arc_index, IntegerValue min_offset,
120 std::vector<Literal>* literal_reason,
121 std::vector<IntegerLiteral>* integer_reason) const;
122
123 // Advanced usage. To be called once all the constraints have been added to
124 // the model. This will loop over all "node" in this class, and if one of its
125 // optional incoming arcs must be chosen, it will add a corresponding
126 // GreaterThanAtLeastOneOfConstraint(). Returns the number of added
127 // constraint.
128 //
129 // TODO(user): This can be quite slow, add some kind of deterministic limit
130 // so that we can use it all the time.
132
133 private:
134 DEFINE_INT_TYPE(ArcIndex, int);
135 DEFINE_INT_TYPE(OptionalArcIndex, int);
136
137 // Given an existing clause, sees if it can be used to add "greater than at
138 // least one of" type of constraints. Returns the number of such constraint
139 // added.
140 int AddGreaterThanAtLeastOneOfConstraintsFromClause(
141 const absl::Span<const Literal> clause, Model* model);
142
143 // Another approach for AddGreaterThanAtLeastOneOfConstraints(), this one
144 // might be a bit slow as it relies on the propagation engine to detect
145 // clauses between incoming arcs presence literals.
146 // Returns the number of added constraints.
147 int AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(
148 Model* model);
149
150 // Information about an individual arc.
151 struct ArcInfo {
152 IntegerVariable tail_var;
153 IntegerVariable head_var;
154
155 IntegerValue offset;
156 IntegerVariable offset_var; // kNoIntegerVariable if none.
157
158 // This arc is "present" iff all these literals are true.
159 absl::InlinedVector<Literal, 6> presence_literals;
160
161 // Used temporarily by our implementation of the Bellman-Ford algorithm. It
162 // should be false at the beginning of BellmanFordTarjan().
163 mutable bool is_marked;
164 };
165
166 // Internal functions to add new precedence relations.
167 //
168 // Note that internally, we only propagate lower bounds, so each time we add
169 // an arc, we actually create two of them: one on the given variables, and one
170 // on their negation.
171 void AdjustSizeFor(IntegerVariable i);
172 void AddArc(IntegerVariable tail, IntegerVariable head, IntegerValue offset,
173 IntegerVariable offset_var,
174 absl::Span<const Literal> presence_literals);
175
176 // Enqueue a new lower bound for the variable arc.head_lb that was deduced
177 // from the current value of arc.tail_lb and the offset of this arc.
178 bool EnqueueAndCheck(const ArcInfo& arc, IntegerValue new_head_lb,
179 Trail* trail);
180 IntegerValue ArcOffset(const ArcInfo& arc) const;
181
182 // Inspect all the optional arcs that needs inspection (to stay sparse) and
183 // check if their presence literal can be propagated to false.
184 void PropagateOptionalArcs(Trail* trail);
185
186 // The core algorithm implementation is split in these functions. One must
187 // first call InitializeBFQueueWithModifiedNodes() that will push all the
188 // IntegerVariable whose lower bound has been modified since the last call.
189 // Then, BellmanFordTarjan() will take care of all the propagation and returns
190 // false in case of conflict. Internally, it uses DisassembleSubtree() which
191 // is the Tarjan variant to detect a possible positive cycle. Before exiting,
192 // it will call CleanUpMarkedArcsAndParents().
193 //
194 // The Tarjan version of the Bellam-Ford algorithm is really nice in our
195 // context because it was really easy to make it incremental. Moreover, it
196 // supports batch increment!
197 //
198 // This implementation is kind of unique because of our context and the fact
199 // that it is incremental, but a good reference is "Negative-cycle detection
200 // algorithms", Boris V. Cherkassky, Andrew V. Goldberg, 1996,
201 // http://people.cs.nctu.edu.tw/~tjshen/doc/ne.pdf
202 void InitializeBFQueueWithModifiedNodes();
203 bool BellmanFordTarjan(Trail* trail);
204 bool DisassembleSubtree(int source, int target,
205 std::vector<bool>* can_be_skipped);
206 void AnalyzePositiveCycle(ArcIndex first_arc, Trail* trail,
207 std::vector<Literal>* must_be_all_true,
208 std::vector<Literal>* literal_reason,
209 std::vector<IntegerLiteral>* integer_reason);
210 void CleanUpMarkedArcsAndParents();
211
212 // Loops over all the arcs and verify that there is no propagation left.
213 // This is only meant to be used in a DCHECK() and is not optimized.
214 bool NoPropagationLeft(const Trail& trail) const;
215
216 // External class needed to get the IntegerVariable lower bounds and Enqueue
217 // new ones.
218 Trail* trail_;
219 IntegerTrail* integer_trail_;
220 GenericLiteralWatcher* watcher_;
221 int watcher_id_;
222
223 // The key to our incrementality. This will be cleared once the propagation
224 // is done, and automatically updated by the integer_trail_ with all the
225 // IntegerVariable that changed since the last clear.
226 SparseBitset<IntegerVariable> modified_vars_;
227
228 // An arc needs to be inspected for propagation (i.e. is impacted) if its
229 // tail_var changed. If an arc has 3 variables (tail, offset, head), it will
230 // appear as 6 different entries in the arcs_ vector, one for each variable
231 // and its negation, each time with a different tail.
232 //
233 // TODO(user): rearranging the index so that the arc of the same node are
234 // consecutive like in StaticGraph should have a big performance impact.
235 //
236 // TODO(user): We do not need to store ArcInfo.tail_var here.
238 impacted_arcs_;
240
241 // This is similar to impacted_arcs_/arcs_ but it is only used to propagate
242 // one of the presence literals when the arc cannot be present. An arc needs
243 // to appear only once in potential_arcs_, but it will be referenced by
244 // all its variable in impacted_potential_arcs_.
246 impacted_potential_arcs_;
248
249 // Temporary vectors used by ComputePrecedences().
252 struct SortedVar {
253 IntegerVariable var;
254 IntegerValue lower_bound;
255 bool operator<(const SortedVar& other) const {
256 return lower_bound < other.lower_bound;
257 }
258 };
259 std::vector<SortedVar> tmp_sorted_vars_;
260 std::vector<IntegerPrecedences> tmp_precedences_;
261
262 // Each time a literal becomes true, this list the set of arcs for which we
263 // need to decrement their count. When an arc count reach zero, it must be
264 // added to the set of impacted_arcs_. Note that counts never becomes
265 // negative.
266 //
267 // TODO(user): Try a one-watcher approach instead. Note that in most cases
268 // arc should be controlled by 1 or 2 literals, so not sure it is worth it.
270 literal_to_new_impacted_arcs_;
272
273 // Temp vectors to hold the reason of an assignment.
274 std::vector<Literal> literal_reason_;
275 std::vector<IntegerLiteral> integer_reason_;
276
277 // Temp vectors for the Bellman-Ford algorithm. The graph in which this
278 // algorithm works is in one to one correspondence with the IntegerVariable in
279 // impacted_arcs_.
280 std::deque<int> bf_queue_;
281 std::vector<bool> bf_in_queue_;
282 std::vector<bool> bf_can_be_skipped_;
283 std::vector<ArcIndex> bf_parent_arc_of_;
284
285 // Temp vector used by the tree traversal in DisassembleSubtree().
286 std::vector<int> tmp_vector_;
287
288 DISALLOW_COPY_AND_ASSIGN(PrecedencesPropagator);
289};
290
291// =============================================================================
292// Implementation of the small API functions below.
293// =============================================================================
294
295inline void PrecedencesPropagator::AddPrecedence(IntegerVariable i1,
296 IntegerVariable i2) {
297 AddArc(i1, i2, /*offset=*/IntegerValue(0), /*offset_var=*/kNoIntegerVariable,
298 {});
299}
300
302 IntegerVariable i1, IntegerVariable i2, IntegerValue offset) {
303 AddArc(i1, i2, offset, /*offset_var=*/kNoIntegerVariable, {});
304}
305
307 IntegerVariable i2,
308 Literal l) {
309 AddArc(i1, i2, /*offset=*/IntegerValue(0), /*offset_var=*/kNoIntegerVariable,
310 {l});
311}
312
314 IntegerVariable i1, IntegerVariable i2, IntegerValue offset, Literal l) {
315 AddArc(i1, i2, offset, /*offset_var=*/kNoIntegerVariable, {l});
316}
317
319 IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var) {
320 AddArc(i1, i2, /*offset=*/IntegerValue(0), offset_var, {});
321}
322
324 IntegerVariable i1, IntegerVariable i2, IntegerValue offset,
325 IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
326 AddArc(i1, i2, offset, offset_var, presence_literals);
327}
328
329// =============================================================================
330// Model based functions.
331// =============================================================================
332
333// a <= b.
334inline std::function<void(Model*)> LowerOrEqual(IntegerVariable a,
335 IntegerVariable b) {
336 return [=](Model* model) {
337 return model->GetOrCreate<PrecedencesPropagator>()->AddPrecedence(a, b);
338 };
339}
340
341// a + offset <= b.
342inline std::function<void(Model*)> LowerOrEqualWithOffset(IntegerVariable a,
343 IntegerVariable b,
344 int64 offset) {
345 return [=](Model* model) {
346 return model->GetOrCreate<PrecedencesPropagator>()->AddPrecedenceWithOffset(
347 a, b, IntegerValue(offset));
348 };
349}
350
351// a + b <= ub.
352inline std::function<void(Model*)> Sum2LowerOrEqual(IntegerVariable a,
353 IntegerVariable b,
354 int64 ub) {
355 return LowerOrEqualWithOffset(a, NegationOf(b), -ub);
356}
357
358// l => (a + b <= ub).
359inline std::function<void(Model*)> ConditionalSum2LowerOrEqual(
360 IntegerVariable a, IntegerVariable b, int64 ub,
361 const std::vector<Literal>& enforcement_literals) {
362 return [=](Model* model) {
364 p->AddPrecedenceWithAllOptions(a, NegationOf(b), IntegerValue(-ub),
365 kNoIntegerVariable, enforcement_literals);
366 };
367}
368
369// a + b + c <= ub.
370inline std::function<void(Model*)> Sum3LowerOrEqual(IntegerVariable a,
371 IntegerVariable b,
372 IntegerVariable c,
373 int64 ub) {
374 return [=](Model* model) {
376 p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b, {});
377 };
378}
379
380// l => (a + b + c <= ub).
381inline std::function<void(Model*)> ConditionalSum3LowerOrEqual(
382 IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub,
383 const std::vector<Literal>& enforcement_literals) {
384 return [=](Model* model) {
386 p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b,
387 enforcement_literals);
388 };
389}
390
391// a >= b.
392inline std::function<void(Model*)> GreaterOrEqual(IntegerVariable a,
393 IntegerVariable b) {
394 return [=](Model* model) {
395 return model->GetOrCreate<PrecedencesPropagator>()->AddPrecedence(b, a);
396 };
397}
398
399// a == b.
400inline std::function<void(Model*)> Equality(IntegerVariable a,
401 IntegerVariable b) {
402 return [=](Model* model) {
403 model->Add(LowerOrEqual(a, b));
404 model->Add(LowerOrEqual(b, a));
405 };
406}
407
408// a + offset == b.
409inline std::function<void(Model*)> EqualityWithOffset(IntegerVariable a,
410 IntegerVariable b,
411 int64 offset) {
412 return [=](Model* model) {
413 model->Add(LowerOrEqualWithOffset(a, b, offset));
414 model->Add(LowerOrEqualWithOffset(b, a, -offset));
415 };
416}
417
418// is_le => (a + offset <= b).
419inline std::function<void(Model*)> ConditionalLowerOrEqualWithOffset(
420 IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le) {
421 return [=](Model* model) {
423 p->AddConditionalPrecedenceWithOffset(a, b, IntegerValue(offset), is_le);
424 };
425}
426
427// is_le => (a <= b).
428inline std::function<void(Model*)> ConditionalLowerOrEqual(IntegerVariable a,
429 IntegerVariable b,
430 Literal is_le) {
431 return ConditionalLowerOrEqualWithOffset(a, b, 0, is_le);
432}
433
434// literals => (a <= b).
435inline std::function<void(Model*)> ConditionalLowerOrEqual(
436 IntegerVariable a, IntegerVariable b, absl::Span<const Literal> literals) {
437 return [=](Model* model) {
439 p->AddPrecedenceWithAllOptions(a, b, IntegerValue(0),
440 /*offset_var*/ kNoIntegerVariable, literals);
441 };
442}
443
444// is_le <=> (a + offset <= b).
445inline std::function<void(Model*)> ReifiedLowerOrEqualWithOffset(
446 IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le) {
447 return [=](Model* model) {
449 p->AddConditionalPrecedenceWithOffset(a, b, IntegerValue(offset), is_le);
450
451 // The negation of (a + offset <= b) is (a + offset > b) which can be
452 // rewritten as (b + 1 - offset <= a).
453 p->AddConditionalPrecedenceWithOffset(b, a, IntegerValue(1 - offset),
454 is_le.Negated());
455 };
456}
457
458// is_eq <=> (a == b).
459inline std::function<void(Model*)> ReifiedEquality(IntegerVariable a,
460 IntegerVariable b,
461 Literal is_eq) {
462 return [=](Model* model) {
463 // We creates two extra Boolean variables in this case.
464 //
465 // TODO(user): Avoid creating them if we already have some literal that
466 // have the same meaning. For instance if a client also wanted to know if
467 // a <= b, he would have called ReifiedLowerOrEqualWithOffset() directly.
468 const Literal is_le = Literal(model->Add(NewBooleanVariable()), true);
469 const Literal is_ge = Literal(model->Add(NewBooleanVariable()), true);
470 model->Add(ReifiedBoolAnd({is_le, is_ge}, is_eq));
471 model->Add(ReifiedLowerOrEqualWithOffset(a, b, 0, is_le));
472 model->Add(ReifiedLowerOrEqualWithOffset(b, a, 0, is_ge));
473 };
474}
475
476// is_eq <=> (a + offset == b).
477inline std::function<void(Model*)> ReifiedEqualityWithOffset(IntegerVariable a,
478 IntegerVariable b,
479 int64 offset,
480 Literal is_eq) {
481 return [=](Model* model) {
482 // We creates two extra Boolean variables in this case.
483 //
484 // TODO(user): Avoid creating them if we already have some literal that
485 // have the same meaning. For instance if a client also wanted to know if
486 // a <= b, he would have called ReifiedLowerOrEqualWithOffset() directly.
487 const Literal is_le = Literal(model->Add(NewBooleanVariable()), true);
488 const Literal is_ge = Literal(model->Add(NewBooleanVariable()), true);
489 model->Add(ReifiedBoolAnd({is_le, is_ge}, is_eq));
490 model->Add(ReifiedLowerOrEqualWithOffset(a, b, offset, is_le));
491 model->Add(ReifiedLowerOrEqualWithOffset(b, a, -offset, is_ge));
492 };
493}
494
495// a != b.
496inline std::function<void(Model*)> NotEqual(IntegerVariable a,
497 IntegerVariable b) {
498 return [=](Model* model) {
499 // We have two options (is_gt or is_lt) and one must be true.
500 const Literal is_lt = Literal(model->Add(NewBooleanVariable()), true);
501 const Literal is_gt = is_lt.Negated();
502 model->Add(ConditionalLowerOrEqualWithOffset(a, b, 1, is_lt));
503 model->Add(ConditionalLowerOrEqualWithOffset(b, a, 1, is_gt));
504 };
505}
506
507} // namespace sat
508} // namespace operations_research
509
510#endif // OR_TOOLS_SAT_PRECEDENCES_H_
void SetPropagatorPriority(int id, int priority)
Definition: integer.cc:1962
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
Definition: integer.h:803
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
void AddPrecedenceReason(int arc_index, IntegerValue min_offset, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
Definition: precedences.cc:212
void AddConditionalPrecedence(IntegerVariable i1, IntegerVariable i2, Literal l)
Definition: precedences.h:306
void AddConditionalPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2, IntegerValue offset, Literal l)
Definition: precedences.h:313
void AddPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
Definition: precedences.h:301
void AddPrecedenceWithAllOptions(IntegerVariable i1, IntegerVariable i2, IntegerValue offset, IntegerVariable offset_var, absl::Span< const Literal > presence_literals)
Definition: precedences.h:323
void ComputePrecedences(const std::vector< IntegerVariable > &vars, std::vector< IntegerPrecedences > *output)
Definition: precedences.cc:135
void AddPrecedence(IntegerVariable i1, IntegerVariable i2)
Definition: precedences.h:295
void AddPrecedenceWithVariableOffset(IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var)
Definition: precedences.h:318
void Untrail(const Trail &trail, int trail_index) final
Definition: precedences.cc:111
bool PropagateOutgoingArcs(IntegerVariable var)
Definition: precedences.cc:96
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
Definition: cleanup.h:22
std::function< void(Model *)> NotEqual(IntegerVariable a, IntegerVariable b)
Definition: precedences.h:496
std::function< void(Model *)> ConditionalSum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub, const std::vector< Literal > &enforcement_literals)
Definition: precedences.h:381
std::function< void(Model *)> Sum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub)
Definition: precedences.h:352
std::function< void(Model *)> ConditionalLowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
Definition: precedences.h:419
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
Definition: integer.h:1495
std::function< void(Model *)> ConditionalSum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub, const std::vector< Literal > &enforcement_literals)
Definition: precedences.h:359
std::function< void(Model *)> Sum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub)
Definition: precedences.h:370
std::function< void(Model *)> ReifiedEqualityWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_eq)
Definition: precedences.h:477
std::function< void(Model *)> ReifiedLowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
Definition: precedences.h:445
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
Definition: integer.h:1509
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
Definition: integer.h:1524
std::function< void(Model *)> LowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset)
Definition: precedences.h:342
std::function< void(Model *)> EqualityWithOffset(IntegerVariable a, IntegerVariable b, int64 offset)
Definition: precedences.h:409
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:968
std::function< void(Model *)> ReifiedEquality(IntegerVariable a, IntegerVariable b, Literal is_eq)
Definition: precedences.h:459
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
std::function< void(Model *)> ConditionalLowerOrEqual(IntegerVariable a, IntegerVariable b, Literal is_le)
Definition: precedences.h:428
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 tail
int64 head