Optimization Modulo Theories

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.