1967 - Cook 定理：SAT 研究路線與 NP 完備概念的孕育#

案件摘要#

1967 年，Stephen Cook 在一份研究報告中發展了可滿足性（SAT）問題的理論框架，孕育出 NP 類、NP-hard 與 NP-complete 的核心概念。這份報告是 1971 年 Cook–Levin 定理的直接前驅：四年後，SAT 成為第一個被證明 NP-complete 的問題。

前因 -- 為什麼會有這個案子#

1960 年代末，數理邏輯與計算理論在 Cook 手中交會：

一階邏輯的有效公式的判定問題已知不可判定（Church 1936、Turing 1936）；
但命題邏輯（無量詞、有限變元）的判定問題顯然可判定（真值表枚舉， \(2^n\) 時間）；
Hartmanis–Stearns (1965) 剛證明複雜度類之間有真包含，Edmonds (1965) 剛提出 good algorithm。

Cook 在康乃爾研究定理證明自動化（如 Davis–Putnam 程序）時面臨謎題：

命題邏輯公式的可滿足性，似乎「檢查一個給定解答」只要多項式時間，但「找到解答」似乎需要指數時間。這個不對稱性的數學本質是什麼？

線索與推理 -- 數學式、程式、理論#

線索一：SAT 問題的定義（CNF 公式）#

定義（可滿足性 SAT）：給定布爾變元 \(x_1, \dots, x_n\) 與 CNF（合取範式）公式

\[ \varphi = \bigwedge_{i=1}^{m} \left( \ell_{i1} \vee \ell_{i2} \vee \cdots \vee \ell_{ik_i} \right), \quad \ell_{ij} \in \{x_t, \neg x_t\} \]

問：是否存在賦值 \(a \in \{0,1\}^n\) 使 \(\varphi(a) = 1\) ？

SAT ∈ NP 的證據：驗證只需 \(O(|\varphi|)\) 時間。Python：

def sat_formula(clauses, n):
    """clauses: 每個子句是變元索引列表，正數=x_i, 負數=非x_i"""
    def verify(assign):
        return all(any(assign[abs(l) - 1] == (l > 0) for l in c)
                   for c in clauses)
    # 窮舉驗證所有賦值（指數），但「驗證單一賦值」只要 O(len(clauses))
    for bits in itertools.product([0, 1], repeat=n):
        if verify(bits):
            return True, bits
    return False, None

線索二：NP 類的定義——非確定性多項式時間#

Cook 採用非確定性圖靈機（NTM）的觀點：NTM 每一步可在多個分支中任選，若有任一分支接受即接受。

定義： \(L \in \text{NP} \iff L\) 可被某 NTM 在多項式時間內判定：

\[ \text{NP} = \bigcup_{k \geq 1} \text{NTIME}(n^k) \]

等價的（後由 Cook 與 Karp、Levin 發展成標準的）驗證者觀點：

\[ L \in \text{NP} \iff \exists V,\ \exists \text{多項式 } p,\ \text{使得 } x \in L \iff \exists y,\ |y| \leq p(|x|),\ V(x, y) = 1 \]

其中 \(y\) 稱為證書（certificate，如 SAT 的賦值）、 \(V\) 是多項式時間的驗證者。兩個觀點的等價：

NTM 的接受分支路徑 = 證書 \(y\) ；模擬該分支 = 驗證 \(V(x,y)\) 。
這個「尋找 vs 驗證」的不對稱，正是 Cook 在 1967 年報告中抓住的核心。

線索三：NP-hard 與 NP-complete 的概念成型#

Cook 在報告中發展了歸約的分層概念：

定義（多項式時間多一歸約 \(\leq_p\) ，Karp 式）： \(L_1 \leq_p L_2 \iff\) 存在多項式時間可計算函數 \(f\) 使

\[ \forall x:\ x \in L_1 \iff f(x) \in L_2 \]

定義（NP-hard）： \(H\) 是 NP-hard，若 \(\forall L \in \text{NP}:\ L \leq_p H\) 。

定義（NP-complete）： \(C\) 是 NP-complete，若 (1) \(C \in \text{NP}\) 且 (2) \(C\) 是 NP-hard。

歸約的關鍵性質（傳染性/傳遞性）：

\[ L_1 \leq_p L_2,\ L_2 \leq_p L_3 \implies L_1 \leq_p L_3 \]

這意味著 NP-complete 問題是 NP 中「最難的一層」：只要有一個 NP-complete 問題找到多項式演算法，所有 NP 問題都隨之解決。

線索四：Cook 的研究路線——從定理證明到 SAT#

Cook 的路線是一條「化繁為簡」的偵探路：

研究一階邏輯定理證明程序的效率（不可判定，但半可判定）；
發現「計算歷程」可以用邏輯公式編碼——圖靈機第 \(t\) 步的帶上內容、狀態、讀寫頭位置都可寫成布爾變元；
意識到：一階邏輯的有效性 可多項式歸約到 SAT（把「機器 \(M\) 在 \(n\) 步內接受 \(x\) 」寫成 CNF）；
反向推論：既然任何 NP 計算都可如此編碼，SAT 就是 NP 的「萬能翻譯目標」——即 NP-complete。

Python 概念示範（把計算限制編碼為 CNF 子句）：

def transition_clauses(t, pos, state_old, state_new, sym):
    """把『第 t 步從狀態 s 到 s'』編碼成 CNF 子句群"""
    clauses = []
    clauses.append([-state_old(t), state_new(t+1)])   # 狀態轉移
    clauses.append([-state_old(t), sym(t, pos)])      # 寫入符號
    return clauses

結案 -- 後果與影響#

1967 年報告的直接果實：1971 年 Cook 論文證明 SAT 是 NP-complete（Cook–Levin 定理）。
NP、NP-hard、NP-complete 三層概念成為此後所有複雜度分類的骨架。
驗證者觀點 \(\exists V, |y| \leq poly\) 開啟了後續整條研究線：交互式證明（IP）、PCP 定理、密碼學中的零知識證明。
Levin 在蘇聯獨立得到等價結果（1973 發表），顯示此概念是「時代必然」而非偶然。
Cook 因定理證明與複雜度貢獻獲 1982 年圖靈獎。

關鍵人物與文獻#

Stephen Cook（Berkeley→Toronto）：1967 年研究報告（未正式發表的手稿/報告，內容發展成 1971 年 STOC 論文）；〈The Complexity of Theorem-Proving Procedures〉, STOC 1971。
前驅：Edmonds (1965) good algorithm；Hartmanis–Stearns (1965) 複雜度類；Davis–Putnam (1960) SAT 求解程序。
同期獨立：Leonid Levin（蘇聯，1973）「universal search problems」。
後續：Karp (1971) 21 問題、Garey & Johnson (1979)、Cook 圖靈獎演講 (1983)〈An overview of computational complexity〉。