摘要
We consider temporal numeric planning problems Π expressed in PDDL2.1, and show how it is possible to produce SMT formulas (i) whose models correspond to valid plans of Π, and (ii) which extends the recently proposed planning with patterns approach from the numeric to the temporal case. We prove the correctness and completeness of the approach and that it outperforms all the publicly available temporal planners on 10 domains with required concurrency.