SMT techniques for planning problems

Espasa Arxer, Joan
Automated planning is a discipline in the field of Artificial Intelligence that can be described as the process of finding a course of action that achieves a specified task. In other words, it focuses on reasoning about causal structures and identifying the necessary actions for achieving a given goal. Although classical planning approaches have been widely successful, the needs of real-world applications go way beyond its potential. In the area of automated planning many formalisms exist in order to express all the needs these problems encompass. This huge variety of problems range from classical planning to reasoning about partially observable Markov decision processes, multi-agent planning, real-time perceiving and acting or temporal and numeric reasoning. There exist a wide range of techniques to confront each of the aforementioned formalisms, each one having its own advantages and weaknesses. In this thesis we restrict ourselves to the setting of hybrid planning. That is, the combination of the propositional planning with extensions to be able to reason about different theories, such as integer or real arithmetic. This thesis presents a set of techniques to efficiently encode planning problems that involve reasoning at propositional level as well as to deal with background theories. To address reasoning about the different theories, we use SAT Modulo Theories (SMT), an extension to SAT that allows the solver to, in a modular way, reason about non-propositional symbols belonging to background theories. This framework is interesting because it is expressive enough to translate many real-world planning problems. The main objective of the thesis is to push forward the state of the art of planning as SMT, by devising encodings of planning problems to SMT. The focus is especially on numeric planning, combining classical planning with the ability to reason about integer or floating point numbers. In this setting, many real-world resource-based problems can be encoded. Our implementation of the encodings resulted in a new planner called Rantanplan, which preprocesses and translates numeric planning problems into SMT formulas, to solve them using a SMT solver of choice. We also provide detailed experimental results on new and well-known domains, to show that our approach is competitive with the existing exact numeric planners ​
​L'accés als continguts d'aquesta tesi queda condicionat a l'acceptació de les condicions d'ús establertes per la següent llicència Creative Commons: