DPLL算法

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

DPLL(Davis-Putnam-Logemann-Loveland)算法,是一種完備的、以回溯為基礎的算法,用於解決在合取範式(CNF)中命題邏輯布爾可滿足性問題;也就是解決CNF-SAT问题。

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

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