Optimal Planning Modulo Theories

International Joint Conference on Artificial Intelligence, pp. 4128–4134

Abstract

We consider the problem of planning with arithmetic theories, and focus on generating optimal plans for numeric domains with constant and state-dependent action costs. Solving these problems efficiently requires a seamless integration between propositional and numeric reasoning. We propose a novel approach that leverages Optimization Modulo Theories (OMT) solvers to implement a domain-independent optimal theory-planner. We present a new encoding for optimal planning in this setting and we evaluate our approach using well-known, as well as new, numeric benchmarks.

Authors 4

1. Francesco Leofante corresponding

   Imperial College London

   Affiliation as printed

   Imperial College London, United Kingdom

2. Enrico Giunchiglia

   University of Genoa

   Affiliation as printed

   University of Genoa, Italy

3. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

4. Armando Tacchella

   University of Genoa

   Affiliation as printed

   University of Genoa, Italy