SMT techniques for planning problems

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 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

La planificació automàtica és una disciplina dins de la intel·ligència artificial que pot ser descrita com el procés 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àries per assolir un objectiu donat. Encara que les aproximacions a la planificació automàtica clàssica han tingut un gran èxit, les necessitats que tenen moltes aplicacions al món real estan per sobre de les seves possibilitats.

Existeixen molts formalismes a l’àrea de la planificació automàtica que poden expressar totes les necessitats que tenen aquest tipus de problemes. Aquesta enorme varietat de problemes van des de la planificació clàssica, passant per problemes expressats amb processos de decisió de Markov parcialment observables, problemes de percepció i decisió en temps real o problemes que incorporen raonament temporal i numèric. Existeixen un ampli ventall de tècniques 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ó híbrida. Exactament, la combinació de la planificació proposicional amb extensions per a poder raonar sobre diferents teories, tals com l’aritmètica real o entera.

Aquesta tesi presenta un conjunt de tècniques per a codificar de manera eficient problemes de planificació que involucren raonament a nivell proposicional així com raonament amb teories de fons. Per abordar el raonament sobre les diferents teories, farem anar SAT Modulo Teories (SMT), una extensió de SAT que permet al resoledor, de manera modular, raonar sobre símbols no proposicionals pertanyents a teories de fons. Aquest marc és interessant perquè és prou expressiu per a poder traduir molts problemes provinents del món real.

L’objectiu principal és millorar l’estat de l’art de la planificació automàtica mitjançant SMT, a través de la codificació dels problemes de planificació a SMT. El focus de la tesi és especialment en la planificació numèrica, on es combina la planificació clàssica amb l’habilitat de raonar sobre nombres enters o reals. En aquest context es poden codificar molts problemes reals amb restriccions sobre recursos.

La nostra implementació de les codificacions ha donat fruit a un planificador anomenat Rantanplan, el qual preprocessa i tradueix problemes de planificació numèrics cap a fòrmules SMT, finalment resolent-los amb el resoledor SMT que l’usuari triï.

També s’inclouen resultats detallats d’alguns dominis ben coneguts i alguns de nous, per a demostrar que el nostre enfocament és competitiu amb els planificadors numèrics exactes existents