Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Temporal Numeric Planning with Patterns

Matteo Cardellini, Enrico Giunchiglia

TL;DR

The paper tackles temporal numeric planning in PDDL2.1 level $3$ by extending Symbolic Pattern Planning (spp) to produce SMT encodings whose models correspond to valid plans and by proving both correctness and completeness. The core methodological advance is the pattern-based encoding, consisting of pattern definition, rolling of durative actions, and two encodings: pattern-state $T^{\prec}_s$ and pattern-time $T^{\prec}_t$, which jointly enforce executability and temporal constraints. Empirical results across 10 domains with required concurrency show that PATTY$_t$ achieves higher coverage and smaller bounds than competing symbolic and search-based planners, often solving problems with fewer SMT calls. The work demonstrates significant practical gains for temporal numeric planning and provides a rigorous foundation for pattern-driven SMT encodings in this setting.

Abstract

We consider temporal numeric planning problems $Π$ expressed in PDDL2.1 level 3, and show how to produce SMT formulas $(i)$ whose models correspond to valid plans of $Π$, and $(ii)$ that extend the recently proposed planning with patterns approach from the numeric to the temporal case. We prove the correctness and completeness of the approach and show that it performs very well on 10 domains with required concurrency.

Temporal Numeric Planning with Patterns

TL;DR

The paper tackles temporal numeric planning in PDDL2.1 level by extending Symbolic Pattern Planning (spp) to produce SMT encodings whose models correspond to valid plans and by proving both correctness and completeness. The core methodological advance is the pattern-based encoding, consisting of pattern definition, rolling of durative actions, and two encodings: pattern-state and pattern-time , which jointly enforce executability and temporal constraints. Empirical results across 10 domains with required concurrency show that PATTY achieves higher coverage and smaller bounds than competing symbolic and search-based planners, often solving problems with fewer SMT calls. The work demonstrates significant practical gains for temporal numeric planning and provides a rigorous foundation for pattern-driven SMT encodings in this setting.

Abstract

We consider temporal numeric planning problems expressed in PDDL2.1 level 3, and show how to produce SMT formulas whose models correspond to valid plans of , and that extend the recently proposed planning with patterns approach from the numeric to the temporal case. We prove the correctness and completeness of the approach and show that it performs very well on 10 domains with required concurrency.

Paper Structure

This paper contains 12 sections, 2 theorems, 6 equations, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Standard Encodings in smt
  4. Temporal Numeric Planning with Patterns
  5. Pattern and Language Definition
  6. Rolling Durative Actions
  7. The Pattern State Encoding
  8. The Pattern Time Encoding
  9. Correctness and Completeness Results
  10. Experimental Results
  11. Conclusion
  12. Acknowledgments

Key Result

Theorem 1

Let $b$ be a durative action eligible for rolling. Let $s$ be a state. The result of executing $b^\vdash;b^{\vdash\mathrel{\mkern-9mu}\dashv};b^\dashv$ consecutively for $p\ge 1$ times in $s$ is defined if and only if for each numeric condition $\psi \unrhd 0$,

Theorems & Definitions (4)

  • Example
  • Theorem 1
  • proof
  • Theorem 2