Problema de la satisfactibilidad

PROBLEMA DE LA SATISFACTIBILIDAD (SAT)

KEVIN ALEJANDRO BETANCOURT ESCOBAR

CÓDIGO: 20141578004

UNIVERSIDAD DISTRITAL FRANCISCO JOSE DE CALDAS

FACULTAD TECNOLOGICA

TECNOLOGIA EN SISTEMATIZACION DE DATOS

LOGICA INFORMATICA

2014

PROBLEMA DE LA SATISFACTIBILIDAD (SAT)

SAT es un procedimiento que se usa para resolver, o decir si una formula proposicional dada en forma normal conjuntiva (FNC) es satis factible; es decir, dada una formula proposicional SAT determina si del conjunto de variables ver si son verdaderas.

SAT se le denomina el primer problema de la forma NP- completo, es decir, es un algoritmo computacional que se puede resolver en un tiempo polinómico o exponencial en el número de cláusulas de la formula, y esto fue descubierto por Stephen Cook en 1971, y dio lugar a decir su muchos otros problemas son del tipo NP- completo.

El hecho de que sea un algoritmo quiere decir que es un problema que se puede resolver computacional mente, existen varias formas como por ejemplo realizar el problema por tablas de verdad asignando valores falsos y verdaderos, pero esta resulta una forma muy ineficiente de realizarlo puesto que para un computador y su capacidad de procesamiento, un problema de este tipo que es 2 a la n variables se hace un proceso demasiado largo si son muchas las variables.

El problema SAT sirve para demostrar la satis factibilidad de una formula con variables no cuantificadas y que esta se encuentre en forma normal conjuntiva. Por supuesto existen otras extensiones del problema SAT las cuales están referidas o restringidas al número de variables en la fórmula de la forma normal conjuntiva, como por ejemplo el 3SAT y el SAT (k).

Algunos programas resolvedores de SAT son:

1.

Chaff es un algoritmo para resolución de las instancias del problema de satisfactibilidad Booleana en la programación. Fue diseñado por los investigadores de la Universidad de Princeton, EE.UU.

2.

GRASP es un conocido ejemplo solucionador SAT. Fue desarrollado por João Marques Silva, investigador informático portugués. Significa Genérico algoritmo de búsqueda para el Problema Satisfacibilidad.

3.

Satz es un conocido ejemplo solucionador SAT. Fue desarrollado por el profesor Chu Min Li, investigador de ciencias de la computación. El Z es la última versión de solucionadores SAT.

El algoritmo Davis-Putnam es un algoritmo que se utiliza para saber la satisfactibilidad de las fórmulas de lógica proposicional que se encuentran en forma normal conjuntiva, este método se desarrolló en el año 1960 por  Martin Davis y Hilary Putnam, y hoy en día sigue siendo la base para los solucionadores de SAT.

El Algoritmo Davis-Putnam (DP) también es conocido como el algoritmo de vuelta atrás y consiste en que se escoge un literal y se le asigna un valor de verdad y se simplifica la formula, de forma recursiva posteriormente se comprueba si la fórmula es satisfactible o no lo es, consiste en usar la regla de la división para hacer de un gran problema, problemas más pequeños. Al simplificar, se eliminan las cláusulas que son verdaderas en función de la formula, y todos los literales de las clausulas restantes se convierten en falsas.

El algoritmo DP tiene ciertas pautas para poder hacerlo más eficaz, como lo son la Unidad de Propagación, la cual consiste en que si una clausula es unitaria, solo puede ser satisfactible si se le asigna un valor de verdad y otra es la Eliminación Pura Literal, que consiste en que si una variable proposicional se produce con una sola polaridad en la formula, esta es pura y está a la vez puede ser asignada de tal forma  que donde se encuentre dentro de la formula hace que esa cláusula sea verdadera, así las cláusulas que contienen el literal puro pueden ser eliminadas y ni limiten la búsqueda.

En este algoritmo la satisfactibilidad está dada si no se encuentra una clausula vacía, y se hace satisfactible cuando todas las variables son asignadas sin generar la clausula vacía.