From d2657d29a0acff7ac318a607d0da8e694e3ced5c Mon Sep 17 00:00:00 2001
From: Laurent Perron <lperron@google.com>
Date: Mon, 21 Nov 2022 15:35:30 +0100
Subject: [PATCH] [CP-SAT] add lin_max presolve; fix bug in int_prod

---
 ortools/sat/cp_model_presolve.cc | 20 +++++++++++++++++++-
 ortools/sat/integer.cc           |  1 +
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index 09c99f0819..bc8edcf4d5 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -672,9 +672,27 @@ bool CpModelPresolver::PresolveLinMax(ConstraintProto* ct) {
   if (context_->ModelIsUnsat()) return false;
   if (HasEnforcementLiteral(*ct)) return false;
 
+  const LinearExpressionProto& target = ct->lin_max().target();
+
+  // x = max(x, xi...) => forall i, x >= xi.
+  for (const LinearExpressionProto& expr : ct->lin_max().exprs()) {
+    if (LinearExpressionProtosAreEqual(expr, target)) {
+      for (const LinearExpressionProto& e : ct->lin_max().exprs()) {
+        if (LinearExpressionProtosAreEqual(e, target)) continue;
+        LinearConstraintProto* prec =
+            context_->working_model->add_constraints()->mutable_linear();
+        prec->add_domain(0);
+        prec->add_domain(std::numeric_limits<int64_t>::max());
+        AddLinearExpressionToLinearConstraint(target, 1, prec);
+        AddLinearExpressionToLinearConstraint(e, -1, prec);
+      }
+      context_->UpdateRuleStats("lin_max: x = max(x, ...)");
+      return RemoveConstraint(ct);
+    }
+  }
+
   // Compute the infered min/max of the target.
   // Update target domain (if it is not a complex expression).
-  const LinearExpressionProto& target = ct->lin_max().target();
   {
     int64_t infered_min = context_->MinOf(target);
     int64_t infered_max = std::numeric_limits<int64_t>::min();
diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc
index a7cbd0ad4e..48cf1bc6a7 100644
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -1158,6 +1158,7 @@ bool IntegerTrail::ReasonIsValid(
       }
     }
     for (const IntegerLiteral i_lit : integer_reason) {
+      if (i_lit.IsAlwaysTrue()) continue;
       if (LevelZeroLowerBound(i_lit.var) < i_lit.bound) {
         num_literal_assigned_after_root_node++;
       }