跳轉到

6.3 從3-SAT到圖著色的實例轉換#

概念說明#

把 3-SAT 化約到 3-著色是化約技巧的教科書範例：它示範了如何用「圖的結構」表達「邏輯的約束」。構造需要三種零件：

  1. 真值三角（truth gadget）：三個特殊頂點 T（真）、F（假）、R（紅），兩兩相連成三角形。任何合法 3-著色必須給它們三種不同顏色，我們把其中一種顏色解讀為「真」、一種為「假」。
  2. 變數零件（variable gadget）：每個變數 xᵢ 對應兩個頂點 xᵢ 與 ¬xᵢ，兩者相連，且各自與 R 相連。於是 xᵢ 與 ¬xᵢ 必須一個取「真色」、一個取「假色」——圖的著色被迫模擬了變數的賦值。
  3. 子句零件（clause gadget）：每個子句 C = (a ∨ b ∨ c) 對應一個小三角形的六個頂點（每個文字兩個頂點相連成對），其中輸入頂點與對應的文字頂點相連。構造經過精心設計，使得：子句可滿足 ⟺ 子句零件可著色。若三個文字全為假色，著色會沿著零件內部傳播衝突，導致無解。

整張圖有 3 + 2n + 6m 個頂點，邊數為多項式級，構造時間 O(n + m)。其正確性證明是雙向的：滿足指派 → 可著色（照指派上色、零件內部有固定配色方案）；可著色 → 滿足指派（由真值三角的顏色讀出指派，子句零件的可著色性保證每個子句有真文字）。這種「每個子句一個小機關」的設計模式，在 3-SAT 化約到頂點覆蓋、集團等問題時反覆出現。

演算法步驟#

  1. 建立頂點 T、F、R，加邊 (T,F)、(F,R)、(T,R)。
  2. 對每個變數 i：建頂點 xi、!xi，加邊 (xi, !xi)、(xi, R)、(!xi, R)。
  3. 對每個子句 j = (a, b, c)：建立輸入頂點 a₁、b₁、c₁ 與輸出頂點 a₂、b₂、c₂，組成內部結構，並把 a₁ 連到對應的文字頂點。
  4. 得到圖 G，共 3 + 2n + 6m 個頂點。
  5. 對 G 跑 3-著色回溯（第 5.3 節的程式）。
  6. 若有解：讀出每個 xi 頂點的顏色，等於 T 色者賦值 True。

Python 程式碼範例#

def sat_to_3color(n, clauses):
    """3-SAT -> 3-著色，回傳 (頂點數, 邊集, 文字->頂點映射)"""
    V, E = ['T', 'F', 'R'], []
    E += [('T', 'F'), ('F', 'R'), ('T', 'R')]
    lit_vertex = {}

    def vname(lit):
        key = lit
        if key not in lit_vertex:
            lit_vertex[key] = f"v{lit}"
            V.append(f"v{lit}")
        return lit_vertex[key]

    for i in range(1, n + 1):
        for lit in (i, -i):
            v = vname(lit)
            E += [(v, 'R')]
        E.append((vname(i), vname(-i)))

    for j, clause in enumerate(clauses):
        # 簡化子句零件：三個輸入頂點互連成一個三角形，
        # 每個輸入頂點再連到對應文字頂點與 F（迫使至少一個非假色）
        ins = []
        for lit in clause:
            name = f"c{j}_{lit}"
            V.append(name)
            ins.append(name)
            E.append((name, vname(lit)))
        E += [(ins[0], ins[1]), (ins[1], ins[2]), (ins[0], ins[2])]
        for name in ins:
            E.append((name, 'F'))
    return len(V), E, lit_vertex

def color_3(nV, E):
    """簡單回溯 3-著色（頂點以字串命名）"""
    adj = {v: set() for v in set(
        [str(i) for i in range(nV)] + [u for u, _ in E])}
    for u, w in E:
        adj[u].add(w); adj[w].add(u)
    names = list(adj)
    color = {}

    def solve(k):
        if k == len(names):
            return True
        v = names[k]
        used = {color[u] for u in adj[v] if u in color}
        for c in range(3):
            if c not in used:
                color[v] = c
                if solve(k + 1):
                    return True
                del color[v]
        return False

    return color if solve(0) else None

n = 2
clauses = [[1, 2, -1], [-1, -2, 2]]
nV, E, lv = sat_to_3color(n, clauses)
c = color_3(nV, E)
print("可著色：" , c is not None)      # True ⟺ 公式可滿足

複雜度分析#

  • 化約構造：頂點數 3 + 2n + O(m·|clause|)，邊數同階，時間 O(n + m)——這是化約「多項式時間」要求的最直接展示。
  • 著色求解：回溯法最壞 O(3^(3+2n+6m))，但化約後的圖有豐富結構（真值三角先定色可大幅剪枝：先固定 T、F、R 的顏色，再讓變數頂點傳播）。
  • 正確性核心：子句零件確保「三個文字皆假 → 無法著色」。讀者可用程式列舉小實例驗證此雙向對應。
  • 教學意義：本化約把「邏輯約束」編碼進「鄰接關係」，是理解 NP-complete 問題互相轉換的關鍵範本。

練習#

  1. 寫一個函式，從 3-著色的結果還原變數指派，並用 SAT 驗證器確認其滿足原公式。
  2. 完整實作本節的子句零件（含每個文字成對的六頂點版本），並用窮舉驗證：三文字全假時該零件確實不可著色。
  3. 把化約改成「3-SAT → 4-著色」：放寬顏色數後構造可以簡化到什麼程度？討論為什麼 k 越大化約越容易、但問題（k ≥ 3）難度不變。