diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index d67f84b727..c0a16f8608 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -443,6 +443,11 @@ bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) { context_->tmp_literals.push_back(literal); } + if (!is_at_most_one && !transform_to_at_most_one && + context_->ExploitExactlyOneInObjective(context_->tmp_literals)) { + context_->UpdateRuleStats("exactly_one: simplified objective"); + } + if (transform_to_at_most_one) { CHECK(changed); ct->Clear(); @@ -2879,7 +2884,7 @@ bool CpModelPresolver::PresolveElement(ConstraintProto* ct) { if (unique_target && !context_->IsFixed(target_ref)) { context_->UpdateRuleStats("TODO element: target not used elsewhere"); } - if (unique_index) { + if (unique_index && !context_->IsFixed(index_ref)) { context_->UpdateRuleStats("TODO element: index not used elsewhere"); } @@ -5945,6 +5950,11 @@ void CpModelPresolver::PresolveToFixPoint() { } } + // This is needed to remove variable with a different representative from + // the objective. This allows to remove them completely in the loop below. + if (context_->ModelIsUnsat()) return; + if (!context_->CanonicalizeObjective()) return; + // We also make sure all affine relations are propagated and any not // yet canonicalized domain is. // @@ -5966,6 +5976,7 @@ void CpModelPresolver::PresolveToFixPoint() { // not enter an infinite loop, we call each (var, constraint) pair at most // once. const int num_vars = context_->working_model->variables_size(); + in_queue.resize(context_->working_model->constraints_size(), false); for (int v = 0; v < num_vars; ++v) { const auto& constraints = context_->VarToConstraints(v); if (constraints.size() != 1) continue; diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 2a9fb06a7c..f3e43c8891 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -133,6 +133,17 @@ struct VarValue { int64_t value; }; +namespace { + +bool ModelContainsNoOverlaps(const CpModelProto& cp_model_proto) { + for (const ConstraintProto& ct : cp_model_proto.constraints()) { + if (ct.constraint_case() == ConstraintProto::kNoOverlap) return true; + } + return false; +} + +} // namespace + const std::function ConstructSearchStrategyInternal( const std::vector& strategies, Model* model) { const auto& view = *model->GetOrCreate(); @@ -280,12 +291,28 @@ std::function ConstructSearchStrategy( const CpModelProto& cp_model_proto, const std::vector& variable_mapping, IntegerVariable objective_var, Model* model) { - // Default strategy is to instantiate the IntegerVariable in order. - std::function default_search_strategy = nullptr; - const bool instantiate_all_variables = - model->GetOrCreate()->instantiate_all_variables(); + std::vector> heuristics; - if (instantiate_all_variables) { + // We start by the user specified heuristic. + { + std::vector strategies; + for (const DecisionStrategyProto& proto : + cp_model_proto.search_strategy()) { + strategies.push_back(proto); + } + heuristics.push_back(ConstructSearchStrategyInternal(strategies, model)); + } + + // If there are some scheduling constraint, we complete with a custom + // "scheduling" strategy. + // + // TODO(user): also deal with cumulative. + if (ModelContainsNoOverlaps(cp_model_proto)) { + heuristics.push_back(SchedulingSearchHeuristic(model)); + } + + // If needed, we finish by instantiating anything left. + if (model->GetOrCreate()->instantiate_all_variables()) { std::vector decisions; for (const IntegerVariable var : variable_mapping) { if (var == kNoIntegerVariable) continue; @@ -297,20 +324,10 @@ std::function ConstructSearchStrategy( decisions.push_back(var); } } - default_search_strategy = - FirstUnassignedVarAtItsMinHeuristic(decisions, model); + heuristics.push_back(FirstUnassignedVarAtItsMinHeuristic(decisions, model)); } - std::vector strategies; - for (const DecisionStrategyProto& proto : cp_model_proto.search_strategy()) { - strategies.push_back(proto); - } - if (instantiate_all_variables) { - return SequentialSearch({ConstructSearchStrategyInternal(strategies, model), - default_search_strategy}); - } else { - return ConstructSearchStrategyInternal(strategies, model); - } + return SequentialSearch(heuristics); } std::function InstrumentSearchStrategy( diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 7ff3d035f9..8314ab692b 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -13,8 +13,10 @@ #include "ortools/sat/presolve_context.h" +#include #include #include +#include #include "ortools/base/map_util.h" #include "ortools/base/mathutil.h" @@ -1477,6 +1479,28 @@ bool PresolveContext::CanonicalizeObjective() { return true; } +void PresolveContext::RemoveVariableFromObjective(int var) { + objective_map_.erase(var); + var_to_constraints_[var].erase(kObjectiveConstraint); +} + +void PresolveContext::AddToObjective(int var, int64_t value) { + int64_t& map_ref = objective_map_[var]; + map_ref += value; + if (map_ref == 0) { + objective_map_.erase(var); + var_to_constraints_[var].erase(kObjectiveConstraint); + } else { + var_to_constraints_[var].insert(kObjectiveConstraint); + } +} + +void PresolveContext::AddToObjectiveOffset(int64_t value) { + // Tricky: The objective domain is without the offset, so we need to shift it. + objective_offset_ += static_cast(value); + objective_domain_ = objective_domain_.AdditionWith(Domain(-value)); +} + bool PresolveContext::SubstituteVariableInObjective( int var_in_equality, int64_t coeff_in_equality, const ConstraintProto& equality, std::vector* new_vars_in_objective) { @@ -1560,6 +1584,55 @@ bool PresolveContext::SubstituteVariableInObjective( return true; } +bool PresolveContext::ExploitExactlyOneInObjective( + absl::Span exactly_one) { + int64_t min_coeff = std::numeric_limits::max(); + for (const int ref : exactly_one) { + const auto it = objective_map_.find(PositiveRef(ref)); + if (it == objective_map_.end()) return false; + + const int64_t coeff = it->second; + if (RefIsPositive(ref)) { + min_coeff = std::min(min_coeff, coeff); + } else { + // Objective = coeff * var = coeff * (1 - ref); + min_coeff = std::min(min_coeff, -coeff); + } + } + + int64_t offset = min_coeff; + for (const int ref : exactly_one) { + const int var = PositiveRef(ref); + int64_t& map_ref = objective_map_.at(var); + if (RefIsPositive(ref)) { + map_ref -= min_coeff; + if (map_ref == 0) { + objective_map_.erase(var); + var_to_constraints_[var].erase(kObjectiveConstraint); + } + } else { + // Term = coeff * (1 - X) = coeff - coeff * X; + // So -coeff -> -coeff -min_coeff + // And Term = coeff + min_coeff - min_coeff - (coeff + min_coeff) * X + // = (coeff + min_coeff) * (1 - X) - min_coeff; + map_ref += min_coeff; + if (map_ref == 0) { + objective_map_.erase(var); + var_to_constraints_[var].erase(kObjectiveConstraint); + } + offset -= min_coeff; + } + } + + // Note that the domain never include the offset, so we need to update it. + if (offset != 0) { + objective_offset_ += offset; + objective_domain_ = objective_domain_.AdditionWith(Domain(-offset)); + } + + return true; +} + void PresolveContext::WriteObjectiveToProto() const { // We need to sort the entries to be deterministic. std::vector> entries; diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index d47b67909c..b9ceb4a52f 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -16,6 +16,7 @@ #include #include +#include #include #include "ortools/sat/cp_model.pb.h" @@ -314,6 +315,15 @@ class PresolveContext { ABSL_MUST_USE_RESULT bool CanonicalizeObjective(); void WriteObjectiveToProto() const; + // Checks if the given exactly_one is included in the objective, and simplify + // the objective by adding a constant value to all the exactly one terms. + bool ExploitExactlyOneInObjective(absl::Span exactly_one); + + // Allows to manipulate the objective coefficients. + void RemoveVariableFromObjective(int var); + void AddToObjective(int var, int64_t value); + void AddToObjectiveOffset(int64_t value); + // 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.