Browsing by Author "Jorquera Navarro, Ignacio Alejandro"
Now showing 1 - 1 of 1
- Results Per Page
- Sort Options
Thesis Distintos enfoques de modelamiento matemático para resolver problemas de optimización usando optimization Modulo Theories(Universidad Técnica Federico Santa María, 2023) Jorquera Navarro, Ignacio Alejandro; Castro Valdebenito, Carlos; Departamento de Informática; Galvez Ramirez, Nicolas SebastianLa 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.
Política de Privacidad 
