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.
PDDL+
PDDL+ is the extension of PDDL that allows modelling of mixed discrete-continuous domains, and it follows the Hybrid Automata semantics. Dealing with hybrid systems is becoming more and more an important challenge, as many real-world scenarios feature a mixture of discrete and continuous behaviours.
Compared to PDDL2.1, PDDL+ includes the following additional features, that can all be handled by SMTPlan+.
| Nonlinear change | Processes | Events | Timed Initial Literals | Epsilon separation | Cascading events | |
| SMTPlan+ |  |
|
|
|
|
|
SMT Encoding
The econding is based on the notion of happening, which is used to capture the change in the state at a given time point due to the effects of actions, processes, or events. Happenings describe discrete change and between happenings there is only continuous change.
A PDDL+ model can be described as a bounded set of happenings X:= {x1...xn } encoded as an SMT formula, such that any proof for the SMT formula represents the trace of a valid plan. The initial state is modelled in x1 , and the goal constraints are added to xn.