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