Planning Modulo Theories: Extending the Planning Paradigm


  • Peter Gregory University of Huddersfield
  • Derek Long King's College London
  • Maria Fox King's College London
  • J. Christopher Beck University of Toronto



Planning, Theories, Expressiveness


Considerable effort has been spent extending the scope of planning beyond propositional domains to include, for example, time and numbers. Each extension has been designed as a separate specific semantic enrichment of the underlying planning model, with its own syntax and customised integration into a planning algorithm. Inspired by work on SAT Modulo Theories (SMT) in the SAT community, we develop a modelling language and planner that treat arbitrary first order theories as parameters. We call the approach Planning Modulo Theories (PMT). We introduce a modular language to represent PMT problems and demonstrate its benefits over PDDL in expressivity and compactness. We present a generalisation of the $h_{max}$ heuristic that allows our planner, PMTPlan, to automatically reason about arbitrary theories added as modules. Over several new and existing benchmarks, exploiting different theories, we show that PMTPlan can significantly out-perform an existing planner using PDDL models.




How to Cite

Gregory, P., Long, D., Fox, M., & Beck, J. C. (2012). Planning Modulo Theories: Extending the Planning Paradigm. Proceedings of the International Conference on Automated Planning and Scheduling, 22(1), 65-73.