Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cuts.h
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
14#ifndef OR_TOOLS_SAT_CUTS_H_
15#define OR_TOOLS_SAT_CUTS_H_
16
17#include <stdint.h>
18
19#include <array>
20#include <cmath>
21#include <cstdlib>
22#include <functional>
23#include <string>
24#include <tuple>
25#include <utility>
26#include <vector>
27
28#include "absl/container/btree_map.h"
29#include "absl/container/btree_set.h"
30#include "absl/container/flat_hash_map.h"
31#include "absl/container/flat_hash_set.h"
32#include "absl/functional/any_invocable.h"
33#include "absl/numeric/int128.h"
34#include "absl/strings/str_cat.h"
35#include "absl/types/span.h"
38#include "ortools/sat/integer.h"
42#include "ortools/sat/model.h"
45
46namespace operations_research {
47namespace sat {
48
49// A "cut" generator on a set of IntegerVariable.
50//
51// The generate_cuts() function can get the current LP solution with
52// manager->LpValues(). Note that a CutGenerator should:
53// - Only look at the lp_values positions that corresponds to its 'vars' or
54// their negation.
55// - Only add cuts in term of the same variables or their negation.
58 std::vector<IntegerVariable> vars;
59 absl::AnyInvocable<bool(LinearConstraintManager* manager)> generate_cuts;
60};
61
62// To simplify cut generation code, we use a more complex data structure than
63// just a LinearConstraint to represent a cut with shifted/complemented variable
64// and implied bound substitution.
65struct CutTerm {
66 bool IsBoolean() const { return bound_diff == 1; }
67 bool IsSimple() const { return expr_coeffs[1] == 0; }
68 bool HasRelevantLpValue() const { return lp_value > 1e-2; }
69 bool IsFractional() const {
70 return std::abs(lp_value - std::round(lp_value)) > 1e-4;
71 }
72 double LpDistToMaxValue() const {
73 return static_cast<double>(bound_diff.value()) - lp_value;
74 }
75
76 std::string DebugString() const;
77
78 // Do the subtitution X -> (1 - X') and update the rhs.
79 //
80 // Our precondition on the sum of variable domains fitting an int64_t should
81 // ensure that this can never overflow.
82 void Complement(absl::int128* rhs);
83
84 // This assumes bound_diff == 1. It replaces the inner expression by either
85 // var or 1 - var depending on the positiveness of var.
86 void ReplaceExpressionByLiteral(IntegerVariable var);
87
88 // If the term correspond to literal_view or (1 - literal_view) return the
89 // integer variable representation of that literal. Returns kNoIntegerVariable
90 // if this is not the case.
91 IntegerVariable GetUnderlyingLiteralOrNone() const;
92
93 // Each term is of the form coeff * X where X is a variable with given
94 // lp_value and with a domain in [0, bound_diff]. Note X is always >= 0.
95 double lp_value = 0.0;
96 IntegerValue coeff = IntegerValue(0);
97 IntegerValue bound_diff = IntegerValue(0);
98
99 // X = the given LinearExpression.
100 // We only support size 1 or 2 here which allow to inline the memory.
101 // When a coefficient is zero, we don't care about the variable.
102 //
103 // TODO(user): We might want to store that elsewhere, as sorting CutTerm is a
104 // bit slow and we don't need to look at that in most places. Same for the
105 // cached_implied_lb/ub below.
106 IntegerValue expr_offset = IntegerValue(0);
107 std::array<IntegerVariable, 2> expr_vars;
108 std::array<IntegerValue, 2> expr_coeffs;
109
110 // Refer to cached_data_ in ImpliedBoundsProcessor.
113};
114
115// Our cut are always of the form linear_expression <= rhs.
116struct CutData {
117 // We need level zero bounds and LP relaxation values to fill a CutData.
118 // Returns false if we encounter any integer overflow.
120 const LinearConstraint& base_ct,
122 IntegerTrail* integer_trail);
123
124 bool FillFromParallelVectors(IntegerValue ub,
125 absl::Span<const IntegerVariable> vars,
126 absl::Span<const IntegerValue> coeffs,
127 absl::Span<const double> lp_values,
128 absl::Span<const IntegerValue> lower_bounds,
129 absl::Span<const IntegerValue> upper_bounds);
130
131 bool AppendOneTerm(IntegerVariable var, IntegerValue coeff, double lp_value,
132 IntegerValue lb, IntegerValue ub);
133
134 // These functions transform the cut by complementation.
135 bool AllCoefficientsArePositive() const;
138
139 // Computes and returns the cut violation.
140 double ComputeViolation() const;
141 double ComputeEfficacy() const;
142
143 // This sorts terms by decreasing lp values and fills both
144 // num_relevant_entries and max_magnitude.
145 void SortRelevantEntries();
146
147 std::string DebugString() const;
148
149 // Note that we use a 128 bit rhs so we can freely complement variable without
150 // running into overflow.
151 absl::int128 rhs;
152 std::vector<CutTerm> terms;
153
154 // Only filled after SortRelevantEntries().
155 IntegerValue max_magnitude;
157};
158
159// Stores temporaries used to build or manipulate a CutData.
161 public:
162 // Returns false if we encounter an integer overflow.
163 bool ConvertToLinearConstraint(const CutData& cut, LinearConstraint* output);
164
165 // These function allow to merges entries corresponding to the same variable
166 // and complementation. That is (X - lb) and (ub - X) are NOT merged and kept
167 // as separate terms. Note that we currently only merge Booleans since this
168 // is the only case we need.
169 //
170 // Return num_merges.
171 int AddOrMergeBooleanTerms(absl::Span<CutTerm> terms, IntegerValue t,
172 CutData* cut);
173
174 private:
175 bool MergeIfPossible(IntegerValue t, CutTerm& to_add, CutTerm& target);
176
177 absl::flat_hash_map<IntegerVariable, int> bool_index_;
178 absl::flat_hash_map<IntegerVariable, int> secondary_bool_index_;
179 absl::btree_map<IntegerVariable, IntegerValue> tmp_map_;
180};
181
182// Given an upper-bounded linear relation (sum terms <= ub), this algorithm
183// inspects the integer variable appearing in the sum and try to replace each of
184// them by a tight lower bound (>= coeff * binary + lb) using the implied bound
185// repository. By tight, we mean that it will take the same value under the
186// current LP solution.
187//
188// We use a class to reuse memory of the tmp terms.
190 public:
191 // We will only replace IntegerVariable appearing in lp_vars_.
192 ImpliedBoundsProcessor(absl::Span<const IntegerVariable> lp_vars_,
193 IntegerTrail* integer_trail,
194 ImpliedBounds* implied_bounds)
195 : lp_vars_(lp_vars_.begin(), lp_vars_.end()),
196 integer_trail_(integer_trail),
197 implied_bounds_(implied_bounds) {}
198
199 // See if some of the implied bounds equation are violated and add them to
200 // the IB cut pool if it is the case.
201 //
202 // Important: This must be called before we process any constraints with a
203 // different lp_values or level zero bounds.
206
207 // This assumes the term is simple: expr[0] = var - LB / UB - var. We use an
208 // implied lower bound on this expr, independently of the term.coeff sign.
209 //
210 // If possible, returns true and express X = bool_term + slack_term.
211 // If coeff of X is positive, then all coeff will be positive here.
213 IntegerValue factor_t, CutTerm& bool_term,
214 CutTerm& slack_term);
215
216 // This assumes the term is simple: expr[0] = var - LB / UB - var. We use
217 // an implied upper bound on this expr, independently of term.coeff sign.
218 //
219 // If possible, returns true and express X = bool_term + slack_term.
220 // If coeff of X is positive, then bool_term will have a positive coeff but
221 // slack_term will have a negative one.
223 IntegerValue factor_t, CutTerm& bool_term,
224 CutTerm& slack_term);
225
226 // We are about to apply the super-additive function f() to the CutData. Use
227 // implied bound information to eventually substitute and make the cut
228 // stronger. Returns the number of {lb_ib, ub_ib, merges} applied.
229 //
230 // This should lead to stronger cuts even if the norms migth be worse.
231 std::tuple<int, int, int> PostprocessWithImpliedBound(
232 const std::function<IntegerValue(IntegerValue)>& f, IntegerValue factor_t,
233 CutData* cut);
234
235 // Precomputes quantities used by all cut generation.
236 // This allows to do that once rather than 6 times.
237 // Return false if there are no exploitable implied bounds.
238 bool CacheDataForCut(IntegerVariable first_slack, CutData* cut);
239
240 bool TryToExpandWithLowerImpliedbound(IntegerValue factor_t, bool complement,
241 CutTerm* term, absl::int128* rhs,
242 std::vector<CutTerm>* new_bool_terms);
243
244 // This can be used to share the hash-map memory.
245 CutDataBuilder* MutableCutBuilder() { return &cut_builder_; }
246
247 // This can be used as a temporary storage for
248 // TryToExpandWithLowerImpliedbound().
249 std::vector<CutTerm>* ClearedMutableTempTerms() {
250 tmp_terms_.clear();
251 return &tmp_terms_;
252 }
253
254 // Add a new variable that could be used in the new cuts.
255 // Note that the cache must be computed to take this into account.
256 void AddLpVariable(IntegerVariable var) { lp_vars_.insert(var); }
257
258 // Once RecomputeCacheAndSeparateSomeImpliedBoundCuts() has been called,
259 // we can get the best implied bound for each variables.
260 //
261 // Note that because the variable level zero lower bound might change since
262 // the time this was cached, we just store the implied bound here.
264 double var_lp_value = 0.0;
265 double bool_lp_value = 0.0;
266 IntegerValue implied_bound;
267
268 // When VariableIsPositive(bool_var) then it is when this is one that the
269 // bound is implied. Otherwise it is when this is zero.
270 IntegerVariable bool_var = kNoIntegerVariable;
271
272 double SlackLpValue(IntegerValue lb) const {
273 const double bool_term =
274 static_cast<double>((implied_bound - lb).value()) * bool_lp_value;
275 return var_lp_value - static_cast<double>(lb.value()) - bool_term;
276 }
277
278 std::string DebugString() const {
279 return absl::StrCat("var - lb == (", implied_bound.value(),
280 " - lb) * bool(", bool_lp_value, ") + slack.");
281 }
282 };
283 BestImpliedBoundInfo GetCachedImpliedBoundInfo(IntegerVariable var) const;
284
285 // As we compute the best implied bounds for each variable, we add violated
286 // cuts here.
287 TopNCuts& IbCutPool() { return ib_cut_pool_; }
288
289 private:
290 BestImpliedBoundInfo ComputeBestImpliedBound(
291 IntegerVariable var,
293
294 absl::flat_hash_set<IntegerVariable> lp_vars_;
295 mutable absl::flat_hash_map<IntegerVariable, BestImpliedBoundInfo> cache_;
296
297 // Temporary data used by CacheDataForCut().
298 std::vector<CutTerm> tmp_terms_;
299 CutDataBuilder cut_builder_;
300 std::vector<BestImpliedBoundInfo> cached_data_;
301
302 TopNCuts ib_cut_pool_ = TopNCuts(50);
303
304 // Data from the constructor.
305 IntegerTrail* integer_trail_;
306 ImpliedBounds* implied_bounds_;
307};
308
309// Visible for testing. Returns a function f on integers such that:
310// - f is non-decreasing.
311// - f is super-additive: f(a) + f(b) <= f(a + b)
312// - 1 <= f(divisor) <= max_scaling
313// - For all x, f(x * divisor) = x * f(divisor)
314// - For all x, f(x * divisor + remainder) = x * f(divisor)
315//
316// Preconditions:
317// - 0 <= remainder < divisor.
318// - 1 <= max_scaling.
319//
320// This is used in IntegerRoundingCut() and is responsible for "strengthening"
321// the cut. Just taking f(x) = x / divisor result in the non-strengthened cut
322// and using any function that stricly dominate this one is better.
323//
324// Algorithm:
325// - We first scale by a factor t so that rhs_remainder >= divisor / 2.
326// - Then, if max_scaling == 2, we use the function described
327// in "Strenghtening Chvatal-Gomory cuts and Gomory fractional cuts", Adam N.
328// Letchfrod, Andrea Lodi.
329// - Otherwise, we use a generalization of this which is a discretized version
330// of the classical MIR rounding function that only take the value of the
331// form "an_integer / max_scaling". As max_scaling goes to infinity, this
332// converge to the real-valued MIR function.
333//
334// Note that for each value of max_scaling we will get a different function.
335// And that there is no dominance relation between any of these functions. So
336// it could be nice to try to generate a cut using different values of
337// max_scaling.
338IntegerValue GetFactorT(IntegerValue rhs_remainder, IntegerValue divisor,
339 IntegerValue max_magnitude);
340std::function<IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction(
341 IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t,
342 IntegerValue max_scaling);
343
344// If we have an equation sum ci.Xi >= rhs with everything positive, and all
345// ci are >= min_magnitude then any ci >= rhs can be set to rhs. Also if
346// some ci are in [rhs - min, rhs) then they can be strenghtened to rhs - min.
347//
348// If we apply this to the negated equation (sum -ci.Xi + sum cj.Xj <= -rhs)
349// with potentially positive terms, this reduce to apply a super-additive
350// function:
351//
352// Plot look like:
353// x=-rhs x=0
354// | |
355// y=0 : | ---------------------------------
356// | ---
357// | /
358// |---
359// y=-rhs -------
360//
361// TODO(user): Extend it for ci >= max_magnitude, we can probaly "lift" such
362// coefficient.
363std::function<IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningFunction(
364 IntegerValue positive_rhs, IntegerValue min_magnitude);
365
366// Similar to above but with scaling of the linear part to just have at most
367// scaling values.
368std::function<IntegerValue(IntegerValue)>
369GetSuperAdditiveStrengtheningMirFunction(IntegerValue positive_rhs,
370 IntegerValue scaling);
371
372// Given a super-additive non-decreasing function f(), we periodically extend
373// its restriction from [-period, 0] to Z. Such extension is not always
374// super-additive and it is up to the caller to know when this is true or not.
375inline std::function<IntegerValue(IntegerValue)> ExtendNegativeFunction(
376 std::function<IntegerValue(IntegerValue)> base_f, IntegerValue period) {
377 const IntegerValue m = -base_f(-period);
378 return [m, period, base_f](IntegerValue v) {
379 const IntegerValue r = PositiveRemainder(v, period);
380 const IntegerValue output_r = m + base_f(r - period);
381 return FloorRatio(v, period) * m + output_r;
382 };
383}
384
385// Given an upper bounded linear constraint, this function tries to transform it
386// to a valid cut that violate the given LP solution using integer rounding.
387// Note that the returned cut might not always violate the LP solution, in which
388// case it can be discarded.
389//
390// What this does is basically take the integer division of the constraint by an
391// integer. If the coefficients where doubles, this would be the same as scaling
392// the constraint and then rounding. We choose the coefficient of the most
393// fractional variable (rescaled by its coefficient) as the divisor, but there
394// are other possible alternatives.
395//
396// Note that if the constraint is tight under the given lp solution, and if
397// there is a unique variable not at one of its bounds and fractional, then we
398// are guaranteed to generate a cut that violate the current LP solution. This
399// should be the case for Chvatal-Gomory base constraints modulo our loss of
400// precision while doing exact integer computations.
401//
402// Precondition:
403// - We assumes that the given initial constraint is tight using the given lp
404// values. This could be relaxed, but for now it should always be the case, so
405// we log a message and abort if not, to ease debugging.
406// - The IntegerVariable of the cuts are not used here. We assumes that the
407// first three vectors are in one to one correspondence with the initial order
408// of the variable in the cut.
409//
410// TODO(user): There is a bunch of heuristic involved here, and we could spend
411// more effort tuning them. In particular, one can try many heuristics and keep
412// the best looking cut (or more than one). This is not on the critical code
413// path, so we can spend more effort in finding good cuts.
415 IntegerValue max_scaling = IntegerValue(60);
418};
420 public:
422
423 // Returns true on success. The cut can be accessed via cut().
424 bool ComputeCut(RoundingOptions options, const CutData& base_ct,
425 ImpliedBoundsProcessor* ib_processor = nullptr);
426
427 // If successful, info about the last generated cut.
428 const CutData& cut() const { return cut_; }
429
430 void SetSharedStatistics(SharedStatistics* stats) { shared_stats_ = stats; }
431
432 // Single line of text that we append to the cut log line.
433 std::string Info() const { return absl::StrCat("ib_lift=", num_ib_used_); }
434
435 private:
436 double GetScaledViolation(IntegerValue divisor, IntegerValue max_scaling,
437 IntegerValue remainder_threshold,
438 const CutData& cut);
439
440 // The helper is just here to reuse the memory for these vectors.
441 std::vector<IntegerValue> divisors_;
442 std::vector<IntegerValue> remainders_;
443 std::vector<IntegerValue> rs_;
444 std::vector<IntegerValue> best_rs_;
445
446 int64_t num_ib_used_ = 0;
447 CutData cut_;
448
449 std::vector<std::pair<int, IntegerValue>> adjusted_coeffs_;
450 std::vector<std::pair<int, IntegerValue>> best_adjusted_coeffs_;
451
452 // Overall stats.
453 SharedStatistics* shared_stats_ = nullptr;
454 int64_t total_num_dominating_f_ = 0;
455 int64_t total_num_pos_lifts_ = 0;
456 int64_t total_num_neg_lifts_ = 0;
457 int64_t total_num_post_complements_ = 0;
458 int64_t total_num_overflow_abort_ = 0;
459 int64_t total_num_coeff_adjust_ = 0;
460 int64_t total_num_merges_ = 0;
461 int64_t total_num_bumps_ = 0;
462 int64_t total_num_final_complements_ = 0;
463
464 int64_t total_num_initial_ibs_ = 0;
465 int64_t total_num_initial_merges_ = 0;
466};
467
468// Helper to find knapsack cover cuts.
470 public:
472
473 // Try to find a cut with a knapsack heuristic. This assumes an input with all
474 // coefficients positive. If this returns true, you can get the cut via cut().
475 //
476 // This uses a lifting procedure similar to what is described in "Lifting the
477 // Knapsack Cover Inequalities for the Knapsack Polytope", Adam N. Letchfod,
478 // Georgia Souli. In particular the section "Lifting via mixed-integer
479 // rounding".
480 bool TrySimpleKnapsack(const CutData& input_ct,
481 ImpliedBoundsProcessor* ib_processor = nullptr);
482
483 // Applies the lifting procedure described in "On Lifted Cover Inequalities: A
484 // New Lifting Procedure with Unusual Properties", Adam N. Letchford, Georgia
485 // Souli. This assumes an input with all coefficients positive.
486 //
487 // The algo is pretty simple, given a cover C for a given rhs. We compute
488 // a rational weight p/q so that sum_C min(w_i, p/q) = rhs. Note that q is
489 // pretty small (lower or equal to the size of C). The generated cut is then
490 // of the form
491 // sum X_i in C for which w_i <= p / q
492 // + sum gamma_i X_i for the other variable <= |C| - 1.
493 //
494 // gamma_i being the smallest k such that w_i <= sum of the k + 1 largest
495 // min(w_i, p/q) for i in C. In particular, it is zero if w_i <= p/q.
496 //
497 // Note that this accept a general constraint that has been canonicalized to
498 // sum coeff_i * X_i <= base_rhs. Each coeff_i >= 0 and each X_i >= 0.
499 //
500 // TODO(user): Generalize to non-Boolean, or use a different cover heuristic
501 // for this:
502 // - We want a Boolean only cover currently.
503 // - We can always use implied bound for this, since there is more chance
504 // for a Bool only cover.
505 // - Also, f() should be super additive on the value <= rhs, i.e. f(a + b) >=
506 // f(a) + f(b), so it is always good to use implied bounds of the form X =
507 // bound * B + Slack.
509 const CutData& input_ct, ImpliedBoundsProcessor* ib_processor = nullptr);
510
511 // It turns out that what FlowCoverCutHelper is doing is really just finding a
512 // cover and generating a cut via coefficient strenghtening instead of MIR
513 // rounding. This more generic version should just always outperform our old
514 // code.
515 bool TrySingleNodeFlow(const CutData& input_ct,
516 ImpliedBoundsProcessor* ib_processor = nullptr);
517
518 // If successful, info about the last generated cut.
519 const CutData& cut() const { return cut_; }
520
521 // Single line of text that we append to the cut log line.
522 std::string Info() const { return absl::StrCat("lift=", num_lifting_); }
523
524 void SetSharedStatistics(SharedStatistics* stats) { shared_stats_ = stats; }
525
526 void ClearCache() { has_bool_base_ct_ = false; }
527
528 private:
529 void InitializeCut(const CutData& input_ct);
530
531 // This looks at base_ct_ and reoder the terms so that the first ones are in
532 // the cover. return zero if no interesting cover was found.
533 template <class CompareAdd, class CompareRemove>
534 int GetCoverSize(int relevant_size);
535
536 // Same as GetCoverSize() but only look at Booleans, and use a different
537 // heuristic.
538 int GetCoverSizeForBooleans();
539
540 template <class Compare>
541 int MinimizeCover(int cover_size, absl::int128 slack);
542
543 // Here to reuse memory, cut_ is both the input and the output.
544 CutData cut_;
545 CutData temp_cut_;
546
547 // Hack to not sort twice.
548 bool has_bool_base_ct_ = false;
549 CutData bool_base_ct_;
550 int bool_cover_size_ = 0;
551
552 // Stats.
553 SharedStatistics* shared_stats_ = nullptr;
554 int64_t num_lifting_ = 0;
555
556 // Stats for the various type of cuts generated here.
557 struct CutStats {
558 int64_t num_cuts = 0;
559 int64_t num_initial_ibs = 0;
560 int64_t num_lb_ibs = 0;
561 int64_t num_ub_ibs = 0;
562 int64_t num_merges = 0;
563 int64_t num_bumps = 0;
564 int64_t num_lifting = 0;
565 int64_t num_overflow_aborts = 0;
566 };
567 CutStats flow_stats_;
568 CutStats cover_stats_;
569 CutStats ls_stats_;
570};
571
572// Separate RLT cuts.
573//
574// See for instance "Efficient Separation of RLT Cuts for Implicit and Explicit
575// Bilinear Products", Ksenia Bestuzheva, Ambros Gleixner, Tobias Achterberg,
576// https://arxiv.org/abs/2211.13545
578 public:
579 explicit BoolRLTCutHelper(Model* model)
580 : product_detector_(model->GetOrCreate<ProductDetector>()),
581 shared_stats_(model->GetOrCreate<SharedStatistics>()),
582 lp_values_(model->GetOrCreate<ModelLpValues>()) {};
584
585 // Precompute data according to the current lp relaxation.
586 // This also restrict any Boolean to be currently appearing in the LP.
587 void Initialize(absl::Span<const IntegerVariable> lp_vars);
588
589 // Tries RLT separation of the input constraint. Returns true on success.
590 bool TrySimpleSeparation(const CutData& input_ct);
591
592 // If successful, this contains the last generated cut.
593 const CutData& cut() const { return cut_; }
594
595 // Single line of text that we append to the cut log line.
596 std::string Info() const { return ""; }
597
598 private:
599 // LP value of a literal encoded as an IntegerVariable.
600 // That is lit(X) = X if X positive or 1 - X otherwise.
601 double GetLiteralLpValue(IntegerVariable var) const;
602
603 // Multiplies input by lit(factor) and linearize in the best possible way.
604 // The result will be stored in cut_.
605 bool TryProduct(IntegerVariable factor, const CutData& input);
606
607 bool enabled_ = false;
608 CutData filtered_input_;
609 CutData cut_;
610
611 ProductDetector* product_detector_;
612 SharedStatistics* shared_stats_;
613 ModelLpValues* lp_values_;
614
615 int64_t num_tried_ = 0;
616 int64_t num_tried_factors_ = 0;
617};
618
619// A cut generator for z = x * y (x and y >= 0).
620CutGenerator CreatePositiveMultiplicationCutGenerator(AffineExpression z,
621 AffineExpression x,
622 AffineExpression y,
623 int linearization_level,
624 Model* model);
625
626// Above hyperplan for square = x * x: square should be below the line
627// (x_lb, x_lb ^ 2) to (x_ub, x_ub ^ 2).
628// The slope of that line is (ub^2 - lb^2) / (ub - lb) = ub + lb.
629// square <= (x_lb + x_ub) * x - x_lb * x_ub
630// This only works for positive x.
631LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x,
632 AffineExpression square,
633 IntegerValue x_lb,
634 IntegerValue x_ub, Model* model);
635
636// Below hyperplan for square = x * x: y should be above the line
637// (x_value, x_value ^ 2) to (x_value + 1, (x_value + 1) ^ 2)
638// The slope of that line is 2 * x_value + 1
639// square >= below_slope * (x - x_value) + x_value ^ 2
640// square >= below_slope * x - x_value ^ 2 - x_value
641LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x,
642 AffineExpression square,
643 IntegerValue x_value,
644 Model* model);
645
646// A cut generator for y = x ^ 2 (x >= 0).
647// It will dynamically add a linear inequality to push y closer to the parabola.
648CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x,
649 int linearization_level, Model* model);
650
651// A cut generator for all_diff(xi). Let the united domain of all xi be D. Sum
652// of any k-sized subset of xi need to be greater or equal to the sum of
653// smallest k values in D and lesser or equal to the sum of largest k values in
654// D. The cut generator first sorts the variables based on LP values and adds
655// cuts of the form described above if they are violated by lp solution. Note
656// that all the fixed variables are ignored while generating cuts.
658 absl::Span<const AffineExpression> exprs, Model* model);
659
660// Consider the Lin Max constraint with d expressions and n variables in the
661// form: target = max {exprs[k] = Sum (wki * xi + bk)}. k in {1,..,d}.
662// Li = lower bound of xi
663// Ui = upper bound of xi.
664// Let zk be in {0,1} for all k in {1,..,d}.
665// The target = exprs[k] when zk = 1.
666//
667// The following is a valid linearization for Lin Max.
668// target >= exprs[k], for all k in {1,..,d}
669// target <= Sum (wli * xi) + Sum((Nlk + bk) * zk), for all l in {1,..,d}
670// Where Nlk is a large number defined as:
671// Nlk = Sum (max((wki - wli)*Li, (wki - wli)*Ui))
672// = Sum (max corner difference for variable i, target expr l, max expr k)
673//
674// Consider a partition of variables xi into set {1,..,d} as I.
675// i.e. I(i) = j means xi is mapped to jth index.
676// The following inequality is valid and sharp cut for the lin max constraint
677// described above.
678//
679// target <= Sum(i=1..n)(wI(i)i * xi + Sum(k=1..d)(MPlusCoefficient_ki * zk))
680// + Sum(k=1..d)(bk * zk) ,
681// Where MPlusCoefficient_ki = max((wki - wI(i)i) * Li,
682// (wki - wI(i)i) * Ui)
683// = max corner difference for variable i,
684// target expr I(i), max expr k.
685//
686// For detailed proof of validity, refer
687// Reference: "Strong mixed-integer programming formulations for trained neural
688// networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf).
689//
690// In the cut generator, we compute the most violated partition I by computing
691// the rhs value (wI(i)i * lp_value(xi) + Sum(k=1..d)(MPlusCoefficient_ki * zk))
692// for each variable for each partition index. We choose the partition index
693// that gives lowest rhs value for a given variable.
694//
695// Note: This cut generator requires all expressions to contain only positive
696// vars.
697CutGenerator CreateLinMaxCutGenerator(IntegerVariable target,
698 absl::Span<const LinearExpression> exprs,
699 absl::Span<const IntegerVariable> z_vars,
700 Model* model);
701
702// Helper for the affine max constraint.
703//
704// This function will reset the bounds of the builder.
706 const LinearExpression& target, IntegerVariable var,
707 absl::Span<const std::pair<IntegerValue, IntegerValue>> affines,
708 Model* model, LinearConstraintBuilder* builder);
709
710// By definition, the Max of affine functions is convex. The linear polytope is
711// bounded by all affine functions on the bottom, and by a single hyperplane
712// that join the two points at the extreme of the var domain, and their y-values
713// of the max of the affine functions.
714CutGenerator CreateMaxAffineCutGenerator(
715 LinearExpression target, IntegerVariable var,
716 std::vector<std::pair<IntegerValue, IntegerValue>> affines,
717 std::string cut_name, Model* model);
718
719// Extracts the variables that have a Literal view from base variables and
720// create a generator that will returns constraint of the form "at_most_one"
721// between such literals.
722CutGenerator CreateCliqueCutGenerator(
723 absl::Span<const IntegerVariable> base_variables, Model* model);
724
725// Utility class for the AllDiff cut generator.
727 public:
728 void Clear();
729 void Add(const AffineExpression& expr, int num_expr,
730 const IntegerTrail& integer_trail);
731
732 // Return int_max if the sum overflows.
733 IntegerValue SumOfMinDomainValues();
734 IntegerValue SumOfDifferentMins();
735 IntegerValue GetBestLowerBound(std::string& suffix);
736
737 int size() const { return expr_mins_.size(); }
738
739 private:
740 absl::btree_set<IntegerValue> min_values_;
741 std::vector<IntegerValue> expr_mins_;
742};
743
744} // namespace sat
745} // namespace operations_research
746
747#endif // OR_TOOLS_SAT_CUTS_H_
Definition model.h:341
bool TrySimpleSeparation(const CutData &input_ct)
Tries RLT separation of the input constraint. Returns true on success.
Definition cuts.cc:1677
void Initialize(absl::Span< const IntegerVariable > lp_vars)
Definition cuts.cc:1671
std::string Info() const
Single line of text that we append to the cut log line.
Definition cuts.h:596
const CutData & cut() const
If successful, this contains the last generated cut.
Definition cuts.h:593
Helper to find knapsack cover cuts.
Definition cuts.h:469
const CutData & cut() const
If successful, info about the last generated cut.
Definition cuts.h:519
bool TrySimpleKnapsack(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Definition cuts.cc:1304
std::string Info() const
Single line of text that we append to the cut log line.
Definition cuts.h:522
bool TryWithLetchfordSouliLifting(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Definition cuts.cc:1526
void SetSharedStatistics(SharedStatistics *stats)
Definition cuts.h:524
bool TrySingleNodeFlow(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Definition cuts.cc:1422
Stores temporaries used to build or manipulate a CutData.
Definition cuts.h:160
bool ConvertToLinearConstraint(const CutData &cut, LinearConstraint *output)
Returns false if we encounter an integer overflow.
Definition cuts.cc:353
int AddOrMergeBooleanTerms(absl::Span< CutTerm > terms, IntegerValue t, CutData *cut)
Definition cuts.cc:300
std::vector< CutTerm > * ClearedMutableTempTerms()
Definition cuts.h:249
void RecomputeCacheAndSeparateSomeImpliedBoundCuts(const util_intops::StrongVector< IntegerVariable, double > &lp_values)
Definition cuts.cc:2111
bool CacheDataForCut(IntegerVariable first_slack, CutData *cut)
Definition cuts.cc:2321
bool TryToExpandWithLowerImpliedbound(IntegerValue factor_t, bool complement, CutTerm *term, absl::int128 *rhs, std::vector< CutTerm > *new_bool_terms)
Definition cuts.cc:2293
ImpliedBoundsProcessor(absl::Span< const IntegerVariable > lp_vars_, IntegerTrail *integer_trail, ImpliedBounds *implied_bounds)
We will only replace IntegerVariable appearing in lp_vars_.
Definition cuts.h:192
void AddLpVariable(IntegerVariable var)
Definition cuts.h:256
BestImpliedBoundInfo GetCachedImpliedBoundInfo(IntegerVariable var) const
Definition cuts.cc:2031
CutDataBuilder * MutableCutBuilder()
This can be used to share the hash-map memory.
Definition cuts.h:245
bool DecomposeWithImpliedLowerBound(const CutTerm &term, IntegerValue factor_t, CutTerm &bool_term, CutTerm &slack_term)
Definition cuts.cc:2121
std::tuple< int, int, int > PostprocessWithImpliedBound(const std::function< IntegerValue(IntegerValue)> &f, IntegerValue factor_t, CutData *cut)
Definition cuts.cc:2212
bool DecomposeWithImpliedUpperBound(const CutTerm &term, IntegerValue factor_t, CutTerm &bool_term, CutTerm &slack_term)
Definition cuts.cc:2191
bool ComputeCut(RoundingOptions options, const CutData &base_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Returns true on success. The cut can be accessed via cut().
Definition cuts.cc:774
const CutData & cut() const
If successful, info about the last generated cut.
Definition cuts.h:428
std::string Info() const
Single line of text that we append to the cut log line.
Definition cuts.h:433
void SetSharedStatistics(SharedStatistics *stats)
Definition cuts.h:430
Simple class to add statistics by name and print them at the end.
Utility class for the AllDiff cut generator.
Definition cuts.h:726
IntegerValue GetBestLowerBound(std::string &suffix)
Definition cuts.cc:2404
void Add(const AffineExpression &expr, int num_expr, const IntegerTrail &integer_trail)
Definition cuts.cc:2357
IntegerValue SumOfMinDomainValues()
Return int_max if the sum overflows.
Definition cuts.cc:2382
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
bool BuildMaxAffineUpConstraint(const LinearExpression &target, IntegerVariable var, absl::Span< const std::pair< IntegerValue, IntegerValue > > affines, Model *model, LinearConstraintBuilder *builder)
Definition cuts.cc:2668
IntegerValue GetFactorT(IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue max_magnitude)
Definition cuts.cc:471
CutGenerator CreatePositiveMultiplicationCutGenerator(AffineExpression z, AffineExpression x, AffineExpression y, int linearization_level, Model *model)
A cut generator for z = x * y (x and y >= 0).
Definition cuts.cc:1876
LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x, AffineExpression square, IntegerValue x_value, Model *model)
Definition cuts.cc:1983
const IntegerVariable kNoIntegerVariable(-1)
CutGenerator CreateLinMaxCutGenerator(const IntegerVariable target, absl::Span< const LinearExpression > exprs, absl::Span< const IntegerVariable > z_vars, Model *model)
Definition cuts.cc:2579
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningFunction(IntegerValue positive_rhs, IntegerValue min_magnitude)
Definition cuts.cc:570
CutGenerator CreateAllDifferentCutGenerator(absl::Span< const AffineExpression > exprs, Model *model)
Definition cuts.cc:2467
CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x, int linearization_level, Model *model)
Definition cuts.cc:1995
CutGenerator CreateCliqueCutGenerator(absl::Span< const IntegerVariable > base_variables, Model *model)
Definition cuts.cc:2744
IntegerValue PositiveRemainder(IntegerValue dividend, IntegerValue positive_divisor)
CutGenerator CreateMaxAffineCutGenerator(LinearExpression target, IntegerVariable var, std::vector< std::pair< IntegerValue, IntegerValue > > affines, const std::string cut_name, Model *model)
Definition cuts.cc:2722
LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x, AffineExpression square, IntegerValue x_lb, IntegerValue x_ub, Model *model)
Definition cuts.cc:1971
std::function< IntegerValue(IntegerValue)> ExtendNegativeFunction(std::function< IntegerValue(IntegerValue)> base_f, IntegerValue period)
Definition cuts.h:375
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningMirFunction(IntegerValue positive_rhs, IntegerValue scaling)
Definition cuts.cc:605
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction(IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t, IntegerValue max_scaling)
Definition cuts.cc:485
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
ClosedInterval::Iterator begin(ClosedInterval interval)
static int input(yyscan_t yyscanner)
Our cut are always of the form linear_expression <= rhs.
Definition cuts.h:116
bool FillFromLinearConstraint(const LinearConstraint &base_ct, const util_intops::StrongVector< IntegerVariable, double > &lp_values, IntegerTrail *integer_trail)
Definition cuts.cc:174
bool AllCoefficientsArePositive() const
These functions transform the cut by complementation.
Definition cuts.cc:232
std::vector< CutTerm > terms
Definition cuts.h:152
bool FillFromParallelVectors(IntegerValue ub, absl::Span< const IntegerVariable > vars, absl::Span< const IntegerValue > coeffs, absl::Span< const double > lp_values, absl::Span< const IntegerValue > lower_bounds, absl::Span< const IntegerValue > upper_bounds)
Definition cuts.cc:192
double ComputeEfficacy() const
Definition cuts.cc:265
std::string DebugString() const
Definition cuts.cc:76
double ComputeViolation() const
Computes and returns the cut violation.
Definition cuts.cc:257
IntegerValue max_magnitude
Only filled after SortRelevantEntries().
Definition cuts.h:155
bool AppendOneTerm(IntegerVariable var, IntegerValue coeff, double lp_value, IntegerValue lb, IntegerValue ub)
Definition cuts.cc:137
absl::AnyInvocable< bool(LinearConstraintManager *manager)> generate_cuts
Definition cuts.h:59
std::vector< IntegerVariable > vars
Definition cuts.h:58
IntegerVariable GetUnderlyingLiteralOrNone() const
Definition cuts.cc:117
std::string DebugString() const
Definition cuts.cc:68
int cached_implied_lb
Refer to cached_data_ in ImpliedBoundsProcessor.
Definition cuts.h:111
double LpDistToMaxValue() const
Definition cuts.h:72
void ReplaceExpressionByLiteral(IntegerVariable var)
Definition cuts.cc:103
void Complement(absl::int128 *rhs)
Definition cuts.cc:84
std::array< IntegerVariable, 2 > expr_vars
Definition cuts.h:107
std::array< IntegerValue, 2 > expr_coeffs
Definition cuts.h:108
bool HasRelevantLpValue() const
Definition cuts.h:68