diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index c8dc7d3032..352857fe6b 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -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 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( diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index d0f4328e8f..a4d2dbd6d3 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -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(); diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 788e4be290..db8043d24f 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -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, int> insert_key = + const int var = PositiveRef(ref); + const int64 var_value = RefIsPositive(ref) ? value : -value; + const std::pair, 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 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 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 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 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 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 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 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(); diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 72bf911330..6165ab6c83 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -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& ConstraintToVars(int c) const { + DCHECK(ConstraintVariableGraphIsUpToDate()); return constraint_to_vars_[c]; } const absl::flat_hash_set& 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