feat: lexicographic optimization over multiple objectives with plan output

planning/engine/src/encode.rs

@@ -155,6 +155,11 @@ pub fn condition_to_constraint(
             }
             ConditionExpression::And(conjuncts).scoped(bindings.presence)
         }
+        planx::Expr::App(planx::Fun::Geq, exprs) if exprs.len() == 2 => {
+            let lhs = reify_expression(exprs[0], Some(timepoint), model, sched, bindings, encoding)?;
+            let rhs = reify_expression(exprs[1], Some(timepoint), model, sched, bindings, encoding)?;
+            ConditionExpression::LeqZero(rhs - lhs).scoped(bindings.presence)
+        }
         _ => return Err(expr.todo("not supported")),
     };
 

planning/engine/src/encode/encoding.rs

@@ -16,7 +16,7 @@ pub struct Encoding {
     /// All actions instances that may appear in the plan.
     pub actions: Vec<ActionInstance>,
     /// Variable encoding the objective value (minimization)
-    pub objective: Option<LinTerm>,
+    pub objectives: Vec<LinTerm>,
     /// for each relaxable constraint, stores a constraint tag so that we can later decide if it should be relaxed.
     pub constraints_tags: BTreeMap<ConstraintID, Tag>,
     /// Associates each preference name with a list of literals that are true iff the preference hold.
@@ -31,7 +31,7 @@ impl Encoding {
     pub fn new() -> Self {
         Encoding {
             actions: vec![],
-            objective: None,
+            objectives: vec![],
             constraints_tags: Default::default(),
             preferences: Default::default(),
             required_values: RequiredValues::new(),
@@ -42,8 +42,8 @@ impl Encoding {
         self.actions.push(instance);
     }
 
-    pub fn set_objective(&mut self, objective: impl Into<LinTerm>) {
-        self.objective = Some(objective.into())
+    pub fn add_objective(&mut self, objective: impl Into<LinTerm>) {
+        self.objectives.push(objective.into())
     }
 
     /// Extracts the plan corresponding to this solution.

planning/engine/src/generate.rs

@@ -43,7 +43,11 @@ pub fn solve_finite_planning_problem(model: &Model, options: &Options) -> Res<()
 
     let _encoding_time = start.elapsed().as_millis();
 
-    let objective = encoding.objective.unwrap(); //TODO: error message
+    let objective = encoding
+        .objectives
+        .first()
+        .copied()
+        .expect("no objective specified (no default)");
 
     // set the objective to a constant if we are not optimizing
     let solver_objective = if options.optimize { objective } else { 0.into() };
@@ -53,7 +57,7 @@ pub fn solve_finite_planning_problem(model: &Model, options: &Options) -> Res<()
         println!("{}\n", encoding.plan(sol));
     };
 
-    if let Some(solution) = solver.find_optimal(solver_objective, &print) {
+    if let Some(solution) = solver.find_optimal(solver_objective, &print, []) {
         println!("\n> Found {}solution:", if options.optimize { "optimal " } else { "" });
         print(&solution);
     } else {
@@ -78,7 +82,7 @@ fn encode_finite_planning_problem(
                 optimize_plan::Relaxation::ActionPresence,
                 optimize_plan::Relaxation::StartTime,
             ],
-            objective: options.objective,
+            objectives: vec![options.objective],
         },
     )
 }

planning/engine/src/main.rs

@@ -123,6 +123,9 @@ pub struct OptimizePlan {
     plan_pb: PlanAndProblem,
     #[command(flatten)]
     options: optimize_plan::Options,
+    /// If provided, the optimized plan will be written to this file.
+    #[arg(short = 'w', long = "write-plan")]
+    plan_file: Option<PathBuf>,
 }
 
 #[derive(Parser, Debug)]
@@ -259,14 +262,10 @@ fn validate_plan(command: &Validate) -> Res<()> {
             if command.invalid {
                 std::process::exit(1);
             }
-            match (command.expected_objective, objective_value) {
-                (Some(_exptected), None) => {
-                    return Message::error("expected an objective value to be computed").failed();
-                }
-                (Some(exptected), Some(computed)) if exptected != computed => {
-                    return Message::error(format!("expected an objective value of {exptected}")).failed();
-                }
-                (_, _) => {}
+            if let Some(expected) = command.expected_objective
+                && expected != objective_value
+            {
+                return Message::error(format!("expected an objective value of {expected}")).failed();
             }
         }
         validate::ValidationResult::Invalid => {
@@ -282,13 +281,25 @@ fn validate_plan(command: &Validate) -> Res<()> {
 fn optimize_plan(command: &OptimizePlan) -> Res<()> {
     let (dom, pb, plan) = command.plan_pb.parse()?;
 
-    // processed model (from planx)
     let model = pddl::build_model(&dom, &pb)?;
     let plan = lifted_plan::parse_lifted_plan(&plan, &model)?;
     println!("{model}");
     println!("\n===== Plan ====\n\n{plan}\n");
 
-    optimize_plan::optimize_plan(&model, &plan, &command.options)
+    // Resolve the output path according to the three cases:
+    //  1. None          → no output file
+    //  2. existing dir  → create <dir>/<problem_name>.plan
+    //  3. file path     → create or overwrite that file
+    let resolved_output: Option<PathBuf> = match &command.plan_file {
+        None => None,
+        Some(path) if path.is_dir() => {
+            let filename = format!("{}.plan", pb.problem_name.canonical_str());
+            Some(path.join(filename))
+        }
+        Some(path) => Some(path.clone()),
+    };
+
+    optimize_plan::optimize_plan(&model, &plan, &command.options, resolved_output.as_deref())
 }
 
 fn solve_finite_problem(command: &SolveFiniteProblem) -> Res<()> {

planning/engine/src/optimize_plan.rs

@@ -1,7 +1,7 @@
-use std::{collections::BTreeMap, time::Instant};
+use std::{collections::BTreeMap, fmt::Debug, time::Instant};
 
 use aries::{
-    core::state::Evaluable,
+    core::{state::Evaluable, views::Boundable},
     model::lang::{IntExpr, Store},
     prelude::*,
 };
@@ -16,7 +16,10 @@ use aries_plan_engine::{
 };
 use derive_more::derive::Display;
 use itertools::Itertools;
+
 use planx::{ActionRef, Goal, Model, Param, Res, SimpleGoal, Sym, errors::*};
+use std::io::Write;
+use std::path::Path;
 use timelines::{
     ConstraintID, IntExp, IntTerm, Sched, SymAtom, Task, Time, boxes::Segment, explain::ExplainableSolver,
 };
@@ -28,8 +31,8 @@ pub struct Options {
     #[arg(short, long, num_args(1..))]
     pub relaxation: Vec<Relaxation>,
 
-    #[arg(short, long, default_value("original"))]
-    pub objective: Objective,
+    #[arg(short, long, num_args(1..), default_values(["original"]))]
+    pub objectives: Vec<Objective>,
 }
 
 #[derive(clap::ValueEnum, Debug, Clone, Copy, Display, PartialEq, PartialOrd, Eq, Ord)]
@@ -48,33 +51,97 @@ pub enum Objective {
     Makespan,
 }
 
-pub fn optimize_plan(model: &Model, plan: &LiftedPlan, options: &Options) -> Res<()> {
+pub fn optimize_plan(model: &Model, plan: &LiftedPlan, options: &Options, output_plan: Option<&Path>) -> Res<()> {
     let start = Instant::now();
+    // Encode the planning problem into a constraint satisfaction problem
     let (mut solver, encoding, _sched) = encode_plan_optimization_problem(model, plan, options)?;
-
     let _encoding_time = start.elapsed().as_millis();
 
-    let objective = encoding.objective.unwrap(); //TODO: error message
+    // Pinning literals from previous phases; grows as objectives are solved
+    let mut phase_assumptions: Vec<Lit> = vec![];
+    let mut last_solution = None;
 
-    let print = |sol: &Solution| {
-        println!("==== Plan (objective: {}) =====", objective.evaluate(sol).unwrap());
-        println!("{}\n", encoding.plan(sol));
+    let print_plan = |sol: &Solution| {
+        println!(
+            "==== Plan (objectives: {:?}) =====\n\n{}",
+            encoding
+                .objectives
+                .iter()
+                .map(move |o| o.evaluate(sol).unwrap())
+                .format(" / "),
+            encoding.plan(sol)
+        );
     };
+    // Solve objectives lexicographically: each phase fixes the previous optimal values
+    for objective in encoding.objectives.iter().copied() {
+        // Minimize objective under normal constraints + previous pinnings
+        let Some(sol) = solver.find_optimal(objective, &print_plan, phase_assumptions.as_slice()) else {
+            println!("No solution !!!!");
+            for mus in solver.muses() {
+                let msg = format_culprit_set(Message::error("Invalid in all relaxation"), &mus, model, plan);
+                println!("\n{msg}\n");
+            }
+            return Ok(());
+        };
+
+        // Pin objective == opt_val for subsequent phases (upper + lower bound)
+        let opt_val = sol.eval(objective).unwrap();
+        phase_assumptions.push(objective.leq(opt_val)); // objective ≤ opt_val
+        phase_assumptions.push(objective.geq(opt_val)); // objective ≥ opt_val
+        last_solution = Some(sol);
+    }
 
-    if let Some(solution) = solver.find_optimal(objective, &print) {
-        println!("\n> Found optimal solution:");
-        print(&solution);
-        // _sched.print(&solution);
-    } else {
-        println!("No solution !!!!");
-        for mus in solver.muses() {
-            let msg = format_culprit_set(Message::error("Invalid in all relaxation"), &mus, model, plan);
-            println!("\n{msg}\n");
+    if let Some(solution) = last_solution {
+        println!("> Found optimal solution\n");
+        print_plan(&solution);
+        let plan_str = encoding.plan(&solution);
+
+        if let Some(path) = output_plan {
+            let mut file = std::fs::File::create(path)
+                .map_err(Message::from)
+                .title(format!("Cannot create output file {}", path.display()))?;
+            writeln!(file, "{plan_str}")
+                .map_err(Message::from)
+                .title(format!("Cannot write output file {}", path.display()))?;
         }
     }
+
     Ok(())
 }
 
+fn build_objective(
+    objective: &Objective,
+    model: &Model,
+    sched: &mut Sched,
+    bindings: &Scope,
+    encoding: &mut Encoding,
+) -> Res<LinTerm> {
+    Ok(match objective {
+        Objective::Original if model.metric.is_some() => {
+            // TODO: use if let guard when stabilized
+            let metric = model.metric.unwrap();
+            match metric {
+                planx::Metric::Minimize(expr_id) => {
+                    let lin_obj = reify_expression(expr_id, Some(sched.horizon), model, sched, bindings, encoding)?;
+                    flatten_expression(lin_obj, sched, bindings)
+                }
+                planx::Metric::Maximize(_) => {
+                    return Message::error("unsupported maximization metric").failed();
+                }
+            }
+        }
+        // Fall back to plan length when no metric is defined in the domain
+        Objective::PlanLength | Objective::Original => {
+            let mut sum = LinSum::zero();
+            for t in sched.tasks.iter() {
+                sum += timelines::constraints::bool2int(t.presence, &mut sched.model);
+            }
+            reify_sum(sum, sched)
+        }
+        Objective::Makespan => sched.makespan.into(),
+    })
+}
+
 pub fn encode_plan_optimization_problem(
     model: &Model,
     lifted_plan: &LiftedPlan,
@@ -212,7 +279,8 @@ pub fn encode_plan_optimization_problem(
         // store the scopes, we will need them when processing the effects
         operations_scopes.push((a, bindings));
     }
-    // for each goal, add a constraint stating it must hold (the constriant is tagged but not relaxed for domain repair)
+
+    // for each goal, add a constraint stating it must hold (the constraint is tagged but not relaxed for domain repair)
     for (gid, x) in model.goals.iter().enumerate() {
         let constraint = parse_goal(x, model, &mut sched, &global_scope, &mut encoding)?;
         constraint.add_required_values(&mut encoding.required_values, model, &sched);
@@ -243,7 +311,7 @@ pub fn encode_plan_optimization_problem(
             .push(reification);
     }
 
-    // enforce all elemts of the initial state as effects
+    // enforce all elements of the initial state as effects
     for x in &model.init {
         let eff = convert_effect(x, false, model, &mut sched, &global_scope, &mut encoding)?;
         sched.add_effect(eff);
@@ -286,39 +354,11 @@ pub fn encode_plan_optimization_problem(
         }
     }
 
-    let objective: LinTerm = match options.objective {
-        Objective::Original if model.metric.is_some() => {
-            // TODO: use if-let-guard when stabilized
-            let metric = model.metric.unwrap();
-            match metric {
-                planx::Metric::Minimize(expr_id) => {
-                    let lin_obj = reify_expression(
-                        expr_id,
-                        Some(sched.horizon),
-                        model,
-                        &mut sched,
-                        &global_scope,
-                        &mut encoding,
-                    )?;
-                    flatten_expression(lin_obj, &mut sched, &global_scope)
-                }
-                planx::Metric::Maximize(_) => {
-                    return Message::error("unsupported maximization metric").failed();
-                }
-            }
-        }
-        // use plan-length as default when no metric is specified
-        Objective::PlanLength | Objective::Original => {
-            let mut sum = IntExp::zero();
-            for (_a, scope) in &operations_scopes {
-                let action_prez = scope.presence;
-                sum += timelines::constraints::bool2int(action_prez, &mut sched.model)
-            }
-            reify_sum(sum, &mut sched)
-        }
-        Objective::Makespan => sched.makespan.into(),
-    };
-    encoding.set_objective(objective);
+    // Build all objectives
+    for obj in &options.objectives {
+        let obj = build_objective(obj, model, &mut sched, &global_scope, &mut encoding)?;
+        encoding.add_objective(obj);
+    }
 
     // set all default negative value
     // The function attempts to only put those that may be useful, based on the required values

planning/engine/src/validate.rs

@@ -8,28 +8,24 @@ use crate::optimize_plan::{self, encode_plan_optimization_problem};
 pub struct Options {}
 
 pub enum ValidationResult {
-    Valid { objective_value: Option<timelines::IntCst> },
+    Valid { objective_value: timelines::IntCst },
     Invalid,
 }
 
 pub fn validate(model: &Model, plan: &LiftedPlan, _options: &Options) -> Res<ValidationResult> {
     // we frame the problem as an optimization problem with no relaxation,
     // hence the solver is forced to reproduce the plan
     let opt_options = crate::optimize_plan::Options {
-        relaxation: vec![],                            // no relaxation
-        objective: optimize_plan::Objective::Original, // TODO: change to domain's metric
+        relaxation: vec![], // no relaxation
+        objectives: vec![optimize_plan::Objective::Original],
     };
     let (mut solver, encoding, _sched) = encode_plan_optimization_problem(model, plan, &opt_options)?;
 
     if let Some(solution) = solver.check_satisfiability() {
         println!("> Plan is valid");
-        let objective_value = if let Some(objective) = encoding.objective {
-            let objective_value = objective.evaluate(&solution).unwrap();
-            println!("> Objective: {objective_value}",);
-            Some(objective_value)
-        } else {
-            None
-        };
+        let objective = encoding.objectives.first().copied().unwrap();
+        let objective_value = objective.evaluate(&solution).unwrap();
+        println!("> Objective: {objective_value}");
         // _sched.print(&solution);
         Ok(ValidationResult::Valid { objective_value })
     } else {