En la lógica y la informática , la Davis-Putnam-Logemann-Loveland ( DPLL ) algoritmo es una completa , dando marcha atrás basado en el algoritmo de búsqueda para decidir el satisfacibilidad de fórmulas de lógica proposicional en forma normal conjuntiva , es decir, para resolver el CNF-SAT problema.
Clase | Problema de satisfacibilidad booleano |
---|---|
Estructura de datos | Árbol binario |
Rendimiento en el peor de los casos | |
Rendimiento en el mejor de los casos | (constante) |
Complejidad espacial en el peor de los casos | (algoritmo básico) |
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 la resolución desarrollado por Davis e Hilary Putnam en 1960. Especialmente en publicaciones más antiguas, el El algoritmo Davis-Logemann-Loveland a menudo se denomina "método Davis-Putnam" o "algoritmo DP". Otros nombres comunes que mantienen la distinción son DLL y DPLL.
Después de más de 50 años, el procedimiento DPLL sigue siendo la base de los solucionadores SAT completos más eficientes. Recientemente se ha ampliado para la demostración automática de teoremas de fragmentos de lógica de primer orden mediante el algoritmo DPLL (T) . [1]
Implementaciones y aplicaciones
El problema SAT es importante tanto desde el punto de vista teórico como práctico. En la teoría de la complejidad , fue el primer problema que demostró ser 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 .
Como tal, ha sido un tema candente en la investigación durante muchos años, y regularmente se llevan a cabo concursos entre los solucionadores de SAT . [2] Las implementaciones modernas de DPLL como Chaff y zChaff , [3] [4] GRASP o MiniSat [5] están en los primeros lugares de las competencias estos últimos años. [ cuando? ]
Otra aplicación que a menudo involucra DPLL es la demostración automatizada de teoremas o las teorías de módulo de satisfacibilidad (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
El algoritmo de retroceso básico se ejecuta eligiendo un literal, asignándole un valor de verdad , simplificando la fórmula y luego comprobando recursivamente si la fórmula simplificada es satisfactoria; si este es el caso, la fórmula original es satisfactoria; de lo contrario, la misma verificación recursiva se realiza 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:
- Propagación unitaria
- Si una cláusula es una cláusula unitaria , es decir, contiene solo un literal no asignado, esta cláusula solo puede satisfacerse asignando el valor necesario para que este literal sea verdadero. Por tanto, no es necesaria ninguna elección. La propagación unitaria consiste en eliminar cada cláusula que contiene un literal de cláusula unitaria y descartar el complemento del literal de una cláusula unitaria de cada cláusula que contiene ese complemento. En la práctica, esto a menudo conduce a cascadas deterministas de unidades, evitando así una gran parte del espacio de búsqueda ingenua.
- Eliminación literal pura
- Si una variable proposicional ocurre con una sola polaridad en la fórmula, se llama pura . Siempre se puede asignar un literal puro de manera que todas las cláusulas que lo contienen sean verdaderas. Por lo tanto, cuando se asigna de esa manera, estas cláusulas ya no restringen la búsqueda y se pueden eliminar.
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 satisfacción de la fórmula se detecta cuando todas las variables se asignan sin generar la cláusula vacía o, en implementaciones modernas, si se cumplen 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 Φ. Resultado: un valor de verdad.
función DPLL (Φ) si Φ es un conjunto consistente de literales entonces devuelve verdadero; si Φ contiene una cláusula vacía , devuelve falso; para cada cláusula unitaria {l} en Φ do Φ ← unit-propagate ( l , Φ); para cada literal l que aparece puro en Φ do Φ ← pure-literal-assign ( l , Φ); l ← elegir-literal (Φ); devuelve DPLL (Φ ∧ {l}) o DPLL (Φ ∧ {no (l)});
- "←" denota asignación . Por ejemplo, " más grande ← artículo significa" que el valor de los mayores cambios en el valor del elemento .
- " return " termina el algoritmo y genera el siguiente valor.
En este pseudocódigo, unit-propagate(l, Φ)
y pure-literal-assign(l, Φ)
son funciones que devuelven el resultado de aplicar la propagación unitaria y la regla literal pura, respectivamente, al literal l
y a la fórmula Φ
. En otras palabras, reemplazan cada aparición de l
por "verdadero" y cada aparición de not l
por "falso" en la fórmula Φ
, y simplifican la fórmula resultante. El or
en la return
declaración es un operador de cortocircuito . denota el resultado simplificado de sustituir "verdadero" por in .Φ ∧ {l}
l
Φ
El algoritmo termina en uno de dos casos. O Φ
se encuentra que la fórmula CNF comprende un conjunto consistente de literales , es decir, no hay l
y ¬l
para cualquier literal l
en la fórmula. Si este es el caso, las variables pueden satisfacerse trivialmente estableciéndolas en la polaridad respectiva del literal abarcador en la valoración. De lo contrario, cuando la fórmula contiene una cláusula vacía, la cláusula es falsamente vacía 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 de pseudocódigo DPLL solo devuelve si la asignación final satisface la fórmula o no. En una implementación real, la asignación satisfactoria parcial típicamente también se devuelve en caso de éxito; esto se puede derivar del conjunto consistente de literales de la primera if
declaración de la función.
El algoritmo de 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, esto 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 muy afectada por la elección del literal de ramificación: existen instancias para las que el tiempo de ejecución es constante o exponencial según la elección de los literales de ramificación. Estas funciones de elección también se denominan funciones heurísticas o heurísticas de ramificación. [6]
Visualización
Davis, Logemann, Loveland (1961) habían desarrollado este algoritmo. Algunas propiedades de este algoritmo original son:
- Se basa en la búsqueda.
- Es la base de casi todos los solucionadores SAT modernos.
- Que no utilizan el aprendizaje o la marcha atrás no cronológico (introducido en 1996).
Un ejemplo con visualización de un algoritmo DPLL con retroceso cronológico:
Todas las cláusulas que componen una fórmula CNF
Elige una variable
Tome una decisión, variable a = Falso (0), por lo que las cláusulas verdes se vuelven Verdaderas
Después de tomar varias decisiones, encontramos un gráfico de implicaciones que conduce a un conflicto.
Ahora retroceda al nivel inmediato y por la fuerza asigne el valor opuesto a esa variable
Pero una decisión forzada aún conduce a otro conflicto.
Retroceda al nivel anterior y tome una decisión forzada.
Toma una nueva decisión, pero conduce a un conflicto.
Tomar una decisión forzada, pero nuevamente conduce a un conflicto.
Retroceder al nivel anterior
Continúe de esta manera y el gráfico de implicaciones final
Trabajo actual
En los años 2010, el trabajo para mejorar el algoritmo se ha realizado en tres direcciones:
- Definición de diferentes políticas para elegir los literales de ramificación.
- Definición de nuevas estructuras de datos para agilizar el algoritmo, especialmente la parte de propagación unitaria .
- Definición de variantes del algoritmo de retroceso básico. La última dirección incluye backtracking no cronológico (aka backjumping ) y aprendizaje cláusula . Estos refinamientos describen un método de retroceso después de llegar a una cláusula de conflicto que "aprende" las causas raíz (asignaciones a variables) del conflicto para evitar volver a llegar al mismo conflicto. Los solucionadores de SAT de aprendizaje de cláusulas basadas en conflictos resultantes son lo último en tecnología en 2014. [ cita requerida ]
Un algoritmo más nuevo de 1990 es el método de Stålmarck . Además, desde 1986 (orden reducido), los diagramas de decisión binarios también se han utilizado para la resolución de SAT.
Relación con otras nociones
Las ejecuciones de algoritmos basados en DPLL en instancias insatisfactorias corresponden a pruebas de refutación de resolución de árbol . [7]
Ver también
- Prueba de complejidad
- Herbrandización
Referencias
General
- Davis, Martin ; Putnam, Hilary (1960). "Un procedimiento informático para la teoría de la cuantificación" . Revista de la ACM . 7 (3): 201–215. doi : 10.1145 / 321033.321034 .
- Davis, Martin; Logemann, George; Loveland, Donald (1961). "Un programa de máquina para la demostración de teoremas" . Comunicaciones de la ACM . 5 (7): 394–397. doi : 10.1145 / 368273.368557 . hdl : 2027 / mdp.39015095248095 .
- Ouyang, Ming (1998). "¿Qué tan buenas son las reglas de ramificación en DPLL?". Matemáticas aplicadas discretas . 89 (1-3): 281-286. doi : 10.1016 / S0166-218X (98) 00045-6 .
- John Harrison (2009). Manual de lógica práctica y razonamiento automatizado . Prensa de la Universidad de Cambridge. págs. 79–90. ISBN 978-0-521-89957-4.
Específico
- ^ Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesar (2004), "Abstract DPLL and Abstract DPLL Modulo Theories" (PDF) , Proceedings Int. Conf. sobre lógica para la programación, la inteligencia artificial y el razonamiento , LPAR 2004 , págs. 36–50
- ^ La página web de los concursos internacionales SAT , sat! En Vivo
- ^ sitio web de zChaff
- ^ Sitio web de Chaff
- ^ "Sitio web de Minisat" .
- ^ Marques-Silva, João P. (1999). "El impacto de la heurística de ramificación en algoritmos de satisfacción proposicional". En Barahona, Pedro; Alferes, José J. (eds.). Progreso en Inteligencia Artificial: 9ª Conferencia Portuguesa sobre Inteligencia Artificial, EPIA '99 Évora, Portugal, 21-24 de septiembre de 1999 Actas . LNCS . 1695 . págs. 62–63. doi : 10.1007 / 3-540-48159-1_5 . ISBN 978-3-540-66548-9.
- ^ Van Beek, Peter (2006). "Algoritmos de búsqueda de retroceso". En Rossi, Francesca; Van Beek, Peter; Walsh, Toby (eds.). Manual de programación de restricciones . Elsevier. pag. 122. ISBN 978-0-444-52726-4.
Otras lecturas
- Malayo Ganai; Aarti Gupta; Dr. Aarti Gupta (2007). Soluciones de verificación formal escalables basadas en SAT . Saltador. págs. 23–32. ISBN 978-0-387-69166-4.
- Gomes, Carla P .; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Solucionadores de satisfacción". En Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.). Manual de representación del conocimiento . Fundamentos de la Inteligencia Artificial. 3 . Elsevier. págs. 89-134. doi : 10.1016 / S1574-6526 (07) 03002-7 . ISBN 978-0-444-52211-5.