Problema De La Satisfactibilidad "SAT"

PROBLEMA DE LA SATISFACTIBILIDAD

1. ¿Qué es SAT?

Se denomina problema de la satisfactibilidad a demostrar la consistencia (o inconsistencia) de un conjunto finito de fórmulas.

Métodos semánticos para probar en lógica proposicional:

• Consistencia: obtener interpretación

• Inconsistencia y validez: tablas de verdad, refutación.

En ciencias de la computación , satisfactibilidad (a menudo escrito en mayúsculas, o SAT abreviado) es el problema de determinar si las variables de un determinado booleano fórmula (Utilizado Para enfatizar la naturaleza binaria de un problema, se refiere con frecuencia como satisfactibilidad booleano o proposicional.) puede ser asignado de tal manera que para que la fórmula se evalúa como TRUE (verdadero). Igualmente importante es determinar si no existen tales asignaciones, lo que implicaría que la función expresada por la fórmula es idéntica FALSE (falso) para todas las asignaciones de variables posibles. En este último caso, diríamos que la función es insatisfactible, de lo contrario es satisfacible. Por ejemplo, la fórmula A y B es satisfacible, porque uno puede encontrar los valores a = TRUE y b = TRUE, lo que hace un VERDADERO.

Variantes del problema SAT:

Existen multitud de variantes del problema SAT, estos problemas surgen de imponer restricciones a la fórmula en FNC de la que se partía inicialmente.

Además, la mayoría de problemas NP-Completos son reducibles en tiempo polinomial a SAT. Esto quiere decir que existe un algoritmo que transforma una instancia del problema en SAT o viceversa y además ese algoritmo es polinomial. Estos problemas, tanto las variantes de SAT como los reducibles a SAT en tiempo polinomial, se pueden considerar equivalentes a SAT en el sentido de que un algoritmo que trabaje eficientemente para SAT resolvería cualquiera de los problemas también eficientemente. Así, es de vital interés la resolución del problema SAT de forma eficiente ya que a su vez estaríamos resolviendo la mayoría de problemas NP-Completos.

Algunos de las variantes y problemas equivalentes a SAT son las siguientes:

• SAT (k): Dada una fórmula en FNC con a lo sumo k literales por cláusula, determinar si esta es satisfactible.

• SAT*(k): Dada una fórmula en FNC con exactamente k literales por cláusula, determinar si esa es satisfactible.

• SAT (3): Dada una fórmula en FNC con a lo sumo 3 literales por cláusula, determinar si esta es satisfactible.

• Vertex Cover: Dado un grafo G y un número natural k, determinar si hay un recubrimiento de vértices de G de tamaño k.

• SUBSET-SUM: Dado un conjunto A, una función de peso w y un número natural k, determinar si existe un subconjunto B de A tal que w (B) = A.

• PARTICIÓN: Dado un conjunto A y una función de peso w, determinar si existe una partición de A {B,C} tal que w(B) = w(C).

• 3-COL: Determinar si un grafo es 3-coloreable.

• HAM-PATH: Dado un grafo G y dos nodos x e y pertenecientes a G, determinar si existe un camino Hamiltoniano de x a y.

Estos son solo algunos ejemplos de problemas equivalentes a SAT. Existen multitud de más problemas interesantes reducibles en tiempo polinomial al problema de satisfactibilidad. Esto hace que SAT tenga infinidad de utilidades prácticas en diversos campos como matemáticas, inteligencia artificial o robótica.

2. ¿Para qué se utiliza?

El problema de satisfactibilidad de fórmula proposicional tiene multitud de aplicaciones, debido a que como hemos visto, el problema se puede equiparar fácilmente con muchos otros. Es por eso que existe en la actualidad mucho interés en resolver SAT de manera eficiente, ya que ese método de resolución sería aplicable a un gran número de problemas en muchísimas áreas.

Mostramos aquí una relación de los principales problemas donde se usa SAT, a continuación se detallarán algunos de ellos, viendo de qué forma podemos modelar el problema mediante fórmulas proposicionales.

Matemáticas:

• Encontrar relaciones n-areas.

• Detectar isomorfismos en grafos.

Esto consiste en dado dos grafos, determinar si existe una relación biyectiva entre uno y otro de tal forma que se mantenga la adyacencia, estructura, ciclos y caminos.

• Coloración de grafos

• Criptografía matemática. De hecho, si se encontrara un algoritmo eficiente para cualquier instancia de SAT, muchos de los algoritmos de encriptación se podría romper.

• Otros problemas relacionados con los grafos, como el problema del viajante, o un problema parecido al de isomorfismo de grafos que consiste en decidir cuando dos autómatas son equivalentes.

Computación e inteligencia artificial:

• El problema de satisfacción de restricciones. Este tipo de problemas vienen definidos por un conjunto de variables con un conjunto de dominios asociados. Además existen una serie de restricciones. La solución es encontrar una asignación de las variables a un valor de su dominio equivalente de tal forma que se satisfagan las restricciones.

Existen multitud de problemas reales que pueden ser expresados en término de satisfacción de restricciones: problema de las N-reinas, repartición de tareas o por poner un ejemplo curioso, el Sudoku.

• Programación lógica

• Criptoaritmética.

En todos estos problemas la tarea consiste en sustituir cada letra por un dígito, de modo que las cuentas (operaciones) sean correctas. Por ejemplo:

SEND + MORE = MONEY.

• Sistemas de producción. Consiste en deducir nuevo conocimiento a partir de un conocimiento base, que será expresado normalmente mediante un conjunto de fórmulas. Un buen ejemplo de la capacidad de este tipo de sistemas es CLIPS (Sistema de producción integrado en el lenguaje C).

Visión artificial:

• Multitud de problemas y algoritmos relacionados con este campo podrían hacer uso de SAT para su resolución. Algunos problemas concretos podrían ser: reconocimiento de imágenes, etiquetado de líneas y bordes, restauración de imágenes o reconocimiento de patrones.

Otro campo a destacar donde se usan algoritmos relacionados con SAT es en la robótica. Por ejemplo, todas las aplicaciones en cuanto a visión artificial citadas anteriormente son susceptibles de ser utilizadas a la hora de diseñar un robot. Pero quizás la tarea más importante donde se aplica la resolución de fórmulas proposicionales

...