Thesis: Automatizando la combinación de lógicas SMT en modelos matemáticos para la resolución de problemas de optimización
| datacite.subject.fos | Engineering and technology::Electrical engineering, Electronic engineering, Information engineering::Automation and control systems | |
| dc.contributor.correferente | Gálvez Ramírez, Nicolás Sebastián | |
| dc.contributor.department | Departamento de Informática | |
| dc.contributor.guia | Castro Valdebenito, Carlos | |
| dc.coverage.spatial | Campus Casa Central Valparaíso | |
| dc.creator | Jorquera Navarro, Ignacio Alejandro | |
| dc.date.accessioned | 2026-07-24T14:05:26Z | |
| dc.date.available | 2026-07-24T14:05:26Z | |
| dc.date.issued | 2026-04 | |
| dc.description.abstract | La optimización ha sido un componente fundamental en la resolución de problemas complejos en ciencia, ingeniería y múltiples aplicaciones prácticas. En este trabajo se estudian problemas clásicos de satisfacción y optimización de restricciones (CSP/CSOP) mediante técnicas de Optimization Modulo Theories (OMT), poniendo especial énfasis en cómo la elección de la lógica de primer orden utilizada para modelar las restricciones afecta significativamente el desempeño del solver. Para ello, se desarrolló un flujo de trabajo para transformar modelos originalmente formulados en aritmética entera lineal (LIA) hacia otras lógicas: LRA, QF_BV y QF_ALIA, mediante reglas de traducción formales y mecanismos de consistencia entre lógicas heterogéneas. Sobre esta base, se incorporó un proceso de búsqueda guiado por Hill Climbing para seleccionar, entre combinaciones homogéneas y heterogéneas, aquellas combinaciones de lógicas capaces de mejorar el desempeño del solver. El enfoque fue evaluado en cinco problemas representativos: N-Queens, Unbounded Knapsack Problem, Nurse Scheduling Problem, Travelling Salesman Problem y Balanced Academic Curriculum Problem. Los resultados muestran que, en cuatro de los cinco problemas, existen combinaciones heterogéneas y homogéneas que superan consistentemente al modelo inicial basado únicamente en LIA, logrando reducciones de tiempo de hasta dos órdenes de magnitud, incrementando la cantidad de instancias resueltas y disminuyendo el tiempo requerido y el uso de memoria. Estos hallazgos confirman la hipótesis de que la mezcla automática de lógicas, junto con la transformación dinámica de restricciones a partir de un modelo inicial, constituye un mecanismo eficaz para potenciar el rendimiento de solvers OMT. Además, se demuestra que sería eficaz construir un sistema general de modelamiento que ajuste automáticamente la lógica usada en cada restricción según la estructura del problema, ampliando la eficiencia, aplicabilidad y capacidad adaptativa de los métodos de optimización. | es |
| dc.description.abstract | Optimization is fundamental in solving complex problems across science, engineering, and numerous applications. This work investigates Constraint Satisfaction and Optimization Problems (CSP/CSOP) using Optimization Modulo Theories (OMT) techniques. We emphasize how the choice of SMT logic used to model constraints significantly impacts solver performance. Building on this, we developed a novel workflow that systematically transforms models initially formulated in Linear Integer Arithmetic (LIA) into LRA, QF_BV, and QF_ALIA. This transformation uses formal encoding rules for consistency between these heterogeneous logics. We incorporated a Hill Climbing search to dynamically select logic combinations, homogeneous and heterogeneous, capable of improving solver performance. To assess this methodology, the approach was evaluated on five representative problems: N-Queens, Unbounded Knapsack, Nurse Scheduling, Traveling Salesman, and Balanced Academic Curriculum. The results consistently demonstrate that, across four of the five problems, the dynamically selected heterogeneous and homogeneous logic combinations significantly outperform the initial single-logic LIA model. These combinations achieve time reductions of up to two orders of magnitude, resulting in an increased number of solved instances while simultaneously reducing the required time and memory usage. These findings confirm the hypothesis that automatic logic mixing, coupled with dynamic constraint transformation from an initial model, is an effective mechanism for enhancing the performance of OMT solvers. Furthermore, they demonstrate the viability of building a general modeling system that automatically adjusts the logic for each constraint based on the problem’s inherent structure, thereby expanding the efficiency, applicability, and adaptive capacity of optimization methods. | en_US |
| dc.description.degree | Magíster en Ciencias de la Ingeniería Informática | |
| dc.description.sponsorship | ANID - FONDECYT de Iniciación - 11250273 | |
| dc.driver | info:eu-repo/semantics/masterThesis | |
| dc.format.extent | 192 páginas | |
| dc.identifier.barcode | MC_IJ_2026 | |
| dc.identifier.doi | 10.71959/nhef-az04 | |
| dc.identifier.uri | https://cris.usm.cl/handle/123456789/4461 | |
| dc.identifier.uri | https://doi.org/10.71959/nhef-az04 | |
| dc.language.iso | es | |
| dc.publisher | Universidad Técnica Federico Santa María | |
| dc.rights | Attribution-ShareAlike 4.0 International | en |
| dc.rights.uri | http://creativecommons.org/licenses/by-sa/4.0/ | |
| dc.subject | Lógicas de primer orden | |
| dc.subject | Modelamiento automático | |
| dc.subject | Optimization Modulo Theories | |
| dc.subject | Satisfacción de restricciones | |
| dc.title | Automatizando la combinación de lógicas SMT en modelos matemáticos para la resolución de problemas de optimización | |
| dc.type.driver | info:eu-repo/semantics/masterThesis | |
| dspace.entity.type | Tesis |
Política de Privacidad 
