From 5b44519e9413e660162bb6d9f141b011addd171b Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 29 Aug 2022 17:47:30 +0200 Subject: [PATCH] [CP-SAT] various bugfixes from fuzzer --- ortools/sat/cp_model.proto | 21 ++++-- ortools/sat/cp_model_checker.cc | 15 +++- ortools/sat/cp_model_expand.cc | 106 +++++++++++++++++---------- ortools/sat/cp_model_expand.h | 8 ++ ortools/sat/cp_model_presolve.cc | 76 +++++-------------- ortools/sat/cp_model_solver.cc | 3 - ortools/sat/cp_model_utils.h | 6 +- ortools/sat/cuts.cc | 43 ++++++----- ortools/sat/cuts.h | 7 +- ortools/sat/linear_constraint.h | 10 ++- ortools/sat/linear_relaxation.cc | 6 +- ortools/sat/lp_utils.cc | 8 +- ortools/sat/optimization.cc | 9 +-- ortools/sat/parameters_validation.cc | 74 ++++++++++--------- ortools/sat/presolve_context.cc | 40 +++++----- ortools/sat/presolve_context.h | 5 +- ortools/util/saturated_arithmetic.h | 9 +++ 17 files changed, 250 insertions(+), 196 deletions(-) diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index f8f648dfb8..c87dac13c3 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -467,15 +467,20 @@ message CpObjectiveProto { // TODO(user): Put the error bounds we computed instead? bool scaling_was_exact = 6; - // Internal field. This is only useful for inner_objective_lower_bound, It - // should never be set in most cases, so we have the simple: - // sum(coefficients[i] * objective_vars[i]) >= inner_objective_lower_bound. + // Internal fields to recover a bound on the original integer objective from + // the presolved one. Basically, initially the integer objective fit on an + // int64 and is in [Initial_lb, Initial_ub]. During presolve, we might change + // the linear expression to have a new domain [Presolved_lb, Presolved_ub] + // that will also always fit on an int64. // - // This is similar to offset/scaling_factor but allows to stay in the integer - // domain. Note that the formula is not the same than for the floating point - // objective. If this is set, we have - // linear_expression * scaling + offset >= inner_objective_lower_bound - int64 integer_offset = 7; + // The two domain will always be linked with an affine transformation between + // the two of the form: + // old = (new + before_offset) * integer_scaling_factor + after_offset. + // Note that we use both offsets to always be able to do the computation while + // staying in the int64 domain. In particular, the after_offset will always + // be in (-integer_scaling_factor, integer_scaling_factor). + int64 integer_before_offset = 7; + int64 integer_after_offset = 9; int64 integer_scaling_factor = 8; } diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 1c0fa6cb24..dc8c315fca 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -1020,6 +1020,18 @@ std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) { } if (model.has_objective()) { RETURN_IF_NOT_EMPTY(ValidateObjective(model, model.objective())); + if (!after_presolve) { + // TODO(user): Instead we could check that under these factors the + // objective domain still fit on an int64_t. + if (model.objective().integer_scaling_factor() != 0 || + model.objective().integer_before_offset() != 0 || + model.objective().integer_after_offset() != 0) { + return absl::StrCat( + "Internal fields related to the postsolve of the integer objective " + "are set in the input objective proto: ", + ProtobufShortDebugString(model.objective())); + } + } } RETURN_IF_NOT_EMPTY(ValidateSearchStrategies(model)); RETURN_IF_NOT_EMPTY(ValidateSolutionHint(model)); @@ -1662,7 +1674,8 @@ bool SolutionIsFeasible(const CpModelProto& model, } if (!model.objective().domain().empty()) { if (!DomainInProtoContains(model.objective(), inner_objective)) { - VLOG(1) << "Objective value not in domain!"; + VLOG(1) << "Objective value " << inner_objective << " not in domain! " + << ReadDomainFromProto(model.objective()); return false; } } diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index f7da0c4e04..302d49ac07 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -41,6 +41,58 @@ namespace operations_research { namespace sat { + +// TODO(user): Note that if we have duplicate variables controlling different +// time point, this might not reach the fixed point. Fix? it is not that +// important as the expansion take care of this case anyway. +void PropagateAutomaton(const AutomatonConstraintProto& proto, + const PresolveContext& context, + std::vector>* states, + std::vector>* labels) { + const int n = proto.vars_size(); + const absl::flat_hash_set final_states( + {proto.final_states().begin(), proto.final_states().end()}); + + labels->clear(); + labels->resize(n); + states->clear(); + states->resize(n + 1); + (*states)[0].insert(proto.starting_state()); + + // Forward pass. + for (int time = 0; time < n; ++time) { + for (int t = 0; t < proto.transition_tail_size(); ++t) { + const int64_t tail = proto.transition_tail(t); + const int64_t label = proto.transition_label(t); + const int64_t head = proto.transition_head(t); + if (!(*states)[time].contains(tail)) continue; + if (!context.DomainContains(proto.vars(time), label)) continue; + if (time == n - 1 && !final_states.contains(head)) continue; + (*labels)[time].insert(label); + (*states)[time + 1].insert(head); + } + } + + // Backward pass. + for (int time = n - 1; time >= 0; --time) { + absl::flat_hash_set new_states; + absl::flat_hash_set new_labels; + for (int t = 0; t < proto.transition_tail_size(); ++t) { + const int64_t tail = proto.transition_tail(t); + const int64_t label = proto.transition_label(t); + const int64_t head = proto.transition_head(t); + + if (!(*states)[time].contains(tail)) continue; + if (!(*labels)[time].contains(label)) continue; + if (!(*states)[time + 1].contains(head)) continue; + new_labels.insert(label); + new_states.insert(tail); + } + (*labels)[time].swap(new_labels); + (*states)[time].swap(new_states); + } +} + namespace { void ExpandReservoir(ConstraintProto* ct, PresolveContext* context) { @@ -650,43 +702,9 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { "automaton: non-empty with no transition."); } - const int n = proto.vars_size(); - const std::vector vars = {proto.vars().begin(), proto.vars().end()}; - - // Compute the set of reachable state at each time point. - const absl::flat_hash_set final_states( - {proto.final_states().begin(), proto.final_states().end()}); - std::vector> reachable_states(n + 1); - reachable_states[0].insert(proto.starting_state()); - - // Forward pass. - for (int time = 0; time < n; ++time) { - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t tail = proto.transition_tail(t); - const int64_t label = proto.transition_label(t); - const int64_t head = proto.transition_head(t); - if (!reachable_states[time].contains(tail)) continue; - if (!context->DomainContains(vars[time], label)) continue; - if (time == n - 1 && !final_states.contains(head)) continue; - reachable_states[time + 1].insert(head); - } - } - - // Backward pass. - for (int time = n - 1; time >= 0; --time) { - absl::flat_hash_set new_set; - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t tail = proto.transition_tail(t); - const int64_t label = proto.transition_label(t); - const int64_t head = proto.transition_head(t); - - if (!reachable_states[time].contains(tail)) continue; - if (!context->DomainContains(vars[time], label)) continue; - if (!reachable_states[time + 1].contains(head)) continue; - new_set.insert(tail); - } - reachable_states[time].swap(new_set); - } + std::vector> reachable_states; + std::vector> reachable_labels; + PropagateAutomaton(proto, *context, &reachable_states, &reachable_labels); // We will model at each time step the current automaton state using Boolean // variables. We will have n+1 time step. At time zero, we start in the @@ -698,6 +716,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { absl::flat_hash_map out_encoding; bool removed_values = false; + const int n = proto.vars_size(); + const std::vector vars = {proto.vars().begin(), proto.vars().end()}; for (int time = 0; time < n; ++time) { // All these vector have the same size. We will use them to enforce a // local table constraint representing one step of the automaton at the @@ -732,6 +752,18 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) { VLOG(1) << "Infeasible automaton."; return; } + + // Tricky: when the same variable is used more than once, the propagation + // above might not reach the fixed point, so we do need to fix literal + // at false. + std::vector at_false; + for (const auto [value, literal] : in_encoding) { + if (value != in_states[0]) at_false.push_back(literal); + } + for (const int literal : at_false) { + if (!context->SetLiteralToFalse(literal)) return; + } + in_encoding.clear(); continue; } diff --git a/ortools/sat/cp_model_expand.h b/ortools/sat/cp_model_expand.h index 6ad01188bf..93990bda8e 100644 --- a/ortools/sat/cp_model_expand.h +++ b/ortools/sat/cp_model_expand.h @@ -14,6 +14,8 @@ #ifndef OR_TOOLS_SAT_CP_MODEL_EXPAND_H_ #define OR_TOOLS_SAT_CP_MODEL_EXPAND_H_ +#include + #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/presolve_context.h" @@ -26,6 +28,12 @@ namespace sat { // simplification of the model. Furthermore, this expansion is mandatory. void ExpandCpModel(PresolveContext* context); +// Fills and propagates the set of reachable states/labels. +void PropagateAutomaton(const AutomatonConstraintProto& proto, + const PresolveContext& context, + std::vector>* states, + std::vector>* labels); + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 1e9be02dd5..aab670d76b 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -5418,11 +5418,28 @@ bool CpModelPresolver::PresolveAutomaton(ConstraintProto* ct) { return true; } - Domain hull = context_->DomainOf(proto.vars(0)); - for (int v = 1; v < proto.vars_size(); ++v) { - hull = hull.UnionWith(context_->DomainOf(proto.vars(v))); + std::vector> reachable_states; + std::vector> reachable_labels; + PropagateAutomaton(proto, *context_, &reachable_states, &reachable_labels); + + // Filter domains and compute the union of all relevant labels. + bool removed_values = false; + Domain hull; + for (int time = 0; time < reachable_labels.size(); ++time) { + if (!context_->IntersectDomainWith( + proto.vars(time), + Domain::FromValues( + {reachable_labels[time].begin(), reachable_labels[time].end()}), + &removed_values)) { + return false; + } + hull = hull.UnionWith(context_->DomainOf(proto.vars(time))); + } + if (removed_values) { + context_->UpdateRuleStats("automaton: reduced variable domains"); } + // Only keep relevant transitions. int new_size = 0; for (int t = 0; t < proto.transition_tail_size(); ++t) { const int64_t label = proto.transition_label(t); @@ -5443,59 +5460,6 @@ bool CpModelPresolver::PresolveAutomaton(ConstraintProto* ct) { return false; } - const int n = proto.vars_size(); - const std::vector vars = {proto.vars().begin(), proto.vars().end()}; - - // Compute the set of reachable state at each time point. - std::vector> reachable_states(n + 1); - reachable_states[0].insert(proto.starting_state()); - reachable_states[n] = {proto.final_states().begin(), - proto.final_states().end()}; - - // Forward. - for (int time = 0; time + 1 < n; ++time) { - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t tail = proto.transition_tail(t); - const int64_t label = proto.transition_label(t); - const int64_t head = proto.transition_head(t); - if (!reachable_states[time].contains(tail)) continue; - if (!context_->DomainContains(vars[time], label)) continue; - reachable_states[time + 1].insert(head); - } - } - - std::vector> reached_values(n); - - // Backward. - for (int time = n - 1; time >= 0; --time) { - absl::btree_set new_set; - for (int t = 0; t < proto.transition_tail_size(); ++t) { - const int64_t tail = proto.transition_tail(t); - const int64_t label = proto.transition_label(t); - const int64_t head = proto.transition_head(t); - - if (!reachable_states[time].contains(tail)) continue; - if (!context_->DomainContains(vars[time], label)) continue; - if (!reachable_states[time + 1].contains(head)) continue; - new_set.insert(tail); - reached_values[time].insert(label); - } - reachable_states[time].swap(new_set); - } - - bool removed_values = false; - for (int time = 0; time < n; ++time) { - if (!context_->IntersectDomainWith( - vars[time], - Domain::FromValues( - {reached_values[time].begin(), reached_values[time].end()}), - &removed_values)) { - return false; - } - } - if (removed_values) { - context_->UpdateRuleStats("automaton: reduced variable domains"); - } return false; } diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 92f81dde08..fa2087c445 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1358,9 +1358,6 @@ void LoadCpModel(const CpModelProto& model_proto, Model* model) { // the other side: objective <= sum terms. // // TODO(user): Use a better condition to detect when this is not useful. - // Note also that for the core algorithm, we might need the other side too, - // otherwise we could return feasible solution with an objective above the - // user specified upper bound. if (!automatic_domain.IsIncludedIn(user_domain)) { std::vector vars; std::vector coeffs; diff --git a/ortools/sat/cp_model_utils.h b/ortools/sat/cp_model_utils.h index 7d72a0fcab..c0f791a02a 100644 --- a/ortools/sat/cp_model_utils.h +++ b/ortools/sat/cp_model_utils.h @@ -143,9 +143,11 @@ inline double ScaleObjectiveValue(const CpObjectiveProto& proto, inline int64_t ScaleInnerObjectiveValue(const CpObjectiveProto& proto, int64_t value) { if (proto.integer_scaling_factor() == 0) { - return value + proto.integer_offset(); + return value + proto.integer_before_offset(); } - return value * proto.integer_scaling_factor() + proto.integer_offset(); + return (value + proto.integer_before_offset()) * + proto.integer_scaling_factor() + + proto.integer_after_offset(); } // Removes the objective scaling and offset from the given value. diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc index 42412f1b05..76d8e9a89e 100644 --- a/ortools/sat/cuts.cc +++ b/ortools/sat/cuts.cc @@ -27,7 +27,6 @@ #include "absl/container/btree_set.h" #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" -#include "absl/meta/type_traits.h" #include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" @@ -1936,10 +1935,10 @@ IntegerValue EvaluateMaxAffine( } // namespace -LinearConstraint BuildMaxAffineUpConstraint( +bool BuildMaxAffineUpConstraint( const LinearExpression& target, IntegerVariable var, const std::vector>& affines, - Model* model) { + Model* model, LinearConstraintBuilder* builder) { auto* integer_trail = model->GetOrCreate(); const IntegerValue x_min = integer_trail->LevelZeroLowerBound(var); const IntegerValue x_max = integer_trail->LevelZeroUpperBound(var); @@ -1947,29 +1946,31 @@ LinearConstraint BuildMaxAffineUpConstraint( const IntegerValue y_at_min = EvaluateMaxAffine(affines, x_min); const IntegerValue y_at_max = EvaluateMaxAffine(affines, x_max); - // TODO(user): Be careful to not have any integer overflow in any of - // the formula used here. const IntegerValue delta_x = x_max - x_min; const IntegerValue delta_y = y_at_max - y_at_min; // target <= y_at_min + (delta_y / delta_x) * (var - x_min) // delta_x * target <= delta_x * y_at_min + delta_y * (var - x_min) // -delta_y * var + delta_x * target <= delta_x * y_at_min - delta_y * x_min - const IntegerValue rhs = delta_x * y_at_min - delta_y * x_min; - LinearConstraintBuilder lc(model, kMinIntegerValue, rhs); - lc.AddLinearExpression(target, delta_x); - lc.AddTerm(var, -delta_y); - LinearConstraint ct = lc.Build(); - - // Prevent to create constraints that can overflow. - if (!ValidateLinearConstraintForOverflow(ct, *integer_trail)) { - VLOG(2) << "Linear constraint can cause overflow: " << ct; - - // TODO(user): Change API instead of returning trivial constraint? - ct.Clear(); + // + // Checks the rhs for overflows. + if (AtMinOrMaxInt64(CapProd(delta_x.value(), y_at_min.value())) || + AtMinOrMaxInt64(CapProd(delta_y.value(), x_min.value()))) { + return false; } - return ct; + builder->ResetBounds(kMinIntegerValue, delta_x * y_at_min - delta_y * x_min); + builder->AddLinearExpression(target, delta_x); + builder->AddTerm(var, -delta_y); + + // Prevent to create constraints that can overflow. + if (!ValidateLinearConstraintForOverflow(builder->Build(), *integer_trail)) { + VLOG(2) << "Linear constraint can cause overflow: " << builder->Build(); + + return false; + } + + return true; } CutGenerator CreateMaxAffineCutGenerator( @@ -1987,8 +1988,10 @@ CutGenerator CreateMaxAffineCutGenerator( const absl::StrongVector& lp_values, LinearConstraintManager* manager) { if (integer_trail->IsFixed(var)) return true; - manager->AddCut(BuildMaxAffineUpConstraint(target, var, affines, model), - cut_name, lp_values); + LinearConstraintBuilder builder(model); + if (BuildMaxAffineUpConstraint(target, var, affines, model, &builder)) { + manager->AddCut(builder.Build(), cut_name, lp_values); + } return true; }; return result; diff --git a/ortools/sat/cuts.h b/ortools/sat/cuts.h index 0c009ec5ac..a6fbf69499 100644 --- a/ortools/sat/cuts.h +++ b/ortools/sat/cuts.h @@ -31,7 +31,6 @@ #include "ortools/sat/linear_constraint_manager.h" #include "ortools/sat/model.h" #include "ortools/util/strong_integers.h" -#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { @@ -477,10 +476,12 @@ CutGenerator CreateLinMaxCutGenerator( const std::vector& z_vars, Model* model); // Helper for the affine max constraint. -LinearConstraint BuildMaxAffineUpConstraint( +// +// This function will reset the bounds of the builder. +bool BuildMaxAffineUpConstraint( const LinearExpression& target, IntegerVariable var, const std::vector>& affines, - Model* model); + Model* model, LinearConstraintBuilder* builder); // By definition, the Max of affine functions is convex. The linear polytope is // bounded by all affine functions on the bottom, and by a single hyperplane diff --git a/ortools/sat/linear_constraint.h b/ortools/sat/linear_constraint.h index 8b9146a3f2..b7296db4c2 100644 --- a/ortools/sat/linear_constraint.h +++ b/ortools/sat/linear_constraint.h @@ -214,6 +214,12 @@ class LinearConstraintBuilder { terms_.clear(); } + // Reset the bounds passed at construction time. + void ResetBounds(IntegerValue lb, IntegerValue ub) { + lb_ = lb; + ub_ = ub; + } + // Builds and returns the corresponding constraint in a canonical form. // All the IntegerVariable will be positive and appear in increasing index // order. @@ -232,8 +238,8 @@ class LinearConstraintBuilder { private: const IntegerEncoder* encoder_; - const IntegerValue lb_; - const IntegerValue ub_; + IntegerValue lb_; + IntegerValue ub_; IntegerValue offset_ = IntegerValue(0); diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index 8d3d2e1c71..4e861b2820 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -938,8 +938,10 @@ void AppendMaxAffineRelaxation(const ConstraintProto& ct, Model* model, CHECK(VariableIsPositive(var)); const LinearExpression target_expr = PositiveVarExpr(mapping->GetExprFromProto(ct.lin_max().target())); - relaxation->linear_constraints.push_back( - BuildMaxAffineUpConstraint(target_expr, var, affines, model)); + LinearConstraintBuilder builder(model); + if (BuildMaxAffineUpConstraint(target_expr, var, affines, model, &builder)) { + relaxation->linear_constraints.push_back(builder.Build()); + } } void AddMaxAffineCutGenerator(const ConstraintProto& ct, Model* model, diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc index e3d6d21367..3724b3d40f 100644 --- a/ortools/sat/lp_utils.cc +++ b/ortools/sat/lp_utils.cc @@ -833,7 +833,8 @@ bool ConvertMPModelProtoToCpModelProto(const SatParameters& params, // Note that we must process the lower bound first. for (const bool lower : {true, false}) { const double bound = lower ? mp_var.lower_bound() : mp_var.upper_bound(); - if (std::abs(bound) >= static_cast(kMaxVariableBound)) { + if (std::abs(bound) + kWantedPrecision >= + static_cast(kMaxVariableBound)) { ++num_truncated_bounds; cp_var->add_domain(bound < 0 ? -kMaxVariableBound : kMaxVariableBound); continue; @@ -1565,10 +1566,11 @@ double ComputeTrueObjectiveLowerBound( lp.CleanUp(); - // This should be fast. + // This should be fast. However, in case of numerical difficulties, we bound + // the number of iterations. glop::LPSolver solver; glop::GlopParameters glop_parameters; - glop_parameters.set_max_deterministic_time(10); + glop_parameters.set_max_number_of_iterations(100 * proto.variables().size()); glop_parameters.set_change_status_to_imprecise(false); solver.SetParameters(glop_parameters); const glop::ProblemStatus& status = solver.Solve(lp); diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 580cbd3697..5623e45919 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -1338,11 +1338,10 @@ bool CoreBasedOptimizer::ProcessSolution() { term.cover_ub = std::min(term.cover_ub, value); } - // We use the level zero upper bound of the objective to indicate an upper - // limit for the solution objective we are looking for. Again, because the - // objective_var is not assumed to be linked, it could take any value in the - // current solution. - if (objective > integer_trail_->LevelZeroUpperBound(objective_var_)) { + // Test that the current objective value fall in the requested objective + // domain, which could potentially have holes. + if (!integer_trail_->InitialVariableDomain(objective_var_) + .Contains(objective.value())) { return true; } diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index 451626ab35..503f8e58c3 100644 --- a/ortools/sat/parameters_validation.cc +++ b/ortools/sat/parameters_validation.cc @@ -37,42 +37,48 @@ namespace sat { return absl::StrCat("parameter '", #name, "' is NaN"); \ } +#define TEST_IS_FINITE(name) \ + if (!std::isfinite(params.name())) { \ + return absl::StrCat("parameter '", #name, "' is NaN or not finite"); \ + } + std::string ValidateParameters(const SatParameters& params) { - // Test that all floating point parameters are not NaN. - TEST_NOT_NAN(random_polarity_ratio); - TEST_NOT_NAN(random_branches_ratio); - TEST_NOT_NAN(initial_variables_activity); - TEST_NOT_NAN(clause_cleanup_ratio); - TEST_NOT_NAN(pb_cleanup_ratio); - TEST_NOT_NAN(variable_activity_decay); - TEST_NOT_NAN(max_variable_activity_value); - TEST_NOT_NAN(glucose_max_decay); - TEST_NOT_NAN(glucose_decay_increment); - TEST_NOT_NAN(clause_activity_decay); - TEST_NOT_NAN(max_clause_activity_value); - TEST_NOT_NAN(restart_dl_average_ratio); - TEST_NOT_NAN(restart_lbd_average_ratio); - TEST_NOT_NAN(blocking_restart_multiplier); - TEST_NOT_NAN(strategy_change_increase_ratio); + // Test that all floating point parameters are not NaN or +/- infinity. + TEST_IS_FINITE(random_polarity_ratio); + TEST_IS_FINITE(random_branches_ratio); + TEST_IS_FINITE(initial_variables_activity); + TEST_IS_FINITE(clause_cleanup_ratio); + TEST_IS_FINITE(pb_cleanup_ratio); + TEST_IS_FINITE(variable_activity_decay); + TEST_IS_FINITE(max_variable_activity_value); + TEST_IS_FINITE(glucose_max_decay); + TEST_IS_FINITE(glucose_decay_increment); + TEST_IS_FINITE(clause_activity_decay); + TEST_IS_FINITE(max_clause_activity_value); + TEST_IS_FINITE(restart_dl_average_ratio); + TEST_IS_FINITE(restart_lbd_average_ratio); + TEST_IS_FINITE(blocking_restart_multiplier); + TEST_IS_FINITE(strategy_change_increase_ratio); + TEST_IS_FINITE(absolute_gap_limit); + TEST_IS_FINITE(relative_gap_limit); + TEST_IS_FINITE(log_frequency_in_seconds); + TEST_IS_FINITE(model_reduction_log_frequency_in_seconds); + TEST_IS_FINITE(presolve_probing_deterministic_time_limit); + TEST_IS_FINITE(propagation_loop_detection_factor); + TEST_IS_FINITE(merge_no_overlap_work_limit); + TEST_IS_FINITE(merge_at_most_one_work_limit); + TEST_IS_FINITE(min_orthogonality_for_lp_constraints); + TEST_IS_FINITE(cut_max_active_count_value); + TEST_IS_FINITE(cut_active_count_decay); + TEST_IS_FINITE(shaving_search_deterministic_time); + TEST_IS_FINITE(mip_max_bound); + TEST_IS_FINITE(mip_var_scaling); + TEST_IS_FINITE(mip_wanted_precision); + TEST_IS_FINITE(mip_check_precision); + TEST_IS_FINITE(mip_max_valid_magnitude); + TEST_NOT_NAN(max_time_in_seconds); TEST_NOT_NAN(max_deterministic_time); - TEST_NOT_NAN(absolute_gap_limit); - TEST_NOT_NAN(relative_gap_limit); - TEST_NOT_NAN(log_frequency_in_seconds); - TEST_NOT_NAN(model_reduction_log_frequency_in_seconds); - TEST_NOT_NAN(presolve_probing_deterministic_time_limit); - TEST_NOT_NAN(propagation_loop_detection_factor); - TEST_NOT_NAN(merge_no_overlap_work_limit); - TEST_NOT_NAN(merge_at_most_one_work_limit); - TEST_NOT_NAN(min_orthogonality_for_lp_constraints); - TEST_NOT_NAN(cut_max_active_count_value); - TEST_NOT_NAN(cut_active_count_decay); - TEST_NOT_NAN(shaving_search_deterministic_time); - TEST_NOT_NAN(mip_max_bound); - TEST_NOT_NAN(mip_var_scaling); - TEST_NOT_NAN(mip_wanted_precision); - TEST_NOT_NAN(mip_check_precision); - TEST_NOT_NAN(mip_max_valid_magnitude); // TODO(user): Consider using annotations directly in the proto for these // validation. It is however not open sourced. @@ -88,7 +94,9 @@ std::string ValidateParameters(const SatParameters& params) { return "Enumerating all solutions does not work with interleaved search"; } + TEST_NON_NEGATIVE(mip_wanted_precision); TEST_NON_NEGATIVE(max_time_in_seconds); + TEST_NON_NEGATIVE(max_deterministic_time); TEST_NON_NEGATIVE(num_workers); TEST_NON_NEGATIVE(num_search_workers); TEST_NON_NEGATIVE(min_num_lns_workers); diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 79074bea13..dc16a5d164 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -1498,7 +1498,8 @@ void PresolveContext::ReadObjectiveFromProto() { objective_scaling_factor_ = 1.0; } - objective_integer_offset_ = obj.integer_offset(); + objective_integer_before_offset_ = obj.integer_before_offset(); + objective_integer_after_offset_ = obj.integer_after_offset(); objective_integer_scaling_factor_ = obj.integer_scaling_factor(); if (objective_integer_scaling_factor_ == 0) { objective_integer_scaling_factor_ = 1; @@ -1648,7 +1649,16 @@ bool PresolveContext::CanonicalizeObjective(bool simplify_domain) { objective_domain_ = objective_domain_.InverseMultiplicationBy(gcd); objective_offset_ /= static_cast(gcd); objective_scaling_factor_ *= static_cast(gcd); + + // We update the offset accordingly. + absl::int128 offset = absl::int128(objective_integer_before_offset_) * + absl::int128(objective_integer_scaling_factor_) + + absl::int128(objective_integer_after_offset_); objective_integer_scaling_factor_ *= gcd; + objective_integer_before_offset_ = static_cast( + offset / absl::int128(objective_integer_scaling_factor_)); + objective_integer_after_offset_ = static_cast( + offset % absl::int128(objective_integer_scaling_factor_)); } if (objective_domain_.IsEmpty()) return false; @@ -1714,13 +1724,16 @@ void PresolveContext::AddLiteralToObjective(int ref, int64_t value) { } } -void PresolveContext::AddToObjectiveOffset(int64_t delta) { +bool PresolveContext::AddToObjectiveOffset(int64_t delta) { + const int64_t temp = CapAdd(objective_integer_before_offset_, delta); + if (temp == std::numeric_limits::min()) return false; + if (temp == std::numeric_limits::max()) return false; + objective_integer_before_offset_ = temp; + // Tricky: The objective domain is without the offset, so we need to shift it. objective_offset_ += static_cast(delta); - objective_integer_offset_ = - CapAdd(objective_integer_offset_, - CapProd(delta, objective_integer_scaling_factor_)); objective_domain_ = objective_domain_.AdditionWith(Domain(-delta)); + return true; } bool PresolveContext::SubstituteVariableInObjective( @@ -1766,14 +1779,7 @@ bool PresolveContext::SubstituteVariableInObjective( CHECK(!offset.IsEmpty()); // We also need to make sure the integer_offset will not overflow. - { - int64_t temp = CapProd(offset.Min(), objective_integer_scaling_factor_); - if (temp == std::numeric_limits::max()) return false; - if (temp == std::numeric_limits::min()) return false; - temp = CapAdd(temp, objective_integer_offset_); - if (temp == std::numeric_limits::max()) return false; - if (temp == std::numeric_limits::min()) return false; - } + if (!AddToObjectiveOffset(offset.Min())) return false; // Perform the substitution. for (int i = 0; i < equality.linear().vars().size(); ++i) { @@ -1800,11 +1806,6 @@ bool PresolveContext::SubstituteVariableInObjective( RemoveVariableFromObjective(var_in_equality); - // Tricky: The objective domain is without the offset, so we need to shift it. - objective_offset_ += static_cast(offset.Min()); - objective_integer_offset_ += offset.Min() * objective_integer_scaling_factor_; - objective_domain_ = objective_domain_.AdditionWith(Domain(-offset.Min())); - // Because we can assume that the constraint we used was constraining // (otherwise it would have been removed), the objective domain should be now // constraining. @@ -1884,7 +1885,8 @@ void PresolveContext::WriteObjectiveToProto() const { CpObjectiveProto* mutable_obj = working_model->mutable_objective(); mutable_obj->set_offset(objective_offset_); mutable_obj->set_scaling_factor(objective_scaling_factor_); - mutable_obj->set_integer_offset(objective_integer_offset_); + mutable_obj->set_integer_before_offset(objective_integer_before_offset_); + mutable_obj->set_integer_after_offset(objective_integer_after_offset_); if (objective_integer_scaling_factor_ == 1) { mutable_obj->set_integer_scaling_factor(0); // Default. } else { diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 1fc012d63a..87ad012641 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -385,7 +385,7 @@ class PresolveContext { // the case, we also have an affine linear constraint, so we can't really do // anything with that variable since it appear in at least two constraints. void ReadObjectiveFromProto(); - void AddToObjectiveOffset(int64_t delta); + bool AddToObjectiveOffset(int64_t delta); ABSL_MUST_USE_RESULT bool CanonicalizeOneObjectiveVariable(int var); ABSL_MUST_USE_RESULT bool CanonicalizeObjective(bool simplify_domain = true); void WriteObjectiveToProto() const; @@ -606,7 +606,8 @@ class PresolveContext { Domain objective_domain_; double objective_offset_; double objective_scaling_factor_; - int64_t objective_integer_offset_; + int64_t objective_integer_before_offset_; + int64_t objective_integer_after_offset_; int64_t objective_integer_scaling_factor_; // Constraints <-> Variables graph. diff --git a/ortools/util/saturated_arithmetic.h b/ortools/util/saturated_arithmetic.h index 70066320b1..1bef05eea9 100644 --- a/ortools/util/saturated_arithmetic.h +++ b/ortools/util/saturated_arithmetic.h @@ -14,6 +14,8 @@ #ifndef OR_TOOLS_UTIL_SATURATED_ARITHMETIC_H_ #define OR_TOOLS_UTIL_SATURATED_ARITHMETIC_H_ +#include + #include "absl/base/casts.h" #include "ortools/base/integral_types.h" #include "ortools/util/bitset.h" @@ -239,6 +241,13 @@ inline int64_t CapProd(int64_t x, int64_t y) { return CapProdGeneric(x, y); #endif } + +// Checks is x is equal to the min or the max value of an int64_t. +inline bool AtMinOrMaxInt64(int64_t x) { + return x == std::numeric_limits::min() || + x == -std::numeric_limits::max(); +} + } // namespace operations_research #endif // OR_TOOLS_UTIL_SATURATED_ARITHMETIC_H_