always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] various bugfixes from fuzzer

Browse Source
This commit is contained in:
Laurent Perron
2022-08-29 17:47:30 +02:00
parent c7c7b46082
commit 5b44519e94
17 changed files with 250 additions and 196 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
ortools/sat/cp_model.proto
View File

@@ -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;
}

15
ortools/sat/cp_model_checker.cc
View File

@@ -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;
}
}

106
ortools/sat/cp_model_expand.cc
View File

@@ -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<absl::flat_hash_set<int64_t>>* states,
std::vector<absl::flat_hash_set<int64_t>>* labels) {
const int n = proto.vars_size();
const absl::flat_hash_set<int64_t> 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<int64_t> new_states;
absl::flat_hash_set<int64_t> 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<int> vars = {proto.vars().begin(), proto.vars().end()};
// Compute the set of reachable state at each time point.
const absl::flat_hash_set<int64_t> final_states(
{proto.final_states().begin(), proto.final_states().end()});
std::vector<absl::flat_hash_set<int64_t>> 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<int64_t> 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<absl::flat_hash_set<int64_t>> reachable_states;
std::vector<absl::flat_hash_set<int64_t>> 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<int64_t, int> out_encoding;
bool removed_values = false;
const int n = proto.vars_size();
const std::vector<int> 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<int> 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;
}

8
ortools/sat/cp_model_expand.h
View File

@@ -14,6 +14,8 @@
#ifndef OR_TOOLS_SAT_CP_MODEL_EXPAND_H_
#define OR_TOOLS_SAT_CP_MODEL_EXPAND_H_
#include <vector>
#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<absl::flat_hash_set<int64_t>>* states,
std::vector<absl::flat_hash_set<int64_t>>* labels);
} // namespace sat
} // namespace operations_research

76
ortools/sat/cp_model_presolve.cc
View File

@@ -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<absl::flat_hash_set<int64_t>> reachable_states;
std::vector<absl::flat_hash_set<int64_t>> 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<int> vars = {proto.vars().begin(), proto.vars().end()};
// Compute the set of reachable state at each time point.
std::vector<absl::btree_set<int64_t>> 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<absl::btree_set<int64_t>> reached_values(n);
// Backward.
for (int time = n - 1; time >= 0; --time) {
absl::btree_set<int64_t> 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;
}

3
ortools/sat/cp_model_solver.cc
View File

@@ -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<IntegerVariable> vars;
std::vector<int64_t> coeffs;

6
ortools/sat/cp_model_utils.h
View File

@@ -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.

43
ortools/sat/cuts.cc
View File

@@ -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<std::pair<IntegerValue, IntegerValue>>& affines,
Model* model) {
Model* model, LinearConstraintBuilder* builder) {
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
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<IntegerVariable, double>& 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;

7
ortools/sat/cuts.h
View File

@@ -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<IntegerVariable>& 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<std::pair<IntegerValue, IntegerValue>>& 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

10
ortools/sat/linear_constraint.h
View File

@@ -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);

6
ortools/sat/linear_relaxation.cc
View File

@@ -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,

8
ortools/sat/lp_utils.cc
View File

@@ -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<double>(kMaxVariableBound)) {
if (std::abs(bound) + kWantedPrecision >=
static_cast<double>(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);

9
ortools/sat/optimization.cc
View File

@@ -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;
}

74
ortools/sat/parameters_validation.cc
View File

@@ -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);

40
ortools/sat/presolve_context.cc
View File

@@ -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<double>(gcd);
objective_scaling_factor_ *= static_cast<double>(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<int64_t>(
offset / absl::int128(objective_integer_scaling_factor_));
objective_integer_after_offset_ = static_cast<int64_t>(
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<int64_t>::min()) return false;
if (temp == std::numeric_limits<int64_t>::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<double>(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<int64_t>::max()) return false;
if (temp == std::numeric_limits<int64_t>::min()) return false;
temp = CapAdd(temp, objective_integer_offset_);
if (temp == std::numeric_limits<int64_t>::max()) return false;
if (temp == std::numeric_limits<int64_t>::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<double>(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 {

5
ortools/sat/presolve_context.h
View File

@@ -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.

9
ortools/util/saturated_arithmetic.h
View File

@@ -14,6 +14,8 @@
#ifndef OR_TOOLS_UTIL_SATURATED_ARITHMETIC_H_
#define OR_TOOLS_UTIL_SATURATED_ARITHMETIC_H_
#include <limits>
#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<int64_t>::min() ||
x == -std::numeric_limits<int64_t>::max();
}
} // namespace operations_research
#endif // OR_TOOLS_UTIL_SATURATED_ARITHMETIC_H_