Page Contributors: adamgreen, Adam Green,

Year Published: 2016

Paper: A Compilation of the Full PDDL+ Language into SMT [Cashmore, M. Fox, M. Long, D. Magazzeni, D.]

SMTPlan+ is a planner for hybrid systems.

It supports all the features of PDDL+, including exogenous events and continuous processes.

SMTPlan+ provides an SMT encoding of the PDDL+ models and can handle linear domains as well as domains with nonlinear polynomial change.


SMTPlan+ Supports the following features according to Eviscerator:

Requirement Supported?
PDDL 1.2  
:strips Yes
:typing Yes
:disjunctive-preconditions Yes
:equality Yes
:existential-preconditions Yes
:universal-preconditions Yes
:conditional-effects Not Tested
:domain-axioms No
:subgoals-through-axioms No
:safety-constraints No
:open-world No
:quantified-preconditions Yes
:adl Not Tested
:ucpop Not Tested
PDDL 2.1  
:numeric-fluents Yes
:durative-actions Yes
:duration-inequalities Yes
:continuous-effects Yes
:negative-preconditions Yes
PDDL 2.2  
:derived-predicates Not Tested
:timed-initial-literals Yes
PDDL 3.0  
:constraints No
:preferences No
PDDL 3.1  
:action-costs Yes
:goal-utilities No
:time Yes

Downloading and compiling SMTPlan+

SMTPlan+ has one of the more modern and more comprehensive set of documentation for it. The GitHub repo for SMTPlan+ can be found here. Documentation on SMTPlan+ can be found on its GitHub pages website. Additional instructions for compilation can also be found here

Additional Notes

SMTPlan+ supports polynomial continuous effects, and linear continuous effects,