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第3级中表达的时间数值规划问题$\Pi$，展示了如何生成SMT公式$(i)$，其模型对应于$\Pi$的有效规划，且$(ii)$将最近提出的基于模式的规划方法从数值情形推广至时间情形。我们证明了该方法的正确性与完备性，并在10个需要并发执行的领域中展示了其优越性能。