Algoritmo DPLL

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

Otros nombres comunes que mantienen la distinción son DLL y DPLL.

El algoritmo de vuelta atrás (backtracking) se ejecuta eligiendo un literal, asignándole un valor de verdad a este, simplificando la fórmula 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.

La satisfacibilidad 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.