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

fix crash in presolve

Browse Source
This commit is contained in:
Laurent Perron
2020-02-26 19:49:50 +01:00
parent c95ed78898
commit 4b7aa31302
4 changed files with 146 additions and 191 deletions
Download Patch File Download Diff File Expand all files Collapse all files

96
ortools/sat/cp_model_presolve.cc
View File

@@ -56,7 +56,7 @@ bool CpModelPresolver::RemoveConstraint(ConstraintProto* ct) {
return true;
}
void CpModelPresolver::SyncDomainAndRemoveEmptyConstraints() {
void CpModelPresolver::RemoveEmptyConstraints() {
// Remove all empty constraints. Note that we need to remap the interval
// references.
std::vector<int> interval_mapping(context_->working_model->constraints_size(),
@@ -84,11 +84,6 @@ void CpModelPresolver::SyncDomainAndRemoveEmptyConstraints() {
},
&ct_ref);
}
for (int i = 0; i < context_->working_model->variables_size(); ++i) {
FillDomainInProto(context_->DomainOf(i),
context_->working_model->mutable_variables(i));
}
}
bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) {
@@ -942,17 +937,6 @@ bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
return false;
}
// Special case. We must not touch the half implications.
// literal => var ==/!= constant
// because in case this is fully reified, var will be shifted back, and the
// constraint will become a no-op.
if (ct->enforcement_literal_size() == 1 && ct->linear().vars_size() == 1 &&
context_->GetAffineRelation(PositiveRef(ct->linear().vars(0)))
.representative == PositiveRef(ct->enforcement_literal(0))) {
VLOG(2) << "Skip half-reified linear: " << ct->DebugString();
return false;
}
// First regroup the terms on the same variables and sum the fixed ones.
//
// TODO(user): move terms in context to reuse its memory? Add a quick pass
@@ -1284,6 +1268,7 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) {
// TODO(user): if we have l1 <=> x == value && l2 => x == value, we
// could rewrite the second constraint into l2 => l1.
context_->UpdateNewConstraintsVariableUsage();
return false;
}
@@ -4161,7 +4146,7 @@ bool CpModelPresolver::ProcessSetPPC() {
return changed;
}
void CpModelPresolver::CanonicalizeAffineDomain(int var) {
void CpModelPresolver::TryToSimplifyDomain(int var) {
CHECK(RefIsPositive(var));
if (context_->ModelIsUnsat()) return;
if (context_->IsFixed(var)) return;
@@ -4169,6 +4154,7 @@ void CpModelPresolver::CanonicalizeAffineDomain(int var) {
const AffineRelation::Relation r = context_->GetAffineRelation(var);
if (r.representative != var) return;
if (context_->VariableIsOnlyUsedInEncoding(var)) {
// TODO(user): We can remove such variable and its constraints by:
// - Adding proper constraints on the enforcement literals. Simple case is
@@ -4178,38 +4164,15 @@ void CpModelPresolver::CanonicalizeAffineDomain(int var) {
context_->UpdateRuleStats("TODO variables: only used in encoding.");
}
// Only process discrete domain.
const Domain& domain = context_->DomainOf(var);
// Special case for non-Boolean domain of size 2. We will try to reuse the
// encoding literals if present.
// Special case for non-Boolean domain of size 2.
if (domain.Size() == 2 && (domain.Min() != 0 || domain.Max() != 1)) {
// Shifted and/or scaled Boolean variable.
const int64 var_min = context_->MinOf(var);
const int64 var_max = context_->MaxOf(var);
int literal;
if (!context_->HasVarValueEncoding(var, var_max, &literal)) {
literal = context_->NewBoolVar();
}
ConstraintProto* const ct = context_->working_model->add_constraints();
LinearConstraintProto* const lin = ct->mutable_linear();
lin->add_vars(var);
lin->add_coeffs(1);
lin->add_vars(PositiveRef(literal));
if (RefIsPositive(literal)) {
lin->add_coeffs(var_min - var_max);
lin->add_domain(var_min);
lin->add_domain(var_min);
context_->StoreAffineRelation(*ct, var, literal, var_max - var_min,
var_min);
} else {
lin->add_coeffs(var_max - var_min);
lin->add_domain(var_max);
lin->add_domain(var_max);
context_->StoreAffineRelation(*ct, var, NegatedRef(literal),
var_min - var_max, var_max);
}
const int new_var_index = context_->NewBoolVar();
context_->InsertVarValueEncoding(new_var_index, var, domain.Max());
context_->UpdateRuleStats("variables: canonicalize size two domain");
return;
}
@@ -4226,7 +4189,6 @@ void CpModelPresolver::CanonicalizeAffineDomain(int var) {
gcd = MathUtil::GCD64(gcd, shifted_value);
if (gcd == 1) break;
}
// TODO(user): Experiment with reduction if gcd == 1 && var_min != 0.
if (gcd == 1) return;
int new_var_index;
@@ -4263,9 +4225,10 @@ void CpModelPresolver::PresolveToFixPoint() {
{
const int num_vars = context_->working_model->variables_size();
for (int var = 0; var < num_vars; ++var) {
CanonicalizeAffineDomain(var);
TryToSimplifyDomain(var);
}
}
context_->UpdateNewConstraintsVariableUsage();
// Limit on number of operations.
const int64 max_num_operations =
@@ -4341,7 +4304,7 @@ void CpModelPresolver::PresolveToFixPoint() {
// Re-add to the queue the constraints that touch a variable that changed.
// Note that it is important to use indices in the loop below because
// CanonicalizeAffineDomain() might create new variables which will change
// TryToSimplifyDomain() might create new variables which will change
// the set of modified domains.
//
// TODO(user): Avoid reprocessing the constraints that changed the variables
@@ -4357,10 +4320,11 @@ void CpModelPresolver::PresolveToFixPoint() {
//
// Important: This code is a bit brittle, because it assumes
// PositionsSetAtLeastOnce() will not change behind our back. That
// should however be the case because CanonicalizeAffineDomain() will
// only mark as modified via AddAffineRelation a variable that is
// already present in the modified set.
CanonicalizeAffineDomain(v);
// should however be the case because TryToSimplifyDomain() will only
// mark as modified via AddAffineRelation a variable that is already
// present in the modified set.
TryToSimplifyDomain(v);
context_->UpdateNewConstraintsVariableUsage();
in_queue.resize(context_->working_model->constraints_size(), false);
}
for (const int c : context_->VarToConstraints(v)) {
@@ -4515,12 +4479,10 @@ void CpModelPresolver::RemoveUnusedEquivalentVariables() {
arg->add_coeffs(-r.coeff);
arg->add_domain(r.offset);
arg->add_domain(r.offset);
context_->UpdateNewConstraintsVariableUsage();
}
VLOG(1) << "num_affine_relations kept = " << num_affine_relations;
// Update the variable usage.
context_->UpdateNewConstraintsVariableUsage();
}
void LogInfoFromContext(const PresolveContext* context) {
@@ -4600,6 +4562,7 @@ bool CpModelPresolver::Presolve() {
// If presolve is false, just run expansion.
if (!options_.parameters.cp_model_presolve()) {
context_->UpdateNewConstraintsVariableUsage();
ExpandCpModel(options_, context_);
if (options_.log_info) LogInfoFromContext(context_);
return true;
@@ -4658,6 +4621,7 @@ bool CpModelPresolver::Presolve() {
// Call expansion.
ExpandCpModel(options_, context_);
DCHECK(context_->ConstraintVariableUsageIsConsistent());
// TODO(user): do that and the pure-SAT part below more than once.
if (options_.parameters.cp_model_probing_level() > 0) {
@@ -4741,13 +4705,6 @@ bool CpModelPresolver::Presolve() {
// Note: Removing unused equivalent variables should be done at the end.
RemoveUnusedEquivalentVariables();
// TODO(user): Past this point the context.constraint_to_vars[] graph is not
// consistent and shouldn't be used. We do use var_to_constraints.size()
// though.
if (options_.time_limit == nullptr || !options_.time_limit->LimitReached()) {
DCHECK(context_->ConstraintVariableUsageIsConsistent());
}
// Remove duplicate constraints.
//
// TODO(user): We might want to do that earlier so that our count of variable
@@ -4770,8 +4727,6 @@ bool CpModelPresolver::Presolve() {
}
}
SyncDomainAndRemoveEmptyConstraints();
// The strategy variable indices will be remapped in ApplyVariableMapping()
// but first we use the representative of the affine relations for the
// variables that are not present anymore.
@@ -4823,6 +4778,12 @@ bool CpModelPresolver::Presolve() {
}
}
// Sync the domains.
for (int i = 0; i < context_->working_model->variables_size(); ++i) {
FillDomainInProto(context_->DomainOf(i),
context_->working_model->mutable_variables(i));
}
// Set the variables of the mapping_model.
context_->mapping_model->mutable_variables()->CopyFrom(
context_->working_model->variables());
@@ -4838,8 +4799,13 @@ bool CpModelPresolver::Presolve() {
mapping[i] = postsolve_mapping_->size();
postsolve_mapping_->push_back(i);
}
DCHECK(context_->ConstraintVariableUsageIsConsistent());
ApplyVariableMapping(mapping, *context_);
// Compact all non-empty constraint at the beginning.
RemoveEmptyConstraints();
// Hack to display the number of deductions stored.
if (context_->deductions.NumDeductions() > 0) {
context_->UpdateRuleStats(absl::StrCat(

4
ortools/sat/cp_model_presolve.h
View File

@@ -75,7 +75,7 @@ class CpModelPresolver {
bool PresolveOneConstraint(int c);
// Public for testing only.
void SyncDomainAndRemoveEmptyConstraints();
void RemoveEmptyConstraints();
private:
void PresolveToFixPoint();
@@ -151,7 +151,7 @@ class CpModelPresolver {
void ExpandObjective();
void CanonicalizeAffineDomain(int var);
void TryToSimplifyDomain(int var);
void MergeNoOverlapConstraints();

204
ortools/sat/presolve_context.cc
View File

@@ -418,7 +418,6 @@ void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) {
arg->add_domain(1);
StoreAffineRelation(*ct, var_a, var_b, /*coeff=*/-1, /*offset=*/1);
}
UpdateNewConstraintsVariableUsage();
}
bool PresolveContext::StoreAbsRelation(int target_ref, int ref) {
@@ -488,48 +487,70 @@ void PresolveContext::InitializeNewDomains() {
var_to_lb_only_constraints.resize(domains.size());
}
bool PresolveContext::GetCanonicalVarValuePair(int ref, int64 value, int* var,
int64* var_value) {
*var = PositiveRef(ref);
*var_value = RefIsPositive(ref) ? value : -value;
// Check affine relation, go back to representative if possible.
const AffineRelation::Relation r = GetAffineRelation(*var);
if (r.representative != *var) {
const int64 rep_value = (*var_value - r.offset) / r.coeff;
if (rep_value * r.coeff + r.offset != *var_value) return false;
*var = r.representative;
*var_value = rep_value;
}
return domains[*var].Contains(*var_value);
}
void PresolveContext::InsertVarValueEncoding(int literal, int ref,
int64 value) {
// If the encoding already exists. Merge the previous and the new encoding
// literals.
int previous_literal;
if (HasVarValueEncoding(ref, value, &previous_literal)) {
StoreBooleanEqualityRelation(literal, previous_literal);
return;
}
int var;
int64 var_value;
CHECK(GetCanonicalVarValuePair(ref, value, &var, &var_value));
const std::pair<std::pair<int, int64>, int> insert_key =
const int var = PositiveRef(ref);
const int64 var_value = RefIsPositive(ref) ? value : -value;
const std::pair<std::pair<int, int64>, int> key =
std::make_pair(std::make_pair(var, var_value), literal);
const auto& insert_status = encoding.insert(insert_key);
CHECK(insert_status.second);
VLOG(2) << "Insert lit(" << literal << ") <=> var(" << var
<< ") == " << value;
const std::pair<int, int64> key{var, var_value};
eq_half_encoding[key].insert(literal);
AddImplyInDomain(literal, var, Domain(var_value));
neq_half_encoding[key].insert(NegatedRef(literal));
AddImplyInDomain(NegatedRef(literal), var, Domain(var_value).Complement());
const auto& insert = encoding.insert(key);
if (insert.second) {
if (DomainOf(var).Size() == 2) {
// Encode the other literal.
const int64 var_min = MinOf(var);
const int64 var_max = MaxOf(var);
const int64 other_value = value == var_min ? var_max : var_min;
const std::pair<int, int64> other_key{var, other_value};
auto other_it = encoding.find(other_key);
if (other_it != encoding.end()) {
// Other value in the domain was already encoded.
const int previous_other_literal = other_it->second;
if (previous_other_literal != NegatedRef(literal)) {
StoreBooleanEqualityRelation(literal,
NegatedRef(previous_other_literal));
}
} else {
encoding[other_key] = NegatedRef(literal);
// Add affine relation.
// TODO(user): In linear presolve, recover var-value encoding from
// linear constraints like the one created below. This would be
// useful in case the variable has an affine representative, and the
// below constraint is rewritten.
ConstraintProto* const ct = working_model->add_constraints();
LinearConstraintProto* const lin = ct->mutable_linear();
lin->add_vars(var);
lin->add_coeffs(1);
lin->add_vars(PositiveRef(literal));
if (RefIsPositive(literal) == (var_value == var_max)) {
lin->add_coeffs(var_min - var_max);
lin->add_domain(var_min);
lin->add_domain(var_min);
StoreAffineRelation(*ct, var, PositiveRef(literal), var_max - var_min,
var_min);
} else {
lin->add_coeffs(var_max - var_min);
lin->add_domain(var_max);
lin->add_domain(var_max);
StoreAffineRelation(*ct, var, PositiveRef(literal), var_min - var_max,
var_max);
}
}
} else {
VLOG(2) << "Insert lit(" << literal << ") <=> var(" << var
<< ") == " << value;
const std::pair<int, int64> key{var, var_value};
eq_half_encoding[key].insert(literal);
AddImplyInDomain(literal, var, Domain(var_value));
neq_half_encoding[key].insert(NegatedRef(literal));
AddImplyInDomain(NegatedRef(literal), var,
Domain(var_value).Complement());
}
} else {
const int previous_literal = insert.first->second;
if (literal != previous_literal) {
StoreBooleanEqualityRelation(literal, previous_literal);
}
}
}
bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var,
@@ -586,33 +607,8 @@ bool PresolveContext::StoreLiteralImpliesVarNEqValue(int literal, int var,
}
bool PresolveContext::HasVarValueEncoding(int ref, int64 value, int* literal) {
int var;
int64 var_value;
if (!GetCanonicalVarValuePair(ref, value, &var, &var_value)) {
if (literal != nullptr) {
*literal = GetOrCreateConstantVar(0);
}
return true;
}
const Domain& domain = domains[var];
if (domain.Size() == 1) {
if (literal != nullptr) {
*literal = GetOrCreateConstantVar(1);
}
return true;
}
// A Boolean variable is always fully encoded (with itself).
if (domain.Size() == 2 && domain.Min() == 0 && domain.Max() == 1) {
if (literal != nullptr) {
*literal = var_value == 1 ? GetLiteralRepresentative(var)
: GetLiteralRepresentative(NegatedRef(var));
}
return true;
}
// We know the variable is canonical w.r.t. the affine representation.
const int var = PositiveRef(ref);
const int64 var_value = RefIsPositive(ref) ? value : -value;
const std::pair<int, int64> key{var, var_value};
const auto& it = encoding.find(key);
if (it != encoding.end()) {
@@ -621,44 +617,20 @@ bool PresolveContext::HasVarValueEncoding(int ref, int64 value, int* literal) {
}
return true;
} else {
// Try to recover literal from the other one if the size of the domain is 2.
// At this point, the variable is not Boolean.
if (domains[var].Size() == 2) {
const int64 var_min = MinOf(var);
const int64 var_max = MaxOf(var);
// Checks if the other value is already encoded.
const int64 other_value = var_value == var_min ? var_max : var_min;
const std::pair<int, int64> other_key{var, other_value};
auto other_it = encoding.find(other_key);
if (other_it != encoding.end()) {
// Update the encoding map. The domain could have been reduced to size
// two after the creation of the first literal.
const int other_literal = GetLiteralRepresentative(other_it->second);
encoding[key] = NegatedRef(other_literal);
if (literal != nullptr) {
*literal = NegatedRef(other_literal);
}
return true;
}
}
return false;
}
}
int PresolveContext::GetOrCreateVarValueEncoding(int ref, int64 value) {
int var;
int64 var_value;
if (!GetCanonicalVarValuePair(ref, value, &var, &var_value)) {
// TODO(user,user): use affine relation here.
const int var = PositiveRef(ref);
const int64 var_value = RefIsPositive(ref) ? value : -value;
// Returns the false literal if the value is not in the domain.
if (!domains[var].Contains(var_value)) {
return GetOrCreateConstantVar(0);
}
const Domain& domain = domains[var];
// Special case for fixed domains.
if (domain.Size() == 1) {
return GetOrCreateConstantVar(1);
}
// Returns the associated literal if already present.
const std::pair<int, int64> key{var, var_value};
auto it = encoding.find(key);
@@ -666,16 +638,17 @@ int PresolveContext::GetOrCreateVarValueEncoding(int ref, int64 value) {
return GetLiteralRepresentative(it->second);
}
// Boolean variables.
if (domain.Size() == 2 && domain.Min() == 0 && domain.Max() == 1) {
return var_value == 1 ? GetLiteralRepresentative(var)
: GetLiteralRepresentative(NegatedRef(var));
// Special case for fixed domains.
if (domains[var].Size() == 1) {
const int true_literal = GetOrCreateConstantVar(1);
encoding[key] = true_literal;
return true_literal;
}
// Special case for non Boolean variables with a domains of size 2.
// Special case for domains of size 2.
const int64 var_min = MinOf(var);
const int64 var_max = MaxOf(var);
if (domains[var].Size() == 2) {
const int64 var_min = MinOf(var);
const int64 var_max = MaxOf(var);
// Checks if the other value is already encoded.
const int64 other_value = var_value == var_min ? var_max : var_min;
const std::pair<int, int64> other_key{var, other_value};
@@ -683,16 +656,23 @@ int PresolveContext::GetOrCreateVarValueEncoding(int ref, int64 value) {
if (other_it != encoding.end()) {
// Update the encoding map. The domain could have been reduced to size
// two after the creation of the first literal.
const int other_literal = GetLiteralRepresentative(other_it->second);
encoding[key] = NegatedRef(other_literal);
return NegatedRef(other_literal);
const int other_literal =
GetLiteralRepresentative(NegatedRef(other_it->second));
encoding[key] = other_literal;
return other_literal;
}
// Create the literal. We try to have literal == true <-> var == var_max.
const int literal = NewBoolVar();
InsertVarValueEncoding(literal, var, var_max);
const int representative = GetLiteralRepresentative(literal);
return var_value == var_max ? representative : NegatedRef(representative);
if (var_min == 0 && var_max == 1) {
const int representative = GetLiteralRepresentative(var);
encoding[{var, 1}] = representative;
encoding[{var, 0}] = NegatedRef(representative);
return value == 1 ? representative : NegatedRef(representative);
} else {
const int literal = NewBoolVar();
InsertVarValueEncoding(literal, var, var_max);
const int representative = GetLiteralRepresentative(literal);
return var_value == var_max ? representative : NegatedRef(representative);
}
}
const int literal = NewBoolVar();

33
ortools/sat/presolve_context.h
View File

@@ -139,6 +139,11 @@ class PresolveContext {
void StoreAffineRelation(const ConstraintProto& ct, int ref_x, int ref_y,
int64 coeff, int64 offset);
// Adds the fact that ref_a == ref_b.
//
// Important: This does not update the constraint<->variable graph, so
// ConstraintVariableGraphIsUpToDate() will be false until
// UpdateNewConstraintsVariableUsage() is called.
void StoreBooleanEqualityRelation(int ref_a, int ref_b);
// Stores the relation target_ref = abs(ref);
@@ -164,27 +169,26 @@ class PresolveContext {
// Clears the "rules" statistics.
void ClearStats();
// Gets the canonical represention of the (ref, value) pair.
// It makes sure var is positive, and is canonical w.r.t. the affine
// relations. It returns false if the value is not valid w.r.t. the domains of
// the variables.
ABSL_MUST_USE_RESULT bool GetCanonicalVarValuePair(int ref, int64 value,
int* var,
int64* var_value);
// Inserts the given literal to encode ref == value.
// If an encoding already exists, it adds the two implications between
// the previous encoding and the new encoding.
//
// Important: This does not update the constraint<->variable graph, so
// ConstraintVariableGraphIsUpToDate() will be false until
// UpdateNewConstraintsVariableUsage() is called.
void InsertVarValueEncoding(int literal, int ref, int64 value);
// Gets the associated literal if it is already created. Otherwise
// create it, add the corresponding constraints and returns it.
ABSL_MUST_USE_RESULT int GetOrCreateVarValueEncoding(int ref, int64 value);
//
// Important: This does not update the constraint<->variable graph, so
// ConstraintVariableGraphIsUpToDate() will be false until
// UpdateNewConstraintsVariableUsage() is called.
int GetOrCreateVarValueEncoding(int ref, int64 value);
// Returns true if a literal attached to ref == var exists.
// It assigns the corresponding to `literal` if non null.
ABSL_MUST_USE_RESULT bool HasVarValueEncoding(int ref, int64 value,
int* literal = nullptr);
bool HasVarValueEncoding(int ref, int64 value, int* literal = nullptr);
// Stores the fact that literal implies var == value.
// It returns true if that information is new.
@@ -269,12 +273,17 @@ class PresolveContext {
// contains -1 so that if the objective appear in only one constraint, the
// constraint cannot be simplified.
const std::vector<int>& ConstraintToVars(int c) const {
DCHECK(ConstraintVariableGraphIsUpToDate());
return constraint_to_vars_[c];
}
const absl::flat_hash_set<int>& VarToConstraints(int var) const {
DCHECK(ConstraintVariableGraphIsUpToDate());
return var_to_constraints_[var];
}
int IntervalUsage(int c) const { return interval_usage_[c]; }
int IntervalUsage(int c) const {
DCHECK(ConstraintVariableGraphIsUpToDate());
return interval_usage_[c];
}
// For each variables, list the constraints that just enforce a lower bound
// (resp. upper bound) on that variable. If all the constraints in which a