Temporal Planning with Clock-Based SMT Encodings

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


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.
Original languageEnglish
Title of host publicationProceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
ISBN (Electronic)978-0-9992411-0-3
Publication statusPublished - 2017
MoE publication typeA4 Article in a conference publication
EventInternational Joint Conference on Artificial Intelligence - Melbourne, Australia
Duration: 19 Aug 201725 Aug 2017
Conference number: 26

Publication series

NameProceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
ISSN (Print)1045-0823


ConferenceInternational Joint Conference on Artificial Intelligence
Abbreviated titleIJCAI
Internet address


  • Constraints and Satisfiability: Modeling/Formulation
  • Planning and Scheduling: Temporal and Hybrid planning
  • Planning and Scheduling: Search in Planning and Scheduling


Dive into the research topics of 'Temporal Planning with Clock-Based SMT Encodings'. Together they form a unique fingerprint.
  • Finnish centre of excellence in computational inference research

    Xu, Y., Rintanen, J., Kaski, S., Anwer, R., Parviainen, P., Soare, M., Vuollekoski, H., Rezazadegan Tavakoli, H., Peltola, T., Blomstedt, P., Puranen, S., Dutta, R., Gebser, M., Mononen, T., Bogaerts, B., Tasharrofi, S., Pesonen, H., Yang, Z. & Weinzierl, A.


    Project: Academy of Finland: Other research funding

Cite this