史上第一個被證明 NP-Complete 的問題：給一堆「三選一」的條件，找出讓全部條件成立的真假指派
想像你在排一場婚宴座位。每位親戚都提出條件：「A 桌要有我、或別讓二叔坐 A 桌、或把我排到 C 桌」——每個條件都是三個要求中至少滿足一個。你要找出一種安排讓所有條件同時成立。這就是 3-SAT：每個子句給你三個機會，你只要讓每個子句至少中一個。
布林變數 \(x_1,\dots,x_n\) 的文字（literal）是 \(x_i\) 或其否定 \(\lnot x_i\)。 子句（clause）是若干文字的 OR，例如 \((x_1 \lor \lnot x_2 \lor x_3)\)。 CNF 公式是若干子句的 AND。 3-SAT 問：每個子句恰有 3 個文字的 CNF 公式，是否存在一組真假指派使公式為真？
公式 \(\varphi = (x_1 \lor x_2 \lor x_3)\land(\lnot x_1 \lor \lnot x_2 \lor x_3)\land(x_1 \lor \lnot x_2 \lor \lnot x_3)\land(\lnot x_1 \lor x_2 \lor \lnot x_3)\)。 取 \(x_1=\text{真},x_2=\text{假},x_3=\text{假}\)：四個子句依序由 \(x_1\)、\(\lnot x_2\)、\(x_1\)、\(\lnot x_3\) 滿足，全部成立，故 \(\varphi\) 可滿足。
為什麼 3-SAT 是「難題之王」
Cook–Levin 定理（1971）：SAT 是第一個被證明的 NP-Complete 問題；3-SAT 是它的標準化版本。任何 NP 問題都能在多項式時間內「翻譯」成 3-SAT。
之後 Karp 用歸約把 3-SAT 的難度傳染給 21 個問題（Clique、Vertex Cover、Hamiltonian……），本系列後面的每一篇，難度的源頭都是 3-SAT。
2 與 3 的分水嶺：2-SAT（每子句兩個文字）可用強連通分量在多項式時間解決；加到 3 個文字就 NP-Complete。難度的跳變常常就發生在一個參數 +1。
「NP-Complete」不代表「每個實例都算不動」。實務 SAT 求解器天天在解上百萬變數的工業實例——難的是最壞情況，不是每種情況。
演算法一：暴力枚舉
\(n\) 個變數共有 \(2^n\) 組指派，逐一檢查每組是否滿足全部 \(m\) 個子句：
\[T(n,m) = O(2^n \cdot m \cdot 3)\]
\(n=20\) 時約 \(10^6\) 組還行；\(n=50\) 時 \(10^{15}\) 組就永遠跑不完。暴力法的價值是當標準答案：用它驗證聰明演算法沒寫錯（本篇程式的 Example 3 正是這麼做）。
演算法二：DPLL
DPLL（Davis–Putnam–Logemann–Loveland, 1962）是所有現代 SAT 求解器的骨架。它仍是回溯搜尋，但加了三個關鍵推理規則，讓搜尋樹大幅縮小。
三個核心規則
單元傳播（Unit Propagation）：若某子句只剩一個未定文字，該文字被迫為真。例如 \((x_3)\) 只剩 \(x_3\)，那 \(x_3\) 必須是真——沒有分支的必要。連鎖反應常常一路推倒一整排骨牌。
純文字消去（Pure Literal Elimination）：若變數 \(x_i\) 在剩餘公式中只以一種極性出現（全是 \(x_i\) 或全是 \(\lnot x_i\)），直接把它設為讓那些子句滿足的值，穩賺不賠。
分支（Splitting）：推不動了才挑一個變數 \(x_i\)，先試 \(x_i=\) 真，失敗再試 \(x_i=\) 假。挑「出現次數最多」的變數是簡單有效的啟發式。
終止條件
公式化簡後沒有子句了 \(\Rightarrow\) 全部滿足，回報 SAT（目前的指派就是解）。
出現空子句（子句的文字全為假）\(\Rightarrow\) 這條路矛盾，回溯。
最壞情況仍是 \(O(2^n)\)——3-SAT 是 NP-Complete，這無法避免——但實務上單元傳播會砍掉絕大多數分支。本篇程式在 \(n=20\)、\(m=80\) 的隨機實例上只拜訪了 8 個節點，而暴力法要看 \(10^6\) 組。
手算走一遍
用 \(\varphi = (x_1 \lor x_2)\land(\lnot x_1 \lor x_3)\land(\lnot x_2 \lor \lnot x_3)\land(x_2)\)（示範用 2–3 文字混合）：
子句 \((x_2)\) 是單元子句 \(\Rightarrow\) 強制 \(x_2=\) 真。
化簡：\((x_1 \lor x_2)\) 已滿足消失；\((\lnot x_2 \lor \lnot x_3)\) 剩 \((\lnot x_3)\)——又是單元子句 \(\Rightarrow\) \(x_3=\) 假。
化簡：\((\lnot x_1 \lor x_3)\) 剩 \((\lnot x_1)\) \(\Rightarrow\) \(x_1=\) 假。
公式清空 \(\Rightarrow\) SAT，解為 \(x_1=\)假、\(x_2=\)真、\(x_3=\)假。全程零分支。
相變現象：隨機 3-SAT 什麼時候最難
隨機生成 \(n\) 個變數、\(m\) 個子句的 3-SAT，實驗發現以 \(m/n \approx 4.27\) 為界：
\(m/n \ll 4.27\)：約束少，幾乎必定 SAT，而且很好找。
\(m/n \gg 4.27\)：約束太多，幾乎必定 UNSAT，矛盾很快就撞到。
\(m/n \approx 4.27\)：SAT 與 UNSAT 各半，搜尋樹最深，最難的實例都住在這裡。
本篇程式的 Example 4 直接重現這條曲線（\(n=24\)、每點 40 次抽樣）。
完整 C++ 程式
程式包含：暴力枚舉、完整 DPLL（單元傳播、純文字消去、最多出現分支啟發）、隨機 3-SAT 產生器、相變實驗。編譯：
g++ -std=c++17 -O2 -Wall -Wextra -o sat3_dpll sat3_dpll.cpp執行結果與解讀
=== Example 1: hand-crafted 3-SAT (satisfiable) ===
brute force: SAT, model: x1=1 x2=0 x3=0
DPLL : SAT, model: x1=1 x2=1 x3=1 (nodes=3)
=== Example 2: all 8 clauses on 3 vars (unsatisfiable) ===
DPLL: UNSAT (nodes=7)
=== Example 3: random 3-SAT, brute force vs DPLL ===
n=16 m=64 | brute: SAT 6.23 ms | DPLL: SAT 0.12 ms, nodes=7 | agree=yes
n=20 m=80 | brute: SAT 6.03 ms | DPLL: SAT 0.71 ms, nodes=8 | agree=yes
=== Example 4: phase transition (fraction SAT over 40 trials) ===
m/n=3 SAT rate=40/40 avg nodes=14
m/n=3.5 SAT rate=38/40 avg nodes=17
m/n=4 SAT rate=37/40 avg nodes=20
m/n=4.27 SAT rate=25/40 avg nodes=21
m/n=4.5 SAT rate=24/40 avg nodes=20
m/n=5 SAT rate=7/40 avg nodes=19
m/n=5.5 SAT rate=5/40 avg nodes=18三個觀察：(1) Example 1 中兩法都回報 SAT 但給出不同的解——SAT 的解可以不唯一，驗證時要驗「是不是解」而非「跟標準答案一不一樣」。(2) Example 2 用 3 變數的全部 8 個子句構造出必然矛盾的公式，DPLL 只花 7 個節點就證明 UNSAT。(3) Example 4 的 SAT 率在 \(m/n=4.27\) 附近從幾乎全 SAT 掉到幾乎全 UNSAT，且平均節點數在該處達到峰值——正是理論預測的相變。
實務應用
硬體驗證：晶片電路等價性檢查被編碼成 SAT——「兩個電路存在輸入使輸出不同」可滿足嗎？Intel、AMD 每天用工業級求解器跑這件事。
軟體套件相依解析：apt、conda、cargo 的版本相依解析本質是 SAT（「裝 A 需要 B\(\geq\)2 或 C；B 與 D 衝突……」）。
排程與規劃：課表、機組人員排班、AI 規劃（STRIPS planning）常被翻譯成 SAT 後丟給求解器。
現代求解器：CDCL（衝突驅動子句學習）= DPLL + 從失敗中學新子句 + 重啟 + 高效資料結構（watched literals）。學會 DPLL，就看懂了 MiniSat、Z3 的心臟。
練習題
手算：對 \((x_1\lor x_2\lor x_3)\land(\lnot x_1\lor x_2\lor x_3)\land(x_1\lor\lnot x_2\lor x_3)\land(x_1\lor x_2\lor\lnot x_3)\land(\lnot x_1\lor\lnot x_2\lor\lnot x_3)\) 跑一遍 DPLL，記錄每次傳播與分支。
把分支啟發從「出現最多」改成「隨機挑」，在 \(m/n=4.27\) 的實例上比較平均節點數。
實作子句學習雛形：回溯時記下導致矛盾的指派組合，作為新子句加入公式，觀察節點數變化。
寫一個 2-SAT 的多項式解法（蘊含圖 + SCC），對照本篇程式驗證答案一致。
挑戰：把 N-Queens 編碼成 SAT（每格一個變數），用你的 DPLL 解 \(n=6\)。
小結
| 方法 | 時間複雜度 | 適用時機 |
|---|---|---|
| 暴力枚舉 | \(O(2^n m)\) | \(n \leq 25\)；當驗證基準 |
| DPLL | 最壞 \(O(2^n)\)，實務遠低 | 中小型實例、教學、理解求解器 |
| CDCL（工業） | 最壞指數，實務百萬變數 | 真實世界的一切 |
延伸閱讀：Cook (1971) The Complexity of Theorem-Proving Procedures；Biere et al.,Handbook of Satisfiability；MiniSat 原始碼（約 2000 行，出乎意料地好讀）。