lunes, 14 de julio de 2014
Problema de la Satisfactibilidad SAT
PROBLEMA DE LA SATISFACTIBILIDAD (SAT)
El problema SAT se puede enunciar como sigue: dada una fórmula proposicional enforma normal conjuntiva, determinar si esta es satisfactible.
Así, el problema consiste en decidir, dada una FNC F, si existe alguna valoración deverdad V sobre el conjunto de variables de la fórmula tal que V(F) = 1.
Una de las características mas importantes del problema es que es NP-Completo, es decir, el tiempo de ejecución para un algoritmo que resuelva el problema es exponencial en el número de cláusulas de la fórmula. Este resultado fue demostrado por S.A. Cook en 1971, dando lugar al nacimiento de la teoría de la complejidad.
Ensayo SAT
EL PROBLEMA DE LA SATISFACTIBILIDAD
SAT
La
tecnología es uno de los factores de más importancia para el ser humano, esta
es capaz de brindarle múltiples capacidades y herramientas para una eficaz
solución de los diversos problemas que abarcan su entorno, desde el más mínimo
problema hasta el más complejo.
La
tecnología abarca varias ramas que se encargan de los diversos campos de la
problemática humana, uno de estas ramas es la lógica computacional también
conocida como la lógica matemática, la cual consiste en el estudio matemático
de la lógica y en la aplicación de dicho estudio a otras áreas de la matemática
y de las ciencias; la lógica matemática es implementada en el desarrollo de los
circuitos computacionales, la programación lógica y el análisis y optimización
de algoritmos y abarca temas de estudio como los sistemas lógicos (lógica
proposicional y de predicados), la deducción natural y el problema de la
satisfactibilidad (SAT).
El
problema de la satisfactibilidad (SAT) es un problema computacional no
polinomial completo (NP-Completo) de gran estudio ya que genera la búsqueda de algoritmos realmente eficientes
para la solución de problemáticas orientadas a diversos campos computacionales
como lo son el diseño de circuitos, la inteligencia artificial, la verificación
de software y hardware entre otros. Encontrar la solución del problema SAT
mediante el análisis de los diversos métodos y técnicas empleados permite
encontrar las más eficaces formas de abordar el problema, aunque son diversos
los métodos de solución uno de los más importantes y representativos en el
esquema Davis-Putnam, el cual es implementado con la inclusión de nuevas
herramientas por los diversos resolvedores obtenidos en la actualidad que
buscan mejorar su rendimiento, algunos de estos resolvedores son: Berkmin,
Grasp, Chaff, GSAT, WalkSat, entre otros.
En
este ensayo se presenta una investigación destinada a trabajador todo lo
relacionado con el problema de la satisfactibilidad SAT, desde su concepto,
utilización, el método de solución del esquema Davis-Putnam hasta los diversos
tipos de resolvedores destinados a encontrar solución a este problema.
El
problema de la satisfactibilidad SAT es definido de la
siguiente forma: Establecida una formula en forma normal conjuntiva (FNC), este
se encarga de determinar si la fórmula establecida es satisfactible; por lo
tanto el problema consiste en decidir si en la fórmula establecida existe algún
valor de verdad (V) asignado a las variables booleanas de la formula tal que la
misma sea igual a uno: V(F) = 1.
El
problema de la satisfactibilidad SAT es caracterizado por ser un problema
NP-Completo, el cual establece que el tiempo de ejecución para el algoritmo
encargado de resolverlo es exponencial en el número de clausulas de la fórmula
FNC.
Aplicaciones:
Las
aplicaciones del problema SAT son múltiples pues este es trabajado en diversos
campos; inicialmente es utilizado en los problemas NP-Completos como la
coloración de grafos, el problema del agente viajero, entre otros.
Como
ya fue mencionado el problema de la satisfactibilidad abarca aplicaciones en
múltiples campos algunos de ellos son:
·
Matemáticas:
En
el cual es aplicado para cierre de transitivos, detección de gráficos y
subgraficos isomorfos, el problema de autónomas homomorfos, búsqueda de arboles
de expansión, solución del problema del agente viajero, el problema de colorear
gráficos, criptología matemática y lógica aritmética.
·
Inteligencia
artificial y ciencias de la computación: En estos campos
trabaja diversos problemas como la inferencia extendida, la lógica de la
programación, la inferencia de sintetización de hipótesis, el mantenimiento
real, el problema de la restricción de la satisfacción, el procesamiento de
información semántica, redes de computadores neuronales, entre otros.
·
Robótica
y cibernética: El problema SAT es implementado en
estos campos para el problema empaquetado, el problema de visión, planes de
problemas de trabajos, entre otros.
·
Sistema
de base de Datos: En el cual se utiliza para las
operaciones con objetos, la optimización de preguntas, el mantenimiento de
bases de datos, la veracidad y credibilidad de mantenimiento, el control de
concurrencia, el sistema de base de datos distribuida, entre otros.
·
Gráficos
computarizados: Es aplicado en la construcción de
dibujos bidimensionales y tridimensionales de diversos objetos gráficos de
restricciones así como considerando las características geométricas de este
ultimo tipo de objetos.
·
Manufacturización
de ayuda computarizada: Utilizado en diseños de modelado
solido, en el diseño celular del sistema de manufacturización, para
programando, planes de trabajo, trabajos de configuración e identificación de
un objeto tridimensional.
·
Procesador
de textos: En el cual se encarga de la
identificación de caracteres ópticos, restringidos de modelos gráficos,
identificación de textos impresos o manuscritos y finalmente la corrección
automática de los errores encontrados en el texto.
·
Arquitectura
de computadores: Atribuido al diseño en el cual es
implementado en la optimización de grupos de instrucciones así como la de
controles de computadoras y de sistemas compiladores también en el diseño de
circuitos lógico-aritméticos, análisis de consistencias en el flujo de datos,
procesamiento paralelo y distribuido y asignaciones de módulos de datos.
·
Diseño
de circuitos integrados: Atribuido a la automatización en la
que abarca problemas como el modelado de circuitos, la asignación de estados,
minimización de estados, entrada y salida de información, particiones lógicas,
esquemas de circuitos y su correspondiente ubicación, minimización lógica,
asignaciones de pines, generación de pruebas y verificación, análisis de
interconexión, ruteo, compactación, optimización del desempeño, entre otros.
También
es aplicado en las redes de alta velocidad, las comunicaciones y en la
seguridad.
Métodos
de solución:
La
satisfactibilidad de una formula puede ser verificada de una manera
combinatoria; sin embargo, esto no es muy factible.
Gu,
Purdom, Franco y Wah se encargaron de presentar una perspectiva general de la
búsqueda de algoritmos, los cuales son clasificados según los valores de las
variables tratadas, diviendose así en discretos y continuos, que a su vez con
restringidos y no restringidos.
Los
algoritmos discretos restringidos tratan a una formula SAT como una instancia
de un problema de decisión restringido, para el cual se aplican procedimientos
de búsqueda discreta e inferencia con los que tratan el problema. En los
algoritmos restringidos el número de las clausulas no satisfechas son
formuladas como el valor de una función objetivo.
Los
algoritmos de programación restringida tienen como base el hecho de que una
formula con un número de clausulas no satisfechas puede trasladarse a
instancias de programación entera y ser solucionados posiblemente mediante el
uso de la relajación de la programación lineal.
Otras
formas de clasificación de los algoritmos para la solución son los métodos
completos y los métodos incompletos.
Métodos
completos: Estos métodos realizan una exploración
a través del espacio de búsqueda de todas y cada una de las interpretaciones
posibles con el fin de probar si una fórmula en FNC es satisfactible o
Insatisfactible.
En
estos métodos completos uno de los más representativos e implementado es el
método Davis y Putnam, el cual elimina una a una cada variable generando así
todos los posibles resolventes basados en las variables seleccionadas y
borrando todas las clausulas en las que esta variable aparece, generando así en
cada paso un subproblema con una variable menos, haciendo uso de la literal pura y la regla de la
clausula unitaria.
Procedimiento
de Davis – Putnam:
Este
método consiste en el uso repetitivo de cuatro reglas que permiten realizar la
comprobación de la insatisfactibilidad de un determinado conjunto de cláusulas.
Estas reglas permiten reducir la cantidad de clausulas hasta llegar al punto en
que se obtiene una fórmula que es válida (satisfactible) o que es
Insatisfactible y que tiene el mínimo numero de cláusulas.
A
continuación se dará explicación a cada una de estas reglas:
Estableciendo
a S como un conjunto de clausulas
generadas en el universo de Herbrand.
1.
Regla de la Tautología: Borra todas
las clausulas aterrizadas de S que
son tautologías, por lo tanto el resultando S’
es Insatisfactible si y solo si S lo
es.
2.
Regla de la Literal Unitaria: Al
existir una cláusula aterrizada unitaria l
en S, se obtiene S’ al borrar aquellas clausulas en S que contengan a l. En el caso en que S’
este vacio la fórmula será satisfactible por lo contrario se obtendrá un
conjunto S’’ al borrar l de S’’
y la formula será insatisfactible si y solo si S lo es.
3.
Regla de la Literal Pura: Una
literal l en una clausula aterrizada S, se dice que es puro en S, si y solo si la literal l no aparece en ninguna clausula
aterrizadas en S. En el caso en que
una literal l sea pura en S, debe proceder a borrarse todas las
clausulas aterrizadas que contengan a l. El
conjunto S’ resultante de esto será
satisfactible si y solo si S lo es.
4.
Regla de Expansión: Si el conjunto S puede ser opuesto en la forma (
donde 
; 
y R están libre de l y 
l, entonces se obtienen
los conjuntos 
y 
, S será insatisfactible si y solo si (
es insatisfactible, esto significa que 
también lo son.
donde ; y R están libre de l y l, entonces se obtienen
los conjuntos y , S será insatisfactible si y solo si ( es insatisfactible, esto significa que también lo son.
Algoritmo David – Putnam:
0 function unit-resolve ( Γ: set of
clause) : set of cluse;
1 var L:
literal;
2 var C:
clause;
3 begin
4 while $ {L} Î Γ and Ï Γ do
5 begin
6 Γ := {C | L Ï C Î Γ};
7 Γ := {C – {L} | C Î Γ}
8 end
9 return
( Γ )
10 end;
Resolvedores
(Algoritmos completos): Algunos otros
resolvedores presentes en esta categoría son:
•
Berkmin: Este
resolvedor se caracteriza por introducir nuevas ideas en lo que se refiere a la
toma de decisiones y en el manejo de la base de datos de las cláusulas. Para
ello crea un rango más amplio de clausulas las cuales se ven involucradas en el
conflicto que las que normalmente utilizan los demás resolvedores y las
organiza en una fila cronológicamente. Luego abandona la búsqueda actual para
eliminar de la base de datos una cláusula, para lo cual se basa no solo en el
tamaño (cantidad de literales en la fórmula)
si no también en la presencia de cláusulas en el conflicto y su
antigüedad.
Del
resolvedor Chaff toma la idea de reducir los conflictos producidos por las
anteriores clausulas, en el proceso de toma de decisiones y en el concepto de
reinicios que permite abandonar la búsqueda en un determinado momento para
reiniciarla en otro punto del espacio de búsqueda. Implementa una heurística
que determina cual asignación de la variable seleccionada deberá examinarse
primero.
•
Grasp: Este
es un algoritmo determinístico completo, el cual se basa en el esquema
David-Putnam. Este algoritmo incorpora varias técnicas para reducir el árbol de
búsqueda. Se caracteriza por implementar el manejo de BCP (Boolean Constraint
Propagation) mediante un grafo de implicaciones, aprendizaje de nuevas
clausulas y un backtracking no cronológico.
Algoritmo:
1. If (Decide (d) = =SUCCESS)
Return
SUCCESS;
2. while (TRUE) {
2.1. if
(Deduce (d) ¡= CONFLICT) {
if
(Search ( d + b
) = = SUCCESS)
return SUCCESS;
else if ( b
!= d ) Erase ( ); return CONFLICT; }
2.1. if
(Diagnose ( d , b
) = = CONFLICT)
Erase ( ); return CONFLICT; }
2.2.
Erase ( );
3.
fin
La
estructura de búsqueda para SAT consta de cuatro operaciones básicas: decide,
deduce, diagnostica y borra.
•
Decide: En este procedimiento el algoritmo permite seleccionar una asignación
encada estado del proceso de búsqueda.
•
Deduce: En este procedimiento se automatiza la regla BCP para lo que es
implementado un grafo de implicaciones. Ej. Para la cláusula w
= (x V ¬ y),
si Y = 1, entonces se tiene que x = 1. Además para una variable x que ocurra en
una cláusula, se asigna el valor 0 a todas las otras literales.
•
Diagnostica: En este procedimiento Grasp lo automatiza de la siguiente forma:
antes de que se presente el conflicto, analiza el grafo de implicaciones en el
nivel actual de decisión. Adiciona nuevas cláusulas que permiten la prevención
de la ocurrencia del mismo conflicto mediante aprendizaje para después regresar
al nivel que contiene la variable responsable del conflicto.
•Chaff:
Este
puede ser llamado como el padre de las nuevas generaciones de resolvedores.
Este resolvedor presenta como aporte central la optimización del BCP.
Chaff
implementa el algoritmo D&P, aumentado con reinicios, backtracking no
cronológico y aprendizaje dirigido por conflictos. Su esquema puede resumirse
en cindo procesos básicos:
1. Cada
variable en cada polaridad tiene un contador inicializado en 0
2. Cuando
una cláusula es adicionada a la base de datos, el contador asociado con cada
literal en la cláusula es incrementado.
3. La
variable y la polaridad con el contador mayor es seleccionada en cada nivel de
decisión.
4. Periódicamente
todos los contadores son divididos por una constante (por defecto 2).
El
resolvedor Chaff depuro los cuatro aspectos fundamentales de la búsqueda SAT
para hacerlo mucho más rápido, luego fue repetido y se realizo un balance.
Utiliza
principios de implementación lazzy en los que se demora el cómputo lo más
posible sin violar la semántica del algoritmo. Se selecciona el caso común más
rápido, aunque este viole los criterios de la semántica para los casos poco
frecuentes.
Finalmente
en el principio de BCP, se observa qué causa una implicación y cuándo puede
ocurrir. Cuando todas las literales de una clausula con asignadas a 0, menos
una, hay implicación. Para una clausula N, esta puede ocurrir solamente en una
N-1 asignaciones de tal modo que pueden ignorarse las primeras N-2
asignaciones, así solo se observaran dos literales de la clausula.
Métodos
incompletos: Este
tipo de métodos no tienen la capacidad de probar la insatisfactibilidad pero se
comportan muy bien al maximizar la cantidad de cláusulas satisfechas. En los
casos en los que el problema sea satisfactible logran probarlo más rápidamente
que algún método completo.
Resolvedores
(Algoritmos incompletos): En
este tipo de algoritmos si una solución es encontrada, la fórmula es declarada
como satisfactible y el algoritmo finaliza con éxito. Encaso contrario cuando
el algoritmo falla al encontrar la solución, no es posible sacar ninguna
conjetura. Entre los algoritmos más representativos se encuentran GSAT y
WalkSat.
•GSAT: Este resolvedor realiza una búsqueda
local para lograr satisfacer las asignaciones de un conjunto de cláusulas
proposicionales.
El
algoritmo inicia con una generación aleatoria de asignaciones de verdad. Luego
cambia la asignación de la variable que conlleva a un incremento en el total de
cláusulas satisfechas. Estos cambios (flips) se repiten hasta encontrarse una
satisfacción a la asignación o en el momento en el que se haya alcanzado un
número máximo de flips asignado.
Algoritmo:
Empieza
for i := to MAX-TRIES
T:= Una asignación de verdad
generada aleatoriamente
for j := 1 to MAX-FLIPS
if
T satisface a then return T
p .= una
variable proposicional tal que un cambio en esta asignación de verdad da lugar al mayor
incremento en el número total de cláusulas a que son satisfechas por T
T := T con la
asignación de verdad de p invertida.
end for
end for
return “no se encontró asignación satisfactoria”
end
El
resolvedor GSAT se caracteriza por la presencia de movimientos laterales,
también se caracteriza porque la variable cuya asignación es cambiada es
escogida aleatoriamente de entre aquellas que pudieran tener un comportamiento
similar.
•
WalkSat:
Este
algoritmo implementa la idea de aleatoriedad por pasos, suma restauraciones y
una heurística para escoger entre variables no satisfechas, para procedimientos
de semi-desición. Igualmente escoge una clausula insatisfecha al azar, y luego
coge una variable insatisfecha para invertir desde la clausula usando la
heurística aleatoria.
Algoritmo:
Procedimientto WalkSat( )
Para
i:= 1 a Max-tries
T:=
random( ); asignamiento aleatorio de verdad
Para j := 1 a Max-flips
Si T satisface entonces
retornar T
De lo contrario Tomar
una cláusula no satisfecha
V:= var en la
cláusula escogida o acordada aleatoriamente
T := T con
asignamiento de verdad para v invertido
Fin
Fin
Retornar
“no-satisfactible de acuerdo a la asignación”
WalkSat
inspecciona si las variables pueden ser cambiadas sin afectar ninguna otra
cláusula, entonces se debe seleccionar aleatoriamente una de ellas. En otro
caso, se procede de la siguiente manera: con probabilidadw,
se cambia una variable que modifique el menor número de cláusulas. Con
probabilidad 1 - w, se cambia una variable al azar.
Para
concluir el problema SAT o problema de la satisfactibilidad es realmente
importante para la solución de diversos problemas complejos que se presentan en
los diversos campos de la problemática humana, su definición en realidad es
compleja pero su función principal es la búsqueda de la satisfactibilidad de un
formula mediante la implementación de diversos tipos de resolvedores, ya sean
de métodos completos los cuales generan la búsqueda al máximo de la
satisfactibilidad o métodos incompletos
que posiblemente encontraran la satisfactibilidad de una formula, entre estos
tipos de métodos se encuentran diversos resolvedores que se encargan mediante
la implementación de diversas herramientas y la aplicación de algoritmos de
encontrar la satisfactibilidad mediante la secuencia de pasos ordenados y
concisos que garantizan un eficaz estudio de la formula.
Suscribirse a:
Entradas (Atom)