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+ 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

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.

Mountain View

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.