Cashmore

Planning in hybrid systems is important for dealing with real-world applications. PDDL supports this representation of domains with mixed discrete and continuous dynamics, and supports events and processes modelling exogenous change. Motivated by numerous SAT-based planning approaches, we propose an approach to PDDL planning through SMT, describing an SMT encoding that captures all the features of the PDDL problem as published by Fox and Long. The encoding can be applied on domains with nonlinear continuous change. We apply this encoding in a simple planning algorithm, demonstrating excellent results on a set of benchmark problems.