En lógica y ciencias de la computación , el algoritmo Davis–Putnam–Logemann–Loveland ( DPLL ) es un algoritmo de búsqueda completo basado en retroceso para decidir la satisfacibilidad de fórmulas lógicas proposicionales en forma normal conjuntiva , es decir, para resolver el problema CNF-SAT .
Fue introducido en 1961 por Martin Davis , George Logemann y Donald W. Loveland y es un refinamiento del algoritmo Davis-Putnam anterior , que es un procedimiento basado en resolución desarrollado por Davis y Hilary Putnam en 1960. Especialmente en publicaciones más antiguas, el algoritmo Davis-Logemann-Loveland a menudo se conoce como el "método Davis-Putnam" o el "algoritmo DP". Otros nombres comunes que mantienen la distinción son DLL y DPLL.
El problema SAT es importante tanto desde el punto de vista teórico como práctico. En teoría de la complejidad, fue el primer problema que se demostró que era NP-completo y puede aparecer en una amplia variedad de aplicaciones, como la verificación de modelos , la planificación y programación automatizadas y el diagnóstico en inteligencia artificial .
Por ello, la creación de solucionadores SAT eficientes ha sido un tema de investigación durante muchos años. GRASP (1996-1999) fue una implementación temprana que utilizó DPLL. [1] En las competiciones SAT internacionales, las implementaciones basadas en DPLL como zChaff [2] y MiniSat [3] ocuparon los primeros lugares de las competiciones en 2004 y 2005. [4]
Otra aplicación que a menudo involucra DPLL es la demostración automatizada de teoremas o teorías de satisfacibilidad módulo (SMT), que es un problema SAT en el que las variables proposicionales se reemplazan con fórmulas de otra teoría matemática .
El algoritmo básico de retroceso se ejecuta eligiendo un literal, asignándole un valor de verdad , simplificando la fórmula y luego verificando recursivamente si la fórmula simplificada es satisfactoria; si este es el caso, la fórmula original es satisfactoria; de lo contrario, se realiza la misma verificación recursiva asumiendo el valor de verdad opuesto. Esto se conoce como la 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 vuelven verdaderas bajo la asignación de la fórmula, y todos los literales que se vuelven falsos de las cláusulas restantes.
El algoritmo DPLL mejora el algoritmo de retroceso mediante el uso entusiasta de las siguientes reglas en cada paso:
La insatisfacción de una asignación parcial dada se detecta si una cláusula queda vacía, es decir, si todas sus variables se han asignado de una manera que hace que los literales correspondientes sean falsos. La satisfacibilidad de la fórmula se detecta cuando se asignan todas las variables sin generar la cláusula vacía o, en implementaciones modernas, si se satisfacen todas las cláusulas. La insatisfacción de la fórmula completa solo se puede detectar después de una búsqueda exhaustiva.
El algoritmo DPLL se puede resumir en el siguiente pseudocódigo, donde Φ es la fórmula CNF :
Algoritmo DPLL Entrada: Un conjunto de cláusulas Φ. Salida: Un valor de verdad que indica si Φ es satisfactoria.
función DPLL (Φ) // propagación de la unidad: mientras haya una cláusula de unidad { l } en Φ hacer Φ ← unidad-propagar ( l , Φ); // eliminación literal pura: mientras haya un literal l que ocurra puro en Φ hacer Φ ← pure-literal-assign ( l , Φ); // condiciones de detención: si Φ está vacío, entonces devuelve verdadero; si Φ contiene una cláusula vacía, entonces devuelve falso; // Procedimiento DPLL: l ← elegir-literal (Φ); devolver DPLL (Φ ∧ {l}) o DPLL (Φ ∧ {¬l});En este pseudocódigo, unit-propagate(l, Φ)y pure-literal-assign(l, Φ)son funciones que devuelven el resultado de aplicar la propagación de unidades y la regla literal pura, respectivamente, al literal ly a la fórmula Φ. En otras palabras, reemplazan cada ocurrencia de lcon "true" y cada ocurrencia de not lcon "false" en la fórmula Φ, y simplifican la fórmula resultante. El orin de la returndeclaración es un operador de cortocircuito . denota el resultado simplificado de sustituir "true" por in .Φ ∧ {l}lΦ
El algoritmo termina en uno de dos casos. O bien la fórmula CNF Φestá vacía, es decir, no contiene ninguna cláusula. En ese caso, se satisface con cualquier asignación, ya que todas sus cláusulas son vacuamente verdaderas. De lo contrario, cuando la fórmula contiene una cláusula vacía, la cláusula es vacuamente falsa porque una disyunción requiere al menos un miembro que sea verdadero para que el conjunto general sea verdadero. En este caso, la existencia de dicha cláusula implica que la fórmula (evaluada como una conjunción de todas las cláusulas) no puede evaluarse como verdadera y debe ser insatisfactoria.
La función DPLL de pseudocódigo solo devuelve si la asignación final satisface la fórmula o no. En una implementación real, la asignación que satisface parcialmente también suele devolverse en caso de éxito; esto se puede derivar haciendo un seguimiento de los literales de ramificación y de las asignaciones literales realizadas durante la propagación de unidades y la eliminación literal pura.
El algoritmo Davis-Logemann-Loveland depende de la elección del literal de ramificación , que es el literal considerado en el paso de retroceso. Como resultado, no es exactamente un algoritmo, sino más bien una familia de algoritmos, uno para cada forma posible de elegir el literal de ramificación. La eficiencia se ve fuertemente afectada por la elección del literal de ramificación: existen instancias para las cuales el tiempo de ejecución es constante o exponencial dependiendo de la elección de los literales de ramificación. Tales funciones de elección también se denominan funciones heurísticas o heurísticas de ramificación. [5]
Davis, Logemann, Loveland (1961) desarrollaron este algoritmo. Algunas propiedades de este algoritmo original son:
Un ejemplo con visualización de un algoritmo DPLL con retroceso cronológico:
Desde 1986, los diagramas de decisión binarios (ordenados reducidos) también se han utilizado para la resolución de SAT. [ cita requerida ]
En 1989-1990 se presentó y patentó el método de Stålmarck para la verificación de fórmulas, que ha encontrado cierta utilidad en aplicaciones industriales. [6]
DPLL se ha ampliado para la demostración automática de teoremas para fragmentos de lógica de primer orden mediante el algoritmo DPLL(T) . [1]
En la década 2010-2019, el trabajo para mejorar el algoritmo ha encontrado mejores políticas para elegir los literales de ramificación y nuevas estructuras de datos para hacer que el algoritmo sea más rápido, especialmente la parte sobre la propagación de unidades . Sin embargo, la mejora principal ha sido un algoritmo más poderoso, Conflict-Driven Clause Learning (CDCL), que es similar a DPLL pero después de llegar a un conflicto "aprende" las causas fundamentales (asignaciones a variables) del conflicto, y usa esta información para realizar un retroceso no cronológico (también conocido como backjumping ) para evitar llegar al mismo conflicto nuevamente. La mayoría de los solucionadores SAT de última generación se basan en el marco CDCL a partir de 2019. [7]
Las ejecuciones de algoritmos basados en DPLL en instancias insatisfactorias corresponden a pruebas de refutación de resolución de árboles . [8]
General
Específico