Anar al contingut (clic a Intro)
UdG Home UdG Home
Tancar
Menú

Tècniques codificadores de problemes de planificació

Tesi doctoral de Joan Espasa Arxer: "SMT techniques for planning problems". Direcció: Dr. Miquel Bofill Arasa i Dr. Mateu Villaret Auselle. Departament d'Informàtica, Matemàtica Aplicada i Estadística

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

Lectura de la tesi: 15/11/2018, Seminari de 3r cicle del departament d'IMAE-EPS IV 245

Notícies relacionades

Escull quins tipus de galetes acceptes que el web de la Universitat de Girona pugui guardar en el teu navegador.

Les imprescindibles per facilitar la vostra connexió. No hi ha opció d'inhabilitar-les, atès que són les necessàries pel funcionament del lloc web.

Permeten recordar les vostres opcions (per exemple llengua o regió des de la qual accediu), per tal de proporcionar-vos serveis avançats.

Proporcionen informació estadística i permeten millorar els serveis. Utilitzem cookies de Google Analytics que podeu desactivar instal·lant-vos aquest plugin.

Per a oferir continguts publicitaris relacionats amb els interessos de l'usuari, bé directament, bé per mitjà de tercers (“adservers”). Cal activar-les si vols veure els vídeos de Youtube incrustats en el web de la Universitat de Girona.