此條目需要精通或熟悉計算機科學的編者參與及協助編輯。 (2011年8月11日) 請邀請適合的人士改善本條目。更多的細節與詳情請參見討論頁。 另見其他需要計算機科學專家關注的頁面。 |
此條目沒有列出任何參考或來源。 (2009年12月30日) 維基百科所有的內容都應該可供查證。請協助補充可靠來源以改善這篇條目。無法查證的內容可能會因為異議提出而被移除。 |
DPLL(Davis-Putnam-Logemann-Loveland)算法,是一種完備的、以回溯為基礎的算法,用於解決在合取範式(CNF)中命題邏輯的布爾可滿足性問題;也就是解決CNF-SAT問題。
它在1962年由馬丁·戴維斯、希拉里·普特南、喬治·洛吉曼和多納·洛夫蘭德共同提出,作為早期戴維斯-普特南算法的一種改進。戴維斯-普特南算法是戴維斯與普特南在1960年發展的一種算法。