[CP-SAT] fix experimental linear code; indent; do not create lb_tree_search when model does not contain objective; fix slow termination

ortools/sat/cp_model.proto

@@ -22,7 +22,6 @@ option java_package = "com.google.ortools.sat";
 option java_multiple_files = true;
 option java_outer_classname = "CpModelProtobuf";
 
-
 // An integer variable.
 //
 // It will be referred to by an int32 corresponding to its index in a

ortools/sat/cp_model_search.cc

@@ -661,6 +661,7 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
       }
       if (name == "less_encoding") continue;
     } else {
+      if (params.optimize_with_lb_tree_search()) continue;
       if (params.optimize_with_core()) continue;
       if (params.search_branching() == SatParameters::LP_SEARCH) continue;
       if (params.search_branching() == SatParameters::PSEUDO_COST_SEARCH) {

ortools/sat/cp_model_solver.cc

@@ -179,6 +179,7 @@ std::string CpModelStats(const CpModelProto& model_proto) {
   absl::btree_map<std::string, int> name_to_num_literals;
   absl::btree_map<std::string, int> name_to_num_terms;
   absl::btree_map<std::string, int> name_to_num_complex_domain;
+  absl::btree_map<std::string, int> name_to_num_expressions;
 
   int no_overlap_2d_num_rectangles = 0;
   int no_overlap_2d_num_optional_rectangles = 0;
@@ -249,6 +250,9 @@ std::string CpModelStats(const CpModelProto& model_proto) {
     } else if (ct.constraint_case() ==
                ConstraintProto::ConstraintCase::kExactlyOne) {
       name_to_num_literals[name] += ct.exactly_one().literals().size();
+    } else if (ct.constraint_case() ==
+               ConstraintProto::ConstraintCase::kLinMax) {
+      name_to_num_expressions[name] += ct.lin_max().exprs().size();
     } else if (ct.constraint_case() ==
                ConstraintProto::ConstraintCase::kNoOverlap2D) {
       const int num_boxes = ct.no_overlap_2d().x_intervals_size();
@@ -444,6 +448,10 @@ std::string CpModelStats(const CpModelProto& model_proto) {
       absl::StrAppend(&constraints.back(),
                       " (#terms: ", name_to_num_terms[name], ")");
     }
+    if (name_to_num_expressions.contains(name)) {
+      absl::StrAppend(&constraints.back(),
+                      " (#expressions: ", name_to_num_expressions[name], ")");
+    }
     if (name_to_num_complex_domain.contains(name)) {
       absl::StrAppend(&constraints.back(),
                       " (#complex_domain: ", name_to_num_complex_domain[name],

ortools/sat/integer_expr.h

@@ -471,8 +471,8 @@ inline std::function<void(Model*)> WeightedSumLowerOrEqual(
             {}, local_vars, local_coeffs, IntegerValue(upper_bound), model);
         constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
         model->TakeOwnership(constraint);
-        return;
       }
+      return;
     }
 
     if (params.new_linear_propagation()) {

ortools/sat/linear_propagation.cc

@@ -62,6 +62,7 @@ bool EnforcementPropagator::Propagate(Trail* /*trail*/) {
     }
     watch_list.resize(new_size);
   }
+  rev_num_enforced_ = static_cast<int>(enforced_.size());
   return true;
 }
 
@@ -126,7 +127,17 @@ void EnforcementPropagator::CallWhenEnforced(EnforcementId id,
 
 // Returns true iff the constraint with given id is currently enforced.
 bool EnforcementPropagator::IsEnforced(EnforcementId id) const {
-  return is_enforced_[id];
+  if (propagation_trail_index_ == trail_.Index()) return is_enforced_[id];
+
+  // TODO(user): In some corner case, when LinearPropagator pushes a literal
+  // we don't repropagate this right away. Maybe we should just simplify this
+  // class and just pay the O(num_enforcement_literal) cost.
+  //
+  // For now we pay the cost to catch bugs.
+  for (const Literal l : GetSpan(id)) {
+    if (!assignment_.LiteralIsTrue(l)) return false;
+  }
+  return true;
 }
 
 // Add the enforcement reason to the given vector.

ortools/sat/linear_relaxation.cc

@@ -991,36 +991,42 @@ void AppendLinMaxRelaxationPart2(
 
   // For the relaxation, we use different constraints with a stronger linear
   // relaxation as explained in the .h
-  //
-  // TODO(user): Consider passing the x_vars to this method instead of
-  // computing it here.
-  std::vector<IntegerVariable> x_vars;
-  for (int i = 0; i < num_exprs; ++i) {
-    x_vars.insert(x_vars.end(), exprs[i].vars.begin(), exprs[i].vars.end());
-  }
-  gtl::STLSortAndRemoveDuplicates(&x_vars);
-
-  // All expressions should only contain positive variables.
-  DCHECK(std::all_of(x_vars.begin(), x_vars.end(), [](IntegerVariable var) {
-    return VariableIsPositive(var);
-  }));
-
   std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
       num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
 
-  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
+  // Cache coefficients.
+  absl::flat_hash_map<std::pair<int, IntegerVariable>, IntegerValue> cache;
   for (int i = 0; i < num_exprs; ++i) {
-    for (int j = 0; j < num_exprs; ++j) {
-      if (i == j) continue;
-      for (const IntegerVariable x_var : x_vars) {
+    for (int j = 0; j < exprs[i].vars.size(); ++j) {
+      cache[std::make_pair(i, exprs[i].vars[j])] = exprs[i].coeffs[j];
+    }
+  }
+  const auto get_coeff = [&cache](IntegerVariable var, int index) {
+    const auto it = cache.find(std::make_pair(index, var));
+    if (it == cache.end()) return IntegerValue(0);
+    return it->second;
+  };
+
+  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
+  std::vector<IntegerVariable> active_vars;
+  for (int i = 0; i + 1 < num_exprs; ++i) {
+    for (int j = i + 1; j < num_exprs; ++j) {
+      active_vars = exprs[i].vars;
+      active_vars.insert(active_vars.end(), exprs[j].vars.begin(),
+                         exprs[j].vars.end());
+      gtl::STLSortAndRemoveDuplicates(&active_vars);
+      for (const IntegerVariable x_var : active_vars) {
+        const IntegerValue diff = get_coeff(x_var, j) - get_coeff(x_var, i);
+        if (diff == 0) continue;
+
         const IntegerValue lb = integer_trail->LevelZeroLowerBound(x_var);
         const IntegerValue ub = integer_trail->LevelZeroUpperBound(x_var);
-        const IntegerValue diff =
-            GetCoefficient(x_var, exprs[j]) - GetCoefficient(x_var, exprs[i]);
         sum_of_max_corner_diff[i][j] += std::max(diff * lb, diff * ub);
+        sum_of_max_corner_diff[j][i] += std::max(-diff * lb, -diff * ub);
       }
     }
   }
+
   for (int i = 0; i < num_exprs; ++i) {
     LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
     lc.AddTerm(target, IntegerValue(1));
@@ -1153,7 +1159,7 @@ void TryToLinearizeConstraint(const CpModelProto& model_proto,
       if (linearization_level > 1) {
         if (is_affine_max) {
           AddMaxAffineCutGenerator(ct, model, relaxation);
-        } else {
+        } else if (ct.lin_max().exprs().size() < 100) {
           AddLinMaxCutGenerator(ct, model, relaxation);
         }
       }

ortools/sat/model.h

@@ -37,7 +37,7 @@ namespace sat {
  * Class that owns everything related to a particular optimization model.
  *
  * This class is actually a fully generic wrapper that can hold any type of
- * constraints, watchers, solvers and provide a mecanism to wire them together.
+ * constraints, watchers, solvers and provide a mechanism to wire them together.
  */
 class Model {
  public:

ortools/sat/sat_parameters.proto

@@ -20,7 +20,6 @@ option java_multiple_files = true;
 
 option csharp_namespace = "Google.OrTools.Sat";
 
-
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //