[CP-SAT] change the element constraint proto to support affine expres…

…sions everywhere; more work on lp folding and support of symmetries in the LP and the linear subsystem

ortools/sat/BUILD.bazel

@@ -149,7 +149,9 @@ cc_library(
         ":sat_base",
         ":sat_parameters_cc_proto",
         ":sat_solver",
+        ":symmetry_util",
         ":util",
+        "//ortools/algorithms:sparse_permutation",
         "//ortools/base",
         "//ortools/base:status_macros",
         "//ortools/base:stl_util",
@@ -2133,6 +2135,7 @@ cc_library(
         ":integer_expr",
         ":linear_constraint",
         ":linear_constraint_manager",
+        ":linear_propagation",
         ":model",
         ":sat_base",
         ":sat_parameters_cc_proto",
@@ -2153,14 +2156,14 @@ cc_library(
         "//ortools/lp_data:lp_data_utils",
         "//ortools/lp_data:scattered_vector",
         "//ortools/lp_data:sparse",
-        "//ortools/lp_data:sparse_column",
         "//ortools/util:bitset",
         "//ortools/util:rev",
         "//ortools/util:saturated_arithmetic",
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
         "@com_google_absl//absl/algorithm:container",
         "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/log",
         "@com_google_absl//absl/log:check",
         "@com_google_absl//absl/numeric:int128",
         "@com_google_absl//absl/strings",

ortools/sat/cp_model.proto

@@ -105,9 +105,13 @@ message LinearConstraintProto {
 // The constraint target = vars[index].
 // This enforces that index takes one of the value in [0, vars_size()).
 message ElementConstraintProto {
-  int32 index = 1;
-  int32 target = 2;
-  repeated int32 vars = 3;
+  int32 index = 1;          // Legacy field.
+  int32 target = 2;         // Legacy field.
+  repeated int32 vars = 3;  // Legacy field.
+  // All expressions below must be affine function with at most one variable.
+  LinearExpressionProto linear_index = 4;
+  LinearExpressionProto linear_target = 5;
+  repeated LinearExpressionProto exprs = 6;
 }
 
 // This is not really a constraint. It is there so it can be referred by other

ortools/sat/cp_model_checker.cc

@@ -418,23 +418,60 @@ std::string ValidateElementConstraint(const CpModelProto& model,
                                       const ConstraintProto& ct) {
   const ElementConstraintProto& element = ct.element();
 
+  if ((element.has_linear_index() || element.has_linear_target() ||
+       !element.exprs().empty()) &&
+      (!element.vars().empty() || element.index() != 0 ||
+       element.target() != 0)) {
+    return absl::StrCat(
+        "Inconsistent element with both legacy and new format defined",
+        ProtobufShortDebugString(ct));
+  }
+
   // We need to be able to manipulate expression like "target - var" without
   // integer overflow.
-  LinearExpressionProto overflow_detection;
-  overflow_detection.add_vars(element.target());
-  overflow_detection.add_coeffs(1);
-  overflow_detection.add_vars(/*dummy*/ 0);
-  overflow_detection.add_coeffs(-1);
-  for (const int ref : element.vars()) {
-    overflow_detection.set_vars(1, ref);
-    if (PossibleIntegerOverflow(model, overflow_detection.vars(),
-                                overflow_detection.coeffs())) {
-      return absl::StrCat(
-          "Domain of the variables involved in element constraint may cause "
-          "overflow",
-          ProtobufShortDebugString(ct));
+  if (!element.vars().empty()) {
+    LinearExpressionProto overflow_detection;
+    overflow_detection.add_vars(element.target());
+    overflow_detection.add_coeffs(1);
+    overflow_detection.add_vars(/*dummy*/ 0);
+    overflow_detection.add_coeffs(-1);
+    for (const int ref : element.vars()) {
+      overflow_detection.set_vars(1, ref);
+      if (PossibleIntegerOverflow(model, overflow_detection.vars(),
+                                  overflow_detection.coeffs())) {
+        return absl::StrCat(
+            "Domain of the variables involved in element constraint may cause "
+            "overflow",
+            ProtobufShortDebugString(ct));
+      }
     }
   }
+
+  if (!element.exprs().empty() || element.has_linear_index() ||
+      element.has_linear_target()) {
+    RETURN_IF_NOT_EMPTY(
+        ValidateAffineExpression(model, element.linear_index()));
+    RETURN_IF_NOT_EMPTY(
+        ValidateAffineExpression(model, element.linear_target()));
+    for (const LinearExpressionProto& expr : element.exprs()) {
+      RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
+      LinearExpressionProto overflow_detection = ct.element().linear_target();
+      for (int i = 0; i < expr.vars_size(); ++i) {
+        overflow_detection.add_vars(expr.vars(i));
+        overflow_detection.add_coeffs(-expr.coeffs(i));
+      }
+      overflow_detection.set_offset(overflow_detection.offset() -
+                                    expr.offset());
+      if (PossibleIntegerOverflow(model, overflow_detection.vars(),
+                                  overflow_detection.coeffs(),
+                                  overflow_detection.offset())) {
+        return absl::StrCat(
+            "Domain of the variables involved in element constraint may cause "
+            "overflow");
+      }
+    }
+  }
+
   return "";
 }
 
@@ -1397,10 +1434,20 @@ class ConstraintChecker {
   }
 
   bool ElementConstraintIsFeasible(const ConstraintProto& ct) {
-    if (ct.element().vars().empty()) return false;
-    const int index = Value(ct.element().index());
-    if (index < 0 || index >= ct.element().vars_size()) return false;
-    return Value(ct.element().vars(index)) == Value(ct.element().target());
+    if (!ct.element().vars().empty()) {
+      const int index = Value(ct.element().index());
+      if (index < 0 || index >= ct.element().vars_size()) return false;
+      return Value(ct.element().vars(index)) == Value(ct.element().target());
+    }
+
+    if (!ct.element().exprs().empty()) {
+      const int index = LinearExpressionValue(ct.element().linear_index());
+      if (index < 0 || index >= ct.element().exprs_size()) return false;
+      return LinearExpressionValue(ct.element().exprs(index)) ==
+             LinearExpressionValue(ct.element().linear_target());
+    }
+
+    return false;
   }
 
   bool TableConstraintIsFeasible(const ConstraintProto& ct) {