 | 此条目需要精通或熟悉计算机科学的编者参与及协助编辑。 (2011年8月11日) 请邀请适合的人士改善本条目。更多的细节与详情请参见讨论页。 另见其他需要计算机科学专家关注的页面。 |
 | 此条目没有列出任何参考或来源。 (2009年12月30日) 维基百科所有的内容都应该可供查证。请协助补充可靠来源以改善这篇条目。无法查证的内容可能会因为异议提出而被移除。 |
DPLL（Davis-Putnam-Logemann-Loveland）算法，是一种完备的、以回溯为基础的算法，用于解决在合取范式（CNF）中命题逻辑的布尔可满足性问题；也就是解决CNF-SAT问题。
它在1962年由马丁·戴维斯、希拉里·普特南、乔治·洛吉曼和多纳·洛夫兰德共同提出，作为早期戴维斯-普特南算法的一种改进。戴维斯-普特南算法是戴维斯与普特南在1960年发展的一种算法。