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

[CP-SAT] reuse vectors in cuts; remove dead code; fix bug in abs(x) in domain presolve; fix #3084

Browse Source
This commit is contained in:
Laurent Perron
2022-01-17 16:31:41 +01:00
parent a425d6ab8e
commit 641d3d2c5e
6 changed files with 170 additions and 180 deletions
Download Patch File Download Diff File Expand all files Collapse all files

79
ortools/sat/cp_model_presolve.cc
View File

@@ -1826,7 +1826,8 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
// replace x by abs_arg and hopefully remove the variable x later.
int abs_arg;
if (ct->linear().coeffs(0) == 1 &&
context_->GetAbsRelation(ct->linear().vars(0), &abs_arg)) {
context_->GetAbsRelation(ct->linear().vars(0), &abs_arg) &&
PositiveRef(ct->linear().vars(0)) != PositiveRef(abs_arg)) {
// TODO(user): Deal with coeff = -1, here or during canonicalization.
context_->UpdateRuleStats("linear1: remove abs from abs(x) in domain");
const Domain implied_abs_target_domain =
@@ -1847,15 +1848,12 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
return MarkConstraintAsFalse(ct);
}
ConstraintProto* new_ct = context_->working_model->add_constraints();
new_ct->set_name(ct->name());
*new_ct->mutable_enforcement_literal() = ct->enforcement_literal();
auto* arg = new_ct->mutable_linear();
arg->add_vars(abs_arg);
arg->add_coeffs(1);
FillDomainInProto(new_abs_var_domain, new_ct->mutable_linear());
context_->UpdateNewConstraintsVariableUsage();
return RemoveConstraint(ct);
// Modify the constraint in-place.
ct->clear_linear();
ct->mutable_linear()->add_vars(PositiveRef(abs_arg));
ct->mutable_linear()->add_coeffs(1);
FillDomainInProto(new_abs_var_domain, ct->mutable_linear());
return true;
}
// Detect encoding.
@@ -7725,6 +7723,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
if (context_->ModelIsUnsat()) return InfeasibleStatus();
// Remove duplicate constraints.
// Note that at this point the objective in the proto should be up to date.
//
// TODO(user): We might want to do that earlier so that our count of variable
// usage is not biased by duplicate constraints.
@@ -7733,8 +7732,11 @@ CpSolverStatus CpModelPresolver::Presolve() {
for (const auto [dup, rep] : duplicates) {
// Note that it is important to look at the type of the representative in
// case the constraint became empty.
DCHECK_LT(kObjectiveConstraint, 0);
const int type =
context_->working_model->constraints(rep).constraint_case();
rep == kObjectiveConstraint
? kObjectiveConstraint
: context_->working_model->constraints(rep).constraint_case();
// TODO(user): we could delete duplicate identical interval, but we need
// to make sure reference to them are updated.
@@ -7745,13 +7747,13 @@ CpSolverStatus CpModelPresolver::Presolve() {
// For linear constraint, we merge their rhs since it was ignored in the
// FindDuplicateConstraints() call.
if (type == ConstraintProto::kLinear) {
const Domain d1 = ReadDomainFromProto(
const Domain rep_domain = ReadDomainFromProto(
context_->working_model->constraints(rep).linear());
const Domain d2 = ReadDomainFromProto(
const Domain d = ReadDomainFromProto(
context_->working_model->constraints(dup).linear());
if (d1 != d2) {
if (rep_domain != d) {
context_->UpdateRuleStats("duplicate: merged rhs of linear constraint");
const Domain rhs = d1.IntersectionWith(d2);
const Domain rhs = rep_domain.IntersectionWith(d);
if (rhs.IsEmpty()) {
if (!MarkConstraintAsFalse(
context_->working_model->mutable_constraints(rep))) {
@@ -7770,6 +7772,27 @@ CpSolverStatus CpModelPresolver::Presolve() {
}
}
if (type == kObjectiveConstraint) {
context_->UpdateRuleStats(
"duplicate: linear constraint parallel to objective");
const Domain objective_domain =
ReadDomainFromProto(context_->working_model->objective());
const Domain d = ReadDomainFromProto(
context_->working_model->constraints(dup).linear());
if (objective_domain != d) {
context_->UpdateRuleStats("duplicate: updated objective domain");
const Domain new_domain = objective_domain.IntersectionWith(d);
if (new_domain.IsEmpty()) {
(void)context_->NotifyThatModelIsUnsat(
"Constraint parallel to the objective makes the objective domain "
"empty.");
return InfeasibleStatus();
}
FillDomainInProto(new_domain,
context_->working_model->mutable_objective());
}
}
context_->working_model->mutable_constraints(dup)->Clear();
context_->UpdateConstraintVariableUsage(dup);
context_->UpdateRuleStats("duplicate: removed constraint");
@@ -8041,6 +8064,7 @@ void ApplyVariableMapping(const std::vector<int>& mapping,
}
namespace {
ConstraintProto CopyConstraintForDuplicateDetection(const ConstraintProto& ct) {
ConstraintProto copy = ct;
copy.clear_name();
@@ -8049,6 +8073,16 @@ ConstraintProto CopyConstraintForDuplicateDetection(const ConstraintProto& ct) {
}
return copy;
}
// We ignore all the fields but the linear expression.
ConstraintProto CopyObjectiveForDuplicateDetection(
const CpObjectiveProto& objective) {
ConstraintProto copy;
*copy.mutable_linear()->mutable_vars() = objective.vars();
*copy.mutable_linear()->mutable_coeffs() = objective.coeffs();
return copy;
}
} // namespace
std::vector<std::pair<int, int>> FindDuplicateConstraints(
@@ -8057,9 +8091,16 @@ std::vector<std::pair<int, int>> FindDuplicateConstraints(
// We use a map hash: serialized_constraint_proto hash -> constraint index.
ConstraintProto copy;
std::string s;
absl::flat_hash_map<uint64_t, int> equiv_constraints;
std::string s;
// Create a special representative for the linear objective.
if (model_proto.has_objective()) {
copy = CopyObjectiveForDuplicateDetection(model_proto.objective());
s = copy.SerializeAsString();
equiv_constraints[absl::Hash<std::string>()(s)] = kObjectiveConstraint;
}
const int num_constraints = model_proto.constraints().size();
for (int c = 0; c < num_constraints; ++c) {
if (model_proto.constraints(c).constraint_case() ==
@@ -8078,8 +8119,10 @@ std::vector<std::pair<int, int>> FindDuplicateConstraints(
if (!inserted) {
// Already present!
const int other_c_with_same_hash = it->second;
copy = CopyConstraintForDuplicateDetection(
model_proto.constraints(other_c_with_same_hash));
copy = other_c_with_same_hash == kObjectiveConstraint
? CopyObjectiveForDuplicateDetection(model_proto.objective())
: CopyConstraintForDuplicateDetection(
model_proto.constraints(other_c_with_same_hash));
if (s == copy.SerializeAsString()) {
result.push_back({c, other_c_with_same_hash});
}

3
ortools/sat/cp_model_presolve.h
View File

@@ -306,6 +306,9 @@ CpSolverStatus PresolveCpModel(PresolveContext* context,
// - We ignore names when comparing constraint.
// - For linear constraints, we ignore the domain. This is because we can
// just merge them if the constraints are the same.
// - We return the special kObjectiveConstraint (< 0) representative if a linear
// constraint is parallel to the objective and has no enforcement literals.
// The domain of such constraint can just be merged with the objective domain.
//
// Visible here for testing. This is meant to be called at the end of the
// presolve where constraints have been canonicalized.

175
ortools/sat/linear_programming_constraint.cc
View File

@@ -742,12 +742,12 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
// and if we complement or not before the MIR rounding. Other solvers seems
// to try different complementation strategies in a "potprocessing" and we
// don't. Try this too.
std::vector<ImpliedBoundsProcessor::SlackInfo> ib_slack_infos;
tmp_ib_slack_infos_.clear();
implied_bounds_processor_.ProcessUpperBoundedConstraintWithSlackCreation(
/*substitute_only_inner_variables=*/false, first_new_var,
expanded_lp_solution_, &cut_, &ib_slack_infos);
expanded_lp_solution_, &cut_, &tmp_ib_slack_infos_);
DCHECK(implied_bounds_processor_.DebugSlack(first_new_var, copy_in_debug,
cut_, ib_slack_infos));
cut_, tmp_ib_slack_infos_));
// Fills data for IntegerRoundingCut().
//
@@ -762,7 +762,7 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
if (var >= first_new_var) {
CHECK(VariableIsPositive(var));
const auto& info =
ib_slack_infos[(var.value() - first_new_var.value()) / 2];
tmp_ib_slack_infos_[(var.value() - first_new_var.value()) / 2];
tmp_lp_values_.push_back(info.lp_value);
tmp_var_lbs_.push_back(info.lb);
tmp_var_ubs_.push_back(info.ub);
@@ -775,8 +775,8 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
// Add slack.
// definition: integer_lp_[row] + slack_row == bound;
const IntegerVariable first_slack(first_new_var +
IntegerVariable(2 * ib_slack_infos.size()));
const IntegerVariable first_slack(
first_new_var + IntegerVariable(2 * tmp_ib_slack_infos_.size()));
tmp_slack_rows_.clear();
tmp_slack_bounds_.clear();
for (const auto pair : integer_multipliers) {
@@ -812,7 +812,7 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
tmp_var_ubs_)) {
at_least_one_added |= PostprocessAndAddCut(
absl::StrCat(name, "_K"), cover_cut_helper_.Info(), first_new_var,
first_slack, ib_slack_infos, cover_cut_helper_.mutable_cut());
first_slack, tmp_ib_slack_infos_, cover_cut_helper_.mutable_cut());
}
}
@@ -827,7 +827,7 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
name,
absl::StrCat("num_lifted_booleans=",
integer_rounding_cut_helper_.NumLiftedBooleans()),
first_new_var, first_slack, ib_slack_infos, &cut_);
first_new_var, first_slack, tmp_ib_slack_infos_, &cut_);
}
return at_least_one_added;
}
@@ -881,16 +881,16 @@ bool LinearProgrammingConstraint::PostprocessAndAddCut(
const int index = (var.value() - first_new_var.value()) / 2;
CHECK_LT(index, ib_slack_infos.size());
std::vector<std::pair<ColIndex, IntegerValue>> terms;
tmp_terms_.clear();
for (const std::pair<IntegerVariable, IntegerValue>& term :
ib_slack_infos[index].terms) {
terms.push_back(
tmp_terms_.push_back(
{gtl::FindOrDie(mirror_lp_variable_,
PositiveVariable(term.first)),
VariableIsPositive(term.first) ? term.second : -term.second});
}
if (!tmp_scattered_vector_.AddLinearExpressionMultiple(multiplier,
terms)) {
tmp_terms_)) {
overflow = true;
break;
}
@@ -951,8 +951,6 @@ bool LinearProgrammingConstraint::PostprocessAndAddCut(
// promising. Or only test a few positions and not all rows.
void LinearProgrammingConstraint::AddCGCuts() {
const RowIndex num_rows = lp_data_.num_constraints();
std::vector<std::pair<RowIndex, double>> lp_multipliers;
std::vector<std::pair<RowIndex, IntegerValue>> integer_multipliers;
for (RowIndex row(0); row < num_rows; ++row) {
ColIndex basis_col = simplex_.GetBasis(row);
const Fractional lp_value = GetVariableValueAtCpScale(basis_col);
@@ -973,7 +971,7 @@ void LinearProgrammingConstraint::AddCGCuts() {
// TODO(user): Avoid code duplication between the sparse/dense path.
double magnitude = 0.0;
lp_multipliers.clear();
tmp_lp_multipliers_.clear();
const glop::ScatteredRow& lambda = simplex_.GetUnitRowLeftInverse(row);
if (lambda.non_zeros.empty()) {
for (RowIndex row(0); row < num_rows; ++row) {
@@ -989,7 +987,7 @@ void LinearProgrammingConstraint::AddCGCuts() {
}
magnitude = std::max(magnitude, std::abs(value));
lp_multipliers.push_back({row, value});
tmp_lp_multipliers_.push_back({row, value});
}
} else {
for (const ColIndex col : lambda.non_zeros) {
@@ -1004,10 +1002,10 @@ void LinearProgrammingConstraint::AddCGCuts() {
}
magnitude = std::max(magnitude, std::abs(value));
lp_multipliers.push_back({row, value});
tmp_lp_multipliers_.push_back({row, value});
}
}
if (lp_multipliers.empty()) continue;
if (tmp_lp_multipliers_.empty()) continue;
Fractional scaling;
for (int i = 0; i < 2; ++i) {
@@ -1016,17 +1014,17 @@ void LinearProgrammingConstraint::AddCGCuts() {
//
// TODO(user): Maybe add an heuristic to know beforehand which sign to
// use?
for (std::pair<RowIndex, double>& p : lp_multipliers) {
for (std::pair<RowIndex, double>& p : tmp_lp_multipliers_) {
p.second = -p.second;
}
}
// TODO(user): We use a lower value here otherwise we might run into
// overflow while computing the cut. This should be fixable.
integer_multipliers =
tmp_integer_multipliers_ =
ScaleLpMultiplier(/*take_objective_into_account=*/false,
lp_multipliers, &scaling, /*max_pow=*/52);
AddCutFromConstraints("CG", integer_multipliers);
tmp_lp_multipliers_, &scaling, /*max_pow=*/52);
AddCutFromConstraints("CG", tmp_integer_multipliers_);
}
}
}
@@ -1068,35 +1066,64 @@ IntegerValue GetCoeff(ColIndex col, const ListOfTerms& terms) {
void LinearProgrammingConstraint::AddObjectiveCut() {
if (integer_objective_.size() <= 1) return;
// Clear temp data.
// We only try to add such cut if the LB objective is "far" from the current
// objective lower bound. Note that this is in term of the "internal" integer
// objective.
const double obj_lp_value = simplex_.GetObjectiveValue();
const IntegerValue obj_lower_bound =
integer_trail_->LevelZeroLowerBound(objective_cp_);
if (obj_lp_value + 1.0 >= ToDouble(obj_lower_bound)) return;
tmp_lp_values_.clear();
tmp_var_lbs_.clear();
tmp_var_ubs_.clear();
cut_.Clear();
// We negate everything to have a <= base constraint.
cut_.lb = kMinIntegerValue;
cut_.ub = integer_objective_offset_ -
integer_trail_->LevelZeroLowerBound(objective_cp_);
LinearConstraint objective_ct;
objective_ct.lb = kMinIntegerValue;
objective_ct.ub = integer_objective_offset_ -
integer_trail_->LevelZeroLowerBound(objective_cp_);
IntegerValue obj_coeff_magnitude(0);
for (const auto& [col, coeff] : integer_objective_) {
const IntegerVariable var = integer_variables_[col.value()];
cut_.vars.push_back(var);
objective_ct.vars.push_back(var);
tmp_lp_values_.push_back(expanded_lp_solution_[var]);
tmp_var_lbs_.push_back(integer_trail_->LevelZeroLowerBound(var));
tmp_var_ubs_.push_back(integer_trail_->LevelZeroUpperBound(var));
cut_.coeffs.push_back(-coeff);
objective_ct.coeffs.push_back(-coeff);
obj_coeff_magnitude = std::max(obj_coeff_magnitude, IntTypeAbs(coeff));
}
// Because the objective has often large coefficient, we always try a MIR1
// like heuristic to round it to reasonable values.
RoundingOptions options;
options.max_scaling = parameters_.max_integer_rounding_scaling();
integer_rounding_cut_helper_.ComputeCut(options, tmp_lp_values_, tmp_var_lbs_,
tmp_var_ubs_,
&implied_bounds_processor_, &cut_);
// If the magnitude is small enough, just try to add the full objective. Other
// cuts will be derived in subsequent passes. Otherwise, try normal cut
// heuristic that should result in a cut with reasonable coefficients.
if (obj_coeff_magnitude < 1e9) {
const bool added = constraint_manager_.AddCut(objective_ct, "Objective",
expanded_lp_solution_);
if (added) return;
}
// Note that the cut will not be added if it is not good enough.
constraint_manager_.AddCut(cut_, "Objective", expanded_lp_solution_);
// Try knapsack.
{
cut_ = objective_ct;
if (cover_cut_helper_.TrySimpleKnapsack(cut_, tmp_lp_values_, tmp_var_lbs_,
tmp_var_ubs_)) {
constraint_manager_.AddCut(cut_, "Objective_K", expanded_lp_solution_);
}
}
// Try MIR1.
{
cut_ = objective_ct;
RoundingOptions options;
options.max_scaling = parameters_.max_integer_rounding_scaling();
integer_rounding_cut_helper_.ComputeCut(options, tmp_lp_values_,
tmp_var_lbs_, tmp_var_ubs_,
&implied_bounds_processor_, &cut_);
// Note that the cut will not be added if it is not good enough.
constraint_manager_.AddCut(cut_, "Objective_MIR", expanded_lp_solution_);
}
}
void LinearProgrammingConstraint::AddMirCuts() {
@@ -2087,21 +2114,20 @@ bool LinearProgrammingConstraint::ExactLpReasonning() {
//
// TODO(user): Provide and use a sparse API in Glop to get the duals.
const RowIndex num_rows = simplex_.GetProblemNumRows();
std::vector<std::pair<RowIndex, double>> lp_multipliers;
tmp_lp_multipliers_.clear();
for (RowIndex row(0); row < num_rows; ++row) {
const double value = -simplex_.GetDualValue(row);
if (std::abs(value) < kZeroTolerance) continue;
lp_multipliers.push_back({row, value});
tmp_lp_multipliers_.push_back({row, value});
}
Fractional scaling;
std::vector<std::pair<RowIndex, IntegerValue>> integer_multipliers =
ScaleLpMultiplier(/*take_objective_into_account=*/true, lp_multipliers,
&scaling);
tmp_integer_multipliers_ = ScaleLpMultiplier(
/*take_objective_into_account=*/true, tmp_lp_multipliers_, &scaling);
IntegerValue rc_ub;
if (!ComputeNewLinearConstraint(integer_multipliers, &tmp_scattered_vector_,
&rc_ub)) {
if (!ComputeNewLinearConstraint(tmp_integer_multipliers_,
&tmp_scattered_vector_, &rc_ub)) {
VLOG(1) << "Issue while computing the exact LP reason. Aborting.";
return true;
}
@@ -2116,30 +2142,29 @@ bool LinearProgrammingConstraint::ExactLpReasonning() {
CHECK(tmp_scattered_vector_.AddLinearExpressionMultiple(obj_scale,
integer_objective_));
CHECK(AddProductTo(-obj_scale, integer_objective_offset_, &rc_ub));
AdjustNewLinearConstraint(&integer_multipliers, &tmp_scattered_vector_,
AdjustNewLinearConstraint(&tmp_integer_multipliers_, &tmp_scattered_vector_,
&rc_ub);
// Create the IntegerSumLE that will allow to propagate the objective and more
// generally do the reduced cost fixing.
LinearConstraint new_constraint;
tmp_scattered_vector_.ConvertToLinearConstraint(integer_variables_, rc_ub,
&new_constraint);
new_constraint.vars.push_back(objective_cp_);
new_constraint.coeffs.push_back(-obj_scale);
DivideByGCD(&new_constraint);
PreventOverflow(&new_constraint);
DCHECK(!PossibleOverflow(new_constraint));
DCHECK(constraint_manager_.DebugCheckConstraint(new_constraint));
&tmp_constraint_);
tmp_constraint_.vars.push_back(objective_cp_);
tmp_constraint_.coeffs.push_back(-obj_scale);
DivideByGCD(&tmp_constraint_);
PreventOverflow(&tmp_constraint_);
DCHECK(!PossibleOverflow(tmp_constraint_));
DCHECK(constraint_manager_.DebugCheckConstraint(tmp_constraint_));
// Corner case where prevent overflow removed all terms.
if (new_constraint.vars.empty()) {
if (tmp_constraint_.vars.empty()) {
trail_->MutableConflict()->clear();
return new_constraint.ub >= 0;
return tmp_constraint_.ub >= 0;
}
IntegerSumLE* cp_constraint =
new IntegerSumLE({}, new_constraint.vars, new_constraint.coeffs,
new_constraint.ub, model_);
new IntegerSumLE({}, tmp_constraint_.vars, tmp_constraint_.coeffs,
tmp_constraint_.ub, model_);
if (trail_->CurrentDecisionLevel() == 0) {
// Since we will never ask the reason for a constraint at level 0, we just
// keep the last one.
@@ -2154,43 +2179,41 @@ bool LinearProgrammingConstraint::ExactLpReasonning() {
bool LinearProgrammingConstraint::FillExactDualRayReason() {
Fractional scaling;
const glop::DenseColumn ray = simplex_.GetDualRay();
std::vector<std::pair<RowIndex, double>> lp_multipliers;
tmp_lp_multipliers_.clear();
for (RowIndex row(0); row < ray.size(); ++row) {
const double value = ray[row];
if (std::abs(value) < kZeroTolerance) continue;
lp_multipliers.push_back({row, value});
tmp_lp_multipliers_.push_back({row, value});
}
std::vector<std::pair<RowIndex, IntegerValue>> integer_multipliers =
ScaleLpMultiplier(/*take_objective_into_account=*/false, lp_multipliers,
&scaling);
tmp_integer_multipliers_ = ScaleLpMultiplier(
/*take_objective_into_account=*/false, tmp_lp_multipliers_, &scaling);
IntegerValue new_constraint_ub;
if (!ComputeNewLinearConstraint(integer_multipliers, &tmp_scattered_vector_,
&new_constraint_ub)) {
if (!ComputeNewLinearConstraint(tmp_integer_multipliers_,
&tmp_scattered_vector_, &new_constraint_ub)) {
VLOG(1) << "Isse while computing the exact dual ray reason. Aborting.";
return false;
}
AdjustNewLinearConstraint(&integer_multipliers, &tmp_scattered_vector_,
AdjustNewLinearConstraint(&tmp_integer_multipliers_, &tmp_scattered_vector_,
&new_constraint_ub);
LinearConstraint new_constraint;
tmp_scattered_vector_.ConvertToLinearConstraint(
integer_variables_, new_constraint_ub, &new_constraint);
DivideByGCD(&new_constraint);
PreventOverflow(&new_constraint);
DCHECK(!PossibleOverflow(new_constraint));
DCHECK(constraint_manager_.DebugCheckConstraint(new_constraint));
integer_variables_, new_constraint_ub, &tmp_constraint_);
DivideByGCD(&tmp_constraint_);
PreventOverflow(&tmp_constraint_);
DCHECK(!PossibleOverflow(tmp_constraint_));
DCHECK(constraint_manager_.DebugCheckConstraint(tmp_constraint_));
const IntegerValue implied_lb = GetImpliedLowerBound(new_constraint);
if (implied_lb <= new_constraint.ub) {
const IntegerValue implied_lb = GetImpliedLowerBound(tmp_constraint_);
if (implied_lb <= tmp_constraint_.ub) {
VLOG(1) << "LP exact dual ray not infeasible,"
<< " implied_lb: " << implied_lb.value() / scaling
<< " ub: " << new_constraint.ub.value() / scaling;
<< " ub: " << tmp_constraint_.ub.value() / scaling;
return false;
}
const IntegerValue slack = (implied_lb - new_constraint.ub) - 1;
SetImpliedLowerBoundReason(new_constraint, slack);
const IntegerValue slack = (implied_lb - tmp_constraint_.ub) - 1;
SetImpliedLowerBoundReason(tmp_constraint_, slack);
return true;
}

7
ortools/sat/linear_programming_constraint.h
View File

@@ -429,6 +429,7 @@ class LinearProgrammingConstraint : public PropagatorInterface,
CoverCutHelper cover_cut_helper_;
IntegerRoundingCutHelper integer_rounding_cut_helper_;
LinearConstraint cut_;
LinearConstraint tmp_constraint_;
ScatteredIntegerVector tmp_scattered_vector_;
@@ -437,6 +438,12 @@ class LinearProgrammingConstraint : public PropagatorInterface,
std::vector<IntegerValue> tmp_var_ubs_;
std::vector<glop::RowIndex> tmp_slack_rows_;
std::vector<IntegerValue> tmp_slack_bounds_;
std::vector<ImpliedBoundsProcessor::SlackInfo> tmp_ib_slack_infos_;
std::vector<std::pair<glop::ColIndex, IntegerValue>> tmp_terms_;
// Used by AddCGCuts().
std::vector<std::pair<glop::RowIndex, double>> tmp_lp_multipliers_;
std::vector<std::pair<glop::RowIndex, IntegerValue>> tmp_integer_multipliers_;
// Used by ScaleLpMultiplier().
mutable std::vector<std::pair<glop::RowIndex, double>> tmp_cp_multipliers_;

67
ortools/sat/lp_utils.cc
View File

@@ -1312,73 +1312,6 @@ void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem& problem,
lp->CleanUp();
}
int FixVariablesFromSat(const SatSolver& solver, glop::LinearProgram* lp) {
int num_fixed_variables = 0;
const Trail& trail = solver.LiteralTrail();
for (int i = 0; i < trail.Index(); ++i) {
const BooleanVariable var = trail[i].Variable();
const int value = trail[i].IsPositive() ? 1.0 : 0.0;
if (trail.Info(var).level == 0) {
++num_fixed_variables;
lp->SetVariableBounds(ColIndex(var.value()), value, value);
}
}
return num_fixed_variables;
}
bool SolveLpAndUseSolutionForSatAssignmentPreference(
const glop::LinearProgram& lp, SatSolver* sat_solver,
double max_time_in_seconds) {
glop::LPSolver solver;
glop::GlopParameters glop_parameters;
glop_parameters.set_max_time_in_seconds(max_time_in_seconds);
solver.SetParameters(glop_parameters);
const glop::ProblemStatus& status = solver.Solve(lp);
if (status != glop::ProblemStatus::OPTIMAL &&
status != glop::ProblemStatus::IMPRECISE &&
status != glop::ProblemStatus::PRIMAL_FEASIBLE) {
return false;
}
for (ColIndex col(0); col < lp.num_variables(); ++col) {
const Fractional& value = solver.variable_values()[col];
sat_solver->SetAssignmentPreference(
Literal(BooleanVariable(col.value()), round(value) == 1),
1 - std::abs(value - round(value)));
}
return true;
}
bool SolveLpAndUseIntegerVariableToStartLNS(const glop::LinearProgram& lp,
LinearBooleanProblem* problem) {
glop::LPSolver solver;
const glop::ProblemStatus& status = solver.Solve(lp);
if (status != glop::ProblemStatus::OPTIMAL &&
status != glop::ProblemStatus::PRIMAL_FEASIBLE)
return false;
int num_variable_fixed = 0;
for (ColIndex col(0); col < lp.num_variables(); ++col) {
const Fractional tolerance = 1e-5;
const Fractional& value = solver.variable_values()[col];
if (value > 1 - tolerance) {
++num_variable_fixed;
LinearBooleanConstraint* constraint = problem->add_constraints();
constraint->set_lower_bound(1);
constraint->set_upper_bound(1);
constraint->add_coefficients(1);
constraint->add_literals(col.value() + 1);
} else if (value < tolerance) {
++num_variable_fixed;
LinearBooleanConstraint* constraint = problem->add_constraints();
constraint->set_lower_bound(0);
constraint->set_upper_bound(0);
constraint->add_coefficients(1);
constraint->add_literals(col.value() + 1);
}
}
LOG(INFO) << "LNS with " << num_variable_fixed << " fixed variables.";
return true;
}
double ComputeTrueObjectiveLowerBound(
const CpModelProto& model_proto_with_floating_point_objective,
const CpObjectiveProto& integer_objective,

19
ortools/sat/lp_utils.h
View File

@@ -135,25 +135,6 @@ bool ConvertBinaryMPModelProtoToBooleanProblem(const MPModelProto& mp_model,
void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem& problem,
glop::LinearProgram* lp);
// Changes the variable bounds of the lp to reflect the variables that have been
// fixed by the SAT solver (i.e. assigned at decision level 0). Returns the
// number of variables fixed this way.
int FixVariablesFromSat(const SatSolver& solver, glop::LinearProgram* lp);
// Solves the given lp problem and uses the lp solution to drive the SAT solver
// polarity choices. The variable must have the same index in the solved lp
// problem and in SAT for this to make sense.
//
// Returns false if a problem occurred while trying to solve the lp.
bool SolveLpAndUseSolutionForSatAssignmentPreference(
const glop::LinearProgram& lp, SatSolver* sat_solver,
double max_time_in_seconds);
// Solves the lp and add constraints to fix the integer variable of the lp in
// the LinearBoolean problem.
bool SolveLpAndUseIntegerVariableToStartLNS(const glop::LinearProgram& lp,
LinearBooleanProblem* problem);
} // namespace sat
} // namespace operations_research