跳转到内容

DPLL算法

维基百科,自由的百科全书

DPLL(Davis-Putnam-Logemann-Loveland)算法,是一种完备的、以回溯为基础的算法,用于解决在合取范式(CNF)中命题逻辑布尔可满足性问题;也就是解决CNF-SAT问题。

它在1962年由马丁·戴维斯希拉里·普特南乔治·洛吉曼多纳·洛夫兰德共同提出,作为早期戴维斯-普特南算法的一种改进。戴维斯-普特南算法是戴维斯与普特南在1960年发展的一种算法。

DPLL是一种高效的程序,并且经过40多年还是最有效的SAT解法,以及很多一阶逻辑自动定理证明的基础。