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