Abstracts Abstract
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 struc- tures 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.
xvii
xviii CONTENTS
Our implementation of the encodings resulted in a new planner called Rantanplan, which preprocesses and translates numeric planning prob- lems 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.
Resum
La planificaci ́o autom`atica  ́es una disciplina dins de la intel·lig`encia artifi- cial que pot ser descrita com el proc ́es de trobar un seguit d’accions que assoleixen una tasca espec ́ıfica. En altres paraules, es focalitza en raonar sobre estructures causals i identificar les accions necess`aries per assolir un objectiu donat. Encara que les aproximacions a la planificaci ́o autom`atica cl`assica han tingut un gran `exit, les necessitats que tenen moltes aplicacions al m ́on real estan per sobre de les seves possibilitats.
Existeixen molts formalismes a l’`area de la planificaci ́o autom`atica que poden expressar totes les necessitats que tenen aquest tipus de problemes. Aquesta enorme varietat de problemes van des de la planificaci ́o cl`assica, passant per problemes expressats amb processos de decisi ́o de Markov par- cialment observables, problemes de percepci ́o i decisi ́o en temps real o prob- lemes que incorporen raonament temporal i num`eric. Existeixen un ampli ventall de t`ecniques per a afrontar cada un dels formalismes esmentats, cada una amb els seus avantatges i inconvenients. En aquesta tesi ens restringim en el marc de la planificaci ́o h ́ıbrida. Exactament, la combinaci ́o de la plan- ificaci ́o proposicional amb extensions per a poder raonar sobre diferents teories, tals com l’aritm`etica real o entera.
Aquesta tesi presenta un conjunt de t`ecniques per a codificar de manera eficient problemes de planificaci ́o que involucren raonament a nivell proposi- cional aix ́ı com raonament amb teories de fons. Per abordar el raonament sobre les diferents teories, farem anar SAT Modulo Teories (SMT), una ex- tensi ́o de SAT que permet al resoledor, de manera modular, raonar sobre s ́ımbols no proposicionals pertanyents a teories de fons. Aquest marc  ́es interessant perqu`e  ́es prou expressiu per a poder traduir molts problemes provinents del m ́on real.
L’objectiu principal  ́es millorar l’estat de l’art de la planificaci ́o au- tom`atica mitjan ̧cant SMT, a trav ́es de la codificaci ́o dels problemes de plani- ficaci ́o a SMT. El focus de la tesi  ́es especialment en la planificaci ́o num`erica, on es combina la planificaci ́o cl`assica amb l’habilitat de raonar sobre nom-

CONTENTS xix
bres enters o reals. En aquest context es poden codificar molts problemes reals amb restriccions sobre recursos.
La nostra implementaci ́o de les codificacions ha donat fruit a un plan- ificador anomenat Rantanplan, el qual preprocessa i tradueix problemes de planificaci ́o num`erics cap a f ́ormules SMT, finalment resolent-los amb el resoledor SMT que l’usuari tri ̈ı.
Tamb ́e s’inclouen resultats detallats d’alguns dominis ben coneguts i alguns de nous, per a demostrar que el nostre enfocament  ́es competitiu amb els planificadors num`erics exactes existents.