DPLL算法 此條目需要精通或熟悉计算机科学的编者参与及协助编辑。 (2011年8月11日)請邀請適合的人士改善本条目。更多的細節與詳情請參见討論頁。另見其他需要计算机科学專家關注的頁面。 此條目没有列出任何参考或来源。 (2009年12月30日)維基百科所有的內容都應該可供查證。请协助補充可靠来源以改善这篇条目。无法查证的內容可能會因為異議提出而被移除。 DPLL（Davis-Putnam-Logemann-Loveland）算法，是一種完備的、以回溯為基礎的算法，用於解決在合取範式（CNF）中命題邏輯的布爾可滿足性問題；也就是解決CNF-SAT问题。 它在1962年由馬丁·戴維斯、希拉里·普特南、喬治·洛吉曼和多納·洛夫蘭德共同提出，作为早期戴維斯-普特南算法的一种改进。戴維斯-普特南算法是戴維斯与普特南在1960年发展的一种算法。 DPLL是一种高效的程序，并且经过40多年还是最有效的SAT解法，以及很多一阶逻辑的自动定理证明的基础。
