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

Mostrar todas las versiones(3)

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 Allo...

Descripción completa

Detalles Bibliográficos
Autor principal: Lanzarotti, Esteban Omar
Otros Autores: Galeotti, Juan Pablo
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2010
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id seminario:seminario_nCOM000454_Lanzarotti
record_format dspace
spelling seminario:seminario_nCOM000454_Lanzarotti2025-05-09T18:45:23Z Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL Lanzarotti, Esteban Omar Galeotti, Juan Pablo Mera, Sergio Fernando 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. Fil: Lanzarotti, Esteban Omar. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2010-04-21 info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion application/pdf spa info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv spa
description 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.
author2 Galeotti, Juan Pablo
author_facet Galeotti, Juan Pablo
Lanzarotti, Esteban Omar
format Tesis de grado
Tesis de grado
publishedVersion
author Lanzarotti, Esteban Omar
spellingShingle Lanzarotti, Esteban Omar
Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
author_sort Lanzarotti, Esteban Omar
title Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
title_short Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
title_full Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
title_fullStr Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
title_full_unstemmed Una generalización de Unsat Core para algoritmos de Sat-Solving basados en DPLL
title_sort una generalización de unsat core para algoritmos de sat-solving basados en dpll
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2010
url https://hdl.handle.net/20.500.12110/seminario_nCOM000454_Lanzarotti
work_keys_str_mv AT lanzarottiestebanomar unageneralizaciondeunsatcoreparaalgoritmosdesatsolvingbasadosendpll
_version_ 1831983711590023168

Ejemplares similares