在邏輯學和計算機科學中，（DPLL）算法是一種完整的、基于回溯的搜索算法，用于決定共軛正常形式下命題邏輯公式的可滿足性，即用于解決CNF-SAT問題。

SAT問題從理論和實踐的角度來看都很重要。在復雜性理論中，它是xxx個被證明是NP-complete的問題，并且可以出現在各種各樣的應用中，如模型檢查，自動計劃和調度，以及人工智能的診斷。因此，編寫高效的SAT求解器已經是一個多年的研究課題。

基本的回溯算法通過選擇一個字面，給它分配一個真值，簡化公式，然后遞歸檢查簡化后的公式是否可滿足；如果是這樣，原公式是可滿足的；否則，假設真值相反，進行同樣的遞歸檢查。這被稱為分割規則，因為它將問題分割成兩個更簡單的子問題。簡化步驟實質上是將所有在賦值下成為真值的子句從公式中移除，并將所有成為假值的字詞從剩余子句中移除。DPLL算法通過在每一步急切地使用以下規則來加強對反向追蹤算法的支持。

如果一個子句是一個單位子句，即它只包含一個未分配的字詞，這個子句只能通過分配必要的值使這個字詞為真來滿足。因此，沒有必要進行選擇。單元傳播包括刪除每一個包含單元子句字樣的子句，以及從每一個包含單元子句字樣的子句中丟棄該補碼。在實踐中，這往往會導致確定的單元級聯，從而避免了很大一部分天真的搜索空間。純粹字面消除如果一個命題變量在公式中只出現一個極性，那么它就被稱為純粹的。純粹的字面意義總是可以以一種方式分配，使包含它的所有子句都為真。因此，當它以這種方式被賦值時，這些子句不再限制搜索，可以被刪除。

如果一個子句變成空的，也就是說，如果它的所有變量被分配的方式使相應的字詞變成了假的，那么就可以檢測到一個給定的部分賦值的不可滿足性。公式的可滿足性在所有變量都被賦值而不產生空子時被檢測出來，或者在現代的實現中，所有子句都被滿足。完整公式的不滿足性只有在窮舉搜索后才能被檢測出來。DPLL算法可以總結為以下的偽代碼，其中Φ是CNF公式。

DPLL輸入。一組子句Φ。輸出。一個表示Φ是否可滿足的真值。函數DPLL(Φ)當Φ中存在一個單元句{l}時，Φ←單元傳播(l,Φ)；當Φ中存在一個純文本l時，Φ←純文本分配(l,Φ)。如果Φ是空的，則返回true；如果Φ包含一個空的子句，則返回false；l←選擇字詞(Φ)；分別返回對字詞l和公式Φ應用單元傳播和純字詞規則的結果。返回語句中的or是一個短路運算符。Φ∧{l}表示在Φ中用真代替l的簡化結果。該算法在兩種情況中的一種終止。要么CNF公式Φ是空的，即它不包含任何子句。那么它可以被任何賦值所滿足，因為它的所有子句都是空的真。