improve presolve; fix #2661

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;

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<BooleanOrIntegerLiteral()> ConstructSearchStrategyInternal(
     const std::vector<DecisionStrategyProto>& strategies, Model* model) {
   const auto& view = *model->GetOrCreate<CpModelView>();
@@ -280,12 +291,28 @@ std::function<BooleanOrIntegerLiteral()> ConstructSearchStrategy(
     const CpModelProto& cp_model_proto,
     const std::vector<IntegerVariable>& variable_mapping,
     IntegerVariable objective_var, Model* model) {
-  // Default strategy is to instantiate the IntegerVariable in order.
-  std::function<BooleanOrIntegerLiteral()> default_search_strategy = nullptr;
-  const bool instantiate_all_variables =
-      model->GetOrCreate<SatParameters>()->instantiate_all_variables();
+  std::vector<std::function<BooleanOrIntegerLiteral()>> heuristics;
 
-  if (instantiate_all_variables) {
+  // We start by the user specified heuristic.
+  {
+    std::vector<DecisionStrategyProto> 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<SatParameters>()->instantiate_all_variables()) {
     std::vector<IntegerVariable> decisions;
     for (const IntegerVariable var : variable_mapping) {
       if (var == kNoIntegerVariable) continue;
@@ -297,20 +324,10 @@ std::function<BooleanOrIntegerLiteral()> ConstructSearchStrategy(
         decisions.push_back(var);
       }
     }
-    default_search_strategy =
-        FirstUnassignedVarAtItsMinHeuristic(decisions, model);
+    heuristics.push_back(FirstUnassignedVarAtItsMinHeuristic(decisions, model));
   }
 
-  std::vector<DecisionStrategyProto> 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<BooleanOrIntegerLiteral()> InstrumentSearchStrategy(

ortools/sat/presolve_context.cc

@@ -13,8 +13,10 @@
 
 #include "ortools/sat/presolve_context.h"
 
+#include <algorithm>
 #include <cstdint>
 #include <limits>
+#include <string>
 
 #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<double>(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<int>* new_vars_in_objective) {
@@ -1560,6 +1584,55 @@ bool PresolveContext::SubstituteVariableInObjective(
   return true;
 }
 
+bool PresolveContext::ExploitExactlyOneInObjective(
+    absl::Span<const int> exactly_one) {
+  int64_t min_coeff = std::numeric_limits<int64_t>::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<std::pair<int, int64_t>> entries;

ortools/sat/presolve_context.h

@@ -16,6 +16,7 @@
 
 #include <cstdint>
 #include <deque>
+#include <string>
 #include <vector>
 
 #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<const int> 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.