Algoritmo DPLL

De WikiRA

El algoritmo DPLL fue creado por Davis, Putnam, Logemann y Loveland en 1962 y su objetivo es comprobar la satisfacibilidad de una fórmula proposicional en forma normal conjuntiva (FNC).

El algoritmo original data de 1960 y fue creado por Davis y Putnam (DP). DPLL es una variante de este algoritmo.

Contenido

Representación en FNC

Una representación útil para una fórmula proposicional en forma normal conjuntiva es un conjunto de conjuntos.

  • Literal: Fórmula atómica o su negación.
  • Cláusula: Conjunto de literales. Representa la disyunción de los literales de la cláusula.
  • Fórmula: Conjunto de cláusulas. Representa la conjunción de las cláusulas.

Procedimiento

El algoritmo transforma un conjunto de cláusulas en otro conjunto de cláusulas manteniendo la satisfacibilidad respecto al original. El algoritmo termina cuando:

  • El conjunto de cláusulas contiene la cláusula vacía, en cuyo caso la cláusula original es insatisfacible
  • El conjunto de cláusulas está vacío, en cuyo caso la cláusula original es satisfacible

Transformaciones

Tranformaciones que conservan la satisfacibilidad del conjunto de cláusulas.

Regla de la tautología

Elimina las cláusulas del conjunto de cláusulas que contengan un par de literales complementarios.

Regla de la cláusula unitaria

Comprueba si alguna cláusula del conjunto de cláusulas que sea unitaria (que esté compuesta por un solo literal), y si la hay, elimina esta cláusula y las que contienen este literal y del resto de las cláusulas, si contienen el complementario del literal antes mencionado, se elimina éste de la cláusula.

Regla del literal puro

Dado un literal puro (aquel que aparece siempre con el mismo signo en el conjunto de cláusulas), se eliminan todas las cláusulas que lo contengan.

Regla de la inclusión

Elimina las cláusulas que son superconjunto de alguna de las cláusulas del conjunto de cláusulas.

Regla de la bifurcación

Reduce la satisfabilidad de un conjunto de cláusulas Δ a la satisfacibilidad de \Delta\cup\{p\} y de \Delta\cup\{-p\}, siendo p un literal. Δ es satisfacible si y solo si \Delta\cup\{p\} o \Delta\cup\{-p\} lo es.

Motor de inferencia

Una vez definido el conjunto de transformaciones que son aplicadas en DPLL, el siguiente paso lógico es definir la forma en la cual serán aplicadas dichas transformaciones. Partiendo de un conjunto de cláusulas inicial, la primera regla que deberemos aplicar será la regla de la tautología, esta regla bastará con que sea llevada a cabo una sola vez, ya que eliminando las cláusulas que tienen literales complementarios, ninguna de las reglas (incluido ella misma) puede producir esta circunstancia. Al eliminar las cláusulas que tienen literales complementarios, lo que en realidad estamos diciendo es que la satisfacibilidad del conjunto de cláusulas no depende de las cláusulas que hemos eliminado, ya que independientemente de la valoración que tengan los literales que las compongan, el conjunto de cláusulas será verdadero. Todas las transformaciones del DPLL funcionan bajo el mismo principio, todas buscan aquel conjunto de cláusulas del cual depende la satisfacibilidad del conjunto inicial.

El siguiente paso será aplicar la regla de la cláusula unitaria. Esta transformación tiene un aspecto que la diferencia del resto de transformaciones. Las otras transformaciones solo eliminan cláusulas del conjunto inicial, sin embargo la regla de la cláusula unitaria además es capaz de modificar el contenido de las cláusulas, de forma que cuando se eliminan de las cláusulas la apariciones negadas del literal que compone la cláusula unitaria, estamos modificando las cláusulas de conjunto. Por este motivo dicha regla debe ser aplicada en primer lugar. ¿En primer lugar?, ¿No era primero la regla tautológica?. Es cierto que la primera regla que se aplica es la de la tautología, sin embargo como dijimos anteriormente, dicha regla solo se aplica una vez, mientras que el resto de cláusulas ha de ser aplicada iterativamente. Por ello cuando nos referimos a que esta regla ha de ser la primera, nos referimos al hecho de que será la primera que se aplicará en el proceso iterativo. Para entender con más claridad dicho proceso iterativo podemos observar la figura

Dpll
. Una vez que apliquemos la regla de la cláusula unitaria, es posible que creemos nuevas cláusulas unitarias, por este motivo deberemos aplicar nuevamente dicha regla hasta que el conjunto de cláusulas de entrada sea igual al resultante.

Una vez aplicada la regla de la cláusula unitaria, la siguiente será la regla del literal puro. El objetivo del DPLL es demostrar la existencia o no de modelos para un conjunto de cláusulas, de forma que si en un conjunto de cláusulas un literal siempre aparece de la misma forma (negado o sin negar), podemos hacer sobre el dos suposiciones: el literal es verdadero o el literal es falso. En el caso de que el literal sea verdadero, podríamos eliminar directamente todas aquellas cláusulas que lo contengan. Si por el contrario dicho literal fuese falso podríamos eliminar las apariciones de dicho literal en el conjunto de cláusulas. No obstante podemos ver que en el caso de que supongamos que el literal puro es verdadero, el conjunto de cláusulas resultante, es un subconjunto de las cláusulas que nos quedarían en el caso de suponer que el literal puro es falso. Por ese motivo, partiremos de la veracidad del citado literal e intentaremos demostrar la satisfacibilidad del conjunto de cláusulas resultantes de dicha suposición. Como podemos ver, tanto la regla de la cláusula unitaria como la regla del literal puro, establecen la veracidad de algunos literales con el fin de estudiar la satisfacibilidad del conjunto de cláusulas, si quisiéramos conseguir el modelo que verifica la satisfacibilidad del conjunto de cláusulas, deberíamos ir almacenando dichas suposiciones, ya que son estas las que formarán el modelo.

La siguiente regla que tenemos que aplicar es regla de la inclusión. Dado un conjunto de cláusulas, si en dicho conjunto existen cláusulas que son subconjunto de otras, es obvio que si demostramos la satisfacibilidad de una cláusula que es subconjunto de otra, la satisfacibilidad de la cláusula superconjunto quedará demostrada directamente. Es por ello que dado un conjunto de cláusulas, podremos eliminar de dicho conjunto todas aquellas cláusulas que sean superconjuntos de otras existentes en el mismo conjunto.

Una vez aplicadas todas las reglas anteriores, es posible que no podamos probar todavía la satisfacibilidad del conjunto de cláusulas resultantes. En este caso, deberemos de aplicar la última de las reglas, la regla de la bifurcación. Esta regla es quizás la más sencilla de todas, basa su funcionamiento en demostrar la satisfacibilidad de un conjunto de cláusulas separando la demostración en dos ramas. Para ello elegimos uno de los literales del conjunto de cláusulas y suponemos que este es verdadero y falso en cada una de las ramas respectivamente. En la rama primera supondremos que el literal es verdadero y en consecuencia eliminaremos todas aquellas cláusulas que lo contienen. Este mismo planteamiento será realizado en la otra rama pero suponiendo la negación de dicho literal. Una vez creados los conjuntos de cláusulas de ambas ramas, solo deberemos volver pasar dichos conjuntos de cláusulas al algoritmo DPLL.

Referencias

  • Handbook of Practical Logic and Automated Reasoning, Harrison, J. Cambridge University Press. 2009.
Herramientas personales