Sistema para generar satisfactibilidad en fórmulas proposicionales
Date
2022-12
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Benemérita Universidad Autónoma de Puebla
Abstract
"El problema de satisfactibilidad proposicional es un caso especial del área de la Inteligencia Artificial y tiene una relación directa con la demostración Automática de Teoremas. El problema SAT es un problema de clase NP-completo, por lo que muchos han tratado de identificar casos restringidos para el problema SAT, así como la versión de optimización y conteo: problemas MaxSAT y #SAT, tratando de que estos puedan ser resueltos eficientemente. Los problemas NP-completo son los problemas que caracterizan la clase de tal forma que al encontrar una solución del problema SAT se pueden resolver los demás problemas de la clase; ya que se puede hacer una transformación en tiempo polinomial al problema correspondiente. Este trabajo de tesis es proponer un sistema para #SAT modelando una fórmula proposicional en FNC y generar una propuesta para la consistencia de F cuando no es consistente. Se presenta un algoritmo y su implementación computacional para contar el número de asignaciones de una fórmula F en FNC, lo que significa que, si la fórmula tiene modelos, entonces F es consistente o satisfactible y en caso contrario se aplica un algoritmo que genera una tabla donde se indica que cláusula es necesario quitar para lograr la satisfactibilidad".
Description
Keywords
Citation
Collections
Document Viewer
Select a file to preview:
Can't see the file? Try reloading