DSpace DSpace UPC
 English   Castellano   Català  

Treballs academics UPC >
Màsters Oficials >
Master in Artificial Intelligence - MAI (Pla 2006) >

Empreu aquest identificador per citar o enllaçar aquest ítem: http://hdl.handle.net/2099.1/14204

Arxiu Descripció MidaFormat
Roc Olier.zipmemòria725,91 kBZIP FileVeure/Obrir

Títol: Optimization Modulo Theories
Autor: Oliver Vendrell, Roc
Tutor/director/avaluador: Oliveras Llunell, Albert Veure Producció científica UPC; Rodríguez-Carbonell, Enric
Universitat: Universitat Politècnica de Catalunya
Càtedra /Departament: Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics
Matèries: Àrees temàtiques de la UPC::Matemàtiques i estadística::Investigació operativa::Optimització
Mathematical optimization
OMT (Optimization Modulo Theories)
Optimització matemàtica
Data: gen-2011
Tipus de document: Master thesis
Resum: Since ancient times, humanity has sought methods for optimizing their resources and their costs, leading to the study of optimization problems. In this thesis Discrete Optimization Problems are dealt with, which are well-known to have a huge economical impact. In order to tackle these problems, we introduce the Optimization Modulo Theories (OMT) framework, an extension of Satisfiability Modulo Theories (SMT). OMT allows one to model Discrete Optimization Problems as optimization problems of a cost function subject to a quantifier-free first-order formula whose atoms are constraints of Linear Integer Arithmetic (LIA), i.e., linear inequalities over integer variables. Thus, this language exploits the advantages of propositional logic and LIA. Two methods based on the DPLL(T ) approach for SMT are proposed so as to solve problems expressed in OMT: first, by means of an off-the-shelf integer linear programming tool used as a theory solver; and second, by adding new optimization functionalities to satisfiability LIA-solving algorithms originally developed for SMT. Finally, in order to assess the practical value of these approaches, an experimental evaluation has been carried out, whose results are reported in this document.
URI: http://hdl.handle.net/2099.1/14204
Condicions d'accés: Open Access
Apareix a les col·leccions:Master in Artificial Intelligence - MAI (Pla 2006)

SFX Query

Aquest ítem (excepte textos i imatges no creats per l'autor) està subjecte a una llicència de Creative Commons Llicència Creative Commons
Creative Commons


Valid XHTML 1.0! Programari DSpace Copyright © 2002-2004 MIT and Hewlett-Packard Comentaris
Universitat Politècnica de Catalunya. Servei de Biblioteques, Publicacions i Arxius