DPLL算法

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

它在1962年由馬丁·戴維斯、希拉蕊·普特南、喬治·洛吉曼和多納·洛夫蘭德共同提出，作為早期戴維斯-普特南算法的一種改進。戴維斯-普特南算法是戴維斯與普特南在1960年發展的一種算法。

DPLL是一種高效的程序，並且經過40多年還是最有效的SAT解法，以及很多一階邏輯的自動定理證明的基礎。