14#ifndef OR_TOOLS_SAT_CUTS_H_
15#define OR_TOOLS_SAT_CUTS_H_
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"
58 std::vector<IntegerVariable>
vars;
96 IntegerValue
coeff = IntegerValue(0);
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);
131 bool AppendOneTerm(IntegerVariable var, IntegerValue coeff,
double lp_value,
132 IntegerValue lb, IntegerValue ub);
175 bool MergeIfPossible(IntegerValue t,
CutTerm& to_add,
CutTerm& target);
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_;
195 : lp_vars_(lp_vars_.begin(), lp_vars_.end()),
196 integer_trail_(integer_trail),
197 implied_bounds_(implied_bounds) {}
213 IntegerValue factor_t,
CutTerm& bool_term,
223 IntegerValue factor_t,
CutTerm& bool_term,
232 const std::function<IntegerValue(IntegerValue)>& f, IntegerValue factor_t,
241 CutTerm* term, absl::int128* rhs,
242 std::vector<CutTerm>* new_bool_terms);
271 const double bool_term =
273 return var_lp_value -
static_cast<double>(lb.value()) - bool_term;
288 BestImpliedBoundInfo ComputeBestImpliedBound(
292 absl::flat_hash_set<IntegerVariable> lp_vars_;
293 mutable absl::flat_hash_map<IntegerVariable, BestImpliedBoundInfo> cache_;
296 std::vector<CutTerm> tmp_terms_;
298 std::vector<BestImpliedBoundInfo> cached_data_;
336IntegerValue
GetFactorT(IntegerValue rhs_remainder, IntegerValue divisor,
337 IntegerValue max_magnitude);
339 IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t,
340 IntegerValue max_scaling);
362 IntegerValue positive_rhs, IntegerValue min_magnitude);
366std::function<IntegerValue(IntegerValue)>
368 IntegerValue scaling);
374 std::function<IntegerValue(IntegerValue)> base_f, IntegerValue period) {
375 const IntegerValue m = -base_f(-period);
376 return [m, period, base_f](IntegerValue v) {
378 const IntegerValue output_r = m + base_f(r - period);
431 std::string
Info()
const {
return absl::StrCat(
"ib_lift=", num_ib_used_); }
434 double GetScaledViolation(IntegerValue divisor, IntegerValue max_scaling,
435 IntegerValue remainder_threshold,
439 std::vector<IntegerValue> divisors_;
440 std::vector<IntegerValue> remainders_;
441 std::vector<IntegerValue> rs_;
442 std::vector<IntegerValue> best_rs_;
444 int64_t num_ib_used_ = 0;
447 std::vector<std::pair<int, IntegerValue>> adjusted_coeffs_;
448 std::vector<std::pair<int, IntegerValue>> best_adjusted_coeffs_;
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;
462 int64_t total_num_initial_ibs_ = 0;
463 int64_t total_num_initial_merges_ = 0;
520 std::string
Info()
const {
return absl::StrCat(
"lift=", num_lifting_); }
527 void InitializeCut(
const CutData& input_ct);
531 template <
class CompareAdd,
class CompareRemove>
532 int GetCoverSize(
int relevant_size);
536 int GetCoverSizeForBooleans();
538 template <
class Compare>
539 int MinimizeCover(
int cover_size, absl::int128 slack);
546 bool has_bool_base_ct_ =
false;
548 int bool_cover_size_ = 0;
552 int64_t num_lifting_ = 0;
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;
565 CutStats flow_stats_;
566 CutStats cover_stats_;
585 void Initialize(absl::Span<const IntegerVariable> lp_vars);
594 std::string
Info()
const {
return ""; }
599 double GetLiteralLpValue(IntegerVariable var)
const;
603 bool TryProduct(IntegerVariable factor,
const CutData&
input);
605 bool enabled_ =
false;
613 int64_t num_tried_ = 0;
614 int64_t num_tried_factors_ = 0;
621 int linearization_level,
630 AffineExpression square,
632 IntegerValue x_ub,
Model* model);
640 AffineExpression square,
641 IntegerValue x_value,
647 int linearization_level,
Model* model);
656 absl::Span<const AffineExpression> exprs,
Model* model);
696 absl::Span<const LinearExpression> exprs,
697 absl::Span<const IntegerVariable> z_vars,
704 const LinearExpression& target, IntegerVariable var,
705 absl::Span<
const std::pair<IntegerValue, IntegerValue>> affines,
706 Model* model, LinearConstraintBuilder* builder);
713 LinearExpression target, IntegerVariable var,
714 std::vector<std::pair<IntegerValue, IntegerValue>> affines,
715 std::string cut_name,
Model* model);
721 absl::Span<const IntegerVariable> base_variables,
Model* model);
735 int size()
const {
return expr_mins_.size(); }
738 absl::btree_set<IntegerValue> min_values_;
739 std::vector<IntegerValue> expr_mins_;
bool TrySimpleSeparation(const CutData &input_ct)
Tries RLT separation of the input constraint. Returns true on success.
BoolRLTCutHelper(Model *model)
void Initialize(absl::Span< const IntegerVariable > lp_vars)
std::string Info() const
Single line of text that we append to the cut log line.
const CutData & cut() const
If successful, this contains the last generated cut.
Helper to find knapsack cover cuts.
const CutData & cut() const
If successful, info about the last generated cut.
bool TrySimpleKnapsack(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
std::string Info() const
Single line of text that we append to the cut log line.
bool TryWithLetchfordSouliLifting(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
void SetSharedStatistics(SharedStatistics *stats)
bool TrySingleNodeFlow(const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Stores temporaries used to build or manipulate a CutData.
bool ConvertToLinearConstraint(const CutData &cut, LinearConstraint *output)
Returns false if we encounter an integer overflow.
int AddOrMergeBooleanTerms(absl::Span< CutTerm > terms, IntegerValue t, CutData *cut)
std::vector< CutTerm > * ClearedMutableTempTerms()
void RecomputeCacheAndSeparateSomeImpliedBoundCuts(const util_intops::StrongVector< IntegerVariable, double > &lp_values)
bool CacheDataForCut(IntegerVariable first_slack, CutData *cut)
bool TryToExpandWithLowerImpliedbound(IntegerValue factor_t, bool complement, CutTerm *term, absl::int128 *rhs, std::vector< CutTerm > *new_bool_terms)
ImpliedBoundsProcessor(absl::Span< const IntegerVariable > lp_vars_, IntegerTrail *integer_trail, ImpliedBounds *implied_bounds)
We will only replace IntegerVariable appearing in lp_vars_.
void AddLpVariable(IntegerVariable var)
BestImpliedBoundInfo GetCachedImpliedBoundInfo(IntegerVariable var) const
CutDataBuilder * MutableCutBuilder()
This can be used to share the hash-map memory.
bool DecomposeWithImpliedLowerBound(const CutTerm &term, IntegerValue factor_t, CutTerm &bool_term, CutTerm &slack_term)
std::tuple< int, int, int > PostprocessWithImpliedBound(const std::function< IntegerValue(IntegerValue)> &f, IntegerValue factor_t, CutData *cut)
bool DecomposeWithImpliedUpperBound(const CutTerm &term, IntegerValue factor_t, CutTerm &bool_term, CutTerm &slack_term)
~IntegerRoundingCutHelper()
bool ComputeCut(RoundingOptions options, const CutData &base_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
Returns true on success. The cut can be accessed via cut().
const CutData & cut() const
If successful, info about the last generated cut.
std::string Info() const
Single line of text that we append to the cut log line.
void SetSharedStatistics(SharedStatistics *stats)
Simple class to add statistics by name and print them at the end.
Utility class for the AllDiff cut generator.
IntegerValue GetBestLowerBound(std::string &suffix)
void Add(const AffineExpression &expr, int num_expr, const IntegerTrail &integer_trail)
IntegerValue SumOfDifferentMins()
IntegerValue SumOfMinDomainValues()
Return int_max if the sum overflows.
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)
IntegerValue GetFactorT(IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue max_magnitude)
CutGenerator CreatePositiveMultiplicationCutGenerator(AffineExpression z, AffineExpression x, AffineExpression y, int linearization_level, Model *model)
A cut generator for z = x * y (x and y >= 0).
LinearConstraint ComputeHyperplanBelowSquare(AffineExpression x, AffineExpression square, IntegerValue x_value, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
CutGenerator CreateLinMaxCutGenerator(const IntegerVariable target, absl::Span< const LinearExpression > exprs, absl::Span< const IntegerVariable > z_vars, Model *model)
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningFunction(IntegerValue positive_rhs, IntegerValue min_magnitude)
CutGenerator CreateAllDifferentCutGenerator(absl::Span< const AffineExpression > exprs, Model *model)
CutGenerator CreateSquareCutGenerator(AffineExpression y, AffineExpression x, int linearization_level, Model *model)
CutGenerator CreateCliqueCutGenerator(absl::Span< const IntegerVariable > base_variables, Model *model)
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)
LinearConstraint ComputeHyperplanAboveSquare(AffineExpression x, AffineExpression square, IntegerValue x_lb, IntegerValue x_ub, Model *model)
std::function< IntegerValue(IntegerValue)> ExtendNegativeFunction(std::function< IntegerValue(IntegerValue)> base_f, IntegerValue period)
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveStrengtheningMirFunction(IntegerValue positive_rhs, IntegerValue scaling)
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction(IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t, IntegerValue max_scaling)
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.
bool FillFromLinearConstraint(const LinearConstraint &base_ct, const util_intops::StrongVector< IntegerVariable, double > &lp_values, IntegerTrail *integer_trail)
bool AllCoefficientsArePositive() const
These functions transform the cut by complementation.
std::vector< CutTerm > terms
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)
double ComputeEfficacy() const
void ComplementForPositiveCoefficients()
std::string DebugString() const
double ComputeViolation() const
Computes and returns the cut violation.
IntegerValue max_magnitude
Only filled after SortRelevantEntries().
bool AppendOneTerm(IntegerVariable var, IntegerValue coeff, double lp_value, IntegerValue lb, IntegerValue ub)
void SortRelevantEntries()
void ComplementForSmallerLpValues()
absl::AnyInvocable< bool(LinearConstraintManager *manager)> generate_cuts
std::vector< IntegerVariable > vars
bool only_run_at_level_zero
IntegerVariable GetUnderlyingLiteralOrNone() const
std::string DebugString() const
int cached_implied_lb
Refer to cached_data_ in ImpliedBoundsProcessor.
double LpDistToMaxValue() const
void ReplaceExpressionByLiteral(IntegerVariable var)
void Complement(absl::int128 *rhs)
std::array< IntegerVariable, 2 > expr_vars
std::array< IntegerValue, 2 > expr_coeffs
bool HasRelevantLpValue() const
bool IsFractional() const
std::string DebugString() const
double SlackLpValue(IntegerValue lb) const
IntegerValue implied_bound
bool use_ib_before_heuristic