Research map / Learning theory and algorithms / Combinatorial and search optimization
Abstract Action Scheduling for Optimal Temporal Planning via OMT
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Refines the abstract step of OMT-based optimal temporal planning with abstract action scheduling constraints that tighten makespan estimates and forbid self-enabling loops, proven sound and complete and shown faster than prior OMT encodings and OPTIC on IPC benchmarks.
Problem
Optimal temporal planning (makespan and action-cost minimization) via OMT suffers from a loose over-approximation of abstract actions beyond the bound, which yields non-executable and spurious self-enabling plans and requires very large bounds to prove optimality.
Approach
Encode abstract actions with start times and precedence constraints: each condition false at the last concrete step must be preceded in time by an enabling future effect, and the makespan objective accounts for abstract action end times. This orders abstract actions, gives better makespan estimates and implicitly forbids circular self-enabling.
Key results
- Z3OUR INC optimally solves 148 instances total versus 65 for Z3PM and 90 for OPTIC in the coverage table (Z3OUR 147 optimal + 1 plan-only for monolithic variant).
- The new encoding never worsens the terminating bound compared to Z3PM INC and in many cases improves it significantly.
- Ablation shows the abstract scheduling encoding accounts for most of the speedup.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add abstract action scheduling constraints | OMT temporal planning · IPC-14 and benchmark set | coverage (optimally solved instances): 65 -> 147 | Helped |
| add abstract action scheduling constraints | OMT temporal planning · IPC-14 and benchmark set | terminating bound | Helped |
| add abstract action scheduling constraints | OMT temporal planning · IPC-14 and benchmark set | runtime | Helped |
| remove the optimization-before-first-plan improvement (ablation) | Z3OUR INC · IPC-14 and benchmark set | coverage (optimally solved instances): 147 -> 145 | Hurt |
| remove the lexicographic secondary objective (ablation) | Z3OUR INC · IPC-14 and benchmark set | coverage (optimally solved instances): 147 -> 147 | No clear effect |
| remove the optimization-before-first-plan improvement (ablation) | Z3OUR · IPC-14 and benchmark set | coverage (optimally solved instances): 148 -> 143 | Hurt |
| remove the lexicographic secondary objective (ablation) | Z3OUR · IPC-14 and benchmark set | coverage (optimally solved instances): 148 -> 142 | Hurt |
| add abstract action scheduling constraints | OMT temporal planning · running example, makespan minimization | makespan estimate: 4 -> 16 | Helped |
| add abstract action scheduling constraints to prevent self-enabling abstract actions | OMT temporal planning · running example, package p3 goal | algorithm termination bound: h = 9 | Helped |
Surprising findings
- Satisfiability-based planners, usually weak on IPC instances, perform strongly with the new encoding compared to heuristic search OPTIC.
Limitations
- Abstraction remains an over-approximation; abstract actions only need to be touched by an effect, so some non-executable models can still appear.
- Evaluated only with the Z3 OMT solver.
- Relies on bounded incremental encoding whose size grows with the bound.
Experimental setup
Datasets: Temporal IPC domains from IPC-14 benchmark set from Panjkovic and Micheli 2023
Benchmarks: IPC-14 temporal domains (makespan and action cost variants) Panjkovic and Micheli 2023 benchmark set
Metrics: coverage (instances optimally solved) solving time terminating bound
Baselines: Z3PM Z3PM INC OPTIC
Builds on: Panjkovic and Micheli 2023 OMT temporal planning encoding Leofante et al. 2020 optimal planning modulo theories Giunchiglia and Taccchella 2022 level ordering constraints
Closest papers by meaning
- Expressive Optimal Temporal Planning via Optimization Modulo Theory (AAAI 2023 · similarity 0.90)
- Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping (AAAI 2022 · similarity 0.88)
- Temporal Planning with Temporal Metric Trajectory Constraints (AAAI 2019 · similarity 0.86)
- Automatic Selection of Macro-Events for Heuristic-Search Temporal Planning (AAAI 2025 · similarity 0.85)
- Temporal Numeric Planning with Patterns (AAAI 2025 · similarity 0.85)
- Planning Anything with Rigor: General-Purpose Zero-Shot Planning with LLM-based Formalized Programming (ICLR 2025 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.