Resumen:
Identicar el núcleo de insatisfactibilidad (unsat core) de un modelo Alloy es bastante útil en varios escenarios [SSJ+03]. 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 vericar especicaciones 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.
Citación:
---------- APA ----------
Lanzarotti, Esteban Omar. (2010). Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti
---------- CHICAGO ----------
Lanzarotti, Esteban Omar. "Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2010.https://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000454_Lanzarotti.pdf
Distrubución geográfica