feat(timelines): add lprelax wrapper reasoner (HiGHS-based)

.github/workflows/aries.yml

@@ -209,6 +209,8 @@ jobs:
         run: just ci-ape-val-opt
       - name: APE solver
         run: just ci-ape-solve 15 # increase the timeout to avoid flaky tests
+      - name: APE solver (LpRelaxHighs)
+        run: just ci-ape-solve-lprelax # timeouts should be large enough to avoid flaky tests
 
   tests:
     # Meta-job that only requires all test-jobs to pass

Cargo.toml

@@ -2,6 +2,7 @@
 
 members = [
     "solver",
+    "solver/lp_highs",
     "bench/data",
     "bench/bench",
     "utils/env_param",

examples/scheduling/src/search.rs

@@ -82,7 +82,7 @@ pub fn get_solver(mut base_solver: Solver, strategy: &SearchStrategy, pb: &Encod
                 "focused" => mode = Mode::Focused,
                 x if x.starts_with("+lbd") => {
                     let lvl = x.strip_prefix("+lbd").unwrap().parse().unwrap();
-                    base_solver.reasoners.sat.clauses.params.locked_lbd_level = lvl;
+                    base_solver.reasoners.sat().clauses.params.locked_lbd_level = lvl;
                 }
                 "" => {} // ignore
                 _ => panic!("Unsupported option: {opt}"),

justfile

@@ -89,10 +89,29 @@ ci-pddl-parse-all lift="false" filter="d":
 ci-ape-val-opt:
     uv run ci/ape-val.py
 
-# Checks that all problems marked are as solvable are indeed solved within their max-depth
+# Checks that all problems marked as solvable are indeed solved within their max-depth
 ci-ape-solve timeout="5":
     uv run ci/ape-solve.py -t {{ timeout }} --from-toml ci/problems.toml
 
+# Checks that all problems marked as solvable are indeed solved within their max-depth. With all lprelax configurations (unsoundness checks).
+ci-ape-solve-lprelax:
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=false ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=false ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=false \
+        uv run ci/ape-solve.py -t 30 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=false ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=false ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=true \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=false ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=true ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=false \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=false ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=true ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=true \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=true ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=false ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=false \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=true ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=false ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=true \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=true ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=true ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=false \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+    ARIES_LPRELAX_USE=true ARIES_LPRELAX_RECOVER_CLOSED_WORLD_DEFAULTS=true ARIES_LPRELAX_WITH_CONDITION_OUT_TRANSITIONS=true ARIES_LPRELAX_MERGE_EQUAL_COLUMNS=true \
+        uv run ci/ape-solve.py -t 90 --from-toml ci/problems.toml
+
 bench-jsp name timeout="10":
     #!/usr/bin/env bash
     set -e  # stop on first error

planning/planners/src/solver.rs

@@ -381,7 +381,7 @@ pub fn init_solver(model: Model<VarLabel>) -> Box<Solver> {
     };
 
     let mut solver = Box::new(aries_solver::solver::Solver::new(model));
-    solver.reasoners.diff.config = stn_config;
+    solver.reasoners.diff().config = stn_config;
     solver
 }
 
@@ -446,11 +446,11 @@ impl Strat {
             }
             Strat::ActivityBoolLight => {
                 solver.set_brancher(ActivityBrancher::new_with_heuristic(ActivityBoolFirstHeuristic));
-                solver.reasoners.diff.config.theory_propagation = TheoryPropagationLevel::Bounds;
+                solver.reasoners.diff().config.theory_propagation = TheoryPropagationLevel::Bounds;
             }
             Strat::Forward => {
                 solver.set_brancher(ForwardSearcher::new(problem));
-                solver.reasoners.diff.config.theory_propagation = TheoryPropagationLevel::Bounds;
+                solver.reasoners.diff().config.theory_propagation = TheoryPropagationLevel::Bounds;
             }
             Strat::Causal => {
                 let strat = causal_brancher(problem, encoding);

planning/timelines/Cargo.toml

@@ -10,9 +10,11 @@ edition = "2024"
 itertools = { workspace = true }
 tracing = { workspace = true }
 aries-solver = { path = "../../solver" }
+aries-solver-lp-highs = { path = "../../solver/lp_highs" }
 aries-datalog = { path = "../../utils/datalog" }
 aries-env-param = { path = "../../utils/env_param" }
 idmap = { workspace = true }
 smallvec = { workspace = true }
 num-rational = { workspace = true }
 streaming-iterator = { workspace = true }
+hashbrown = { workspace = true }

planning/timelines/src/analysis/grounding/mod.rs

@@ -57,6 +57,11 @@ impl Groundings {
             .iter()
             .filter_map(|(k, v)| k.map(|task_id| (task_id, v.as_slice())))
     }
+
+    /// Groundings of the empty source. Since it is usually fully ground (no variables involved), there is usually exactly one, empty assignment.
+    pub fn empty_source_groundings(&self) -> &[ParametersAssignment] {
+        self.groundings.get(&None).map(|v| v.as_slice()).unwrap_or(&[])
+    }
 }
 
 /// Ground all tasks appear in this problem.

planning/timelines/src/analysis/mod.rs

@@ -1,5 +1,6 @@
 pub mod grounding;
 mod nonsimple;
+pub mod transitions;
 
 pub use nonsimple::collect_nonsimple_conditions_and_effects_to_relax;
 

planning/timelines/src/analysis/nonsimple.rs

@@ -49,24 +49,33 @@ fn collect_nonsimple_effects(ctx: &SchedEncoder) -> HashSet<EffectId> {
 fn collect_nonsimple_conditions(nonsimple_effects: &mut HashSet<EffectId>, ctx: &SchedEncoder) -> HashSet<CondId> {
     let mut res = HashSet::new();
 
-    for cl in ctx.causal_links.get_links() {
-        if res.contains(&cl.cond_id) {
-            nonsimple_effects.insert(cl.eff_id);
-            continue;
+    for (cond_id, cond) in ctx.causal_links.conditions.iter().enumerate() {
+        if !all_nonconstant_terms_are_included_in_source_terms(
+            cond.state_var.args.iter().chain(&[cond.value]).copied(),
+            cond.source,
+            ctx,
+        ) {
+            res.insert(cond_id);
         }
-        let cond = &ctx.causal_links.conditions[cl.cond_id];
+    }
 
-        if nonsimple_effects.contains(&cl.eff_id)
-            || !all_nonconstant_terms_are_included_in_source_terms(
-                cond.state_var.args.iter().chain(&[cond.value]).copied(),
-                cond.source,
-                ctx,
-            )
-        {
-            nonsimple_effects.insert(cl.eff_id);
+    // Propagate "nonsimple-ness":
+    // if a causal link uses an effect or condition marked as nonsimple, mark the other member (condition or effect) as nonsimple too.
+    for cl in ctx.causal_links.get_links() {
+        if nonsimple_effects.contains(&cl.eff_id) {
             res.insert(cl.cond_id);
+        } else if res.contains(&cl.cond_id) {
+            nonsimple_effects.insert(cl.eff_id);
         }
     }
+
+    // A nonsimple effect / condition is such that for all its causal links, the other member is also nonsimple
+    debug_assert!(
+        ctx.causal_links
+            .get_links()
+            .all(|cl| nonsimple_effects.contains(&cl.eff_id) == res.contains(&cl.cond_id))
+    );
+
     res
 }
 

planning/timelines/src/analysis/transitions/closed_world_default.rs

@@ -0,0 +1,104 @@
+use std::collections::{HashMap, HashSet};
+
+use aries_solver::{core::IntCst, lang::Lit};
+
+use super::EffectBasicInfo;
+use crate::{EffectId, EffectOp, IntTerm, SchedEncoder, StateVar, encoder::CondId};
+
+/// Closed-world default (ground) initial effects in place of those omitted in (or "missing" from) the main encoding
+/// after being derived as unable to support any condition (see [`add_closed_world_negative_effects`]).
+///
+/// Note that the values of the effects we're "recovering" here do not need to match those of the "original" omitted initial effects,
+/// because if they were needed, they wouldn't have been pruned in the main encoding.
+///
+/// Effect ids below `first_id` correspond to the "original" effects of the encoding.
+#[derive(Clone, Default)]
+pub(super) struct ClosedWorldDefaultEffects {
+    first_id: EffectId,
+    store: Vec<EffectBasicInfo>,
+    pub ignored_fluents: HashSet<crate::Sym>,
+    original_initial_effects_ground_args: HashMap<crate::Sym, Vec<smallvec::SmallVec<[IntCst; 4]>>>,
+}
+impl ClosedWorldDefaultEffects {
+    pub fn new(
+        ctx: &SchedEncoder,
+        effects_to_ignore: impl IntoIterator<Item = EffectId>,
+        conditions_to_ignore: impl IntoIterator<Item = CondId>,
+        mut original_initial_effects_ground_args: HashMap<crate::Sym, Vec<smallvec::SmallVec<[IntCst; 4]>>>,
+    ) -> Self {
+        for (_, entry) in original_initial_effects_ground_args.iter_mut() {
+            debug_assert!({
+                use itertools::Itertools;
+                entry.iter().all_unique()
+            });
+            entry.sort_unstable();
+        }
+
+        Self {
+            first_id: ctx.sched.effects.iter().count(),
+            store: vec![],
+            ignored_fluents: HashSet::<crate::Sym>::from_iter(
+                effects_to_ignore
+                    .into_iter()
+                    .map(|e_id| ctx.sched.effects.get(e_id).state_var.fluent.clone())
+                    .chain(
+                        conditions_to_ignore
+                            .into_iter()
+                            .map(|c_id| ctx.causal_links.conditions.get(c_id).state_var.fluent.clone()),
+                    ),
+            ),
+            original_initial_effects_ground_args,
+        }
+    }
+    pub fn is_empty(&self) -> bool {
+        self.store.is_empty()
+    }
+    pub fn contains(&self, eff_id: EffectId) -> bool {
+        eff_id >= self.first_id && eff_id < self.first_id + self.store.len()
+    }
+    pub fn get(&self, offset_eff_id: EffectId) -> &EffectBasicInfo {
+        &self.store[offset_eff_id - self.first_id]
+    }
+    pub fn add(
+        &mut self,
+        fluent: crate::Sym,
+        args: impl Into<smallvec::SmallVec<[IntCst; 4]>>,
+        value: IntCst,
+    ) -> Result<EffectId, ()> {
+        let args = args.into();
+
+        // Ignore if there already is a (non-ignored) initial effect with these ground args.
+        if self
+            .original_initial_effects_ground_args
+            .get(&fluent)
+            .is_some_and(|known_grs| known_grs.contains(&args))
+        {
+            return Err(());
+        }
+
+        let eff_view = EffectBasicInfo {
+            state_var: StateVar {
+                fluent,
+                args: args.into_iter().map(IntTerm::int_cst).collect(),
+            },
+            operation: EffectOp::Assign(IntTerm::int_cst(value)),
+            prez: Lit::TRUE,
+            source: None,
+        };
+
+        debug_assert!(
+            eff_view
+                .state_var
+                .args
+                .iter()
+                .chain(match &eff_view.operation {
+                    EffectOp::Assign(term) => [term],
+                    EffectOp::Step(_term) => todo!(),
+                })
+                .all(|term| term.is_cst())
+        );
+
+        self.store.push(eff_view);
+        Ok(self.first_id + self.store.len() - 1)
+    }
+}