Defensa Tesis Licenciatura Esteban Lanzarotti

• Título: Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
• Directores: Juan Pablo Galeotti, Sergio Mera
• Jurados: Marcelo Frías, Ricardo Rodriguez
• Resumen:

Identificar el núcleo de insatisfactibilidad (Unsat Core) de un modelo Alloy es bastante útil en varios escenarios. En este trabajo se extiende este concepto al Hot Core, una aproximación heurística al Unsat Core que permite al usuario obtener información cuando el proceso Sat-Solving de Alloy es interrumpido. El hecho de que verificar especificaciones usando SAT sea NP-Completo hace de Hot Core una herramienta muy interesante, dado que es bastante frecuente que el usuario interrumpa el proceso por haber excedido el tiempo de espera. Exhibimos resultados experimentales satisfactorios que validan nuestros propósitos y muestran el buen funcionamiento de la heurística.