Algoritmo DPLL

El algoritmo DPLL/Davis-Putnam-Logemann-Loveland es un algoritmo completo basado en la vuelta atrás que sirve para decidir la satisfacibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva, es decir, para resolver el problema CNF-SAT.

Fue presentado en 1962 por Martin Davis, Hilary Putnam, George Logemann y Donald W. Loveland y es una refinación del previo algoritmo de Davis-Putnam, el cual es un procedimiento de resolución desarrollado por Davis y Putnam en 1960. El algoritmo Davis-Putnam-Logemann-Loveland es nombrado a menudo como el "método Davis-Putnam" o el "algoritmo DP", especialmente en publicaciones antiguas. Otros nombres comunes que mantienen la distinción son DLL y DPLL.

El DPLL es un procedimiento muy eficiente y tras más de 40 años aún conforma la base de los solucionadores más eficaces de SAT, así como de muchos demostradores de teoremas para fragmentos de lógica de primer orden.

Algoritmo

El Algoritmo de vuelta atrás (backtracking) se ejecuta eligiendo un literal, asignándole un valor de verdad a este, simplificando la formula y a continuación, en forma recursiva comprobando si la fórmula simplificada es satisfacible; si este es el caso la fórmula original es satisfacible; de lo contrario, la misma verificación recursiva termina asumiendo el valor de verdad contrario. Esto se conoce como regla de división, ya que divide el problema en dos subproblemas más simples. El paso de simplificación esencialmente elimina todas las cláusulas que se convierten en verdaderas en función de la formula, y todos los literales de las cláusulas restantes se convierten en falsas.

El algoritmo DPLL mejora sobre el algoritmo de vuelta atrás (backtracking) por el uso eficaz de las siguientes reglas:

Unidad de propagación 

Si una cláusula es una cláusula unitaria, es decir, sólo contiene un solo literal sin asignar, esta cláusula sólo puede ser satisfacible mediante la asignación del valor necesario para hacer verdadero al literal. Por lo tanto, otra hay otra opción. En la práctica, esto a menudo conduce a las cascadas deterministas de las unidades, evitando así una gran parte del ingenuo espacio de búsqueda.

Eliminación pura literal 

Si una variable proposicional se produce con una sola polaridad en la fórmula, se llama pura. El literal puro siempre puede ser asignado de manera que haga que todas las cláusulas que las contienen sean verdaderas. De esta manera, estas cláusulas no limiten la búsqueda y puedan ser eliminadas. Si bien esta optimización es parte del algoritmo DPLL original, las implementaciones más actuales las omiten, ya que su efecto para una implementación eficiente es insignificante o, incluso para la detección de pureza, negativo.

La insatisfabilidad de una asignacion parcial dada, se detecta si una clausula se vacía, es decir, si todas las variables han sido asignadas de manera que hace a los literales correspondientes falsos. La satisfabilidad de la fórmula se detecta cuando todas las variables se asignan sin generar la cláusula vacía, o en las implementaciones modernas, si todas las cláusulas son satisfechas. La insatisfabilidad de la fórmula completa sólo puede detectarse después de una búsqueda exhaustiva.

Trabajo Actual

El trabajo actual sobre la mejora del algoritmo se ha realizado en tres direcciones: la definición de políticas diferentes para la elección de los literales de ramificación, la definición de nuevas estructuras de datos para hacer el algoritmo más rápido, especialmente la parte sobre la propagación de la unidad; y la definición de las variantes del algoritmo de vuelta atrás básico. La dirección de este último incluye Vuelta atrás no cronológico (non-chronological backtracking) y Aprendizaje de clausulas. Estos refinamientos describe un método de vuelta atrás después de llegar a una cláusula de conflicto que "aprende" la raíz de las causas (asignaciones a variables) de los conflictos a fin de evitar llegar al mismo conflicto.

Véase también

• Algoritmo de Davis-Putnam

Referencias

• Ansotegui, Carlos; Manyà Felip (2003). «Una Introducción a los Algoritmos de Satisfactibilidad». Revista Iberoamericana de Inteligencia Artificial 7 (20). ISSN , 2-10. http://redalyc.uaemex.mx/redalyc/pdf/925/92572004.pdf. 

• «A Computing Procedure for Quantification Theory». Journal of the ACM 7 (3):  pp. 201–215. 1960. doi:10.1145/321033.321034. http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034. 

• «A Machine Program for Theorem Proving». Communications of the ACM 5 (7):  pp. 394–397. 1962. doi:10.1145/368273.368557. http://portal.acm.org/citation.cfm?doid=368273.368557. 

• «How Good Are Branching Rules in DPLL?». Discrete Applied Mathematics 89 (1–3):  pp. 281–286. 1998. doi:10.1016/S0166-218X(98)00045-6.