feat(planning): numeric symmetry breaking

planning/planners/src/encode.rs

@@ -12,7 +12,7 @@ use aries::core::*;
 use aries::model::extensions::{AssignmentExt, Shaped};
 use aries::model::lang::linear::LinearSum;
 use aries::model::lang::mul::EqVarMulLit;
-use aries::model::lang::{expr::*, Atom, IVar, Kind, Type};
+use aries::model::lang::{expr::*, Atom, IVar, Type};
 use aries::model::lang::{FAtom, FVar, IAtom, Variable};
 use aries_planning::chronicles::constraints::encode_constraint;
 use aries_planning::chronicles::*;
@@ -486,16 +486,6 @@ pub struct EncodedProblem {
     pub encoding: Encoding,
 }
 
-/// Returns whether the effect is an assignment.
-fn is_assignment(eff: &Effect) -> bool {
-    matches!(eff.operation, EffectOp::Assign(_))
-}
-
-/// Returns whether the state variable is numeric.
-fn is_integer(sv: &StateVar) -> bool {
-    matches!(sv.fluent.return_type().into(), Kind::Int)
-}
-
 /// Returns whether two state variables are unifiable.
 fn unifiable_sv(model: &Model, sv1: &StateVar, sv2: &StateVar) -> bool {
     sv1.fluent == sv2.fluent && model.unifiable_seq(&sv1.args, &sv2.args)
@@ -664,7 +654,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
 
         for &(cond_id, prez_cond, cond) in &conds {
             // skip conditions on numeric state variables, they are supported by numeric support constraints
-            if is_integer(&cond.state_var) {
+            if is_numeric(&cond.state_var) {
                 continue;
             }
             if solver.model.entails(!prez_cond) {
@@ -736,7 +726,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
         let mut num_numeric_assignment_coherence_constraints = 0;
 
         for &(_, prez, ass) in &assigns {
-            if !is_integer(&ass.state_var) {
+            if !is_numeric(&ass.state_var) {
                 continue;
             }
             let Type::Int { lb, ub } = ass.state_var.fluent.return_type() else {
@@ -755,15 +745,16 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
         solver.propagate()?;
     }
 
-    let mut increase_coherence_conditions: Vec<(Lit, Condition)> = Vec::with_capacity(incs.len());
+    let mut increase_coherence_conditions: Vec<(CondID, Lit, Condition)> = Vec::with_capacity(incs.len());
     {
         // numeric increase coherence constraints
         let span = tracing::span!(tracing::Level::TRACE, "numeric increase coherence");
         let _span = span.enter();
         let mut num_numeric_increase_coherence_constraints = 0;
+        let mut next_cond_id = 10000; // TODO: use a proper ID
 
         for &(inc_id, prez, inc) in &incs {
-            assert!(is_integer(&inc.state_var));
+            assert!(is_numeric(&inc.state_var));
             assert!(
                 inc.transition_start + FAtom::EPSILON == inc.transition_end && inc.min_mutex_end.is_empty(),
                 "Only instantaneous increases are supported"
@@ -778,6 +769,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
             // Check that the state variable value is equals to the new variable `var`.
             // It will force the state variable to be in the bounds of the new variable after the increase.
             increase_coherence_conditions.push((
+                CondID::new(inc_id.instance_id, next_cond_id),
                 prez,
                 Condition {
                     start: inc.transition_end,
@@ -786,6 +778,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                     value: var.into(),
                 },
             ));
+            next_cond_id += 1;
             num_numeric_increase_coherence_constraints += 1;
         }
 
@@ -801,21 +794,22 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
 
         let numeric_conds: Vec<_> = conds
             .iter()
-            .filter(|(_, _, cond)| is_integer(&cond.state_var))
-            .map(|&(_, prez, cond)| (prez, cond.clone()))
+            .filter(|(_, _, cond)| is_numeric(&cond.state_var))
+            .map(|&(id, prez, cond)| (id, prez, cond.clone()))
             .chain(increase_coherence_conditions)
             .collect();
 
-        for (cond_prez, cond) in &numeric_conds {
+        for (cond_id, cond_prez, cond) in &numeric_conds {
             // skip conditions on non-numeric state variables, they have already been supported by support constraints
-            assert!(is_integer(&cond.state_var));
+            assert!(is_numeric(&cond.state_var));
             if solver.model.entails(!*cond_prez) {
                 continue;
             }
             let Atom::Int(cond_val) = cond.value else {
                 unreachable!()
             };
             let mut supported: Vec<Lit> = Vec::with_capacity(128);
+            let mut inc_support: HashMap<EffID, Vec<Lit>> = HashMap::new();
 
             for &(ass_id, ass_prez, ass) in &assigns {
                 if solver.model.entails(!ass_prez) {
@@ -851,11 +845,12 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                 if solver.model.entails(!supported_by) {
                     continue;
                 }
+                encoding.tag(supported_by, Tag::Support(*cond_id, ass_id));
 
                 // the expected condition value
                 let mut cond_val_sum = LinearSum::from(ass_val) - cond_val;
 
-                for &(_, inc_prez, inc) in &incs {
+                for &(inc_id, inc_prez, inc) in &incs {
                     if solver.model.entails(!inc_prez) {
                         continue;
                     }
@@ -895,6 +890,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                     if solver.model.entails(!active_inc) {
                         continue;
                     }
+                    inc_support.entry(inc_id).or_default().push(active_inc);
                     for term in inc_val.terms() {
                         // compute some static implication for better propagation
                         let p = solver.model.presence_literal(term.var().into());
@@ -922,6 +918,11 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                 num_numeric_support_constraints += 1;
             }
 
+            for (inc_id, inc_support) in inc_support {
+                let supported_by_inc = solver.reify(or(inc_support));
+                encoding.tag(supported_by_inc, Tag::Support(*cond_id, inc_id));
+            }
+
             solver.enforce(or(supported), [*cond_prez]);
         }
 

planning/planners/src/encode/symmetry.rs

@@ -4,7 +4,7 @@ use analysis::CausalSupport;
 use aries::core::Lit;
 use aries::model::extensions::AssignmentExt;
 use aries::model::lang::expr::{and, f_leq, implies, or};
-use aries_planning::chronicles::analysis::{Feature, Metadata};
+use aries_planning::chronicles::analysis::Metadata;
 use aries_planning::chronicles::{ChronicleOrigin, FiniteProblem};
 use env_param::EnvParam;
 use itertools::Itertools;
@@ -46,7 +46,7 @@ impl std::str::FromStr for SymmetryBreakingType {
 }
 
 fn supported_by_psp(meta: &Metadata) -> bool {
-    !meta.class.is_hierarchical() && !meta.features.contains(&Feature::Numeric)
+    !meta.class.is_hierarchical()
 }
 
 pub fn add_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encoding: &Encoding) {
@@ -139,7 +139,13 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         .sorted()
         .dedup()
         .collect_vec();
-    let mut causal_link: HashMap<(ChronicleId, CondID), Lit> = Default::default();
+
+    #[derive(Clone, Copy)]
+    struct Link {
+        active: Lit,
+        exclusive: bool,
+    }
+    let mut causal_link: HashMap<(ChronicleId, CondID), Link> = Default::default();
     let mut conds_by_templates: HashMap<TemplateID, HashSet<CondID>> = Default::default();
     for template in &templates {
         conds_by_templates.insert(*template, HashSet::new());
@@ -164,7 +170,13 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         // non-optional literal that is true iff the causal link is active
         let link_active = model.reify(and([v, model.presence_literal(v.variable())]));
         // list of outgoing causal links of the supporting action
-        causal_link.insert((eff.instance_id, cond), link_active);
+        causal_link.insert(
+            (eff.instance_id, cond),
+            Link {
+                active: link_active,
+                exclusive: eff.is_assign,
+            },
+        );
     }
 
     let sort = |conds: HashSet<CondID>| {
@@ -185,7 +197,12 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
     };
     let conds_by_templates: HashMap<TemplateID, Vec<CondID>> =
         conds_by_templates.into_iter().map(|(k, v)| (k, sort(v))).collect();
-    let supports = |ch: ChronicleId, cond: CondID| causal_link.get(&(ch, cond)).copied().unwrap_or(Lit::FALSE);
+    let supports = |ch: ChronicleId, cond: CondID| {
+        causal_link.get(&(ch, cond)).copied().unwrap_or(Link {
+            active: Lit::FALSE,
+            exclusive: true,
+        })
+    };
 
     for template_id in &templates {
         let conditions = &conds_by_templates[template_id];
@@ -206,32 +223,36 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         //     }
         // }
 
-        for (i, instance) in instances.iter().copied().enumerate() {
-            let mut clause = Vec::with_capacity(64);
+        for (i, crt_instance) in instances.iter().copied().enumerate() {
+            let mut clause = Vec::with_capacity(conditions.len());
             if i > 0 {
-                let prev = instances[i - 1];
+                let prv_instance = instances[i - 1];
 
-                // the chronicle is allowed to support a condition only if the previous chronicle
-                // supports a condition at an earlier level
-                for (cond_index, cond) in conditions.iter().enumerate() {
+                // The current instance is allowed to support a condition only if the previous instance
+                // supports a condition at an earlier level or at the same level.
+                for (j, crt_cond) in conditions.iter().enumerate() {
                     clause.clear();
-                    clause.push(!supports(*instance, *cond));
 
-                    for prev_cond in &conditions[0..cond_index] {
-                        clause.push(supports(*prev, *prev_cond));
+                    let crt_link = supports(*crt_instance, *crt_cond);
+                    let prv_link = supports(*prv_instance, *crt_cond);
+                    clause.push(!crt_link.active);
+                    if !(crt_link.exclusive && prv_link.exclusive) {
+                        clause.push(prv_link.active);
                     }
+
+                    for prv_cond in &conditions[0..j] {
+                        let crt_link = supports(*crt_instance, *prv_cond);
+                        let prv_link = supports(*prv_instance, *prv_cond);
+                        if crt_link.exclusive && prv_link.exclusive {
+                            clause.push(prv_link.active);
+                        } else {
+                            clause.push(model.reify(and([prv_link.active, !crt_link.active])));
+                        }
+                    }
+
                     model.enforce(or(clause.as_slice()), []);
                 }
             }
-            clause.clear();
-            if discard_useless_supports {
-                // enforce that a chronicle be present only if it supports at least one condition
-                clause.push(!pb.chronicles[*instance].chronicle.presence);
-                for cond in conditions {
-                    clause.push(supports(*instance, *cond))
-                }
-                model.enforce(or(clause.as_slice()), []);
-            }
         }
     }
 

planning/planners/src/encoding.rs

@@ -1,5 +1,5 @@
-use aries::core::Lit;
 use aries::model::lang::FAtom;
+use aries::{core::Lit, model::lang::Kind};
 use aries_planning::chronicles::*;
 use env_param::EnvParam;
 use std::collections::{BTreeSet, HashSet};
@@ -31,10 +31,16 @@ pub struct EffID {
     pub instance_id: ChronicleId,
     /// Index of the effect in the effects of the instance
     pub eff_id: usize,
+    /// Whether the effect is an assignment
+    pub is_assign: bool,
 }
 impl EffID {
-    pub fn new(instance_id: usize, eff_id: usize) -> Self {
-        Self { instance_id, eff_id }
+    pub fn new(instance_id: usize, eff_id: usize, is_assign: bool) -> Self {
+        Self {
+            instance_id,
+            eff_id,
+            is_assign,
+        }
     }
 }
 pub type ChronicleId = usize;
@@ -64,22 +70,34 @@ impl Encoding {
 /// - a literal that is true iff the effect is present in the solution.
 pub fn effects(pb: &FiniteProblem) -> impl Iterator<Item = (EffID, Lit, &Effect)> {
     pb.chronicles.iter().enumerate().flat_map(|(instance_id, ch)| {
-        ch.chronicle
-            .effects
-            .iter()
-            .enumerate()
-            .map(move |(eff_id, eff)| (EffID { instance_id, eff_id }, ch.chronicle.presence, eff))
+        ch.chronicle.effects.iter().enumerate().map(move |(eff_id, eff)| {
+            (
+                EffID::new(instance_id, eff_id, is_assignment(eff)),
+                ch.chronicle.presence,
+                eff,
+            )
+        })
     })
 }
 
+/// Returns true if the effect is an assignment effect.
+pub fn is_assignment(eff: &Effect) -> bool {
+    matches!(eff.operation, EffectOp::Assign(_))
+}
+
 /// Iterator over all assignment effects in a finite problem.
 pub fn assignments(pb: &FiniteProblem) -> impl Iterator<Item = (EffID, Lit, &Effect)> {
-    effects(pb).filter(|(_, _, eff)| matches!(eff.operation, EffectOp::Assign(_)))
+    effects(pb).filter(|(_, _, eff)| is_assignment(eff))
+}
+
+/// Returns true if the effect is an increase effect.
+pub fn is_increase(eff: &Effect) -> bool {
+    matches!(eff.operation, EffectOp::Increase(_))
 }
 
 /// Iterator over all increase effects in a finite problem.
 pub fn increases(pb: &FiniteProblem) -> impl Iterator<Item = (EffID, Lit, &Effect)> {
-    effects(pb).filter(|(_, _, eff)| matches!(eff.operation, EffectOp::Increase(_)))
+    effects(pb).filter(|(_, _, eff)| is_increase(eff))
 }
 
 /// Iterates over all conditions in a finite problem.
@@ -97,6 +115,11 @@ pub fn conditions(pb: &FiniteProblem) -> impl Iterator<Item = (CondID, Lit, &Con
     })
 }
 
+/// Returns true if the state variable is numeric.
+pub fn is_numeric(sv: &StateVar) -> bool {
+    matches!(sv.fluent.return_type().into(), Kind::Int)
+}
+
 pub struct TaskRef<'a> {
     pub presence: Lit,
     pub start: FAtom,