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

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