We consider temporal numeric planning problems $\Pi$ expressed in PDDL2.1 level 3, and show how to produce SMT formulas $(i)$ whose models correspond to valid plans of $\Pi$, 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.

翻译：我们考虑用PDDL2.1第三级语言描述的时间数值规划问题$\Pi$，并展示了如何生成满足以下条件的SMT公式：$(i)$ 其模型对应于$\Pi$的有效规划；$(ii)$ 将最近提出的基于模式的规划方法从数值情形推广至时间情形。我们证明了该方法的正确性与完备性，并展示其在10个需要并发处理的领域上表现优异。