Google OR-Tools v9.12
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;
267 IntegerValue implied_bound;
268 IntegerVariable bool_var = kNoIntegerVariable;
269
270 double SlackLpValue(IntegerValue lb) const {
271 const double bool_term =
272 static_cast<double>((implied_bound - lb).value()) * bool_lp_value;
273 return var_lp_value - static_cast<double>(lb.value()) - bool_term;
274 }
275
276 std::string DebugString() const {
277 return absl::StrCat("var - lb == (", implied_bound.value(),
278 " - lb) * bool(", bool_lp_value, ") + slack.");
279 }
280 };
281 BestImpliedBoundInfo GetCachedImpliedBoundInfo(IntegerVariable var) const;
282
283 // As we compute the best implied bounds for each variable, we add violated
284 // cuts here.
285 TopNCuts& IbCutPool() { return ib_cut_pool_; }
286
287 private:
288 BestImpliedBoundInfo ComputeBestImpliedBound(
289 IntegerVariable var,
291
292 absl::flat_hash_set<IntegerVariable> lp_vars_;
293 mutable absl::flat_hash_map<IntegerVariable, BestImpliedBoundInfo> cache_;
294
295 // Temporary data used by CacheDataForCut().
296 std::vector<CutTerm> tmp_terms_;
297 CutDataBuilder cut_builder_;
298 std::vector<BestImpliedBoundInfo> cached_data_;
299
300 TopNCuts ib_cut_pool_ = TopNCuts(50);
301
302 // Data from the constructor.
303 IntegerTrail* integer_trail_;
304 ImpliedBounds* implied_bounds_;
305};
306
307// Visible for testing. Returns a function f on integers such that:
308// - f is non-decreasing.
309// - f is super-additive: f(a) + f(b) <= f(a + b)
310// - 1 <= f(divisor) <= max_scaling
311// - For all x, f(x * divisor) = x * f(divisor)
312// - For all x, f(x * divisor + remainder) = x * f(divisor)
313//
314// Preconditions:
315// - 0 <= remainder < divisor.
316// - 1 <= max_scaling.
317//
318// This is used in IntegerRoundingCut() and is responsible for "strengthening"
319// the cut. Just taking f(x) = x / divisor result in the non-strengthened cut
320// and using any function that stricly dominate this one is better.
321//
322// Algorithm:
323// - We first scale by a factor t so that rhs_remainder >= divisor / 2.
324// - Then, if max_scaling == 2, we use the function described
325// in "Strenghtening Chvatal-Gomory cuts and Gomory fractional cuts", Adam N.
326// Letchfrod, Andrea Lodi.
327// - Otherwise, we use a generalization of this which is a discretized version
328// of the classical MIR rounding function that only take the value of the
329// form "an_integer / max_scaling". As max_scaling goes to infinity, this
330// converge to the real-valued MIR function.
331//
332// Note that for each value of max_scaling we will get a different function.
333// And that there is no dominance relation between any of these functions. So
334// it could be nice to try to generate a cut using different values of
335// max_scaling.
336IntegerValue GetFactorT(IntegerValue rhs_remainder, IntegerValue divisor,
337 IntegerValue max_magnitude);
338std::function<IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction(
339 IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t,
340 IntegerValue max_scaling);
341
342// If we have an equation sum ci.Xi >= rhs with everything positive, and all
343// ci are >= min_magnitude then any ci >= rhs can be set to rhs. Also if
344// some ci are in [rhs - min, rhs) then they can be strenghtened to rhs - min.
345//
346// If we apply this to the negated equation (sum -ci.Xi + sum cj.Xj <= -rhs)
347// with potentially positive terms, this reduce to apply a super-additive
348// function:
349//
350// Plot look like:
351// x=-rhs x=0
352// | |
353// y=0 : | ---------------------------------
354// | ---
355// | /
356// |---
357// y=-rhs -------
358//
359// TODO(user): Extend it for ci >= max_magnitude, we can probaly "lift" such
360// coefficient.
361std::function<IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningFunction(
362 IntegerValue positive_rhs, IntegerValue min_magnitude);
363
364// Similar to above but with scaling of the linear part to just have at most
365// scaling values.
366std::function<IntegerValue(IntegerValue)>
367GetSuperAdditiveStrengtheningMirFunction(IntegerValue positive_rhs,
368 IntegerValue scaling);
369
370// Given a super-additive non-decreasing function f(), we periodically extend
371// its restriction from [-period, 0] to Z. Such extension is not always
372// super-additive and it is up to the caller to know when this is true or not.
373inline std::function<IntegerValue(IntegerValue)> ExtendNegativeFunction(
374 std::function<IntegerValue(IntegerValue)> base_f, IntegerValue period) {
375 const IntegerValue m = -base_f(-period);
376 return [m, period, base_f](IntegerValue v) {
377 const IntegerValue r = PositiveRemainder(v, period);
378 const IntegerValue output_r = m + base_f(r - period);
379 return FloorRatio(v, period) * m + output_r;
380 };
381}
382
383// Given an upper bounded linear constraint, this function tries to transform it
384// to a valid cut that violate the given LP solution using integer rounding.
385// Note that the returned cut might not always violate the LP solution, in which
386// case it can be discarded.
387//
388// What this does is basically take the integer division of the constraint by an
389// integer. If the coefficients where doubles, this would be the same as scaling
390// the constraint and then rounding. We choose the coefficient of the most
391// fractional variable (rescaled by its coefficient) as the divisor, but there
392// are other possible alternatives.
393//
394// Note that if the constraint is tight under the given lp solution, and if
395// there is a unique variable not at one of its bounds and fractional, then we
396// are guaranteed to generate a cut that violate the current LP solution. This
397// should be the case for Chvatal-Gomory base constraints modulo our loss of
398// precision while doing exact integer computations.
399//
400// Precondition:
401// - We assumes that the given initial constraint is tight using the given lp
402// values. This could be relaxed, but for now it should always be the case, so
403// we log a message and abort if not, to ease debugging.
404// - The IntegerVariable of the cuts are not used here. We assumes that the
405// first three vectors are in one to one correspondence with the initial order
406// of the variable in the cut.
407//
408// TODO(user): There is a bunch of heuristic involved here, and we could spend
409// more effort tuning them. In particular, one can try many heuristics and keep
410// the best looking cut (or more than one). This is not on the critical code
411// path, so we can spend more effort in finding good cuts.
413 IntegerValue max_scaling = IntegerValue(60);
416};
418 public:
420
421 // Returns true on success. The cut can be accessed via cut().
422 bool ComputeCut(RoundingOptions options, const CutData& base_ct,
423 ImpliedBoundsProcessor* ib_processor = nullptr);
424
425 // If successful, info about the last generated cut.
426 const CutData& cut() const { return cut_; }
427
428 void SetSharedStatistics(SharedStatistics* stats) { shared_stats_ = stats; }
429
430 // Single line of text that we append to the cut log line.
431 std::string Info() const { return absl::StrCat("ib_lift=", num_ib_used_); }
432
433 private:
434 double GetScaledViolation(IntegerValue divisor, IntegerValue max_scaling,
435 IntegerValue remainder_threshold,
436 const CutData& cut);
437
438 // The helper is just here to reuse the memory for these vectors.
439 std::vector<IntegerValue> divisors_;
440 std::vector<IntegerValue> remainders_;
441 std::vector<IntegerValue> rs_;
442 std::vector<IntegerValue> best_rs_;
443
444 int64_t num_ib_used_ = 0;
445 CutData cut_;
446
447 std::vector<std::pair<int, IntegerValue>> adjusted_coeffs_;
448 std::vector<std::pair<int, IntegerValue>> best_adjusted_coeffs_;
449
450 // Overall stats.
451 SharedStatistics* shared_stats_ = nullptr;
452 int64_t total_num_dominating_f_ = 0;
453 int64_t total_num_pos_lifts_ = 0;
454 int64_t total_num_neg_lifts_ = 0;
455 int64_t total_num_post_complements_ = 0;
456 int64_t total_num_overflow_abort_ = 0;
457 int64_t total_num_coeff_adjust_ = 0;
458 int64_t total_num_merges_ = 0;
459 int64_t total_num_bumps_ = 0;
460 int64_t total_num_final_complements_ = 0;
461
462 int64_t total_num_initial_ibs_ = 0;
463 int64_t total_num_initial_merges_ = 0;
464};
465
466// Helper to find knapsack cover cuts.
468 public:
470
471 // Try to find a cut with a knapsack heuristic. This assumes an input with all
472 // coefficients positive. If this returns true, you can get the cut via cut().
473 //
474 // This uses a lifting procedure similar to what is described in "Lifting the
475 // Knapsack Cover Inequalities for the Knapsack Polytope", Adam N. Letchfod,
476 // Georgia Souli. In particular the section "Lifting via mixed-integer
477 // rounding".
478 bool TrySimpleKnapsack(const CutData& input_ct,
479 ImpliedBoundsProcessor* ib_processor = nullptr);
480
481 // Applies the lifting procedure described in "On Lifted Cover Inequalities: A
482 // New Lifting Procedure with Unusual Properties", Adam N. Letchford, Georgia
483 // Souli. This assumes an input with all coefficients positive.
484 //
485 // The algo is pretty simple, given a cover C for a given rhs. We compute
486 // a rational weight p/q so that sum_C min(w_i, p/q) = rhs. Note that q is
487 // pretty small (lower or equal to the size of C). The generated cut is then
488 // of the form
489 // sum X_i in C for which w_i <= p / q
490 // + sum gamma_i X_i for the other variable <= |C| - 1.
491 //
492 // gamma_i being the smallest k such that w_i <= sum of the k + 1 largest
493 // min(w_i, p/q) for i in C. In particular, it is zero if w_i <= p/q.
494 //
495 // Note that this accept a general constraint that has been canonicalized to
496 // sum coeff_i * X_i <= base_rhs. Each coeff_i >= 0 and each X_i >= 0.
497 //
498 // TODO(user): Generalize to non-Boolean, or use a different cover heuristic
499 // for this:
500 // - We want a Boolean only cover currently.
501 // - We can always use implied bound for this, since there is more chance
502 // for a Bool only cover.
503 // - Also, f() should be super additive on the value <= rhs, i.e. f(a + b) >=
504 // f(a) + f(b), so it is always good to use implied bounds of the form X =
505 // bound * B + Slack.
507 const CutData& input_ct, ImpliedBoundsProcessor* ib_processor = nullptr);
508
509 // It turns out that what FlowCoverCutHelper is doing is really just finding a
510 // cover and generating a cut via coefficient strenghtening instead of MIR
511 // rounding. This more generic version should just always outperform our old
512 // code.
513 bool TrySingleNodeFlow(const CutData& input_ct,
514 ImpliedBoundsProcessor* ib_processor = nullptr);
515
516 // If successful, info about the last generated cut.
517 const CutData& cut() const { return cut_; }
518
519 // Single line of text that we append to the cut log line.
520 std::string Info() const { return absl::StrCat("lift=", num_lifting_); }
521
522 void SetSharedStatistics(SharedStatistics* stats) { shared_stats_ = stats; }
523
524 void ClearCache() { has_bool_base_ct_ = false; }
525
526 private:
527 void InitializeCut(const CutData& input_ct);
528
529 // This looks at base_ct_ and reoder the terms so that the first ones are in
530 // the cover. return zero if no interesting cover was found.
531 template <class CompareAdd, class CompareRemove>
532 int GetCoverSize(int relevant_size);
533
534 // Same as GetCoverSize() but only look at Booleans, and use a different
535 // heuristic.
536 int GetCoverSizeForBooleans();
537
538 template <class Compare>
539 int MinimizeCover(int cover_size, absl::int128 slack);
540
541 // Here to reuse memory, cut_ is both the input and the output.
542 CutData cut_;
543 CutData temp_cut_;
544
545 // Hack to not sort twice.
546 bool has_bool_base_ct_ = false;
547 CutData bool_base_ct_;
548 int bool_cover_size_ = 0;
549
550 // Stats.
551 SharedStatistics* shared_stats_ = nullptr;
552 int64_t num_lifting_ = 0;
553
554 // Stats for the various type of cuts generated here.
555 struct CutStats {
556 int64_t num_cuts = 0;
557 int64_t num_initial_ibs = 0;
558 int64_t num_lb_ibs = 0;
559 int64_t num_ub_ibs = 0;
560 int64_t num_merges = 0;
561 int64_t num_bumps = 0;
562 int64_t num_lifting = 0;
563 int64_t num_overflow_aborts = 0;
564 };
565 CutStats flow_stats_;
566 CutStats cover_stats_;
567 CutStats ls_stats_;
568};
569
570// Separate RLT cuts.
571//
572// See for instance "Efficient Separation of RLT Cuts for Implicit and Explicit
573// Bilinear Products", Ksenia Bestuzheva, Ambros Gleixner, Tobias Achterberg,
574// https://arxiv.org/abs/2211.13545
576 public:
577 explicit BoolRLTCutHelper(Model* model)
578 : product_detector_(model->GetOrCreate<ProductDetector>()),
579 shared_stats_(model->GetOrCreate<SharedStatistics>()),
580 lp_values_(model->GetOrCreate<ModelLpValues>()) {};
582
583 // Precompute data according to the current lp relaxation.
584 // This also restrict any Boolean to be currently appearing in the LP.
585 void Initialize(absl::Span<const IntegerVariable> lp_vars);
586
587 // Tries RLT separation of the input constraint. Returns true on success.
588 bool TrySimpleSeparation(const CutData& input_ct);
589
590 // If successful, this contains the last generated cut.
591 const CutData& cut() const { return cut_; }
592
593 // Single line of text that we append to the cut log line.
594 std::string Info() const { return ""; }
595
596 private:
597 // LP value of a literal encoded as an IntegerVariable.
598 // That is lit(X) = X if X positive or 1 - X otherwise.
599 double GetLiteralLpValue(IntegerVariable var) const;
600
601 // Multiplies input by lit(factor) and linearize in the best possible way.
602 // The result will be stored in cut_.
603 bool TryProduct(IntegerVariable factor, const CutData& input);
604
605 bool enabled_ = false;
606 CutData filtered_input_;
607 CutData cut_;
608
609 ProductDetector* product_detector_;
610 SharedStatistics* shared_stats_;
611 ModelLpValues* lp_values_;
612
613 int64_t num_tried_ = 0;
614 int64_t num_tried_factors_ = 0;
615};
616
617// A cut generator for z = x * y (x and y >= 0).
618CutGenerator CreatePositiveMultiplicationCutGenerator(AffineExpression z,
619 AffineExpression x,
620 AffineExpression y,
621 int linearization_level,
622 Model* model);
623
624// Above hyperplan for square = x * x: square should be below the line
625// (x_lb, x_lb ^ 2) to (x_ub, x_ub ^ 2).
626// The slope of that line is (ub^2 - lb^2) / (ub - lb) = ub + lb.
627// square <= (x_lb + x_ub) * x - x_lb * x_ub
628// This only works for positive x.
629LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x,
630 AffineExpression square,
631 IntegerValue x_lb,
632 IntegerValue x_ub, Model* model);
633
634// Below hyperplan for square = x * x: y should be above the line
635// (x_value, x_value ^ 2) to (x_value + 1, (x_value + 1) ^ 2)
636// The slope of that line is 2 * x_value + 1
637// square >= below_slope * (x - x_value) + x_value ^ 2
638// square >= below_slope * x - x_value ^ 2 - x_value
639LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x,
640 AffineExpression square,
641 IntegerValue x_value,
642 Model* model);
643
644// A cut generator for y = x ^ 2 (x >= 0).
645// It will dynamically add a linear inequality to push y closer to the parabola.
646CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x,
647 int linearization_level, Model* model);
648
649// A cut generator for all_diff(xi). Let the united domain of all xi be D. Sum
650// of any k-sized subset of xi need to be greater or equal to the sum of
651// smallest k values in D and lesser or equal to the sum of largest k values in
652// D. The cut generator first sorts the variables based on LP values and adds
653// cuts of the form described above if they are violated by lp solution. Note
654// that all the fixed variables are ignored while generating cuts.
656 absl::Span<const AffineExpression> exprs, Model* model);
657
658// Consider the Lin Max constraint with d expressions and n variables in the
659// form: target = max {exprs[k] = Sum (wki * xi + bk)}. k in {1,..,d}.
660// Li = lower bound of xi
661// Ui = upper bound of xi.
662// Let zk be in {0,1} for all k in {1,..,d}.
663// The target = exprs[k] when zk = 1.
664//
665// The following is a valid linearization for Lin Max.
666// target >= exprs[k], for all k in {1,..,d}
667// target <= Sum (wli * xi) + Sum((Nlk + bk) * zk), for all l in {1,..,d}
668// Where Nlk is a large number defined as:
669// Nlk = Sum (max((wki - wli)*Li, (wki - wli)*Ui))
670// = Sum (max corner difference for variable i, target expr l, max expr k)
671//
672// Consider a partition of variables xi into set {1,..,d} as I.
673// i.e. I(i) = j means xi is mapped to jth index.
674// The following inequality is valid and sharp cut for the lin max constraint
675// described above.
676//
677// target <= Sum(i=1..n)(wI(i)i * xi + Sum(k=1..d)(MPlusCoefficient_ki * zk))
678// + Sum(k=1..d)(bk * zk) ,
679// Where MPlusCoefficient_ki = max((wki - wI(i)i) * Li,
680// (wki - wI(i)i) * Ui)
681// = max corner difference for variable i,
682// target expr I(i), max expr k.
683//
684// For detailed proof of validity, refer
685// Reference: "Strong mixed-integer programming formulations for trained neural
686// networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf).
687//
688// In the cut generator, we compute the most violated partition I by computing
689// the rhs value (wI(i)i * lp_value(xi) + Sum(k=1..d)(MPlusCoefficient_ki * zk))
690// for each variable for each partition index. We choose the partition index
691// that gives lowest rhs value for a given variable.
692//
693// Note: This cut generator requires all expressions to contain only positive
694// vars.
695CutGenerator CreateLinMaxCutGenerator(IntegerVariable target,
696 absl::Span<const LinearExpression> exprs,
697 absl::Span<const IntegerVariable> z_vars,
698 Model* model);
699
700// Helper for the affine max constraint.
701//
702// This function will reset the bounds of the builder.
704 const LinearExpression& target, IntegerVariable var,
705 absl::Span<const std::pair<IntegerValue, IntegerValue>> affines,
706 Model* model, LinearConstraintBuilder* builder);
707
708// By definition, the Max of affine functions is convex. The linear polytope is
709// bounded by all affine functions on the bottom, and by a single hyperplane
710// that join the two points at the extreme of the var domain, and their y-values
711// of the max of the affine functions.
712CutGenerator CreateMaxAffineCutGenerator(
713 LinearExpression target, IntegerVariable var,
714 std::vector<std::pair<IntegerValue, IntegerValue>> affines,
715 std::string cut_name, Model* model);
716
717// Extracts the variables that have a Literal view from base variables and
718// create a generator that will returns constraint of the form "at_most_one"
719// between such literals.
720CutGenerator CreateCliqueCutGenerator(
721 absl::Span<const IntegerVariable> base_variables, Model* model);
722
723// Utility class for the AllDiff cut generator.
725 public:
726 void Clear();
727 void Add(const AffineExpression& expr, int num_expr,
728 const IntegerTrail& integer_trail);
729
730 // Return int_max if the sum overflows.
731 IntegerValue SumOfMinDomainValues();
732 IntegerValue SumOfDifferentMins();
733 IntegerValue GetBestLowerBound(std::string& suffix);
734
735 int size() const { return expr_mins_.size(); }
736
737 private:
738 absl::btree_set<IntegerValue> min_values_;
739 std::vector<IntegerValue> expr_mins_;
740};
741
742} // namespace sat
743} // namespace operations_research
744
745#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:1675
void Initialize(absl::Span< const IntegerVariable > lp_vars)
Definition cuts.cc:1669
std::string Info() const
Single line of text that we append to the cut log line.
Definition cuts.h:594
const CutData & cut() const
If successful, this contains the last generated cut.
Definition cuts.h:591
Helper to find knapsack cover cuts.
Definition cuts.h:467
const CutData & cut() const
If successful, info about the last generated cut.
Definition cuts.h:517
bool TrySimpleKnapsack(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Definition cuts.cc:1302
std::string Info() const
Single line of text that we append to the cut log line.
Definition cuts.h:520
bool TryWithLetchfordSouliLifting(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Definition cuts.cc:1524
void SetSharedStatistics(SharedStatistics *stats)
Definition cuts.h:522
bool TrySingleNodeFlow(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Definition cuts.cc:1420
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:351
int AddOrMergeBooleanTerms(absl::Span< CutTerm > terms, IntegerValue t, CutData *cut)
Definition cuts.cc:298
std::vector< CutTerm > * ClearedMutableTempTerms()
Definition cuts.h:249
void RecomputeCacheAndSeparateSomeImpliedBoundCuts(const util_intops::StrongVector< IntegerVariable, double > &lp_values)
Definition cuts.cc:2109
bool CacheDataForCut(IntegerVariable first_slack, CutData *cut)
Definition cuts.cc:2319
bool TryToExpandWithLowerImpliedbound(IntegerValue factor_t, bool complement, CutTerm *term, absl::int128 *rhs, std::vector< CutTerm > *new_bool_terms)
Definition cuts.cc:2291
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:2029
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:2119
std::tuple< int, int, int > PostprocessWithImpliedBound(const std::function< IntegerValue(IntegerValue)> &f, IntegerValue factor_t, CutData *cut)
Definition cuts.cc:2210
bool DecomposeWithImpliedUpperBound(const CutTerm &term, IntegerValue factor_t, CutTerm &bool_term, CutTerm &slack_term)
Definition cuts.cc:2189
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:772
const CutData & cut() const
If successful, info about the last generated cut.
Definition cuts.h:426
std::string Info() const
Single line of text that we append to the cut log line.
Definition cuts.h:431
void SetSharedStatistics(SharedStatistics *stats)
Definition cuts.h:428
Simple class to add statistics by name and print them at the end.
Utility class for the AllDiff cut generator.
Definition cuts.h:724
IntegerValue GetBestLowerBound(std::string &suffix)
Definition cuts.cc:2402
void Add(const AffineExpression &expr, int num_expr, const IntegerTrail &integer_trail)
Definition cuts.cc:2355
IntegerValue SumOfMinDomainValues()
Return int_max if the sum overflows.
Definition cuts.cc:2380
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:2666
IntegerValue GetFactorT(IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue max_magnitude)
Definition cuts.cc:469
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:1874
LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x, AffineExpression square, IntegerValue x_value, Model *model)
Definition cuts.cc:1981
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:2577
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningFunction(IntegerValue positive_rhs, IntegerValue min_magnitude)
Definition cuts.cc:568
CutGenerator CreateAllDifferentCutGenerator(absl::Span< const AffineExpression > exprs, Model *model)
Definition cuts.cc:2465
CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x, int linearization_level, Model *model)
Definition cuts.cc:1993
CutGenerator CreateCliqueCutGenerator(absl::Span< const IntegerVariable > base_variables, Model *model)
Definition cuts.cc:2742
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:2720
LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x, AffineExpression square, IntegerValue x_lb, IntegerValue x_ub, Model *model)
Definition cuts.cc:1969
std::function< IntegerValue(IntegerValue)> ExtendNegativeFunction(std::function< IntegerValue(IntegerValue)> base_f, IntegerValue period)
Definition cuts.h:373
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningMirFunction(IntegerValue positive_rhs, IntegerValue scaling)
Definition cuts.cc:603
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction(IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t, IntegerValue max_scaling)
Definition cuts.cc:483
In SWIG mode, we don't want anything besides these top-level includes.
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:172
bool AllCoefficientsArePositive() const
These functions transform the cut by complementation.
Definition cuts.cc:230
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:190
double ComputeEfficacy() const
Definition cuts.cc:263
std::string DebugString() const
Definition cuts.cc:74
double ComputeViolation() const
Computes and returns the cut violation.
Definition cuts.cc:255
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:135
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:115
std::string DebugString() const
Definition cuts.cc:66
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:101
void Complement(absl::int128 *rhs)
Definition cuts.cc:82
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