In this paper, we present a procedure for numeric planning based on Symbolic Pattern Planning (SPP). Given a numeric planning problem $Π$, a pattern $\prec$ is a sequence of actions used to define a formula encoding the subsequences of $\prec$ executable from a starting state $S$. Cardellini, Giunchiglia, and Maratea (2024a) follow the Planning as Satisfiability approach by defining, at each step $n \ge 0$, a formula $Π^\prec_n$ in which $(i)$ the pattern $\prec$ is computed only for $n=0$ in the initial state $I$ of $Π$, and then exploited at each step $n$, $(ii)$ the starting state $S$ is set to $I$, and $(iii)$ the set $G$ of goals is required to hold in the last state that can be reached by one of the subsequences of $\prec$ concatenated $n$ times. The procedure begins with $n=0$, terminates as soon as $Π^\prec_n$ is satisfiable, and otherwise proceeds by incrementing $n$. In this paper, possibly at each step, $(i)$ we symbolically search for an intermediate state $P$ reachable from $I$, closer to a goal state, $(ii)$ dynamically recompute the pattern $\prec_h$ -- to be used in the next step -- in $P$, $(iii)$ refine the pattern $\prec_g$ used to reach $P$, and $(iv)$ start the new search from the state $S$ which can be either the initial state $I$ or the last computed intermediate state $P$, exploiting the computed patterns $\prec_g$ and $\prec_h$ to define the pattern $\prec$ to be used in the search. In particular, at each step, we define a formula $Π^{\prec}_{S,P}$ encoding the existence of a state $P'$ closer than $P$ to a goal state, with $P'$ reachable from the starting state $S$ when using the pattern $\prec$. We present different techniques for producing such formulas, each corresponding to a different strategy for exploring the search space. We prove their correctness and completeness, the latter under certain conditions.

翻译：本文提出了一种基于符号模式规划（SPP）的数值规划方法。对于数值规划问题 $Π$，模式 $\prec$ 是一个动作序列，用于定义编码从起始状态 $S$ 可执行的 $\prec$ 子序列的公式。Cardellini、Giunchiglia 与 Maratea（2024a）遵循“规划即可满足性”方法，在每一步 $n \ge 0$ 中定义公式 $Π^\prec_n$，其中：$(i)$ 模式 $\prec$ 仅在 $n=0$ 时针对 $Π$ 的初始状态 $I$ 计算，并在后续每一步 $n$ 中利用；$(ii)$ 起始状态 $S$ 设为 $I$；$(iii)$ 要求目标集合 $G$ 在通过将 $\prec$ 的子序列串联 $n$ 次后所能到达的最后一个状态中成立。该过程从 $n=0$ 开始，当 $Π^\prec_n$ 可满足时立即终止，否则递增 $n$ 继续。在本文中，我们可能在每一步中：$(i)$ 符号化搜索从 $I$ 可达且更接近目标状态的中间状态 $P$；$(ii)$ 在 $P$ 中动态重新计算下一步使用的模式 $\prec_h$；$(iii)$ 细化用于到达 $P$ 的模式 $\prec_g$；$(iv)$ 从初始状态 $I$ 或最近计算的中间状态 $P$ 中选取起始状态 $S$，利用计算所得的 $\prec_g$ 和 $\prec_h$ 定义搜索中使用的模式 $\prec$，从而启动新搜索。具体而言，我们在每一步定义一个公式 $Π^{\prec}_{S,P}$，该公式编码存在一个比 $P$ 更接近目标状态的状态 $P'$，且 $P'$ 可在使用模式 $\prec$ 时从起始状态 $S$ 到达。我们提出了多种生成此类公式的技术，每种对应不同的搜索空间探索策略，并证明了它们的正确性以及在特定条件下的完备性。