DPLL算法

DPLL 算法

DPLL/Davis-Putnam-Logemann-Loveland 算法 是一种完备的，基于回溯算法的决定CNF型命题逻辑的满足性的算法，即CNF-SAT问题。

它在1962年由Martin Davis, Hilary Putnam, George Logemann 和 Donald W. Loveland 提出,作为早期Davis-Putnam 算法的一种改进。Davis-Putnam 算法是Davis 与 Putnam在1960年发展的一种算法。

尤其是在旧的出版物中，Davis-Logemann-Loveland 算法常常被称为“Davis-Putnam method”或“DP algorithm”。其他常见的名称是DLL和DPLL。DPLL是一种高效的程序，并且经过40多年还是最有效的SAT解法，以及很多一阶逻辑的自动定理证明的基础。