minor improvements in CP-SAT

ortools/sat/cp_model_loader.cc

@@ -711,7 +711,11 @@ void LoadIntDivConstraint(const ConstraintProto& ct, Model* m) {
       mapping->Integers(ct.int_div().vars());
   if (m->Get(IsFixed(vars[1]))) {
     const IntegerValue denom(m->Get(Value(vars[1])));
-    m->Add(FixedDivisionConstraint(vars[0], denom, div));
+    if (denom == 1) {
+      m->Add(Equality(vars[0], div));
+    } else {
+      m->Add(FixedDivisionConstraint(vars[0], denom, div));
+    }
   } else {
     m->Add(DivisionConstraint(vars[0], vars[1], div));
   }

ortools/sat/integer_expr.cc

@@ -538,7 +538,8 @@ bool FixedDivisionPropagator::Propagate() {
     }
   } else if (max_a / b_ > max_c) {
     const IntegerValue new_max_a =
-        max_c >= 0 ? max_c * b_ + b_ - 1 : max_c * b_;
+        max_c >= 0 ? max_c * b_ + b_ - 1
+                   : IntegerValue(CapProd(max_c.value(), b_.value()));
     CHECK_LT(new_max_a, max_a);
     if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(a_, new_max_a),
                                  {},
@@ -554,7 +555,9 @@ bool FixedDivisionPropagator::Propagate() {
       return false;
     }
   } else if (min_a / b_ < min_c) {
-    const IntegerValue new_min_a = min_c > 0 ? min_c * b_ : min_c * b_ - b_ + 1;
+    const IntegerValue new_min_a =
+        min_c > 0 ? IntegerValue(CapProd(min_c.value(), b_.value()))
+                  : min_c * b_ - b_ + 1;
     CHECK_GT(new_min_a, min_a);
     if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(a_, new_min_a),
                                  {},

ortools/sat/integer_expr.h

@@ -188,10 +188,7 @@ class DivisionPropagator : public PropagatorInterface {
 };
 
 // Propagates var_a / cst_b = var_c. Basic version, we don't extract any special
-// cases, and we only propagates the bounds.
-//
-// TODO(user): Deal with overflow.
-// TODO(user): Unit-test this like the ProductPropagator.
+// cases, and we only propagates the bounds. cst_b must be > 0.
 class FixedDivisionPropagator : public PropagatorInterface {
  public:
   FixedDivisionPropagator(IntegerVariable a, IntegerValue b, IntegerVariable c,

ortools/sat/integer_search.cc

@@ -173,6 +173,71 @@ std::function<LiteralIndex()> SequentialSearch(
   };
 }
 
+std::function<LiteralIndex()> SequentialValueSelection(
+    std::vector<std::function<LiteralIndex(IntegerVariable)>>
+        value_selection_heuristics,
+    std::function<LiteralIndex()> var_selection_heuristic, Model* model) {
+  auto* encoder = model->GetOrCreate<IntegerEncoder>();
+  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+  return [=]() {
+    // Get the current decision.
+    const LiteralIndex current_decision = var_selection_heuristic();
+    if (current_decision == kNoLiteralIndex) return kNoLiteralIndex;
+
+    // Decode the decision and get the variable.
+    for (const IntegerLiteral l :
+         encoder->GetAllIntegerLiterals(Literal(current_decision))) {
+      if (integer_trail->IsCurrentlyIgnored(l.var)) continue;
+
+      // Sequentially try the value selection heuristics.
+      for (const auto& value_heuristic : value_selection_heuristics) {
+        const LiteralIndex decision = value_heuristic(l.var);
+        if (decision != kNoLiteralIndex) {
+          return decision;
+        }
+      }
+    }
+
+    VLOG(2) << "Value selection: using default decision.";
+    return current_decision;
+  };
+}
+
+std::function<LiteralIndex()> IntegerValueSelectionHeuristic(
+    std::function<LiteralIndex()> var_selection_heuristic, Model* model) {
+  std::vector<std::function<LiteralIndex(IntegerVariable)>>
+      value_selection_heuristics;
+
+  // TODO(user): Experiment with value selection heuristics.
+
+  // LP based value.
+  const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
+  if (LinearizedPartIsLarge(model) &&
+      (parameters.exploit_integer_lp_solution() ||
+       parameters.exploit_all_lp_solution())) {
+    std::function<LiteralIndex(IntegerVariable)> lp_value =
+        [model](IntegerVariable var) {
+          if (LpSolutionIsExploitable(model)) {
+            return SplitAroundLpValue(PositiveVariable(var), model);
+          }
+          return kNoLiteralIndex;
+        };
+    value_selection_heuristics.push_back(lp_value);
+    VLOG(1) << "Using LP value selection heuristic";
+  }
+
+  // Solution based value.
+  std::function<LiteralIndex(IntegerVariable)> solution_value =
+      [model](IntegerVariable var) {
+        return SplitDomainUsingBestSolutionValue(var, model);
+      };
+  value_selection_heuristics.push_back(solution_value);
+  VLOG(1) << "Using best solution value selection heuristic";
+
+  return SequentialValueSelection(value_selection_heuristics,
+                                  var_selection_heuristic, model);
+}
+
 std::function<LiteralIndex()> SatSolverHeuristic(Model* model) {
   SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
   Trail* trail = model->GetOrCreate<Trail>();
@@ -201,13 +266,6 @@ std::function<LiteralIndex()> PseudoCost(Model* model) {
 
     if (chosen_var == kNoIntegerVariable) return kNoLiteralIndex;
 
-    // TODO(user): Experiment with value selection heuristics.
-    const LiteralIndex best_solution_decision =
-        SplitDomainUsingBestSolutionValue(chosen_var, model);
-    if (best_solution_decision != kNoLiteralIndex) {
-      return best_solution_decision;
-    }
-
     return GreaterOrEqualToMiddleValue(chosen_var, model);
   };
 }
@@ -274,30 +332,45 @@ std::function<LiteralIndex()> FollowHint(
   };
 }
 
-LiteralIndex ExploitLpSolution(const LiteralIndex decision, Model* model) {
-  auto* encoder = model->GetOrCreate<IntegerEncoder>();
-  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
-
+bool LpSolutionIsExploitable(Model* model) {
   auto* lp_constraints =
       model->GetOrCreate<LinearProgrammingConstraintCollection>();
   const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
 
-  if (decision == kNoLiteralIndex) {
-    return decision;
-  }
-
-  bool lp_solution_is_exploitable = true;
   // TODO(user,user): When we have more than one LP, their set of variable
   // is always disjoint. So we could still change the polarity if the next
   // variable we branch on is part of a LP that has a solution.
   for (LinearProgrammingConstraint* lp : *lp_constraints) {
     if (!lp->HasSolution() ||
         !(parameters.exploit_all_lp_solution() || lp->SolutionIsInteger())) {
-      lp_solution_is_exploitable = false;
-      break;
+      return false;
     }
   }
-  if (lp_solution_is_exploitable) {
+  return true;
+}
+
+bool LinearizedPartIsLarge(Model* model) {
+  auto* lp_constraints =
+      model->GetOrCreate<LinearProgrammingConstraintCollection>();
+
+  int num_lp_variables = 0;
+  for (LinearProgrammingConstraint* lp : *lp_constraints) {
+    num_lp_variables += lp->NumVariables();
+  }
+  const int num_integer_variables =
+      model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value() / 2;
+  return (num_integer_variables <= 2 * num_lp_variables);
+}
+
+LiteralIndex ExploitLpSolution(const LiteralIndex decision, Model* model) {
+  auto* encoder = model->GetOrCreate<IntegerEncoder>();
+  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+
+  if (decision == kNoLiteralIndex) {
+    return decision;
+  }
+
+  if (LpSolutionIsExploitable(model)) {
     for (const IntegerLiteral l :
          encoder->GetAllIntegerLiterals(Literal(decision))) {
       const IntegerVariable positive_var = PositiveVariable(l.var);
@@ -313,21 +386,10 @@ LiteralIndex ExploitLpSolution(const LiteralIndex decision, Model* model) {
 
 std::function<LiteralIndex()> ExploitLpSolution(
     std::function<LiteralIndex()> heuristic, Model* model) {
-  auto* lp_constraints =
-      model->GetOrCreate<LinearProgrammingConstraintCollection>();
-
   // Use the normal heuristic if the LP(s) do not seem to cover enough variables
   // to be relevant.
   // TODO(user): Instead, try and depending on the result call it again or not?
-  {
-    int num_lp_variables = 0;
-    for (LinearProgrammingConstraint* lp : *lp_constraints) {
-      num_lp_variables += lp->NumVariables();
-    }
-    const int num_integer_variables =
-        model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value() / 2;
-    if (num_integer_variables > 2 * num_lp_variables) return heuristic;
-  }
+  if (!LinearizedPartIsLarge(model)) return heuristic;
 
   return [=]() mutable {
     const LiteralIndex decision = heuristic();
@@ -435,10 +497,7 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(
     case SatParameters::PSEUDO_COST_SEARCH: {
       std::function<LiteralIndex()> search = SequentialSearch(
           {PseudoCost(model), SatSolverHeuristic(model), next_decision});
-      if (parameters.exploit_integer_lp_solution() ||
-          parameters.exploit_all_lp_solution()) {
-        search = ExploitLpSolution(search, model);
-      }
+      search = IntegerValueSelectionHeuristic(search, model);
       return SolveProblemWithPortfolioSearch(
           {search}, {SatSolverRestartPolicy(model)}, model);
     }

ortools/sat/integer_search.h

@@ -91,6 +91,28 @@ std::function<LiteralIndex()> FollowHint(
 std::function<LiteralIndex()> SequentialSearch(
     std::vector<std::function<LiteralIndex()>> heuristics);
 
+// Changes the value of the given decision by 'var_selection_heuristic'. We try
+// to see if the decision is "associated" with an IntegerVariable, and if it is
+// the case, we choose the new value by the first 'value_selection_heuristics'
+// that is applicable (return value != kNoLiteralIndex). If none of the
+// heuristics are applicable then the given decision by
+// 'var_selection_heuristic' is returned.
+std::function<LiteralIndex()> SequentialValueSelection(
+    std::vector<std::function<LiteralIndex(IntegerVariable)>>
+        value_selection_heuristics,
+    std::function<LiteralIndex()> var_selection_heuristic, Model* model);
+
+// Changes the value of the given decision by 'var_selection_heuristic'. The new
+// value is chosen in the following way:
+// 1) If the LP part is large and the LP solution is exploitable, change the
+//    value to LP solution value.
+// 2) Else if there is at least one solution found, change the value to the best
+//    solution value.
+// If none of the above heuristics are applicable then it uses the default value
+// given in the decision.
+std::function<LiteralIndex()> IntegerValueSelectionHeuristic(
+    std::function<LiteralIndex()> var_selection_heuristic, Model* model);
+
 // Returns the LiteralIndex advised by the underliying SAT solver.
 std::function<LiteralIndex()> SatSolverHeuristic(Model* model);
 
@@ -114,6 +136,14 @@ std::function<LiteralIndex()> ExploitLpSolution(
 // variable if LP solution is exploitable.
 LiteralIndex ExploitLpSolution(const LiteralIndex decision, Model* model);
 
+// Returns true if we currently have an available LP solution that is
+// "exploitable" according to the current parameters.
+bool LpSolutionIsExploitable(Model* model);
+
+// Returns true if the number of variables in the linearized part is at least
+// 0.5 times the total number of variables.
+bool LinearizedPartIsLarge(Model* model);
+
 // A restart policy that restarts every k failures.
 std::function<bool()> RestartEveryKFailures(int k, SatSolver* solver);