1962 年 DPLL：分裂法庭與 SAT 之祖#

案件編號：No.1962 — 偵探：Davis、Logemann、Loveland。關鍵證詞：「別一次消滅證人，一個一個問。」

案發現場#

1960 年的 Davis Putnam 程序剛破案就惹出新麻煩。消去規則雖優雅，卻是記憶體殺手：對變元 \(p\) 生成所有 \(C_i \lor D_j\) ，子句數可從 \(m\) 暴增到 \(m^2\) 。在 IBM 704 只有 32K 字的年代，多消去幾個變元機器就窒息。

Davis 本人最清楚這個痛點。他找來普林斯頓的 George Logemann 與 Donald Loveland，重新勘查現場。三人發現：與其用推理一次消滅變元 \(p\) ，不如用搜尋「假設 \(p\) 為真／為假」分兩路偵辦。這是從推理到搜尋的典範轉移。

當時 Logic Theorist 已展示搜尋的威力， Herbrand 定理仍在後方大量生產子句，工業界對電路驗證與組合問題的需求正在升溫。SAT 需要一個省記憶體、可回溯的程序。1962 年的論文 A Machine Program for Theorem Proving 就是答卷，後世稱之為 DPLL。

偵查過程#

DPLL 保留了前作的兩條便宜規則，唯獨把昂貴的消去規則換成分裂規則。這一換，SAT 史轉彎。

線索一：三條現行規則#

規則	條件	行動	偵探比喻
Unit propagate	存在單子句 \(\{l\}\)	令 \(l\) 為真，化簡子句集 \(S\)	唯一目擊證人指認，直接採信
Pure literal	\(p\) 只單極性出現	令其為真並刪相關子句	無對立證詞，逕行採信
Splitting	以上皆無可用	選變元 \(p\) ，分 \(p = True\) 與 \(p = False\) 兩案遞迴偵辦	分頭訊問，任一成立即破案

分裂規則的形式化為： \(S\) 可滿足當且僅當 \(S[p := True]\) 可滿足或 \(S[p := False]\) 可滿足。這是簡單的語義分案，卻避開了消去規則的指數級子句生成。

線索二：虛擬碼#

DPLL(S, assignment):
  S := unit_propagate(S, assignment)
  S := pure_literal_eliminate(S, assignment)
  if S 為空集: return SAT(assignment)
  if S 含空子句: return UNSAT
  選一未賦值變元 p
  if DPLL(S ∪ {{p}}, assignment ∪ {p=True}) 為 SAT:
    return SAT
  else:
    return DPLL(S ∪ {{¬p}}, assignment ∪ {p=False})

其中 \(S\) 為子句集， \(assignment\) 為部分賦值。 \(unit\_propagate\) 需閉包執行直到無單子句，這是今日 SAT 求解器仍在用的核心迴圈。

線索三：實戰演練#

xét \(S = \{ \{p, q\}, \{\lnot p, q\}, \{p, \lnot q\}, \{\lnot p, \lnot q\} \}\) ，正是前案 Davis Putnam 用消去法解過的死結。DPLL 改用分裂：

無 unit，無 pure，選 \(p\) 分裂。
左支設 \(p = True\) ，化簡得 \(\{ \{q\}, \{\lnot q\} \}\) 。
此時 \(\{q\}\) 為單子句， propagate 得 \(\{ \{\lnot q\} \}\) ，再 propagate 得 \(\{ \Box \}\) ，左支 UNSAT。
回溯至右支 \(p = False\) ，同理化簡得 \(\{ \{q\}, \{\lnot q\} \}\) ，亦得 \(\Box\) ，右支 UNSAT。
兩支皆死，全案 UNSAT。

全程子句數從未膨脹，記憶體用量僅與變元數 \(n\) 加子句數 \(m\) 線性相關。這就是分裂勝過消去之處：以時間換空間，以回溯換生成。

線索四：選擇變元的藝術#

DPLL 沒有規定如何選 \(p\) 。最早版本隨便選，後人發現這是效能命門。MOM 啟發式、VSIDS、相位儲存等皆源於此一空格。本案埋下的正是現代 CDCL 的種子：unit propagate 加聰明分支，遲早能征服百萬變元。

這也呼應布林的代數直覺：賦值即計算，搜尋即推理。

結案報告#

DPLL 用一條分裂規則取代消去規則，奠定此後六十年 SAT 求解的骨架：

SAT 之祖：從 1962 到 2001 年 Chaff 的 CDCL 革命，再到 Z3 與 SMT ，所有現代求解器都是 DPLL 的子孫，差別只在學習子句與回跳策略。
證明與搜尋合流：它證明定理證明不必全是推理規則，回溯搜尋本身就是證明。其搜尋樹即是 Gentzen 意義下的證明物件。
實用 перелом：記憶體從指數降為線性，SAT 從玩具變成工具，電路驗證、規劃、模型檢測皆受其惠。

局限是：原始 DPLL 仍是指數最壞時間，不會學習衝突，不會非時序回跳。這些要等 1996 年 GRASP 與 2001 年 Chaff 補完。但法庭架構已定：unit、pure、branch 三權分立。

下一案，Robinson 將把命題層的消解推廣到一階，讓量詞也束手就擒。請見歸結原理。

證據與工具#

完備性速寫：設 \(S\) 為有限子句集， \(p\) 為其中變元。引理為 \(S\) 可滿足 iff \(S[p := True]\) 或 \(S[p := False]\) 可滿足。對變元數 \(n\) 歸納： \(n = 0\) 時 \(S\) 為空或含 \(\Box\) ，顯然可判定；歸納步由引理與 unit、pure 規則的保可滿足性即得終止且正確。

複雜度備註：最壞仍需 \(O(2^n)\) 分支，但 unit propagate 常大幅剪枝。純文字規則在現代已少用，因檢測成本高，但思想仍在。

習題：手跑 \(S = \{ \{p, q, r\}, \{\lnot p, q\}, \{\lnot q, r\}, \{\lnot r\} \}\) 。先由 \(\lnot r\) 觸發 unit，再連鎖推得 \(q\) 與 \(p\) 之值，最終得 SAT 賦值 \(p = True\) 、 \(q = True\) 、 \(r = False\) 。體會 propagate 鏈的威力。

延伸閱讀：Davis Logemann Loveland 1962 原文、Donald Knuth《The Art of Computer Programming》卷四 SAT 章。前案重溫請見 Davis Putnam 程序，後續一階推廣請見 Robinson 歸結。