4.3 Cook-Levin 定理與 SAT#

概念說明#

1971 年，Stephen Cook 在論文《The Complexity of Theorem Proving Procedures》中提出一個劃時代的定理；同年蘇聯學者 Leonid Levin 也獨立得出相同結果。這就是 Cook-Levin 定理：

SAT 是 NP-complete。 也就是說，SAT ∈ NP，且 NP 中任何問題都可以在多項式時間內化約到 SAT。

這是第一個被證明的 NP-complete 問題，它就像第一塊多米諾骨牌：有了它，後續所有 NP-complete 的證明都不必重頭做起，只要從 SAT（或其後代）出發即可。

定理的證明思路是「把整台圖靈機的執行過程壓縮進一條邏輯公式」。設 L ∈ NP，L 由非決定性圖靈機 N 在多項式時間 p(n) 內決定。對任意輸入 x，我們構造一條布爾公式 φ_x，此公式的變數描述：

時間-空間棋盤（Tableau）：一個 p(n)×p(n) 的格子系統，每格是 M 的一個組態（configuration）的快照，記錄分公司（cell）在該時間步、該紙帶格上寫了什麼符號、讀寫頭在哪、機器處於哪個狀態。
形式上需要以下幾類變數（用「位元表示符號」的方式為每格標記）：
Q_{t,i,q}：時間 t 時，第 i 格的儲存格上的符號是某個特定符號（每格還要用有限個「或」的架構確保恰一個符號成立）；
H_{t,i,q}：時間 t 時，讀寫頭位於第 i 格；
S_{t,q}：時間 t 時，狀態為 q。

接著寫下一組子句，它們共同規定了該棋盤是 N 對 x 的一次合法接受執行路徑：

起始組態子句：時刻 0 的棋盤內容與初始輸入一致（紙帶條形為 x#空格，讀寫頭在 0，狀態為起始狀態）。
接受子句：某個時刻 N 進入接受狀態 q_accept。
合法轉移子句：每一個相鄰時刻的「2×3 電窗」（當前格與右鄰格、時間 t 與 t+1 的交錯）滿足 N 的轉移函數 δ，也就是「局部規則成立」。這可寫成固定大小的布爾公式，用常數數量的子句描述。

於是 φ_x 可滿足 ⟺ 存在一條合法的接受路徑 ⟺ N 接受 x。公式大小是 p(n) 的多項式（實際上是 O(p(n)²) 級，因為要描述每格的符號），且可由演算法在多項式時間內生成。SAT 屬於 NP 是平常的：給定一個真值賦值，我們線性時間檢查每個子句。

由於 f(x) = φ_x 是多項式時間可計算且滿足「x ∈ L ⟺ φ_x ∈ SAT」，故 L ≤ₚ SAT。因 L 是任意 NP 問題，故 SAT 是 NP-hard；加上 SAT ∈ NP，結論就是 SAT 是 NP-complete。

SAT 問題本身：給定一條周述式（CNF，連言/一般形式）φ = c₁ ∧ c₂ ∧ ... ∧ cₘ，其中每個子句 cᵢ = (ℓᵢ₁ ∨ ℓᵢ₂ ∨ ... ∨ ℓᵢₖ) 是文字的選言（文字是變數 xᵢ 或其否定 ¬xᵢ）。SAT 問：是否存在一個賦值使所有子句同時為真？

演算法步驟：用 SAT 驗證器體驗 Cook-Levin#

我們不需證明整個定理，但可用程式示範其中最關鍵的一步——「從一個『是』實例到一條可滿足的公式」。做法是將 N 對 x 的執行棋盤手動錄製成符號位，再生成合法轉移子句。

設定一個簡化的圖靈機 N（有限狀態機 + 單向讀寫）。
選定輸入 x，將 N 的執行過程錄製下來（手工或用模擬器）。
把每個時間步/每格的內容對應到布爾變數的賦值。
檢查傳入的「賦值」是否能滿足所有合法轉移子句。
由此可見：能不能滿足公式 ⟺ 是否存在一條接受路徑。

Python 程式碼範例：SAT 的驗證與暴力解法#

from itertools import product

def sat_brute_force(num_vars, clauses):
    """暴力解 SAT：2^n 賦值。clauses: [[1, -2], [3, ...]]"""
    for bits in product([False, True], repeat=num_vars):
        assign = {i + 1: bits[i] for i in range(num_vars)}
        ok = all(any(assign[abs(l)] != (l < 0) for l in cl)
                 for cl in clauses)
        if ok:
            return assign
    return None

def sat_verify(assign, clauses):
    """驗證器：線性時間。"""
    return all(any(assign[abs(l)] != (l < 0) for l in cl)
               for cl in clauses)

# 例：(x1∨x2) ∧ (¬x1∨¬x2) → x1=False, x2=True 是解
clauses = [[1, 2], [-1, -2]]
sol = sat_brute_force(2, clauses)
print(sol, sat_verify(sol, clauses))   # {1: False, 2: True} True

# 另一例：x1∨x2, x1∨¬x2, ¬x1∨x2, ¬x1∨¬x2 （不可滿足）
clauses2 = [[1, 2], [1, -2], [-1, 2], [-1, -2]]
print(sat_brute_force(2, clauses2))    # None

複雜度分析#

驗證：O(總文字數)，線性時間。
暴力解：O(2ⁿ · m)。雖然至今沒有已知多項式演算法，但實務上有高效的高效能求解器（見第 7.3 節的 DPLL 與 CDCL），可在很多真實實例上秒殺上千萬變數的公式——這是理論中心理論與工程中心的精彩對接。
Cook-Levin 證明中生成的公式，大小是 O(p(n)²)，因此化約是多項式的，定理成立。

練習#

用 Python 為給定的 3-CNF 公式實作一個小小的「真值表枚舉 + 提前剪枝」求解器，並比較它與純暴力法在 n = 15 時的步數差異。
Cook-Levin 的證明構造了「時間-空間棋盤」。請思考：為什麼每個格子只需「固定大小」的文字數量？（提示：每個格子只需表達「這格上的符號是 k 種之一」，用「恰一個為真」的代價也只需 k 個子句。）
Claude Shannon 有一個很有名的猜測：「大多數『實際遇到的』 SAT 實例，要嘛很容易滿足，要嘛很容易否定，很難出現真正的『最難』情況」。請使用下面的程式架構，生成 n = 5、每個子句 3 個文字、m 從 3 增長到 30 的隨機公式，並記錄「可滿足性」與「暴力步數/2ⁿ」的關係，觀察所謂的「難度之牆」（相變現象）大約出現在哪個 m 值。