diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 040e5fa2..5525b9a5 100644 --- a/planning/planners/src/encode.rs +++ b/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) -> 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) -> 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) -> 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) -> 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) -> std::result::Result value: var.into(), }, )); + next_cond_id += 1; num_numeric_increase_coherence_constraints += 1; } @@ -801,14 +794,14 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> 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; } @@ -816,6 +809,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result unreachable!() }; let mut supported: Vec = Vec::with_capacity(128); + let mut inc_support: HashMap> = 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) -> 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) -> 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) -> 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]); } diff --git a/planning/planners/src/encode/symmetry.rs b/planning/planners/src/encode/symmetry.rs index 46c5bd14..a4b56e2e 100644 --- a/planning/planners/src/encode/symmetry.rs +++ b/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> = 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| { @@ -185,7 +197,12 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod }; let conds_by_templates: HashMap> = 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()), []); - } } } diff --git a/planning/planners/src/encoding.rs b/planning/planners/src/encoding.rs index 470dafe2..989ae86c 100644 --- a/planning/planners/src/encoding.rs +++ b/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 { 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 { - 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 { - 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 bool { + matches!(sv.fluent.return_type().into(), Kind::Int) +} + pub struct TaskRef<'a> { pub presence: Lit, pub start: FAtom,