Temporal Planning with Clock-Based SMT Encodings
Abstract
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.
Cite
Text
Rintanen. "Temporal Planning with Clock-Based SMT Encodings." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/103Markdown
[Rintanen. "Temporal Planning with Clock-Based SMT Encodings." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/rintanen2017ijcai-temporal/) doi:10.24963/IJCAI.2017/103BibTeX
@inproceedings{rintanen2017ijcai-temporal,
title = {{Temporal Planning with Clock-Based SMT Encodings}},
author = {Rintanen, Jussi},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {743-749},
doi = {10.24963/IJCAI.2017/103},
url = {https://mlanthology.org/ijcai/2017/rintanen2017ijcai-temporal/}
}