[CP-SAT] more checks

google · Nov 5, 2024 · e85a139 · e85a139
1 parent 349952b
commit e85a139
Show file tree

Hide file tree

Showing 3 changed files with 110 additions and 2 deletions.
diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto
@@ -251,6 +251,13 @@ message RoutesConstraintProto {
 // the listed n-tuples in values. The n-tuples are encoded in a flattened way:
 //     [tuple0_v0, tuple0_v1, ..., tuple0_v{n-1}, tuple1_v0, ...].
 // Expressions must be affine (a * var + b).
+// Corner cases:
+//  - If all `vars`, `values` and `exprs` are empty, the constraint is trivially
+//    true, irrespective of the value of `negated`.
+//  - If `values` is empty but either vars or exprs is not, the constraint is
+//    trivially false if `negated` is false, and trivially true if `negated` is
+//    true.
+//  - If `vars` and `exprs` are empty but `values` is not, the model is invalid.
 message TableConstraintProto {
   repeated int32 vars = 1;  // Legacy field.
   repeated int64 values = 2;

diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
@@ -475,7 +475,8 @@ std::string ValidateElementConstraint(const CpModelProto& model,
   return "";
 }
 
-std::string ValidateTableConstraint(const ConstraintProto& ct) {
+std::string ValidateTableConstraint(const CpModelProto& model,
+                                    const ConstraintProto& ct) {
   const TableConstraintProto& arg = ct.table();
   if (!arg.vars().empty() && !arg.exprs().empty()) {
     return absl::StrCat(
@@ -487,13 +488,20 @@ std::string ValidateTableConstraint(const ConstraintProto& ct) {
         "Inconsistent table empty expressions and non-empty tuples: ",
         ProtobufShortDebugString(ct));
   }
+  if (arg.vars().empty() && arg.exprs().empty() && arg.values().empty()) {
+    return "";
+  }
   const int arity = arg.vars().empty() ? arg.exprs().size() : arg.vars().size();
   if (arg.values().size() % arity != 0) {
     return absl::StrCat(
         "The flat encoding of a table constraint tuples must be a multiple of "
         "the number of expressions: ",
         ProtobufDebugString(ct));
   }
+
+  for (const LinearExpressionProto& expr : arg.exprs()) {
+    RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
+  }
   return "";
 }
 
@@ -1051,7 +1059,7 @@ std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) {
         RETURN_IF_NOT_EMPTY(ValidateElementConstraint(model, ct));
         break;
       case ConstraintProto::ConstraintCase::kTable:
-        RETURN_IF_NOT_EMPTY(ValidateTableConstraint(ct));
+        RETURN_IF_NOT_EMPTY(ValidateTableConstraint(model, ct));
         support_enforcement = true;
         break;
       case ConstraintProto::ConstraintCase::kAutomaton:

diff --git a/ortools/sat/table_test.cc b/ortools/sat/table_test.cc
@@ -15,6 +15,7 @@
 
 #include <cstdint>
 #include <string>
+#include <string_view>
 #include <vector>
 
 #include "absl/container/btree_set.h"
@@ -39,6 +40,98 @@ namespace {
 
 using ::google::protobuf::contrib::parse_proto::ParseTestProto;
 
+CpSolverStatus SolveTextProto(std::string_view text_proto) {
+  const CpModelProto model_proto = ParseTestProto(text_proto);
+  Model model;
+  model.Add(NewSatParameters("enumerate_all_solutions:true"));
+  return SolveCpModel(model_proto, &model).status();
+}
+
+TEST(TableConstraintTest, EmptyOrTrivialSemantics) {
+  EXPECT_EQ(SolveTextProto(R"pb(
+              constraints {
+                table {
+                  values: []
+                  exprs: []
+                }
+              }
+            )pb"),
+            CpSolverStatus::OPTIMAL);
+
+  EXPECT_EQ(SolveTextProto(R"pb(
+              constraints {
+                table {
+                  values: []
+                  exprs: []
+                  negated: true
+                }
+              }
+            )pb"),
+            CpSolverStatus::OPTIMAL);
+
+  EXPECT_EQ(SolveTextProto(R"pb(
+              constraints {
+                table {
+                  values: [ 0 ]
+                  exprs: []
+                }
+              }
+            )pb"),
+            CpSolverStatus::MODEL_INVALID);
+
+  // Invalid linear expression: coeffs without vars
+  EXPECT_EQ(SolveTextProto(R"pb(
+              constraints {
+                table {
+                  values: []
+                  exprs:
+                  [ { coeffs: 1 }]
+                }
+              }
+            )pb"),
+            CpSolverStatus::MODEL_INVALID);
+
+  EXPECT_EQ(SolveTextProto(R"pb(
+              constraints {
+                table {
+                  values: []
+                  exprs:
+                  [ { offset: 1 }]
+                }
+              }
+            )pb"),
+            CpSolverStatus::INFEASIBLE);
+
+  EXPECT_EQ(SolveTextProto(R"pb(
+              constraints {
+                table {
+                  values: []
+                  exprs:
+                  [ { offset: 1 }]
+                  negated: true
+                }
+              }
+            )pb"),
+            CpSolverStatus::OPTIMAL);
+
+  // Invalid: not affine
+  EXPECT_EQ(SolveTextProto(R"pb(
+              variables { domain: [ 0, 0 ] }
+              variables { domain: [ 0, 0 ] }
+              constraints {
+                table {
+                  values: [ 0 ]
+                  exprs:
+                  [ {
+                    vars: [ 0, 1 ]
+                    coeffs: [ 1, 1 ]
+                  }]
+                }
+              }
+            )pb"),
+            CpSolverStatus::MODEL_INVALID);
+}
+
 TEST(TableConstraintTest, EnumerationAndEncoding) {
   const CpModelProto model_proto = ParseTestProto(R"pb(
     variables {