Optimization Modulo Theories
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2099.1/14204
Tipus de documentProjecte Final de Màster Oficial
Data2011-01
Condicions d'accésAccés obert
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement-NoComercial-SenseObraDerivada 3.0 Espanya
Abstract
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.
TitulacióMÀSTER UNIVERSITARI EN INTEL·LIGÈNCIA ARTIFICIAL (Pla 2009)
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
Roc Olier.zip | memòria | 725,9Kb | application/zip | Visualitza/Obre |