DPLL算法

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

基本介紹

• 中文名：DPLL算法
• 學科：計算機

簡介

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

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

回溯法

回溯法（英語：backtracking）是暴力搜尋法中的一種。

對於某些計算問題而言，回溯法是一種可以找出所有（或一部分）解的一般性算法，尤其適用於約束滿足問題（在解決約束滿足問題時，我們逐步構造更多的候選解，並且在確定某一部分候選解不可能補全成正確解之後放棄繼續搜尋這個部分候選解本身及其可以拓展出的子候選解，轉而測試其他的部分候選解）。

在經典的教科書中，八皇后問題展示了回溯法的用例。（八皇后問題是在標準西洋棋棋盤中尋找八個皇后的所有分布，使得沒有一個皇后能攻擊到另外一個。）

回溯法採用試錯的思想，它嘗試分步的去解決一個問題。在分步解決問題的過程中，當它通過嘗試發現現有的分步答案不能得到有效的正確的解答的時候，它將取消上一步甚至是上幾步的計算，再通過其它的可能的分步解答再次嘗試尋找問題的答案。回溯法通常用最簡單的遞歸方法來實現，在反覆重複上述的步驟後可能出現兩種情況：

• 找到一個可能存在的正確的答案
  
• 在嘗試了所有可能的分步方法後宣告該問題沒有答案
  

在最壞的情況下，回溯法會導致一次複雜度為指數時間的計算。

布爾可滿足性問題

可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一組變數賦值，使問題為可滿足。布爾可滿足性問題（Boolean satisfiability problem；SAT)）屬於決定性問題，也是第一個被證明屬於NP完全的問題。此問題在計算機科學上許多領域的皆相當重要，包括計算機科學基礎理論、算法、人工智慧、硬體設計等等。

定理機器證明

定理機器證明（Automated theorem proving，簡稱ATP）目前是自動推理（Automated reasoning，簡稱AR）體系中發展最好的部分，它的目的是為使用電子電腦程式來進行數學定理的證明。對於不同的數學邏輯，它能夠推論出一個定理是正確的，還是不可證明的，或者錯誤的。