Temporal Planning with Clock-Based SMT Encodings

Temporal Planning with Clock-Based SMT Encodings

Jussi Rintanen

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 743-749. https://doi.org/10.24963/ijcai.2017/103

We propose more scalable encodings of temporal planning in SMT. The first contribution is practical clock-based encodings of resources and effect delays. Existing encodings of effect delays (Shin and Davis, 2015) have a quadratic size, due to the necessity to determine the time differences between steps for a linear number of steps. Clocks improve this to linear. The second contribution is a new relaxed scheme for steps. Existing schemes require a step for every time point with discontinuous change. This is relaxed, improving scalability.
Keywords:
Constraints and Satisfiability: Modeling/Formulation
Planning and Scheduling: Temporal and Hybrid planning
Planning and Scheduling: Search in Planning and Scheduling