[FZ] support _opt disjunctive and cumulative constraints

google · Jul 6, 2023 · c82aa08 · c82aa08
1 parent cabf55e
commit c82aa08
Show file tree

Hide file tree

Showing 5 changed files with 137 additions and 17 deletions.
diff --git a/ortools/flatzinc/checker.cc b/ortools/flatzinc/checker.cc
@@ -338,23 +338,49 @@ bool CheckCumulative(const Constraint& ct,
   return true;
 }
 
-bool CheckDiffn(const Constraint& ct,
-                const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckCumulativeOpt(const Constraint& ct,
+                        const std::function<int64_t(Variable*)>& evaluator) {
+  // TODO: Improve complexity for large durations.
+  const int64_t capacity = Eval(ct.arguments[4], evaluator);
+  const int size = Size(ct.arguments[0]);
+  CHECK_EQ(size, Size(ct.arguments[1]));
+  CHECK_EQ(size, Size(ct.arguments[2]));
+  CHECK_EQ(size, Size(ct.arguments[3]));
+  absl::flat_hash_map<int64_t, int64_t> usage;
+  for (int i = 0; i < size; ++i) {
+    if (EvalAt(ct.arguments[0], i, evaluator) == 0) continue;
+    const int64_t start = EvalAt(ct.arguments[1], i, evaluator);
+    const int64_t duration = EvalAt(ct.arguments[2], i, evaluator);
+    const int64_t requirement = EvalAt(ct.arguments[3], i, evaluator);
+    for (int64_t t = start; t < start + duration; ++t) {
+      usage[t] += requirement;
+      if (usage[t] > capacity) {
+        return false;
+      }
+    }
+  }
   return true;
 }
 
-bool CheckDiffnK(const Constraint& ct,
-                 const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckDiffn(const Constraint& /*ct*/,
+                const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return true;
 }
 
-bool CheckDiffnNonStrict(const Constraint& ct,
-                         const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckDiffnK(const Constraint& /*ct*/,
+                 const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return true;
 }
 
-bool CheckDiffnNonStrictK(const Constraint& ct,
-                          const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckDiffnNonStrict(
+    const Constraint& /*ct*/,
+    const std::function<int64_t(Variable*)>& /*evaluator*/) {
+  return true;
+}
+
+bool CheckDiffnNonStrictK(
+    const Constraint& /*ct*/,
+    const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return true;
 }
 
@@ -382,7 +408,6 @@ bool CheckDisjunctiveStrict(
   // TODO(user): Improve complexity for large size.
   const int size = Size(ct.arguments[0]);
   CHECK_EQ(size, Size(ct.arguments[1]));
-  absl::flat_hash_map<int64_t, int64_t> usage;
   for (int i = 0; i + 1 < size; ++i) {
     const int64_t start_i = EvalAt(ct.arguments[0], i, evaluator);
     const int64_t duration_i = EvalAt(ct.arguments[1], i, evaluator);
@@ -398,8 +423,32 @@ bool CheckDisjunctiveStrict(
   return true;
 }
 
-bool CheckFalseConstraint(const Constraint& ct,
-                          const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckDisjunctiveStrictOpt(
+    const Constraint& ct, const std::function<int64_t(Variable*)>& evaluator) {
+  // TODO: Improve complexity for large size.
+  const int size = Size(ct.arguments[0]);
+  CHECK_EQ(size, Size(ct.arguments[1]));
+  CHECK_EQ(size, Size(ct.arguments[2]));
+  for (int i = 0; i + 1 < size; ++i) {
+    if (EvalAt(ct.arguments[0], i, evaluator) == 0) continue;
+    const int64_t start_i = EvalAt(ct.arguments[1], i, evaluator);
+    const int64_t duration_i = EvalAt(ct.arguments[2], i, evaluator);
+    for (int j = i + 1; j < size; ++j) {
+      if (EvalAt(ct.arguments[0], j, evaluator) == 0) continue;
+      const int64_t start_j = EvalAt(ct.arguments[1], j, evaluator);
+      const int64_t duration_j = EvalAt(ct.arguments[2], j, evaluator);
+      if (start_i + duration_i <= start_j || start_j + duration_j <= start_i) {
+        continue;
+      }
+      return false;
+    }
+  }
+  return true;
+}
+
+bool CheckFalseConstraint(
+    const Constraint& /*ct*/,
+    const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return false;
 }
 
@@ -992,13 +1041,13 @@ bool CheckNvalue(const Constraint& ct,
   return count == all_values.size();
 }
 
-bool CheckRegular(const Constraint& ct,
-                  const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckRegular(const Constraint& /*ct*/,
+                  const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return true;
 }
 
-bool CheckRegularNfa(const Constraint& ct,
-                     const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckRegularNfa(const Constraint& /*ct*/,
+                     const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return true;
 }
 
@@ -1095,8 +1144,8 @@ bool CheckSubCircuit(const Constraint& ct,
   return visited.size() == Size(ct.arguments[0]);
 }
 
-bool CheckTableInt(const Constraint& ct,
-                   const std::function<int64_t(Variable*)>& evaluator) {
+bool CheckTableInt(const Constraint& /*ct*/,
+                   const std::function<int64_t(Variable*)>& /*evaluator*/) {
   return true;
 }
 
@@ -1183,12 +1232,14 @@ CallMap CreateCallMap() {
   m["var_cumulative"] = CheckCumulative;
   m["variable_cumulative"] = CheckCumulative;
   m["fixed_cumulative"] = CheckCumulative;
+  m["ortools_cumulative_opt"] = CheckCumulativeOpt;
   m["fzn_diffn"] = CheckDiffn;
   m["diffn_k_with_sizes"] = CheckDiffnK;
   m["fzn_diffn_nonstrict"] = CheckDiffnNonStrict;
   m["diffn_nonstrict_k_with_sizes"] = CheckDiffnNonStrictK;
   m["fzn_disjunctive"] = CheckDisjunctive;
   m["fzn_disjunctive_strict"] = CheckDisjunctiveStrict;
+  m["ortools_disjunctive_strict_opt"] = CheckDisjunctiveStrictOpt;
   m["false_constraint"] = CheckFalseConstraint;
   m["global_cardinality"] = CheckGlobalCardinality;
   m["global_cardinality_closed"] = CheckGlobalCardinalityClosed;

diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc
@@ -903,6 +903,43 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
         }
       }
     }
+  } else if (fz_ct.type == "ortools_cumulative_opt") {
+    const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
+    const std::vector<int> starts = LookupVars(fz_ct.arguments[1]);
+    const std::vector<VarOrValue> durations =
+        LookupVarsOrValues(fz_ct.arguments[2]);
+    const std::vector<VarOrValue> demands =
+        LookupVarsOrValues(fz_ct.arguments[3]);
+
+    auto* arg = ct->mutable_cumulative();
+    if (fz_ct.arguments[3].HasOneValue()) {
+      arg->mutable_capacity()->set_offset(fz_ct.arguments[4].Value());
+    } else {
+      arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[4]));
+      arg->mutable_capacity()->add_coeffs(1);
+    }
+    for (int i = 0; i < starts.size(); ++i) {
+      arg->add_intervals(
+          GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
+      LinearExpressionProto* demand = arg->add_demands();
+      if (demands[i].var == kNoVar) {
+        demand->set_offset(demands[i].value);
+      } else {
+        demand->add_vars(demands[i].var);
+        demand->add_coeffs(1);
+      }
+    }
+  } else if (fz_ct.type == "ortools_disjunctive_strict_opt") {
+    const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
+    const std::vector<int> starts = LookupVars(fz_ct.arguments[1]);
+    const std::vector<VarOrValue> durations =
+        LookupVarsOrValues(fz_ct.arguments[2]);
+
+    auto* arg = ct->mutable_no_overlap();
+    for (int i = 0; i < starts.size(); ++i) {
+      arg->add_intervals(
+          GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
+    }
   } else if (fz_ct.type == "fzn_diffn" || fz_ct.type == "fzn_diffn_nonstrict") {
     const bool is_strict = fz_ct.type == "fzn_diffn";
     const std::vector<int> x = LookupVars(fz_ct.arguments[0]);

diff --git a/ortools/flatzinc/mznlib/fzn_cumulative_opt.mzn b/ortools/flatzinc/mznlib/fzn_cumulative_opt.mzn
@@ -0,0 +1,16 @@
+predicate ortools_cumulative_opt(array [int] of var bool: o,
+                                 array[int] of var int: s,
+                                 array[int] of var int: d,
+                                 array[int] of var int: r,
+                                 var int: b);
+
+predicate fzn_cumulative_opt(array[int] of var opt int: s,
+                             array[int] of var int: d,
+                             array[int] of var int: r,
+                             var int: b) = let {
+    array[int] of var bool: os = [occurs(si) | si in s];
+    array[int] of var int: ds = [if is_fixed(absent(si)) /\ fix(absent(si))
+                                 then 0
+                                 else deopt(si)
+                                 endif | si in s];
+} in ortools_cumulative_opt(os, ds, d, r, b);
diff --git a/ortools/flatzinc/mznlib/fzn_disjunctive_opt.mzn b/ortools/flatzinc/mznlib/fzn_disjunctive_opt.mzn
@@ -0,0 +1,4 @@
+predicate fzn_disjunctive_opt(array[int] of var opt int: s,
+                              array[int] of var int: d) =
+        forall(i in index_set(d))(d[i] >= 0)
+    /\  fzn_cumulative_opt(s, d, [1 | i in index_set(s)], 1);
diff --git a/ortools/flatzinc/mznlib/fzn_disjunctive_strict_opt.mzn b/ortools/flatzinc/mznlib/fzn_disjunctive_strict_opt.mzn
@@ -0,0 +1,12 @@
+predicate ortools_disjunctive_strict_opt(array [int] of var bool: o,
+                                         array[int] of var int: s,
+                                         array[int] of var int: d);
+
+predicate fzn_disjunctive_strict_opt(array[int] of var opt int: s,
+                                     array[int] of var int: d) = let {
+    array[int] of var bool: os = [occurs(si) | si in s];
+    array[int] of var int: ds = [if is_fixed(absent(si)) /\ fix(absent(si))
+                                 then 0
+                                 else deopt(si)
+                                 endif | si in s];
+} in ortools_disjunctive_strict_opt(os, ds, d);