7.3 SAT求解器與DPLL#

概念說明#

雖然 SAT 是 NP-complete 的原型問題，但工業級 SAT 求解器（MiniSat、CaDiCaL、Kissat 等）每天在晶片驗證、排程、密碼分析中處理數百萬變數的實例。這個「理論最壞指數、實務卻能擴展」的奇蹟，起源於 1962 年的 DPLL 演算法（Davis–Putnam–Logemann–Loveland），以及 1990 年代加入的兩大改良：單元傳播（unit propagation）與學習子句（clause learning, CDCL）。

DPLL 的核心是「遞迴回溯 + 三條化簡規則」：

單元傳播：若某子句只剩一個未指派文字（單元子句），該文字必須為真，直接賦值並傳播。這條規則能引發連鎖反應，一次決定大量變數。
純文字消去：若某變數在所有子句中都以同一極性出現，直接賦它為真。
分支：否則選一個變數，分別嘗試 True 與 False。

CDCL（Conflict-Driven Clause Learning）更進一步：當某分支衝突（子句全假）時，分析衝突成因，學出一條新子句記錄「這組賦值組合必導致衝突」，然後回跳（non-chronological backtracking）到相關決策層。學到的子句永久保留，使求解器「記住教訓」，避免同樣衝突重複出現——這是現代求解器威力倍增的關鍵。

演算法步驟#

預處理：移除恆真子句（同時含 l 與 ¬l）、刪除重複文字。
單元傳播：反覆掃描，遇到單元子句就賦值、簡化其餘子句；若出現空子句則衝突。
純文字消去：極性單一的變數直接賦值。
若無子句剩餘 → SAT；若有空子句 → 回溯。
分支：選取出現頻率最高的變數（簡易啟發式），先試 True。
遞迴進入下一層；兩個極性都失敗則回報 UNSAT。

Python 程式碼範例#

def dpll(clauses, assign=None):
    """DPLL：單元傳播 + 純文字消去 + 回溯"""
    assign = dict(assign or {})
    clauses = [set(c) for c in clauses]

    def propagate(clauses, assign):
        changed = True
        while changed:
            changed = False
            for c in clauses:
                c -= {l for l in c if assign.get(abs(l)) == (l < 0)}
                if not c:
                    return None, assign          # 衝突
                units = [l for l in c
                         if abs(l) not in assign]
                if len(c) == len(units) == 1:    # 單元子句
                    l = units[0]
                    assign[abs(l)] = (l > 0)
                    changed = True
        return clauses, assign

    def pure_elim(clauses, assign):
        lits = {l for c in clauses for l in c}
        for v in {abs(l) for l in lits}:
            if v in assign:
                continue
            pos = any(l == v for l in lits)
            neg = any(l == -v for l in lits)
            if pos != neg:                       # 純文字
                assign[v] = pos
        return clauses, assign

    clauses, assign = propagate(clauses, assign)
    if clauses is None:
        return None
    if not clauses:
        return assign
    clauses, assign = pure_elim(clauses, assign)

    # 分支：選最常出現的變數
    from collections import Counter
    cnt = Counter(abs(l) for c in clauses for l in c
                  if abs(l) not in assign)
    if not cnt:
        return assign
    var = cnt.most_common(1)[0][0]
    for val in (True, False):
        trial = [c | {-var} for c in clauses]
        trial = [c for c in trial if var not in c or
                 not assign.get(var, False)]
        result = dpll(
            [[l for l in c if abs(l) != var] for c in clauses],
            assign)
        if result is None:
            continue
        result[var] = val
        return result
    return None

clauses = [[1, -2], [-1, 3, 2], [-3, 4], [2, -4, 1]]
sol = dpll(clauses)
print(sol)   # 一組滿足指派

複雜度分析#

DPLL 最壞情況 O(2ⁿ)，與暴力法同階。
單元傳播是多項式時間（每輪 O(總文字數)），但它能把搜尋樹的分支因子壓到極小；純文字消去同理。
CDCL 在許多結構化實例上呈現「接近多項式」的行為；理論上已證明 CDCL 可模擬解析證明系統（resolution），其最壞下界仍是指數的（如鴿籠原理公式族）。
工程關鍵：有效率地實作「被監看文字」（watched literals）使單元傳播接近 O(1) 均攤；VSIDS 變數活動度啟發式；重啟策略。

練習#

為 dpll 加上節點計數器，在隨機 3-SAT（n = 15，子句/變數比 4.3）上統計與純回溯法的節點數比例。
產生鴿籠原理公式 PHP(n+1, n)（n+1 隻鴿子進 n 個籠無解），觀察 DPLL 需要的節點數隨 n 的爆炸成長，體會「UNSAT 證明難」的意涵。
實作簡化的子句學習：衝突時記錄「導致衝突的賦值組合」為一條新子句，比較前後在重複實例上的節點數。