perf(stn): allow the addition of dynamic edges that redundantly captu…

…res a subset of linear constraints

solver/Cargo.toml

@@ -14,8 +14,6 @@ edition = "2021"
 cpu_cycles = []
 
 
-
-
 [dependencies]
 anyhow = { workspace = true }
 streaming-iterator = "0.1.5"
@@ -31,6 +29,7 @@ tracing = { workspace = true }
 lru = "0.12.3"
 rand = { workspace = true }
 num-rational = { workspace = true }
+hashbrown = "0.15"
 
 [dev-dependencies]
 rand = "0.8"

solver/src/reasoners/stn/theory.rs

@@ -181,6 +181,9 @@ pub struct StnTheory {
     /// Hence, the presence of an event index does NOT indicate that the edge is currently deactivated.
     last_disabling_timestamp: RefMap<PropagatorId, EventIndex>,
     pending_bound_changes: Vec<BoundChangeEvent>,
+    /// A set of edges whose upper bound is dynamic (i.e. depends on the variable)
+    /// The map is indexed on the variable from which the variable is computed.
+    dyn_edges: hashbrown::HashMap<SignedVar, Vec<DynamicEdge>>,
 }
 
 #[derive(Copy, Clone)]
@@ -252,6 +255,16 @@ struct BoundChangeEvent {
     is_from_bound_propagation: bool,
 }
 
+/// An edge `src -> tgt` whose label (defining the upper bound on `tgt - src`)
+/// is given by `ub_var * ub_factor`.
+#[derive(Clone)]
+struct DynamicEdge {
+    src: Timepoint,
+    tgt: Timepoint,
+    ub_var: SignedVar,
+    ub_factor: IntCst,
+}
+
 impl StnTheory {
     /// Creates a new STN. Initially, the STN contains a single timepoint
     /// representing the origin whose domain is `[0,0]`. The id of this timepoint can
@@ -270,6 +283,7 @@ impl StnTheory {
             explanation: vec![],
             last_disabling_timestamp: Default::default(),
             pending_bound_changes: Default::default(),
+            dyn_edges: Default::default(),
         }
     }
     pub fn num_nodes(&self) -> u32 {
@@ -359,6 +373,35 @@ impl StnTheory {
         }
     }
 
+    /// Add an edge with a dynamic upper bound, representing the fact that `tgt - src <= ub_factor * ub_var`
+    pub fn add_dynamic_edge(
+        &mut self,
+        src: impl Into<Timepoint>,
+        tgt: impl Into<Timepoint>,
+        ub_var: SignedVar,
+        ub_factor: IntCst,
+        domains: &Domains,
+    ) {
+        let src = src.into();
+        let tgt = tgt.into();
+        let edge_valid = domains.presence(ub_var);
+        debug_assert!(domains.implies(edge_valid, domains.presence(src)));
+        debug_assert!(domains.implies(edge_valid, domains.presence(tgt)));
+
+        let dyn_edge = DynamicEdge {
+            src,
+            tgt,
+            ub_var,
+            ub_factor,
+        };
+        let cur_var_ub = domains.ub(ub_var);
+        let cur_ub = cur_var_ub * ub_factor;
+        // add immediately an edge for our current bound
+        self.add_reified_edge(ub_var.leq(cur_var_ub), src, tgt, cur_ub, domains);
+        // record the dynamic edge so that future updates on the variable would trigger a new edge insertion
+        self.dyn_edges.entry(ub_var).or_default().push(dyn_edge);
+    }
+
     /// Creates and record a new propagator associated with the given [DirEdge], making sure
     /// to set up the watches to enable it when it becomes active and valid.
     fn record_propagator(&mut self, prop: Propagator, domains: &Domains) {
@@ -381,12 +424,7 @@ impl StnTheory {
                         require_theory_propagation: true,
                     });
                 } else {
-                    if domains.current_decision_level() != DecLvl::ROOT {
-                        // FIXME: when backtracking, we should remove this edge (or at least ensure that it is definitely deactivated)
-                        println!(
-                            "WARNING: adding a dynamically enabled edge beyond the root decision level is unsupported."
-                        )
-                    }
+                    // Not present nor necessarily absent yet, add watches
                     self.constraints.add_propagator_enabler(prop, enabler);
                 }
             }
@@ -519,6 +557,22 @@ impl StnTheory {
                         });
                     }
                 }
+
+                // go through all dynamic edges whose upper bound is given by this variable.
+                let num_dyn_edges = self.dyn_edges.get(&ev.affected_bound).map_or(0, |dyns| dyns.len());
+                for i in 0..num_dyn_edges {
+                    // for each such edge, add new edge to the STN. Note that the edge will be automatically removed
+                    // when backtracking
+                    // Note: we iterate on the index of the edges to please the borrow checker.
+                    let var_ub = ev.affected_bound;
+                    let dyn_edge = &mut self.dyn_edges.get_mut(&ev.affected_bound).unwrap()[i];
+                    debug_assert_eq!(var_ub, dyn_edge.ub_var);
+                    let src = dyn_edge.src;
+                    let tgt = dyn_edge.tgt;
+                    let cur_var_ub = ev.new_upper_bound;
+                    let cur_ub = cur_var_ub * dyn_edge.ub_factor;
+                    self.add_reified_edge(var_ub.leq(cur_var_ub), src, tgt, cur_ub, model);
+                }
                 if self.constraints.is_vertex(ev.affected_bound) {
                     // ignore events from bound propagation as they would be already propagated
                     self.pending_bound_changes.push(BoundChangeEvent {

solver/src/solver/solver_impl.rs

@@ -277,6 +277,41 @@ impl<Lbl: Label> Solver<Lbl> {
                     assert!(self.model.entails(value), "Unsupported reified linear constraints."); // FIXME: Support reified linear constraints
                     let scope = self.model.state.presence(value);
                     self.reasoners.cp.add_opt_linear_constraint(&lin, scope);
+
+                    // if the linear sum is on three variables, try adding a redundant dynamic variable to the STN
+                    if lin.upper_bound == 0 && lin.sum.len() == 3 {
+                        let doms = &mut self.model.state;
+                        // we may be eligible for encoding as a dynamic STN edge
+                        // for all possible ordering of items in the sum, check if it representable as a dynamic STN edge
+                        // and if so add it to the STN
+                        let permutations = [[0, 1, 2], [0, 2, 1], [1, 0, 2], [1, 2, 0], [2, 0, 1], [2, 1, 0]];
+                        for [xi, yi, di] in permutations {
+                            // we are interested in the form `y - x <= d`
+                            // get it from the sum `y + (-x) + (-d) <= 0)
+                            let x = -lin.sum[xi];
+                            let y = lin.sum[yi];
+                            let d = -lin.sum[di];
+                            if x.factor != 1 || y.factor != 1 {
+                                continue;
+                            }
+                            if !doms.implies(doms.presence(d.var), doms.presence(x.var))
+                                || !doms.implies(doms.presence(d.var), doms.presence(y.var))
+                            {
+                                continue;
+                            }
+                            // if we get there we are eligible, massage the constriant into the right format and post it
+                            let src = x.var;
+                            let tgt = y.var;
+                            let (ub_var, ub_factor) = if d.factor >= 0 {
+                                (SignedVar::plus(d.var), d.factor)
+                            } else {
+                                (SignedVar::minus(d.var), -d.factor)
+                            };
+                            // add a dynamic edge to the STN, specifying that `tgt -src <= ub_var * ub_factor`
+                            // Each time a new upper bound is inferred on `ub_var` a new edge will temporarily added.
+                            self.reasoners.diff.add_dynamic_edge(src, tgt, ub_var, ub_factor, doms)
+                        }
+                    }
                 }
                 Ok(())
             }