2-SAT：O(n+m) 解布林可滿足性問題

SAT 是 NP-complete，但 2-SAT 是 P——只差一個「每個子句最多兩個變數」的限制，難度天壤之別。

問題形式

n 個布林變數 x₁, x₂, …, xₙ，m 個子句，每個子句是「兩個文字的 OR」：

(x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₃) ∧ (x₂ ∨ x₃)
 
文字 = 變數 xᵢ 或其否定 ¬xᵢ
 
問：是否存在賦值使所有子句同時為真？若存在，給出一組解。

轉化為蘊含圖

每個子句 (a ∨ b) 等價於兩條蘊含：

(a ∨ b) = (¬a → b) ∧ (¬b → a)
  若 a 為假，b 必須為真
  若 b 為假，a 必須為真
 
建圖：
  節點 2i = xᵢ（正文字）
  節點 2i+1 = ¬xᵢ（負文字）
 
每個子句 → 兩條有向邊

(x₁ ∨ ¬x₂)：
  ¬x₁ → ¬x₂（若 x₁ 假則 x₂ 必假）
  x₂  → x₁ （若 x₂ 真則 x₁ 必真）

用 Tarjan SCC 求解

boolean solve() {
    tarjanSCC(graph);
 
    for (int i = 0; i < n; i++) {
        // xᵢ 和 ¬xᵢ 在同一個 SCC → 邏輯矛盾，無解
        if (sccId[2*i] == sccId[2*i + 1])
            return false;
    }
 
    // 賦值：Tarjan 按逆拓撲序編號
    // sccId[xᵢ] > sccId[¬xᵢ] → xᵢ = true
    for (int i = 0; i < n; i++)
        assignment[i] = sccId[2*i] > sccId[2*i + 1];
 
    return true;
}

為什麼 SCC 能解決這個問題？

蘊含圖的 SCC 內所有節點「邏輯上等價」——若某條路徑能從 xᵢ 推出 ¬xᵢ，且也能從 ¬xᵢ 推出 xᵢ，那麼兩者在同一個 SCC 裡，就是矛盾無解。

賦值時，在拓撲序後面的 SCC（Tarjan 編號更大的）代表「更多蘊含的結果」——把這一側設為 true 更容易同時滿足所有蘊含。

競程應用

2-SAT 的典型轉化：

「xᵢ 和 xⱼ 不能同時為真」= (¬xᵢ ∨ ¬xⱼ)
→ 一個子句
 
「xᵢ 必須為真」= (xᵢ ∨ xᵢ)
→ 只新增 ¬xᵢ → xᵢ 一條蘊含邊

排班問題（每個人值班或休假，某些組合不行）、電路設計約束、圖著色的特殊情況，都可以建模成 2-SAT。

拿「圖的 2-著色」當例子看它多順手：每個節點 v 用 xᵥ 代表紅、¬xᵥ 代表藍，每條邊 (u,v) 只要求兩端不同色，寫成 (xᵤ ∨ xᵥ) ∧ (¬xᵤ ∨ ¬xᵥ)——一條邊剛好兩個子句。跑完 2-SAT 有解就代表能 2-著色，也就是二分圖判定。當然這題用 BFS 染色更直接，但重點是：一旦你把「非黑即白 + 成對限制」的問題看成 2-SAT，很多乍看不同的題目其實是同一台引擎在轉。

🎬 互動視覺化： 2-SAT — 看子句怎麼變成蘊含圖的有向邊，Tarjan 縮出 SCC 後，xᵢ 和 ¬xᵢ 落在同一團就當場宣告無解。

---

2-SAT 的優雅在於：把「能否同時滿足」的問題轉化成「圖上是否有矛盾路徑」——邏輯問題變成圖論問題。

接下來往哪走

• Binary Lifting：O(log n) 跳祖先、找 LCA — 下一篇：進入樹上演算法四部曲的第一部
• Advanced Graph 進階圖論 — 2-SAT 的引擎是 Tarjan SCC，演算法本體在這裡