Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL

Lanzarotti, Esteban Omar

Navegar

Documento Últimos publicados Autor Año Título Obtenido - Año Departamento - Año Director y Director Asistente Jurado Consejero de Estudios Palabras Clave

Colección

Datos Estadísticas

Tesis de Grado

Lanzarotti, Esteban Omar. "Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL" . (2010). Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.

Registro Resumen Citación Estadísticas

Registro:

Documento:	Tesis de Grado
Título:	Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
Autor:	Lanzarotti, Esteban Omar
Editor:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Publicación en la web:	2023-09-12
Fecha de defensa:	2010-04-21
Fecha en portada:	[2010]
Grado Obtenido:	Grado
Título Obtenido:	Licenciado en Ciencias de la Computación
Director:	Galeotti, Juan Pablo; Mera, Sergio Fernando
Idioma:	Español
Formato:	PDF
Handle:	http://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti
PDF:	https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000454_Lanzarotti.pdf
Registro:	https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000454_Lanzarotti
Ubicación:	Dep.COM 000454
Derechos de Acceso:	Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. 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 http://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti

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