Algoritmo DPLL

Un procedimiento de búsqueda recursiva con retroceso para la satisfacibilidad proposicional que integra división de variables, propagación de unidades (propagación de restricciones booleanas), eliminación de literales puros y retroceso sistemático para decidir si una fórmula en CNF es satisfacible.