[CP-SAT] improve presolve; improve linear subsystem

ortools/sat/cp_model.cc

@@ -612,6 +612,28 @@ Constraint CpModelBuilder::AddMinEquality(IntVar target,
   return Constraint(proto);
 }
 
+void CpModelBuilder::LinearExprToProto(const LinearExpr& expr,
+                                       LinearExpressionProto* expr_proto) {
+  for (const IntVar var : expr.variables()) {
+    expr_proto->add_vars(GetOrCreateIntegerIndex(var.index_));
+  }
+  for (const int64 coeff : expr.coefficients()) {
+    expr_proto->add_coeffs(coeff);
+  }
+  expr_proto->set_offset(expr.constant());
+}
+
+Constraint CpModelBuilder::AddLinMinEquality(
+    const LinearExpr& target, absl::Span<const LinearExpr> exprs) {
+  ConstraintProto* const proto = cp_model_.add_constraints();
+  LinearExprToProto(target, proto->mutable_lin_min()->mutable_target());
+  for (const LinearExpr& expr : exprs) {
+    LinearExpressionProto* expr_proto = proto->mutable_lin_min()->add_exprs();
+    LinearExprToProto(expr, expr_proto);
+  }
+  return Constraint(proto);
+}
+
 Constraint CpModelBuilder::AddMaxEquality(IntVar target,
                                           absl::Span<const IntVar> vars) {
   ConstraintProto* const proto = cp_model_.add_constraints();
@@ -622,6 +644,17 @@ Constraint CpModelBuilder::AddMaxEquality(IntVar target,
   return Constraint(proto);
 }
 
+Constraint CpModelBuilder::AddLinMaxEquality(
+    const LinearExpr& target, absl::Span<const LinearExpr> exprs) {
+  ConstraintProto* const proto = cp_model_.add_constraints();
+  LinearExprToProto(target, proto->mutable_lin_max()->mutable_target());
+  for (const LinearExpr& expr : exprs) {
+    LinearExpressionProto* expr_proto = proto->mutable_lin_max()->add_exprs();
+    LinearExprToProto(expr, expr_proto);
+  }
+  return Constraint(proto);
+}
+
 Constraint CpModelBuilder::AddDivisionEquality(IntVar target, IntVar numerator,
                                                IntVar denominator) {
   ConstraintProto* const proto = cp_model_.add_constraints();

ortools/sat/cp_model.h

@@ -737,9 +737,17 @@ class CpModelBuilder {
   /// Adds target == min(vars).
   Constraint AddMinEquality(IntVar target, absl::Span<const IntVar> vars);
 
+  /// Adds target == min(exprs).
+  Constraint AddLinMinEquality(const LinearExpr& target,
+                               absl::Span<const LinearExpr> exprs);
+
   /// Adds target == max(vars).
   Constraint AddMaxEquality(IntVar target, absl::Span<const IntVar> vars);
 
+  /// Adds target == max(exprs).
+  Constraint AddLinMaxEquality(const LinearExpr& target,
+                               absl::Span<const LinearExpr> exprs);
+
   /// Adds target = num / denom (integer division rounded towards 0).
   Constraint AddDivisionEquality(IntVar target, IntVar numerator,
                                  IntVar denominator);
@@ -812,6 +820,10 @@ class CpModelBuilder {
   friend class CumulativeConstraint;
   friend class ReservoirConstraint;
 
+  // Fills the 'expr_proto' with the linear expression represented by 'expr'.
+  void LinearExprToProto(const LinearExpr& expr,
+                         LinearExpressionProto* expr_proto);
+
   // Returns a (cached) integer variable index with a constant value.
   int IndexFromConstant(int64 value);
 

ortools/sat/cp_model.proto

@@ -76,6 +76,17 @@ message IntegerArgumentProto {
   repeated int32 vars = 2;
 }
 
+message LinearExpressionProto {
+  repeated int32 vars = 1;
+  repeated int32 coeffs = 2;
+  int64 offset = 3;
+}
+
+message LinearArgumentProto {
+  LinearExpressionProto target = 1;
+  repeated LinearExpressionProto exprs = 2;
+}
+
 // All variables must take different values.
 message AllDifferentConstraintProto {
   repeated int32 vars = 1;
@@ -246,7 +257,7 @@ message AutomatonConstraintProto {
   repeated int32 vars = 7;
 }
 
-// Next id: 27
+// Next id: 29
 message ConstraintProto {
   // For debug/logging only. Can be empty.
   string name = 1;
@@ -297,12 +308,22 @@ message ConstraintProto {
 
     // The int_max constraint forces the target to equal the maximum of all
     // variables.
+    // TODO(user): Remove int_max in favor of lin_max.
     IntegerArgumentProto int_max = 9;
 
+    // The lin_max constraint forces the target to equal the maximum of all
+    // linear expressions.
+    LinearArgumentProto lin_max = 27;
+
     // The int_min constraint forces the target to equal the minimum of all
     // variables.
+    // TODO(user): Remove int_min in favor of lin_min.
     IntegerArgumentProto int_min = 10;
 
+    // The lin_max constraint forces the target to equal the minimum of all
+    // linear expressions.
+    LinearArgumentProto lin_min = 28;
+
     // The int_min constraint forces the target to equal the product of all
     // variables.
     IntegerArgumentProto int_prod = 11;

ortools/sat/cp_model_checker.cc

@@ -194,6 +194,19 @@ std::string ValidateLinearConstraint(const CpModelProto& model,
   return "";
 }
 
+std::string ValidateLinearExpression(const CpModelProto& model,
+                                     const LinearExpressionProto& expr) {
+  if (expr.coeffs_size() != expr.vars_size()) {
+    return absl::StrCat("coeffs_size() != vars_size() in linear expression: ",
+                        ProtobufShortDebugString(expr));
+  }
+  if (PossibleIntegerOverflow(model, expr)) {
+    return absl::StrCat("Possible overflow in linear expression: ",
+                        ProtobufShortDebugString(expr));
+  }
+  return "";
+}
+
 std::string ValidateCircuitConstraint(const CpModelProto& model,
                                       const ConstraintProto& ct) {
   const int size = ct.circuit().tails().size();
@@ -387,6 +400,29 @@ std::string ValidateCpModel(const CpModelProto& model) {
         }
         RETURN_IF_NOT_EMPTY(ValidateLinearConstraint(model, ct));
         break;
+      case ConstraintProto::ConstraintCase::kLinMax: {
+        const std::string target_error =
+            ValidateLinearExpression(model, ct.lin_min().target());
+        if (!target_error.empty()) return target_error;
+        for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
+          const std::string expr_error =
+              ValidateLinearExpression(model, ct.lin_max().exprs(i));
+          if (!expr_error.empty()) return expr_error;
+        }
+        break;
+      }
+      case ConstraintProto::ConstraintCase::kLinMin: {
+        const std::string target_error =
+            ValidateLinearExpression(model, ct.lin_min().target());
+        if (!target_error.empty()) return target_error;
+        for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
+          const std::string expr_error =
+              ValidateLinearExpression(model, ct.lin_min().exprs(i));
+          if (!expr_error.empty()) return expr_error;
+        }
+        break;
+      }
+
       case ConstraintProto::ConstraintCase::kInterval:
         support_enforcement = true;
         RETURN_IF_NOT_EMPTY(ValidateIntervalConstraint(model, ct));
@@ -524,6 +560,25 @@ class ConstraintChecker {
     return max == actual_max;
   }
 
+  int64 LinearExpressionValue(const LinearExpressionProto& expr) {
+    int64 sum = expr.offset();
+    const int num_variables = expr.vars_size();
+    for (int i = 0; i < num_variables; ++i) {
+      sum += Value(expr.vars(i)) * expr.coeffs(i);
+    }
+    return sum;
+  }
+
+  bool LinMaxConstraintIsFeasible(const ConstraintProto& ct) {
+    const int64 max = LinearExpressionValue(ct.lin_max().target());
+    int64 actual_max = kint64min;
+    for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
+      const int64 expr_value = LinearExpressionValue(ct.lin_max().exprs(i));
+      actual_max = std::max(actual_max, expr_value);
+    }
+    return max == actual_max;
+  }
+
   bool IntProdConstraintIsFeasible(const ConstraintProto& ct) {
     const int64 prod = Value(ct.int_prod().target());
     int64 actual_prod = 1;
@@ -552,6 +607,16 @@ class ConstraintChecker {
     return min == actual_min;
   }
 
+  bool LinMinConstraintIsFeasible(const ConstraintProto& ct) {
+    const int64 min = LinearExpressionValue(ct.lin_min().target());
+    int64 actual_min = kint64max;
+    for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
+      const int64 expr_value = LinearExpressionValue(ct.lin_min().exprs(i));
+      actual_min = std::min(actual_min, expr_value);
+    }
+    return min == actual_min;
+  }
+
   bool AllDiffConstraintIsFeasible(const ConstraintProto& ct) {
     absl::flat_hash_set<int64> values;
     for (const int v : ct.all_diff().vars()) {
@@ -949,9 +1014,15 @@ bool SolutionIsFeasible(const CpModelProto& model,
       case ConstraintProto::ConstraintCase::kIntMin:
         is_feasible = checker.IntMinConstraintIsFeasible(ct);
         break;
+      case ConstraintProto::ConstraintCase::kLinMin:
+        is_feasible = checker.LinMinConstraintIsFeasible(ct);
+        break;
       case ConstraintProto::ConstraintCase::kIntMax:
         is_feasible = checker.IntMaxConstraintIsFeasible(ct);
         break;
+      case ConstraintProto::ConstraintCase::kLinMax:
+        is_feasible = checker.LinMaxConstraintIsFeasible(ct);
+        break;
       case ConstraintProto::ConstraintCase::kAllDiff:
         is_feasible = checker.AllDiffConstraintIsFeasible(ct);
         break;

ortools/sat/cp_model_expand.cc

@@ -817,6 +817,33 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
   ct->Clear();
 }
 
+// Fills the target as negated ref.
+void NegatedLinearExpression(const LinearExpressionProto& ref,
+                             LinearExpressionProto* target) {
+  for (int i = 0; i < ref.vars_size(); ++i) {
+    target->add_vars(NegatedRef(ref.vars(i)));
+    target->add_coeffs(ref.coeffs(i));
+  }
+  target->set_offset(-ref.offset());
+}
+
+void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
+  ConstraintProto* const lin_min = context->working_model->add_constraints();
+  for (int i = 0; i < ct->enforcement_literal_size(); ++i) {
+    lin_min->add_enforcement_literal(ct->enforcement_literal(i));
+  }
+
+  // Target
+  NegatedLinearExpression(ct->lin_max().target(),
+                          lin_min->mutable_lin_min()->mutable_target());
+
+  for (int i = 0; i < ct->lin_max().exprs_size(); ++i) {
+    LinearExpressionProto* const expr = lin_min->mutable_lin_min()->add_exprs();
+    NegatedLinearExpression(ct->lin_max().exprs(i), expr);
+  }
+  ct->Clear();
+}
+
 }  // namespace
 
 void ExpandCpModel(PresolveOptions options, PresolveContext* context) {
@@ -838,6 +865,9 @@ void ExpandCpModel(PresolveOptions options, PresolveContext* context) {
       case ConstraintProto::ConstraintCase::kIntProd:
         ExpandIntProd(ct, context);
         break;
+      case ConstraintProto::ConstraintCase::kLinMax:
+        ExpandLinMax(ct, context);
+        break;
       case ConstraintProto::ConstraintCase::kElement:
         if (options.parameters.expand_element_constraints()) {
           ExpandElement(ct, context);

ortools/sat/cp_model_lns.cc

@@ -711,7 +711,9 @@ WeightedRandomRelaxationNeighborhoodGenerator::
       case ConstraintProto::kIntDiv:
       case ConstraintProto::kIntMod:
       case ConstraintProto::kIntMax:
+      case ConstraintProto::kLinMax:
       case ConstraintProto::kIntMin:
+      case ConstraintProto::kLinMin:
       case ConstraintProto::kNoOverlap:
       case ConstraintProto::kNoOverlap2D:
         constraint_weights_.push_back(2.0);

ortools/sat/cp_model_loader.cc

@@ -19,6 +19,7 @@
 #include <set>
 #include <string>
 #include <utility>
+#include <vector>
 
 #include "absl/container/flat_hash_map.h"
 #include "absl/container/flat_hash_set.h"
@@ -30,6 +31,7 @@
 #include "ortools/sat/all_different.h"
 #include "ortools/sat/circuit.h"
 #include "ortools/sat/cp_constraints.h"
+#include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/cumulative.h"
 #include "ortools/sat/diffn.h"
@@ -1249,6 +1251,29 @@ void LoadIntMinConstraint(const ConstraintProto& ct, Model* m) {
   m->Add(IsEqualToMinOf(min, vars));
 }
 
+LinearExpression GetExprFromProto(const LinearExpressionProto& expr_proto,
+                                  const CpModelMapping& mapping) {
+  LinearExpression expr;
+  expr.vars = mapping.Integers(expr_proto.vars());
+  for (int j = 0; j < expr_proto.coeffs_size(); ++j) {
+    expr.coeffs.push_back(IntegerValue(expr_proto.coeffs(j)));
+  }
+  expr.offset = IntegerValue(expr_proto.offset());
+  return CanonicalizeExpr(expr);
+}
+
+void LoadLinMinConstraint(const ConstraintProto& ct, Model* m) {
+  auto* mapping = m->GetOrCreate<CpModelMapping>();
+  const LinearExpression min =
+      GetExprFromProto(ct.lin_min().target(), *mapping);
+  std::vector<LinearExpression> exprs;
+  exprs.reserve(ct.lin_min().exprs_size());
+  for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
+    exprs.push_back(GetExprFromProto(ct.lin_min().exprs(i), *mapping));
+  }
+  m->Add(IsEqualToMinOf(min, exprs));
+}
+
 void LoadIntMaxConstraint(const ConstraintProto& ct, Model* m) {
   auto* mapping = m->GetOrCreate<CpModelMapping>();
   const IntegerVariable max = mapping->Integer(ct.int_max().target());
@@ -1738,6 +1763,9 @@ bool LoadConstraint(const ConstraintProto& ct, Model* m) {
     case ConstraintProto::ConstraintProto::kIntMin:
       LoadIntMinConstraint(ct, m);
       return true;
+    case ConstraintProto::ConstraintProto::kLinMin:
+      LoadLinMinConstraint(ct, m);
+      return true;
     case ConstraintProto::ConstraintProto::kIntMax:
       LoadIntMaxConstraint(ct, m);
       return true;

ortools/sat/cp_model_loader.h

@@ -227,6 +227,7 @@ void LoadAllDiffConstraint(const ConstraintProto& ct, Model* m);
 void LoadIntProdConstraint(const ConstraintProto& ct, Model* m);
 void LoadIntDivConstraint(const ConstraintProto& ct, Model* m);
 void LoadIntMinConstraint(const ConstraintProto& ct, Model* m);
+void LoadLinMinConstraint(const ConstraintProto& ct, Model* m);
 void LoadIntMaxConstraint(const ConstraintProto& ct, Model* m);
 void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m);
 void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m);

ortools/sat/cp_model_presolve.h

@@ -104,6 +104,7 @@ class CpModelPresolver {
   bool PresolveInterval(int c, ConstraintProto* ct);
   bool PresolveIntDiv(ConstraintProto* ct);
   bool PresolveIntProd(ConstraintProto* ct);
+  // TODO(user) : Add presolve rules for LinMin.
   bool PresolveIntMin(ConstraintProto* ct);
   bool PresolveIntMax(ConstraintProto* ct);
   bool PresolveBoolXor(ConstraintProto* ct);

ortools/sat/cp_model_solver.cc

@@ -1968,6 +1968,7 @@ class LnsSolver : public SubSolver {
       SatParameters local_params(parameters_);
       local_params.set_max_deterministic_time(data.deterministic_limit);
       local_params.set_stop_after_first_solution(false);
+      local_params.set_log_search_progress(false);
 
       if (FLAGS_cp_model_dump_lns) {
         const std::string name =