From 1d8059da3e358be5daf239caddaa7fdedb09bd19 Mon Sep 17 00:00:00 2001
From: Arthur Bit-Monnot <abitmonnot@laas.fr>
Date: Fri, 29 Nov 2024 23:32:46 +0100
Subject: [PATCH] perf(planning): Add a dynamic redundant constraint for
 strictly positive durations in the STN

---
 planning/planning/src/chronicles/constraints.rs | 16 ++++++++++++++--
 solver/src/model/lang/fixed.rs                  | 12 +++++++++++-
 solver/src/model/lang/linear.rs                 | 16 ++++++++++++++++
 3 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/planning/planning/src/chronicles/constraints.rs b/planning/planning/src/chronicles/constraints.rs
index 9be5b9e5..9125474b 100644
--- a/planning/planning/src/chronicles/constraints.rs
+++ b/planning/planning/src/chronicles/constraints.rs
@@ -281,22 +281,34 @@ pub fn encode_constraint<L: Label>(
             let start_linear = LinearSum::from(start);
             let end_linear = LinearSum::from(end);
 
-            match dur {
+            // impose the duration constraint and try to extract a lower bound on the duration as a single variable or constant
+            let lb = match dur {
                 Duration::Fixed(d) => {
                     let sum = build_sum(start_linear, end_linear, d);
                     model.bind(sum.clone().leq(LinearSum::zero()), value);
                     model.bind(sum.geq(LinearSum::zero()), value);
+                    FAtom::try_from(d)
                 }
                 Duration::Bounded { lb, ub } => {
                     let lb_sum = build_sum(start_linear.clone(), end_linear.clone(), lb);
                     let ub_sum = build_sum(start_linear, end_linear, ub);
                     model.bind(lb_sum.geq(LinearSum::zero()), value);
                     model.bind(ub_sum.leq(LinearSum::zero()), value);
+                    FAtom::try_from(lb)
                 }
             };
             // Redundant constraint to enforce the precedence between start and end.
             // This form ensures that the precedence in posted in the STN.
-            model.enforce(f_leq(start, end), [presence])
+            model.enforce(f_leq(start, end), [presence]);
+
+            // if we have the lower bound in a simple form, add a constraint that will post the STN edge corresponding to a strictly positive duration
+            // as soon as it is entailed by the lower bound
+            // THis enables eager detection of some negative cycles in the STN (as opposed to a ping pong between the STN and the linear CP propagator
+            // that would iteratibely increase bounds until we reach a potentially very big upper bound).
+            if let Ok(lb) = lb {
+                let strictly_postive_edge = model.reify(f_lt(start, end));
+                model.enforce(implies(lb.strictly_positive(), strictly_postive_edge), [presence]);
+            }
         }
         ConstraintType::Or => {
             let mut disjuncts = Vec::with_capacity(constraint.variables.len());
diff --git a/solver/src/model/lang/fixed.rs b/solver/src/model/lang/fixed.rs
index 55d6b9c8..be423117 100644
--- a/solver/src/model/lang/fixed.rs
+++ b/solver/src/model/lang/fixed.rs
@@ -1,4 +1,4 @@
-use crate::core::{IntCst, VarRef};
+use crate::core::{IntCst, Lit, VarRef};
 use crate::model::lang::{ConversionError, IAtom, IVar};
 use num_rational::Rational32;
 use std::cmp::Ordering;
@@ -80,6 +80,16 @@ impl FAtom {
         assert_ne!(denom, 0);
         FAtom { num, denom }
     }
+
+    /// Returns a literal that is true iff the FAtom is positive (>= 0)
+    pub fn positive(self) -> Lit {
+        self.num.ge_lit(0)
+    }
+
+    /// Returns a literal that is true iff the FAtom is strictly positive (> 0)
+    pub fn strictly_positive(self) -> Lit {
+        self.num.gt_lit(0)
+    }
 }
 
 impl PartialOrd for FAtom {
diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs
index 28e2adfd..64381a28 100644
--- a/solver/src/model/lang/linear.rs
+++ b/solver/src/model/lang/linear.rs
@@ -121,6 +121,22 @@ pub struct LinearSum {
     denom: IntCst,
 }
 
+impl<'a> TryFrom<&'a LinearSum> for FAtom {
+    type Error = ConversionError;
+
+    fn try_from(value: &'a LinearSum) -> Result<Self, Self::Error> {
+        let value = value.simplify(); // TODO: it would desirable to always have the constraint in its simplified (canonical) form
+        match *value.terms() {
+            [] => Ok(FAtom::new(value.constant.into(), value.denom)),
+            [term] if value.denom % term.factor == 0 => {
+                debug_assert_eq!(term.denom, value.denom);
+                Ok(FAtom::new(term.var + value.constant, value.denom / term.factor))
+            }
+            _ => Err(ConversionError::NotVariable),
+        }
+    }
+}
+
 impl std::fmt::Display for LinearSum {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         for (i, e) in self.terms.iter().enumerate() {