Distintos enfoques de modelamiento matemático para resolver problemas de optimización usando optimization Modulo Theories

Abstract

La optimización ha sido una parte fundamental de la humanidad desde sus orígenes, ya sea para administrar recursos o resolver problemas cotidianos. En esta tesis se abordan algunos problemas de optimización lineal y el impacto que tiene la decisión de diseño de elegir una lógica o dominio al momento de construir un modelo matemático. En particular, se modelan los problemas N-queens, Travelling Salesman Problem (TSP), Nurse Scheduling Problem (NSP), Balanced Academic Curriculum Problem (BACP) y Unbounded Knapsack Problem (UKP) usando las lógicas Closed linear formulas over Linear Integer Arithmetic (LIA), Closed linear formulas in Linear Real Arithmetic (LRA), Closed Quantifier-Free formulas over the theory of fixed-size BitVectors (QF_BV) y Closed Quantifier-Free formulas over the theory of Integer Arrays (QF_ALIA) definidas en la SMT-LIB, y luego se resuelven usando el solver para Optimization Modulo Theories (OMT) de Z3 con el objetivo de analizar y comparar cualitativa y cuantitativamente distintos enfoques matemáticos para conocer los beneficios y desventajas que presentan al momento de resolver problemas de OMT según el tipo de problema. En particular se busca: Modelar y resolver usando OMT al menos 3 problemas de satisfacción de restricciones usando al menos 3 lógicas distintas de Satisfiability Modulo Theories (SMT). Estudiar la opción de combinar distintas lógicas en un mismo problema para construir nuevos casos de estudio. Evaluar y comparar el rendimiento de los problemas resueltos. Dentro de lo logrado con esta propuesta se presenta evidencia empírica sobre diferencias en el desempeño al resolver Constraint Satisfaction Problems (CSP) y Constraint Satisfaction and Optimization Problems (CSOP) usando modelos basados en las lógicas mencionadas, sin embargo, la falta de patrones claros para determinar que lógica usar dependiendo del problema hace que este se vuelva un problema de ajustar parámetros para ver que lógica entrega mayores beneficios para el problema que se quiera resolver. También se presentan reglas para traducir problemas modelados con lógica LIA a LRA, QF_BV y QF_ALIA, lo que permite probar rápidamente cambios de dominio en modelos ya existentes para determinados CSP/CSOP. Optimization has been a fundamental part of humanity since its origins, whether to manage resources or solve everyday problems. This thesis addresses some linear optimization problems and the impact of the design decision to choose a logic or domain when building a mathematical model. In particular, the problems N-queens, Travelling Salesman Problem (TSP), Nurse Scheduling Problem (NSP), Balanced Academic Curriculum Problem (BACP) and Unbounded Knapsack Problem (UKP) using the logics Closed linear formulas over Linear Integer Arithmetic (LIA), Closed linear formulas in Linear Real Arithmetic (LRA), Closed Quantifier-Free formulas over the theory of fixed-size BitVectors (QF_BV) and Closed Quantifier-Free formulas over the theory of Integer Arrays (QF_ALIA) defined in the SMT-LIB, and then solved using the solver for Optimization Modulo Theories (OMT) of Z3 to analyze and compare qualitatively and quantitatively different mathematical approaches to know the benefits and disadvantages they present when solving OMT problems according to the type of problem. In particular, we are looking for: Model and solve using OMT at least 3 constraint satisfaction problems using at least 3 different logics from Satisfiability Modulo Theories (SMT). Analyze the option of mixing different SMT logics in the same problem to build new case studies. Evaluate and compare the performance of the solved problems. Within what was achieved with this proposal, empirical evidence is presented on differences in performance when solving Constraint Satisfaction Problems (CSP) and Constraint Satisfaction and Optimization Problems (CSOP) using models based on the logic mentioned above, however, the lack of clear patterns to determine which logic to use depending on the problem makes this become a problem of adjusting parameters to see which logic provides greater benefits for the problem to be solved. Rules for translating problems modeled with LIA logic to LRA, QF_BV, and QF_ALIA are also presented, allowing you to quickly test domain changes in existing models for certain CSP/CSOP.