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 en este campo es en planificación, tanto de trayectorias como de tareas.

Un problema de planificación consiste en encontrar una secuencia de acciones que nos lleven de un estado inicial conocido a un estado final dado. Para ello, se pueden escoger acciones de un conjunto, teniendo en cuenta que la aplicación de estas tienen repercusión en el estado actual. Existen lenguajes para la representación de estados y acciones, por ejemplo STRIPS, y el problema de planificación puede ser equiparado con un SAT.

Base de datos:

• Comprobar la consistencia de una base de datos.

• Organización del conocimiento.

Procesamiento de textos:

• Reconocimiento de caracteres.

• Corrección automática de errores en el texto.

Una de los campos donde más se han usado los algoritmos para resolver fórmulas lógicas proposicionales en el diseño de circuitos. Se puede expresar en términos lógicos el funcionamiento de un circuito de tal forma que la demostración de que la fórmula es satisfactible nos ayude a la construcción del circuito que representa la fórmula. Además, se utiliza SAT para la minimización de puertas lógicas empleadas en la construcción del componente así como en la validación de su funcionamiento, es decir, utilizando este tipo de técnicas podemos demostrar que el circuito funcionara de modo apropiado.

Vamos a detallar a continuación algunos de los ejemplos citados anteriormente, de manera que formalicemos el problema en términos lógicos para convertirlo en una instancia del problema SAT y poder resolverlo usando uno de los múltiples algoritmos existentes.

3. Algoritmos existentes

Existen algoritmos correctos y complejos que resuelven el problema de satisfactibilidad. Al tratarse de un NP-Completo, se tiene que estos algoritmos son en la práctica intratable para una fórmula suficientemente ‘grande’. Así pues, también existen otro conjunto de algoritmos, mucho más eficientes en la práctica, que no garantizan encontrar el modelo de la fórmula de entrada en caso de este existir.

Algoritmos completos:

• Tablas de verdad.

Se trata del método más obvio para comprobar si existe un modelo para una fórmula. Dado que el conjunto de variables de una fórmula es finito, tenemos que el número posible de asignaciones a esas variables también es finito, en concreto dos elevado al número de variables que tengamos. El método de tableros de verdad va probando uno a uno cada posible modelo comprobando en cada caso si hace cierta la fórmula. En caso de encontrar alguno para y sabemos que la fórmula es satisfactible, en caso contrario sabemos que es falsable (no tiene ningún modelo). El gran problema de este algoritmo es su coste computacional, ya que en el caso peor tenemos que tratar todos los modelos posibles,

...