speedup presolve and loader
This commit is contained in:
File diff suppressed because it is too large
Load Diff
@@ -102,10 +102,6 @@ class CpModelPresolver {
|
||||
bool PresolveTable(ConstraintProto* ct);
|
||||
bool PresolveElement(ConstraintProto* ct);
|
||||
bool PresolveInterval(int c, ConstraintProto* ct);
|
||||
bool PresolveLinear(ConstraintProto* ct);
|
||||
bool PresolveLinearOnBooleans(ConstraintProto* ct);
|
||||
bool CanonicalizeLinear(ConstraintProto* ct);
|
||||
bool RemoveSingletonInLinear(ConstraintProto* ct);
|
||||
bool PresolveIntDiv(ConstraintProto* ct);
|
||||
bool PresolveIntProd(ConstraintProto* ct);
|
||||
bool PresolveIntMin(ConstraintProto* ct);
|
||||
@@ -116,6 +112,13 @@ class CpModelPresolver {
|
||||
bool PresolveBoolOr(ConstraintProto* ct);
|
||||
bool PresolveEnforcementLiteral(ConstraintProto* ct);
|
||||
|
||||
// For the linear constraints, we have more than one function.
|
||||
bool CanonicalizeLinear(ConstraintProto* ct);
|
||||
bool PropagateDomainsInLinear(ConstraintProto* ct);
|
||||
bool RemoveSingletonInLinear(ConstraintProto* ct);
|
||||
bool PresolveSmallLinear(ConstraintProto* ct);
|
||||
bool PresolveLinearOnBooleans(ConstraintProto* ct);
|
||||
|
||||
// SetPPC is short for set packing, partitioning and covering constraints.
|
||||
// These are sum of booleans <=, = and >= 1 respectively.
|
||||
bool ProcessSetPPC();
|
||||
@@ -144,7 +147,7 @@ class CpModelPresolver {
|
||||
|
||||
void ExpandObjective();
|
||||
|
||||
void TryToSimplifyDomains();
|
||||
void TryToSimplifyDomain(int var);
|
||||
|
||||
void MergeNoOverlapConstraints();
|
||||
|
||||
@@ -161,6 +164,9 @@ class CpModelPresolver {
|
||||
const PresolveOptions& options_;
|
||||
std::vector<int>* postsolve_mapping_;
|
||||
PresolveContext* context_;
|
||||
|
||||
// Used by CanonicalizeLinear().
|
||||
std::vector<std::pair<int, int64>> tmp_terms_;
|
||||
};
|
||||
|
||||
// Convenient wrapper to call the full presolve.
|
||||
|
||||
@@ -163,8 +163,17 @@ void LinearConstraintManager::ComputeObjectiveParallelism(
|
||||
constraint_infos_[ct_index].objective_parallelism = 0.0;
|
||||
return;
|
||||
}
|
||||
|
||||
const LinearConstraint& lc = constraint_infos_[ct_index].constraint;
|
||||
double unscaled_objective_parallelism = 0.0;
|
||||
for (int i = 0; i < lc.vars.size(); ++i) {
|
||||
if (lc.vars[i] < dense_objective_coeffs_.size()) {
|
||||
unscaled_objective_parallelism +=
|
||||
ToDouble(lc.coeffs[i]) * dense_objective_coeffs_[lc.vars[i]];
|
||||
}
|
||||
}
|
||||
const double objective_parallelism =
|
||||
ScalarProduct(constraint_infos_[ct_index].constraint, objective_) /
|
||||
unscaled_objective_parallelism /
|
||||
(constraint_infos_[ct_index].l2_norm * objective_l2_norm_);
|
||||
constraint_infos_[ct_index].objective_parallelism =
|
||||
std::abs(objective_parallelism);
|
||||
@@ -335,6 +344,8 @@ bool LinearConstraintManager::SimplifyConstraint(LinearConstraint* ct) {
|
||||
|
||||
bool LinearConstraintManager::ChangeLp(
|
||||
const gtl::ITIVector<IntegerVariable, double>& lp_solution) {
|
||||
VLOG(3) << "Enter ChangeLP, scan " << constraint_infos_.size()
|
||||
<< " constraints";
|
||||
std::vector<ConstraintIndex> new_constraints;
|
||||
std::vector<double> new_constraints_efficacies;
|
||||
std::vector<double> new_constraints_orthogonalities;
|
||||
@@ -346,6 +357,7 @@ bool LinearConstraintManager::ChangeLp(
|
||||
// We keep any constraints that is already present, and otherwise, we add the
|
||||
// ones that are currently not satisfied by at least "tolerance".
|
||||
const double tolerance = 1e-6;
|
||||
FillDenseObjectiveCoeffs();
|
||||
for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
|
||||
if (constraint_infos_[i].permanently_removed) continue;
|
||||
|
||||
@@ -387,6 +399,17 @@ bool LinearConstraintManager::ChangeLp(
|
||||
new_constraints_efficacies.push_back(violation /
|
||||
constraint_infos_[i].l2_norm);
|
||||
new_constraints_orthogonalities.push_back(1.0);
|
||||
|
||||
if (objective_is_defined_ &&
|
||||
!constraint_infos_[i].objective_parallelism_computed) {
|
||||
ComputeObjectiveParallelism(i);
|
||||
} else if (!objective_is_defined_) {
|
||||
constraint_infos_[i].objective_parallelism = 0.0;
|
||||
}
|
||||
|
||||
constraint_infos_[i].current_score =
|
||||
new_constraints_efficacies.back() +
|
||||
constraint_infos_[i].objective_parallelism;
|
||||
}
|
||||
}
|
||||
|
||||
@@ -396,18 +419,36 @@ bool LinearConstraintManager::ChangeLp(
|
||||
RemoveMarkedConstraints();
|
||||
}
|
||||
|
||||
// Note that the algo below is in O(limit * new_constraint), so this limit
|
||||
// should stay low.
|
||||
// Note that the algo below is in O(limit * new_constraint). In order to
|
||||
// limit spending too much time on this, we first sort all the constraints
|
||||
// with an imprecise score (no orthogonality), then limit the size of the
|
||||
// vector of constraints to precisely score, then we do the actual scoring.
|
||||
//
|
||||
// On problem crossword_opt_grid-19.05_dict-80_sat with linearization_level=2,
|
||||
// new_constraint.size() > 1.5M.
|
||||
//
|
||||
// TODO(user): This blowup factor could be adaptative w.r.t. the constraint
|
||||
// limit.
|
||||
const int kBlowupFactor = 4;
|
||||
int constraint_limit = std::min(50, static_cast<int>(new_constraints.size()));
|
||||
if (lp_constraints_.empty()) {
|
||||
constraint_limit = std::min(1000, static_cast<int>(new_constraints.size()));
|
||||
}
|
||||
VLOG(3) << " - size = " << new_constraints.size()
|
||||
<< ", limit = " << constraint_limit;
|
||||
|
||||
// TODO(user,user): on problem crossword_opt_grid-19.05_dict-80_sat with
|
||||
// linearization_level=2, new_constraint.size() > 1.5M. Improve
|
||||
// complexity of the following loop.
|
||||
std::stable_sort(new_constraints.begin(), new_constraints.end(),
|
||||
[&](ConstraintIndex a, ConstraintIndex b) {
|
||||
return constraint_infos_[a].current_score >
|
||||
constraint_infos_[b].current_score;
|
||||
});
|
||||
if (new_constraints.size() > kBlowupFactor * constraint_limit) {
|
||||
VLOG(3) << "Resize candidate constraints from " << new_constraints.size()
|
||||
<< " down to " << kBlowupFactor * constraint_limit;
|
||||
new_constraints.resize(kBlowupFactor * constraint_limit);
|
||||
}
|
||||
|
||||
int skipped_checks = 0;
|
||||
int num_skipped_checks = 0;
|
||||
const int kCheckFrequency = 100;
|
||||
ConstraintIndex last_added_candidate = kInvalidConstraintIndex;
|
||||
for (int i = 0; i < constraint_limit; ++i) {
|
||||
@@ -416,10 +457,10 @@ bool LinearConstraintManager::ChangeLp(
|
||||
double best_score = 0.0;
|
||||
ConstraintIndex best_candidate = kInvalidConstraintIndex;
|
||||
for (int j = 0; j < new_constraints.size(); ++j) {
|
||||
// Checks the time limit, and returns not_changed if crossed.
|
||||
if (++skipped_checks >= kCheckFrequency) {
|
||||
if (time_limit_->LimitReached()) return false;
|
||||
skipped_checks = 0;
|
||||
// Checks the time limit, and returns if the lp has changed.
|
||||
if (++num_skipped_checks >= kCheckFrequency) {
|
||||
if (time_limit_->LimitReached()) return current_lp_is_changed_;
|
||||
num_skipped_checks = 0;
|
||||
}
|
||||
|
||||
const ConstraintIndex new_constraint = new_constraints[j];
|
||||
@@ -449,16 +490,10 @@ bool LinearConstraintManager::ChangeLp(
|
||||
continue;
|
||||
}
|
||||
|
||||
if (objective_is_defined_ &&
|
||||
!constraint_infos_[new_constraint].objective_parallelism_computed) {
|
||||
ComputeObjectiveParallelism(new_constraint);
|
||||
}
|
||||
|
||||
// TODO(user): Experiment with different weights or different
|
||||
// functions for computing score.
|
||||
const double score =
|
||||
new_constraints_orthogonalities[j] + new_constraints_efficacies[j] +
|
||||
constraint_infos_[new_constraint].objective_parallelism;
|
||||
const double score = new_constraints_orthogonalities[j] +
|
||||
constraint_infos_[new_constraint].current_score;
|
||||
CHECK_GE(score, 0.0);
|
||||
if (score > best_score || best_candidate == kInvalidConstraintIndex) {
|
||||
best_score = score;
|
||||
@@ -478,6 +513,7 @@ bool LinearConstraintManager::ChangeLp(
|
||||
}
|
||||
}
|
||||
|
||||
VLOG(3) << " - Exit ChangeLP";
|
||||
// The LP changed only if we added new constraints or if some constraints
|
||||
// already inside changed (simplification or tighter bounds).
|
||||
if (current_lp_is_changed_) {
|
||||
@@ -495,5 +531,16 @@ void LinearConstraintManager::AddAllConstraintsToLp() {
|
||||
}
|
||||
}
|
||||
|
||||
void LinearConstraintManager::FillDenseObjectiveCoeffs() {
|
||||
if (objective_.vars.empty()) return;
|
||||
DCHECK(std::is_sorted(objective_.vars.begin(), objective_.vars.end()));
|
||||
const IntegerVariable last_var = objective_.vars.back();
|
||||
dense_objective_coeffs_.assign(last_var.value() + 1, 0.0);
|
||||
for (int i = 0; i < objective_.vars.size(); ++i) {
|
||||
dense_objective_coeffs_[objective_.vars[i]] =
|
||||
ToDouble(objective_.coeffs[i]);
|
||||
}
|
||||
}
|
||||
|
||||
} // namespace sat
|
||||
} // namespace operations_research
|
||||
|
||||
@@ -53,6 +53,7 @@ class LinearConstraintManager {
|
||||
// parallel to one of the existing constraints in the LP.
|
||||
bool permanently_removed;
|
||||
size_t hash;
|
||||
double current_score;
|
||||
};
|
||||
|
||||
explicit LinearConstraintManager(Model* model)
|
||||
@@ -114,6 +115,9 @@ class LinearConstraintManager {
|
||||
// Returns true if the terms of the constraint changed.
|
||||
bool SimplifyConstraint(LinearConstraint* ct);
|
||||
|
||||
// Helper method to fill in the objective_values_ vector.
|
||||
void FillDenseObjectiveCoeffs();
|
||||
|
||||
// Helper method to compute objective parallelism for a given constraint. This
|
||||
// also lazily computes objective norm.
|
||||
void ComputeObjectiveParallelism(const ConstraintIndex ct_index);
|
||||
@@ -155,6 +159,9 @@ class LinearConstraintManager {
|
||||
bool objective_norm_computed_ = false;
|
||||
LinearConstraint objective_;
|
||||
double objective_l2_norm_ = 0.0;
|
||||
// Dense representation of the objective coeffs indexed by variables indices.
|
||||
// It contains 0.0 where the variables does not appear in the objective.
|
||||
gtl::ITIVector<IntegerVariable, double> dense_objective_coeffs_;
|
||||
|
||||
TimeLimit* time_limit_;
|
||||
};
|
||||
|
||||
@@ -1243,7 +1243,10 @@ SatSolver::Status FindCores(std::vector<Literal> assumptions,
|
||||
std::vector<std::vector<Literal>>* cores) {
|
||||
cores->clear();
|
||||
SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
|
||||
TimeLimit* limit = model->GetOrCreate<TimeLimit>();
|
||||
do {
|
||||
if (limit->LimitReached()) return SatSolver::LIMIT_REACHED;
|
||||
|
||||
const SatSolver::Status result =
|
||||
ResetAndSolveIntegerProblem(assumptions, model);
|
||||
if (result != SatSolver::ASSUMPTIONS_UNSAT) return result;
|
||||
|
||||
@@ -14,6 +14,7 @@
|
||||
#include "ortools/sat/presolve_context.h"
|
||||
|
||||
#include "ortools/base/map_util.h"
|
||||
#include "ortools/base/mathutil.h"
|
||||
#include "ortools/port/proto_utils.h"
|
||||
|
||||
namespace operations_research {
|
||||
@@ -66,8 +67,8 @@ bool PresolveContext::DomainIsEmpty(int ref) const {
|
||||
}
|
||||
|
||||
bool PresolveContext::IsFixed(int ref) const {
|
||||
CHECK(!DomainIsEmpty(ref));
|
||||
return domains[PositiveRef(ref)].Min() == domains[PositiveRef(ref)].Max();
|
||||
DCHECK(!DomainIsEmpty(ref));
|
||||
return domains[PositiveRef(ref)].IsFixed();
|
||||
}
|
||||
|
||||
bool PresolveContext::LiteralIsTrue(int lit) const {
|
||||
@@ -263,10 +264,13 @@ void PresolveContext::StoreAffineRelation(const ConstraintProto& ct, int ref_x,
|
||||
added |= var_equiv_relations.TryAdd(x, y, c, o, allow_rep_x, allow_rep_y);
|
||||
}
|
||||
if (added) {
|
||||
// The domain didn't change, but this notification allows to re-process
|
||||
// any constraint containing these variables.
|
||||
modified_domains.Set(x);
|
||||
modified_domains.Set(y);
|
||||
// The domain didn't change, but this notification allows to re-process any
|
||||
// constraint containing these variables. Note that we do not need to
|
||||
// retrigger a propagation of the constraint containing a variable whose
|
||||
// representative didn't change.
|
||||
const int new_rep = affine_relations.Get(rep_x).representative;
|
||||
if (new_rep != rep_x) modified_domains.Set(x);
|
||||
if (new_rep != rep_y) modified_domains.Set(y);
|
||||
affine_constraints.insert(&ct);
|
||||
}
|
||||
}
|
||||
@@ -277,20 +281,6 @@ void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) {
|
||||
is_unsat = true;
|
||||
return;
|
||||
}
|
||||
bool added = false;
|
||||
if (RefIsPositive(ref_a) == RefIsPositive(ref_b)) {
|
||||
added |=
|
||||
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), 1, 0);
|
||||
added |= var_equiv_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b),
|
||||
1, 0);
|
||||
} else {
|
||||
added |=
|
||||
affine_relations.TryAdd(PositiveRef(ref_a), PositiveRef(ref_b), -1, 1);
|
||||
}
|
||||
if (!added) return;
|
||||
|
||||
modified_domains.Set(PositiveRef(ref_a));
|
||||
modified_domains.Set(PositiveRef(ref_b));
|
||||
|
||||
// For now, we do need to add the relation ref_a == ref_b so we have a
|
||||
// proper variable usage count and propagation between ref_a and ref_b.
|
||||
@@ -308,14 +298,17 @@ void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) {
|
||||
arg->add_coeffs(-1);
|
||||
arg->add_domain(0);
|
||||
arg->add_domain(0);
|
||||
StoreAffineRelation(*ct, PositiveRef(ref_a), PositiveRef(ref_b), 1,
|
||||
/*offset=*/0);
|
||||
} else {
|
||||
// a = 1 - b
|
||||
arg->add_coeffs(1);
|
||||
arg->add_coeffs(1);
|
||||
arg->add_domain(1);
|
||||
arg->add_domain(1);
|
||||
StoreAffineRelation(*ct, PositiveRef(ref_a), PositiveRef(ref_b), -1,
|
||||
/*offset=*/1);
|
||||
}
|
||||
affine_constraints.insert(ct);
|
||||
UpdateNewConstraintsVariableUsage();
|
||||
}
|
||||
|
||||
@@ -454,22 +447,194 @@ int PresolveContext::GetOrCreateVarValueEncoding(int ref, int64 value) {
|
||||
return literal;
|
||||
}
|
||||
|
||||
void PresolveContext::SubstituteVariableInObjective(
|
||||
int var, int64 coeff, const ConstraintProto& equality) {
|
||||
// Remove objective entry from var_to_constraint lists. The objective
|
||||
// entries will be added back after the substitution.
|
||||
const CpObjectiveProto& objective = working_model->objective();
|
||||
for (const int ref : objective.vars()) {
|
||||
var_to_constraints[PositiveRef(ref)].erase(-1);
|
||||
void PresolveContext::ReadObjectiveFromProto() {
|
||||
const CpObjectiveProto& obj = working_model->objective();
|
||||
|
||||
objective_offset = obj.offset();
|
||||
objective_scaling_factor = obj.scaling_factor();
|
||||
if (objective_scaling_factor == 0.0) {
|
||||
objective_scaling_factor = 1.0;
|
||||
}
|
||||
if (!obj.domain().empty()) {
|
||||
objective_domain = ReadDomainFromProto(obj);
|
||||
} else {
|
||||
objective_domain = Domain::AllValues();
|
||||
}
|
||||
|
||||
::operations_research::sat::SubstituteVariableInObjective(
|
||||
var, coeff, equality, working_model->mutable_objective());
|
||||
objective_map.clear();
|
||||
for (int i = 0; i < obj.vars_size(); ++i) {
|
||||
const int ref = obj.vars(i);
|
||||
int64 coeff = obj.coeffs(i);
|
||||
if (!RefIsPositive(ref)) coeff = -coeff;
|
||||
int var = PositiveRef(ref);
|
||||
|
||||
// Add back the objective entry for the variables in objective in
|
||||
// var_to_constraint lists.
|
||||
for (const int ref : objective.vars()) {
|
||||
var_to_constraints[PositiveRef(ref)].insert(-1);
|
||||
objective_map[var] += coeff;
|
||||
if (objective_map[var] == 0) {
|
||||
objective_map.erase(var);
|
||||
var_to_constraints[var].erase(-1);
|
||||
} else {
|
||||
var_to_constraints[var].insert(-1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void PresolveContext::CanonicalizeObjective() {
|
||||
int64 offset_change = 0;
|
||||
|
||||
// We replace each entry by its affine representative.
|
||||
// Note that the non-deterministic loop is fine.
|
||||
//
|
||||
// TODO(user): This is a bit dupplicated with the presolve linear code.
|
||||
// We also do not propagate back any domain restriction from the objective to
|
||||
// the variables if any.
|
||||
for (const auto& entry : objective_map) {
|
||||
const int var = entry.first;
|
||||
const int64 coeff = entry.second;
|
||||
|
||||
if (IsFixed(var)) {
|
||||
offset_change += coeff * MinOf(var);
|
||||
var_to_constraints[var].erase(-1);
|
||||
objective_map.erase(var);
|
||||
continue;
|
||||
}
|
||||
|
||||
const AffineRelation::Relation r = GetAffineRelation(var);
|
||||
if (r.representative == var) continue;
|
||||
|
||||
objective_map.erase(var);
|
||||
var_to_constraints[var].erase(-1);
|
||||
|
||||
// Do the substitution.
|
||||
offset_change += coeff * r.offset;
|
||||
const int64 new_coeff = objective_map[r.representative] += coeff * r.coeff;
|
||||
|
||||
// Process new term.
|
||||
if (new_coeff == 0) {
|
||||
objective_map.erase(r.representative);
|
||||
var_to_constraints[r.representative].erase(-1);
|
||||
} else {
|
||||
var_to_constraints[r.representative].insert(-1);
|
||||
if (IsFixed(r.representative)) {
|
||||
offset_change += new_coeff * MinOf(r.representative);
|
||||
var_to_constraints[r.representative].erase(-1);
|
||||
objective_map.erase(r.representative);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Domain implied_domain(0);
|
||||
int64 gcd(0);
|
||||
|
||||
// We need to sort the entries to be deterministic.
|
||||
{
|
||||
std::vector<std::pair<int, int64>> entries;
|
||||
for (const auto& entry : objective_map) {
|
||||
entries.push_back(entry);
|
||||
}
|
||||
std::sort(entries.begin(), entries.end());
|
||||
for (const auto& entry : entries) {
|
||||
const int var = entry.first;
|
||||
const int64 coeff = entry.second;
|
||||
gcd = MathUtil::GCD64(gcd, std::abs(coeff));
|
||||
implied_domain =
|
||||
implied_domain.AdditionWith(DomainOf(var).MultiplicationBy(coeff))
|
||||
.RelaxIfTooComplex();
|
||||
}
|
||||
}
|
||||
|
||||
// This is the new domain.
|
||||
// Note that the domain never include the offset.
|
||||
objective_domain = objective_domain.AdditionWith(Domain(-offset_change))
|
||||
.IntersectionWith(implied_domain);
|
||||
objective_domain =
|
||||
objective_domain.SimplifyUsingImpliedDomain(implied_domain);
|
||||
|
||||
// Updat the offset.
|
||||
objective_offset += offset_change;
|
||||
|
||||
// Maybe divide by GCD.
|
||||
if (gcd > 1) {
|
||||
for (auto& entry : objective_map) {
|
||||
entry.second /= gcd;
|
||||
}
|
||||
objective_domain = objective_domain.InverseMultiplicationBy(gcd);
|
||||
objective_offset /= static_cast<double>(gcd);
|
||||
objective_scaling_factor *= static_cast<double>(gcd);
|
||||
}
|
||||
}
|
||||
|
||||
void PresolveContext::SubstituteVariableInObjective(
|
||||
int var_in_equality, int64 coeff_in_equality,
|
||||
const ConstraintProto& equality, std::vector<int>* new_vars_in_objective) {
|
||||
CHECK(equality.enforcement_literal().empty());
|
||||
CHECK(RefIsPositive(var_in_equality));
|
||||
CHECK_EQ(std::abs(coeff_in_equality), 1);
|
||||
|
||||
if (new_vars_in_objective != nullptr) new_vars_in_objective->clear();
|
||||
|
||||
const int64 coeff_in_objective = gtl::FindOrDie(objective_map, var_in_equality);
|
||||
for (int i = 0; i < equality.linear().vars().size(); ++i) {
|
||||
int var = equality.linear().vars(i);
|
||||
int64 coeff = equality.linear().coeffs(i);
|
||||
if (!RefIsPositive(var)) {
|
||||
var = NegatedRef(var);
|
||||
coeff = -coeff;
|
||||
}
|
||||
if (var == var_in_equality) continue;
|
||||
|
||||
// We should divided by coeff_in_equality, but since its magnitude is one,
|
||||
// multiplying is the same.
|
||||
int64& map_ref = objective_map[var];
|
||||
if (map_ref == 0 && new_vars_in_objective != nullptr) {
|
||||
new_vars_in_objective->push_back(var);
|
||||
}
|
||||
map_ref -= coeff_in_objective * coeff * coeff_in_equality;
|
||||
|
||||
if (map_ref == 0) {
|
||||
objective_map.erase(var);
|
||||
var_to_constraints[var].erase(-1);
|
||||
} else {
|
||||
var_to_constraints[var].insert(-1);
|
||||
}
|
||||
}
|
||||
|
||||
objective_map.erase(var_in_equality);
|
||||
var_to_constraints[var_in_equality].erase(-1);
|
||||
|
||||
// Deal with the offset.
|
||||
Domain offset = ReadDomainFromProto(equality.linear());
|
||||
DCHECK_EQ(offset.Min(), offset.Max());
|
||||
bool exact = true;
|
||||
offset =
|
||||
offset.MultiplicationBy(coeff_in_objective * coeff_in_equality, &exact);
|
||||
CHECK(exact);
|
||||
|
||||
// Tricky: The objective domain is without the offset, so we need to shift it
|
||||
objective_offset += static_cast<double>(offset.Min());
|
||||
objective_domain = objective_domain.AdditionWith(Domain(-offset.Min()));
|
||||
}
|
||||
|
||||
void PresolveContext::WriteObjectiveToProto() {
|
||||
if (objective_domain.IsEmpty()) {
|
||||
return (void)NotifyThatModelIsUnsat();
|
||||
}
|
||||
|
||||
// We need to sort the entries to be deterministic.
|
||||
std::vector<std::pair<int, int64>> entries;
|
||||
for (const auto& entry : objective_map) {
|
||||
entries.push_back(entry);
|
||||
}
|
||||
std::sort(entries.begin(), entries.end());
|
||||
|
||||
CpObjectiveProto* mutable_obj = working_model->mutable_objective();
|
||||
mutable_obj->set_offset(objective_offset);
|
||||
mutable_obj->set_scaling_factor(objective_scaling_factor);
|
||||
FillDomainInProto(objective_domain, mutable_obj);
|
||||
mutable_obj->clear_vars();
|
||||
mutable_obj->clear_coeffs();
|
||||
for (const auto& entry : entries) {
|
||||
mutable_obj->add_vars(entry.first);
|
||||
mutable_obj->add_coeffs(entry.second);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -133,19 +133,33 @@ struct PresolveContext {
|
||||
// create it, add the corresponding constraints and returns it.
|
||||
int GetOrCreateVarValueEncoding(int ref, int64 value);
|
||||
|
||||
// Objective handling functions. We load it at the beginning so that during
|
||||
// presolve we can work on the more efficient hash_map representation.
|
||||
//
|
||||
// Note that ReadObjectiveFromProto() makes sure that var_to_constraints of
|
||||
// all the variable that appear in the objective contains -1. This is later
|
||||
// enforced by all the functions modifying the objective.
|
||||
void ReadObjectiveFromProto();
|
||||
void CanonicalizeObjective();
|
||||
void WriteObjectiveToProto();
|
||||
|
||||
// Given a variable defined by the given inequality that also appear in the
|
||||
// objective, remove it from the objective by transferring its cost to other
|
||||
// variables in the equality.
|
||||
//
|
||||
// TODO(user): Each time this is called, we do a linear scan of the objective
|
||||
// that can sometimes be really large (millions of variables). It will be more
|
||||
// efficient to just store the objective in a map at the beginning of the
|
||||
// presolve so this can be done in O(equality_size) and re-encode the
|
||||
// objective in the proto at the end. This code already exist in
|
||||
// ExpandObjective() and can be factored out. Look at the "ivu*.mps" problems
|
||||
// where the presolve is slow because of that.
|
||||
void SubstituteVariableInObjective(int var, int64 coeff,
|
||||
const ConstraintProto& equality);
|
||||
// If new_vars_in_objective is not nullptr, it will be filled with "new"
|
||||
// variables that where not in the objective before and are after
|
||||
// substitution.
|
||||
void SubstituteVariableInObjective(
|
||||
int var_in_equality, int64 coeff_in_equality,
|
||||
const ConstraintProto& equality,
|
||||
std::vector<int>* new_vars_in_objective = nullptr);
|
||||
|
||||
// Objective getters.
|
||||
const Domain& ObjectiveDomain() const { return objective_domain; }
|
||||
const absl::flat_hash_map<int, int64>& ObjectiveMap() const {
|
||||
return objective_map;
|
||||
}
|
||||
|
||||
// This regroups all the affine relations between variables. Note that the
|
||||
// constraints used to detect such relations will not be removed from the
|
||||
@@ -228,6 +242,15 @@ struct PresolveContext {
|
||||
|
||||
// The current domain of each variables.
|
||||
std::vector<Domain> domains;
|
||||
|
||||
// Internal representation of the objective. During presolve, we first load
|
||||
// the objective in this format in order to have more efficient substitution
|
||||
// on large problems (also because the objective is often dense). At the end
|
||||
// we re-convert it to its proto form.
|
||||
absl::flat_hash_map<int, int64> objective_map;
|
||||
Domain objective_domain;
|
||||
double objective_offset;
|
||||
double objective_scaling_factor;
|
||||
};
|
||||
|
||||
} // namespace sat
|
||||
|
||||
@@ -206,46 +206,5 @@ void SubstituteVariable(int var, int64 var_coeff_in_definition,
|
||||
SortAndMergeTerms(&terms, ct->mutable_linear());
|
||||
}
|
||||
|
||||
bool VarFoundInObjective(int var, CpObjectiveProto* obj) {
|
||||
const int size = obj->vars_size();
|
||||
for (int i = 0; i < size; ++i) {
|
||||
if (PositiveRef(obj->vars(i)) == PositiveRef(var)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void SubstituteVariableInObjective(int var, int64 var_coeff_in_definition,
|
||||
const ConstraintProto& definition,
|
||||
CpObjectiveProto* obj) {
|
||||
CHECK(RefIsPositive(var));
|
||||
CHECK_EQ(std::abs(var_coeff_in_definition), 1);
|
||||
|
||||
// Copy all the terms (except the one refering to var).
|
||||
std::vector<std::pair<int, int64>> terms;
|
||||
int64 var_coeff_in_obj = GetVarCoeffAndCopyOtherTerms(var, *obj, &terms);
|
||||
|
||||
if (var_coeff_in_definition < 0) var_coeff_in_obj *= -1;
|
||||
|
||||
AddTermsFromVarDefinition(var, var_coeff_in_obj, definition, &terms);
|
||||
|
||||
bool exact = false;
|
||||
Domain offset = ReadDomainFromProto(definition.linear());
|
||||
DCHECK_EQ(offset.Min(), offset.Max());
|
||||
offset = offset.MultiplicationBy(var_coeff_in_obj, &exact);
|
||||
CHECK(exact);
|
||||
|
||||
// Tricky: The objective domain is without the offset, so we need to shift it.
|
||||
obj->set_offset(offset.Min() + obj->offset());
|
||||
if (!obj->domain().empty()) {
|
||||
Domain old_domain = ReadDomainFromProto(*obj);
|
||||
FillDomainInProto(old_domain.AdditionWith(Domain(-offset.Min())), obj);
|
||||
}
|
||||
|
||||
// Sort and merge terms refering to the same variable.
|
||||
SortAndMergeTerms(&terms, obj);
|
||||
}
|
||||
|
||||
} // namespace sat
|
||||
} // namespace operations_research
|
||||
|
||||
@@ -88,15 +88,6 @@ class DomainDeductions {
|
||||
void SubstituteVariable(int var, int64 var_coeff_in_definition,
|
||||
const ConstraintProto& definition, ConstraintProto* ct);
|
||||
|
||||
// Returns true if the variable is found in objective linear terms.
|
||||
bool VarFoundInObjective(int var, CpObjectiveProto* obj);
|
||||
|
||||
// Replaces the variable var in objective using the definition constraint.
|
||||
// Currently the coefficient in the definition must be 1 or -1.
|
||||
void SubstituteVariableInObjective(int var, int64 var_coeff_in_definition,
|
||||
const ConstraintProto& definition,
|
||||
CpObjectiveProto* obj);
|
||||
|
||||
} // namespace sat
|
||||
} // namespace operations_research
|
||||
|
||||
|
||||
@@ -167,6 +167,8 @@ Domain Domain::FromVectorIntervals(
|
||||
|
||||
bool Domain::IsEmpty() const { return intervals_.empty(); }
|
||||
|
||||
bool Domain::IsFixed() const { return Min() == Max(); }
|
||||
|
||||
int64 Domain::Size() const {
|
||||
int64 size = 0;
|
||||
for (const ClosedInterval interval : intervals_) {
|
||||
@@ -180,12 +182,12 @@ int64 Domain::Size() const {
|
||||
}
|
||||
|
||||
int64 Domain::Min() const {
|
||||
CHECK(!IsEmpty());
|
||||
DCHECK(!IsEmpty());
|
||||
return intervals_.front().start;
|
||||
}
|
||||
|
||||
int64 Domain::Max() const {
|
||||
CHECK(!IsEmpty());
|
||||
DCHECK(!IsEmpty());
|
||||
return intervals_.back().end;
|
||||
}
|
||||
|
||||
|
||||
@@ -143,18 +143,22 @@ class Domain {
|
||||
|
||||
/**
|
||||
* Returns the min value of the domain.
|
||||
*
|
||||
* This checks that the domain is not empty.
|
||||
* The domain must not be empty.
|
||||
*/
|
||||
int64 Min() const;
|
||||
|
||||
/**
|
||||
* Returns the max value of the domain.
|
||||
*
|
||||
* This checks that the domain is not empty.
|
||||
* The domain must not be empty.
|
||||
*/
|
||||
int64 Max() const;
|
||||
|
||||
/**
|
||||
* Returns true iff the domain is reduced to a single value.
|
||||
* The domain must not be empty.
|
||||
*/
|
||||
bool IsFixed() const;
|
||||
|
||||
/**
|
||||
* Returns true iff value is in Domain.
|
||||
*/
|
||||
|
||||
Reference in New Issue
Block a user