1960 年 Davis Putnam 程序：CNF 掃蕩三鐵律#

案件編號：No.1960 — 報案人：命題可滿足性。偵探：Martin Davis、Hilary Putnam。現場：一堆子句。

案發現場#

1958 年，美國軍方把一台 IBM 704 借給兩位邏輯學家。Davis 與 Putnam 接到的報案很單純，卻很要命：給定一個命題公式，它到底有沒有讓它為真的賦值？這就是 SAT 問題。

此時背景是： Logic Theorist 剛用啟發式證明了 《數學原理》 定理， Herbrand 定理 把一階問題化為命題窮舉， 布林代數 早已把邏輯變成計算。但窮舉 \(n\) 個變元要試 \(2^n\) 種賦值， \(n = 30\) 就超過十億。IBM 704 再快也扛不住。

更具體的麻煩是：Herbrand 程序會生成海量子句集，急需一個命題層的清道夫。Davis 與 Putnam 決定不再「證明定理」，而是反向思考：假設公式不可滿足，推導出空子句；若推不出，則可滿足。這是典型的反證偵查法。

他們把所有公式先化為合取範式 CNF：子句集 \(S = \{ C_1, C_2, \dots, C_m \}\) ，每個子句 \(C_i\) 是文字 \(l\) 的析取。例如 \((p \lor q) \land (\lnot p \lor r)\) 對應子句集 \(\{ \{p, q\}, \{\lnot p, r\} \}\) 。案件於是簡化為：子句集可否同時為真？

偵查過程#

Davis 與 Putnam 在 1960 年論文 A Computing Procedure for Quantification Theory 中提出三條掃蕩規則。偵探每次巡邏都先用前兩條低成本規則，能不用重武器就不用。

線索一：單子句規則#

若子句集中出現單子句 \(\{l\}\) ，則任何滿足賦值必須讓 \(l\) 為真。於是刪去所有含 \(l\) 的子句，並從其餘子句中刪去 \(\lnot l\) 。記作 \(S[l := True]\) 。

例如 \(S = \{ \{p\}, \{\lnot p, q\}, \{\lnot q, r\} \}\) ，見 \(\{p\}\) 即令 \(p\) 為真，得 \(\{ \{q\}, \{\lnot q, r\} \}\) ，再令 \(q\) 為真，得 \(\{ \{r\} \}\) ，再令 \(r\) 為真，得空集，宣告可滿足。

這招後來被稱為 unit propagate，是整個 SAT 史的心臟。

線索二：純文字規則#

若變元 \(p\) 在全集中只以一種極性出現，例如只出現 \(p\) 從不出現 \(\lnot p\) ，則可放心令 \(p\) 為真，刪去所有含 \(p\) 的子句。這種文字稱為 pure literal。

直覺是：既然 \(\lnot p\) 從未成為障礙，讓 \(p\) 為真只有好處沒有壞處。偵探比喻為「從未涉案的嫌犯，直接釋放」。

線索三：消去規則#

重頭戲登場。對變元 \(p\) ，把含 \(p\) 的子句 \(C_i \lor p\) 與含 \(\lnot p\) 的子句 \(D_j \lor \lnot p\) 兩兩配對，生成消解子句 \(C_i \lor D_j\) ，再刪去所有含 \(p\) 或 \(\lnot p\) 的原句。這其實是消解的雛形：

Davis 與 Putnam 證明此規則保持可滿足性不變：原集可滿足當且僅當新集可滿足。不斷消去變元，若產出空子句 \(\Box\) 則不可滿足；若子句集清空則可滿足。

線索四：小例子逐步推導#

考慮 \(S = \{ \{p, q\}, \{\lnot p, q\}, \{p, \lnot q\}, \{\lnot p, \lnot q\} \}\) 。無單子句，無純文字，只好對 \(p\) 消去：

• 含 \(p\) 者： \(\{p, q\}\) 、 \(\{p, \lnot q\}\) 。
• 含 \(\lnot p\) 者： \(\{\lnot p, q\}\) 、 \(\{\lnot p, \lnot q\}\) 。
• 配對得： \(\{q\}\) 、 \(\{q, \lnot q\}\) 、 \(\{q, \lnot q\}\) 、 \(\{\lnot q\}\) 。

化簡後得 \(\{ \{q\}, \{\lnot q\} \}\) ，再對 \(q\) 消去得 \(\{ \Box \}\) 。空子句現身，證明不可滿足。這正是鴿巢式的經典矛盾： \(p\) 與 \(q\) 無法同時滿足四種組合。

此例暴露消去規則的弱點：子句數可能暴增。Davis 自己兩年後就動手改掉了它。

結案報告#

Davis Putnam 程序是第一個實用的 SAT 判定程序，也是 Herbrand 程序的命題引擎。它把「試遍 \(2^n\) 賦值」變成「用規則化簡子句集」，在當年 IBM 704 上已能處理數十個變元。

它的歷史位置極關鍵：

• 上承 Logic Theorist 的搜尋精神與 Herbrand 定理 的子句化需求，下啟 DPLL 的分裂革命。
• 消去規則直接預告了 Robinson 歸結原理 的單一推理規則，只是當時還限於命題層。
• 純文字與單子句思想沿用至今，現代 CDCL 求解器的 unit propagate 即其嫡傳。

局限也很清楚：消去規則的記憶體爆炸讓它很快撞牆。兩年後 Davis、Logemann、Loveland 決定不再生成所有消解子句，改用「猜一個、分兩案」的分裂法庭。這就是下一案 DPLL 的開場。

但無論如何，1960 年這一夜，SAT 終於有了第一套警用手冊。

證據與工具#

判定流程摘要：輸入 CNF 子句集 \(S\) ，重複以下步驟直到 \(S\) 為空或含 \(\Box\) ：

1. 若有單子句 \(l\) ，執行 \(S := S[l := True]\) 。
2. 否則若有純文字 \(p\) ，執行 \(S := S[p := True]\) 或 \(S[p := False]\) 依極性而定。
3. 否則選一變元 \(p\) ，執行消去生成新集 \(S := Resolve(S, p)\) 。

正確性要點：前兩條規則顯然保可滿足性，消去規則需證雙向：若 \(v\) 滿足原集則滿足新集；若 \(v'\) 滿足新集則可擴充 \(p\) 之賦值滿足原集。完備性由變元數遞減歸納得到。

習題：用三規則判定 \(S = \{ \{p\}, \{\lnot p, q\}, \{\lnot q\} \}\) 。答案應得 \(\Box\) ，故不可滿足。試比較窮舉四種賦值的工作量。

延伸閱讀：Davis Putnam 1960 原文、Malik 與 Zhang《Boolean Satisfiability》綜述。前情提要可回顧 Church 型別論 如何限縮語言，本案則是讓機器在限縮後的命題荒野中高效巡邏。