[CP-SAT] more presolve around int_abs

ortools/sat/cp_model_loader.cc

@@ -1401,64 +1401,88 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
                                                   coeffs, ub));
       }
     }
-  } else {
-    // In this case, we can create just one Boolean instead of two since one
-    // is the negation of the other.
-    const bool special_case =
-        ct.enforcement_literal().empty() && ct.linear().domain_size() == 4;
-
-    std::vector<Literal> clause;
-    for (int i = 0; i < ct.linear().domain_size(); i += 2) {
-      int64_t lb = ct.linear().domain(i);
-      int64_t ub = ct.linear().domain(i + 1);
-      if (min_sum >= lb) lb = std::numeric_limits<int64_t>::min();
-      if (max_sum <= ub) ub = std::numeric_limits<int64_t>::max();
-
-      const Literal subdomain_literal(
-          special_case && i > 0 ? clause.back().Negated()
-                                : Literal(m->Add(NewBooleanVariable()), true));
-      clause.push_back(subdomain_literal);
+    return;
+  }
 
-      if (lb != std::numeric_limits<int64_t>::min()) {
-        m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars,
-                                                    coeffs, lb));
-      }
-      if (ub != std::numeric_limits<int64_t>::max()) {
-        m->Add(ConditionalWeightedSumLowerOrEqual({subdomain_literal}, vars,
-                                                  coeffs, ub));
+  // We have a linear with a complex Domain, we need to create extra Booleans.
+
+  // In this case, we can create just one Boolean instead of two since one
+  // is the negation of the other.
+  const bool special_case =
+      ct.enforcement_literal().empty() && ct.linear().domain_size() == 4;
+
+  // For enforcement => var \in domain, we can potentially reuse the encoding
+  // literal directly rather than creating new ones.
+  const bool is_linear1 = !special_case && vars.size() == 1 && coeffs[0] == 1;
+
+  std::vector<Literal> clause;
+  std::vector<Literal> for_enumeration;
+  auto* encoding = m->GetOrCreate<IntegerEncoder>();
+  for (int i = 0; i < ct.linear().domain_size(); i += 2) {
+    const int64_t lb = ct.linear().domain(i);
+    const int64_t ub = ct.linear().domain(i + 1);
+
+    if (is_linear1) {
+      if (lb == ub) {
+        clause.push_back(
+            encoding->GetOrCreateLiteralAssociatedToEquality(vars[0], lb));
+        continue;
+      } else if (min_sum >= lb) {
+        clause.push_back(encoding->GetOrCreateAssociatedLiteral(
+            IntegerLiteral::LowerOrEqual(vars[0], ub)));
+        continue;
+      } else if (max_sum <= ub) {
+        clause.push_back(encoding->GetOrCreateAssociatedLiteral(
+            IntegerLiteral::GreaterOrEqual(vars[0], lb)));
+        continue;
       }
     }
 
-    const std::vector<Literal> enforcement_literals =
-        mapping->Literals(ct.enforcement_literal());
+    const Literal subdomain_literal(
+        special_case && i > 0 ? clause.back().Negated()
+                              : Literal(m->Add(NewBooleanVariable()), true));
+    clause.push_back(subdomain_literal);
+    for_enumeration.push_back(subdomain_literal);
 
-    // Make sure all booleans are tights when enumerating all solutions.
-    if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
-      Literal linear_is_enforced;
-      if (enforcement_literals.size() == 1) {
-        linear_is_enforced = enforcement_literals[0];
-      } else {
-        linear_is_enforced = Literal(m->Add(NewBooleanVariable()), true);
-        std::vector<Literal> maintain_linear_is_enforced;
-        for (const Literal e_lit : enforcement_literals) {
-          m->Add(Implication(e_lit.Negated(), linear_is_enforced.Negated()));
-          maintain_linear_is_enforced.push_back(e_lit.Negated());
-        }
-        maintain_linear_is_enforced.push_back(linear_is_enforced);
-        m->Add(ClauseConstraint(maintain_linear_is_enforced));
-      }
-      for (const Literal lit : clause) {
-        m->Add(Implication(linear_is_enforced.Negated(), lit.Negated()));
-        if (special_case) break;  // For the unique Boolean var to be false.
-      }
+    if (min_sum < lb) {
+      m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars,
+                                                  coeffs, lb));
+    }
+    if (max_sum > ub) {
+      m->Add(ConditionalWeightedSumLowerOrEqual({subdomain_literal}, vars,
+                                                coeffs, ub));
     }
+  }
 
-    if (!special_case) {
+  const std::vector<Literal> enforcement_literals =
+      mapping->Literals(ct.enforcement_literal());
+
+  // Make sure all booleans are tights when enumerating all solutions.
+  if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
+    Literal linear_is_enforced;
+    if (enforcement_literals.size() == 1) {
+      linear_is_enforced = enforcement_literals[0];
+    } else {
+      linear_is_enforced = Literal(m->Add(NewBooleanVariable()), true);
+      std::vector<Literal> maintain_linear_is_enforced;
       for (const Literal e_lit : enforcement_literals) {
-        clause.push_back(e_lit.Negated());
+        m->Add(Implication(e_lit.Negated(), linear_is_enforced.Negated()));
+        maintain_linear_is_enforced.push_back(e_lit.Negated());
       }
-      m->Add(ClauseConstraint(clause));
+      maintain_linear_is_enforced.push_back(linear_is_enforced);
+      m->Add(ClauseConstraint(maintain_linear_is_enforced));
+    }
+    for (const Literal lit : for_enumeration) {
+      m->Add(Implication(linear_is_enforced.Negated(), lit.Negated()));
+      if (special_case) break;  // For the unique Boolean var to be false.
+    }
+  }
+
+  if (!special_case) {
+    for (const Literal e_lit : enforcement_literals) {
+      clause.push_back(e_lit.Negated());
     }
+    m->Add(ClauseConstraint(clause));
   }
 }
 

ortools/sat/cp_model_postsolve.cc

@@ -208,20 +208,25 @@ int64_t EvaluateLinearExpression(const LinearExpressionProto& expr,
 
 }  // namespace
 
-// Compute the max of each expression, and assign it to the target expr (which
-// must be of the form +ref or -ref); We only support post-solving the case
-// where whatever the value of all expression, there will be a valid target.
+// Compute the max of each expression, and assign it to the target expr. We only
+// support post-solving the case where whatever the value of all expression,
+// there will be a valid target.
 void PostsolveLinMax(const ConstraintProto& ct, std::vector<Domain>* domains) {
   int64_t max_value = std::numeric_limits<int64_t>::min();
   for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
     // In most case all expression are fixed, except in the corner case where
     // one of the expression refer to the target itself !
     max_value = std::max(max_value, EvaluateLinearExpression(expr, *domains));
   }
-  const int target_ref = GetSingleRefFromExpression(ct.lin_max().target());
-  const int target_var = PositiveRef(target_ref);
-  (*domains)[target_var] =
-      Domain(RefIsPositive(target_ref) ? max_value : -max_value);
+
+  const LinearExpressionProto& target = ct.lin_max().target();
+  CHECK_EQ(target.vars().size(), 1);
+  CHECK(RefIsPositive(target.vars(0)));
+
+  max_value -= target.offset();
+  CHECK_EQ(max_value % target.coeffs(0), 0);
+  max_value /= target.coeffs(0);
+  (*domains)[target.vars(0)] = Domain(max_value);
 }
 
 // We only support 3 cases in the presolve currently.