improve performance of flatzinc presolve

This commit is contained in:
Laurent Perron
2017-09-06 10:19:30 +02:00
parent 2003500276
commit 26293b2b0f
5 changed files with 720 additions and 546 deletions

View File

@@ -77,44 +77,47 @@ Domain Domain::Boolean() {
return result;
}
void Domain::IntersectWithDomain(const Domain& other) {
if (other.is_interval) {
if (!other.values.empty()) {
IntersectWithInterval(other.values[0], other.values[1]);
bool Domain::IntersectWithDomain(const Domain& domain) {
if (domain.is_interval) {
if (!domain.values.empty()) {
return IntersectWithInterval(domain.values[0], domain.values[1]);
}
return;
return false;
}
if (is_interval) {
is_interval = false; // Other is not an interval.
if (values.empty()) {
values = other.values;
values = domain.values;
} else {
const int64 imin = values[0];
const int64 imax = values[1];
values = other.values;
values = domain.values;
IntersectWithInterval(imin, imax);
}
return;
return true;
}
// now deal with the intersection of two lists of values
IntersectWithListOfIntegers(other.values);
return IntersectWithListOfIntegers(domain.values);
}
void Domain::IntersectWithSingleton(int64 value) {
IntersectWithInterval(value, value);
bool Domain::IntersectWithSingleton(int64 value) {
return IntersectWithInterval(value, value);
}
void Domain::IntersectWithInterval(int64 imin, int64 imax) {
if (imin > imax) { // Empty interval -> empty domain.
bool Domain::IntersectWithInterval(int64 interval_min, int64 interval_max) {
if (interval_min > interval_max) { // Empty interval -> empty domain.
is_interval = false;
values.clear();
return true;
} else if (is_interval) {
if (values.empty()) {
values.push_back(imin);
values.push_back(imax);
values.push_back(interval_min);
values.push_back(interval_max);
return true;
} else {
values[0] = std::max(values[0], imin);
values[1] = std::min(values[1], imax);
if (values[0] >= interval_min && values[1] <= interval_max) return false;
values[0] = std::max(values[0], interval_min);
values[1] = std::min(values[1], interval_max);
if (values[0] > values[1]) {
values.clear();
is_interval = false;
@@ -122,29 +125,39 @@ void Domain::IntersectWithInterval(int64 imin, int64 imax) {
is_interval = false;
values.pop_back();
}
return true;
}
} else {
if (!values.empty()) {
std::sort(values.begin(), values.end());
std::vector<int64> new_values;
new_values.reserve(values.size());
bool changed = false;
for (const int64 val : values) {
if (val > imax) break;
if (val >= imin && (new_values.empty() || val != new_values.back())) {
if (val > interval_max) {
changed = true;
break;
}
if (val >= interval_min &&
(new_values.empty() || val != new_values.back())) {
new_values.push_back(val);
} else {
changed = true;
}
}
values.swap(new_values);
return changed;
}
}
return false;
}
void Domain::IntersectWithListOfIntegers(const std::vector<int64>& ovalues) {
bool Domain::IntersectWithListOfIntegers(const std::vector<int64>& integers) {
if (is_interval) {
const int64 dmin = values.empty() ? kint64min : values[0];
const int64 dmax = values.empty() ? kint64max : values[1];
values.clear();
for (const int64 v : ovalues) {
for (const int64 v : integers) {
if (v >= dmin && v <= dmax) values.push_back(v);
}
STLSortAndRemoveDuplicates(&values);
@@ -157,23 +170,30 @@ void Domain::IntersectWithListOfIntegers(const std::vector<int64>& ovalues) {
values.resize(2);
values[1] = last;
}
return values[0] != dmin || values[1] != dmax;
} else {
// This also covers and invalid (empty) domain.
is_interval = false;
return true;
}
} else {
// TODO(user): Investigate faster code for small arrays.
std::sort(values.begin(), values.end());
std::unordered_set<int64> other_values(ovalues.begin(), ovalues.end());
std::unordered_set<int64> other_values(integers.begin(), integers.end());
std::vector<int64> new_values;
new_values.reserve(std::min(values.size(), ovalues.size()));
new_values.reserve(std::min(values.size(), integers.size()));
bool changed = false;
for (const int64 val : values) {
if (ContainsKey(other_values, val) &&
(new_values.empty() || val != new_values.back())) {
new_values.push_back(val);
if (ContainsKey(other_values, val)) {
if (new_values.empty() || val != new_values.back()) {
new_values.push_back(val);
}
} else {
changed = true;
}
}
values.swap(new_values);
return changed;
}
}
@@ -553,6 +573,9 @@ bool IntegerVariable::Merge(const std::string& other_name,
}
if (defining_constraint == nullptr) {
defining_constraint = other_constraint;
if (defining_constraint != nullptr) {
defining_constraint->target_variable = this;
}
}
domain.IntersectWithDomain(other_domain);
return true;

View File

@@ -75,10 +75,10 @@ struct Domain {
// All the following modifiers change the internal representation
// list to interval or interval to list.
void IntersectWithSingleton(int64 value);
void IntersectWithDomain(const Domain& domain);
void IntersectWithInterval(int64 interval_min, int64 interval_max);
void IntersectWithListOfIntegers(const std::vector<int64>& values);
bool IntersectWithSingleton(int64 value);
bool IntersectWithDomain(const Domain& domain);
bool IntersectWithInterval(int64 interval_min, int64 interval_max);
bool IntersectWithListOfIntegers(const std::vector<int64>& integers);
// Returns true iff the value did belong to the domain, and was removed.
// Try to remove the value. It returns true if it was actually removed.

View File

@@ -19,6 +19,7 @@
#include "ortools/base/commandlineflags.h"
#include "ortools/base/commandlineflags.h"
#include "ortools/base/timer.h"
#include "ortools/flatzinc/logging.h"
#include "ortools/flatzinc/model.h"
#include "ortools/flatzinc/parser.h"
@@ -32,7 +33,10 @@ DEFINE_bool(statistics, false, "Print model statistics");
namespace operations_research {
namespace fz {
void ParseFile(const std::string& filename, bool presolve) {
FZLOG << "Parsing " << filename << FZENDL;
WallTimer timer;
timer.Start();
FZLOG << "Loading " << filename << FZENDL;
std::string problem_name = filename;
// Remove the .fzn extension.
@@ -43,13 +47,18 @@ void ParseFile(const std::string& filename, bool presolve) {
if (found != std::string::npos) {
problem_name = problem_name.substr(found + 1);
}
FZLOG << " - parsed in " << timer.GetInMs() << " ms" << FZENDL;
Model model(problem_name);
CHECK(ParseFlatzincFile(filename, &model));
if (presolve) {
FZLOG << "Presolve model" << FZENDL;
timer.Reset();
timer.Start();
Presolver presolve;
presolve.CleanUpModelForTheCpSolver(&model, /*use_sat=*/true);
presolve.Run(&model);
FZLOG << " - done in " << timer.GetInMs() << " ms" << FZENDL;
}
if (FLAGS_statistics) {
ModelStatistics stats(model);

File diff suppressed because it is too large Load Diff

View File

@@ -54,11 +54,19 @@ class Presolver {
// (defining_constraint, target_variable) for Boolean constraints.
void CleanUpModelForTheCpSolver(Model* model, bool use_sat);
// Returns true iff the model was modified.
// This method is public for tests.
bool PresolveOneConstraint(Constraint* ct);
void PresolveOneConstraint(Constraint* ct);
private:
enum RuleStatus {
NOT_CHANGED = 0, // Constraint has not changed.
CONTEXT_CHANGED, // The constraint has not changed, but some mapping,
// or some variables have been updated.
CONSTRAINT_REWRITTEN, // The constraint has been rewritten.
CONSTRAINT_ALWAYS_FALSE, // The constraint is always false.
CONSTRAINT_ALWAYS_TRUE, // The constraint is always true, and now inactive.
};
// This struct stores the affine mapping of one variable:
// it represents new_var = var * coefficient + offset. It also stores the
// constraint that defines this mapping.
@@ -123,52 +131,63 @@ class Presolver {
// Presolve rules. They returns true iff some presolve has been
// performed. These methods are called by the PresolveOneConstraint() method.
bool PresolveBool2Int(Constraint* ct, std::string* log);
bool PresolveIntEq(Constraint* ct, std::string* log);
bool Unreify(Constraint* ct, std::string* log);
bool PresolveInequalities(Constraint* ct, std::string* log);
bool PresolveIntNe(Constraint* ct, std::string* log);
bool PresolveSetNotIn(Constraint* ct, std::string* log);
bool PresolveSetIn(Constraint* ct, std::string* log);
bool PresolveSetInReif(Constraint* ct, std::string* log);
bool PresolveArrayBoolAnd(Constraint* ct, std::string* log);
bool PresolveArrayBoolOr(Constraint* ct, std::string* log);
bool PresolveBoolEqNeReif(Constraint* ct, std::string* log);
bool PresolveArrayIntElement(Constraint* ct, std::string* log);
bool PresolveIntDiv(Constraint* ct, std::string* log);
bool PresolveIntTimes(Constraint* ct, std::string* log);
bool PresolveIntLinGt(Constraint* ct, std::string* log);
bool PresolveIntLinLt(Constraint* ct, std::string* log);
bool PresolveLinear(Constraint* ct, std::string* log);
bool RegroupLinear(Constraint* ct, std::string* log);
bool SimplifyLinear(Constraint* ct, std::string* log);
bool PropagatePositiveLinear(Constraint* ct, std::string* log);
bool PresolveStoreMapping(Constraint* ct, std::string* log);
bool PresolveSimplifyElement(Constraint* ct, std::string* log);
bool PresolveSimplifyExprElement(Constraint* ct, std::string* log);
bool PropagateReifiedComparisons(Constraint* ct, std::string* log);
bool RemoveAbsFromIntLeReif(Constraint* ct, std::string* log);
bool SimplifyUnaryLinear(Constraint* ct, std::string* log);
bool SimplifyBinaryLinear(Constraint* ct, std::string* log);
bool CheckIntLinReifBounds(Constraint* ct, std::string* log);
bool CreateLinearTarget(Constraint* ct, std::string* log);
bool PresolveBoolNot(Constraint* ct, std::string* log);
bool PresolveBoolXor(Constraint* ct, std::string* log);
bool SimplifyIntLinEqReif(Constraint* ct, std::string* log);
bool PresolveIntMod(Constraint* ct, std::string* log);
bool PresolveBoolClause(Constraint* ct, std::string* log);
bool StoreIntEqReif(Constraint* ct, std::string* log);
bool SimplifyIntNeReif(Constraint* ct, std::string* log);
bool PresolveTableInt(Constraint* ct, std::string* log);
bool PresolveRegular(Constraint* ct, std::string* log);
bool PresolveDiffN(Constraint* ct, std::string* log);
RuleStatus PresolveBool2Int(Constraint* ct, std::string* log);
RuleStatus PresolveIntEq(Constraint* ct, std::string* log);
RuleStatus Unreify(Constraint* ct, std::string* log);
RuleStatus PresolveInequalities(Constraint* ct, std::string* log);
RuleStatus PresolveIntNe(Constraint* ct, std::string* log);
RuleStatus PresolveSetNotIn(Constraint* ct, std::string* log);
RuleStatus PresolveSetIn(Constraint* ct, std::string* log);
RuleStatus PresolveSetInReif(Constraint* ct, std::string* log);
RuleStatus PresolveArrayBoolAnd(Constraint* ct, std::string* log);
RuleStatus PresolveArrayBoolOr(Constraint* ct, std::string* log);
RuleStatus PresolveBoolEqNeReif(Constraint* ct, std::string* log);
RuleStatus PresolveArrayIntElement(Constraint* ct, std::string* log);
RuleStatus PresolveIntDiv(Constraint* ct, std::string* log);
RuleStatus PresolveIntTimes(Constraint* ct, std::string* log);
RuleStatus PresolveIntLinGt(Constraint* ct, std::string* log);
RuleStatus PresolveIntLinLt(Constraint* ct, std::string* log);
RuleStatus PresolveLinear(Constraint* ct, std::string* log);
RuleStatus RegroupLinear(Constraint* ct, std::string* log);
RuleStatus SimplifyLinear(Constraint* ct, std::string* log);
RuleStatus PropagatePositiveLinear(Constraint* ct, std::string* log);
RuleStatus PresolveStoreMapping(Constraint* ct, std::string* log);
RuleStatus PresolveSimplifyElement(Constraint* ct, std::string* log);
RuleStatus PresolveSimplifyExprElement(Constraint* ct, std::string* log);
RuleStatus PropagateReifiedComparisons(Constraint* ct, std::string* log);
RuleStatus StoreAbs(Constraint* ct, std::string* log);
RuleStatus RemoveAbsFromIntLeReif(Constraint* ct, std::string* log);
RuleStatus RemoveAbsFromIntEqNeReif(Constraint* ct, std::string* log);
RuleStatus SimplifyUnaryLinear(Constraint* ct, std::string* log);
RuleStatus SimplifyBinaryLinear(Constraint* ct, std::string* log);
RuleStatus CheckIntLinReifBounds(Constraint* ct, std::string* log);
RuleStatus CreateLinearTarget(Constraint* ct, std::string* log);
RuleStatus PresolveBoolNot(Constraint* ct, std::string* log);
RuleStatus PresolveBoolXor(Constraint* ct, std::string* log);
RuleStatus SimplifyIntLinEqReif(Constraint* ct, std::string* log);
RuleStatus PresolveIntMod(Constraint* ct, std::string* log);
RuleStatus PresolveBoolClause(Constraint* ct, std::string* log);
RuleStatus StoreIntEqReif(Constraint* ct, std::string* log);
RuleStatus SimplifyIntNeReif(Constraint* ct, std::string* log);
RuleStatus PresolveTableInt(Constraint* ct, std::string* log);
RuleStatus PresolveRegular(Constraint* ct, std::string* log);
RuleStatus PresolveDiffN(Constraint* ct, std::string* log);
// Helpers.
void IntersectDomainWith(const Argument& arg, Domain* domain);
bool IntersectVarWithArg(IntegerVariable* var, const Argument& arg);
bool IntersectVarWithSingleton(IntegerVariable* var, int64 value);
bool IntersectVarWithInterval(IntegerVariable* var, int64 imin, int64 imax);
bool RemoveValue(IntegerVariable* var, int64 value);
void AddConstraintToMapping(Constraint* ct);
void RemoveConstraintFromMapping(Constraint* ct);
// Mark changed variables.
void MarkChangedVariable(IntegerVariable* var);
// This method wraps each rule, calls it and log its effect.
bool ApplyRule(Constraint* ct, const std::string& rule_name,
const std::function<bool(Constraint* ct, std::string*)>& rule);
void ApplyRule(
Constraint* ct, const std::string& rule_name,
const std::function<RuleStatus(Constraint* ct, std::string*)>& rule);
// The presolver will discover some equivalence classes of variables [two
// variable are equivalent when replacing one by the other leads to the same
@@ -211,6 +230,10 @@ class Presolver {
// Count applications of presolve rules. Use a sorted map for reporting
// purposes.
std::map<std::string, int> successful_rules_;
// Store changed objects.
std::unordered_set<IntegerVariable*> changed_variables_;
std::unordered_set<Constraint*> changed_constraints_;
};
} // namespace fz
} // namespace operations_research