Optimización Genética de Problemas SAT

Abstract

El problema de satisfactibilidad (SAT) tiene relevancia desde un contexto teórico y práctico. En el contexto teórico el problema SAT es fundamental para el análisis de la complejidad computacional de diversos problemas. En el contexto práctico, la solución de problemas SAT es requisito fundamental de diversos métodos de razonamiento. De esta manera el encontrar un procedimiento eficiente para resolver el problema SAT es muy importante. En esta tesis se plantea un enfoque novedoso para resolver problemas SAT usando algoritmos genéticos (AG), el algoritmo está basado en el reordenamiento de las variables que intervienen en las cláusulas del problema SAT, y la aplicación posterior de un AG tradicional. Los resultados presentados en este trabajo evidencian que el enfoque propuesto es consistentemente mejor que un AG tradicional para resolver problemas SAT duros. Por otra parte, las principales aportaciones de esta tesis son: - La implementación de un algoritmo de Recocido Simulado que permite resolver el Problema de Minimización del Ancho de Banda de Grafos (PMABG) de manera competitiva. - El uso de una métrica especial para el PMABG (7) que es substancialmente mejor que la medida empleada comÚnmente (B), y además permite bandear grafos pesados. - Lograr identificar las características que debe cumplir un buen generador de casos de prueba para problemas SAT. Estas son: garantizar el control del grado de repetibilidad de las variables que intervienen en el problema; proveer un mecanismo que garantice el balance entre las apariciones positivas y negativas de cada variable del problema; evitar generar cláusulas triviales, así como cuidar que la razón entre cláusulas y variables sea aproximadamente entre 2 y 4. - Un enfoque novedoso para generar casos de prueba duros del problema SAT a partir de su analogía geométrica con grafos.