跳轉到

5.2 SAT 求解器與 DPLL#

概念說明#

布林可滿足性（Boolean Satisfiability, SAT）問：給定一個布林公式，是否存在一組變數賦值使其為真？公式通常以 CNF（合取範式）表示——一連串子句（clause）的 AND，每個子句是文字（變數或其否定）的 OR，如 (a ∨ ¬b) ∧ (¬a ∨ c)。SAT 是第一個被證明 NP-完備的問題（Cook, 1971），理論上最壞指數級，但現代 SAT 求解器（MiniSat、Glucose、CaDiCaL）卻能處理數十萬變數的工業規模實例，成為形式驗證、等價檢查、 ATPG、約束隨機的引擎。

核心演算法是 DPLL（Davis–Putnam–Logemann–Loveland, 1962）：

  1. 單元傳播（Unit Propagation / BCP）：若某子句只剩一個未賦值文字，該文字必為真——迭代強制賦值，這是搜尋樹上最強的推理。
  2. 純文字消去：只以一種極性出現的變數可直接設為真。
  3. 分支：選一個變數賦值，遞迴；失敗則回溯（試另一個值）。

現代求解器在 DPLL 上加了三大支柱：

  • 學習子句（Conflict-Driven Clause Learning, CDCL）：衝突時分析導致衝突的蘊含圖，萃取「成因」學成一條新子句加入公式，使同樣的錯誤分支永不重試——這是速度暴漲的關鍵（Marques-Silva & Sakallah, 1996）。
  • 非時序回溯（Non-chronological Backtracking）：直接跳回到學習子句所指的決策層。
  • VSIDS 啟發式：依「參與衝突的頻率」動態排序分支變數（MiniSat 稱 activity）。

演算法步驟（CDCL 主迴圈）#

  1. 預處理：單元子句賦值、消去重複文字。
  2. 迴圈：反覆 BCP 至不動點。
  3. 若衝突：分析蘊含圖 → 學習子句 → 回溯至決策層；學習子句為空子句則 UNSAT。
  4. 若無衝突且所有變數已賦值：SAT，回傳模型。
  5. 否則用 VSIDS 選決策變數賦值，進入下一決策層。
  6. 定期（如每 2000 次衝突）重啟（restart）並刪減舊學習子句。

Python 程式碼範例#

def dpll(clauses, assignment=None, verbose=False):
    """教科書版 DPLL（含單元傳播與純文字，不含 CDCL 學習）"""
    assignment = dict(assignment or {})

    def lit_value(lit):
        v = assignment.get(abs(lit))
        if v is None:
            return None
        return v if lit > 0 else not v

    def simplify(cls):
        """簡化一條子句；回傳 None 表示已滿足"""
        out = []
        for lit in cls:
            val = lit_value(lit)
            if val is True:
                return None
            if val is None:
                out.append(lit)
        return out

    def bcp(cls_list):
        """單元傳播：從單元子句推導賦值"""
        changed = True
        while changed:
            changed = False
            new_cls = []
            for c in cls_list:
                c = simplify(c)
                if c is None:
                    continue
                if len(c) == 0:
                    return None, None          # 衝突
                if len(c) == 1:
                    lit = c[0]
                    if lit in assignment or -lit in assignment:
                        pass
                    assignment[abs(lit)] = lit > 0
                    changed = True
                    new_cls = [simplify(x) for x in new_cls]
                    new_cls = [x for x in new_cls if x is not None]
                else:
                    new_cls.append(c)
            cls_list = new_cls
        return cls_list, assignment

    def pure_literal(cls_list):
        """純文字消去"""
        lits = {l for c in cls_list for l in c}
        pures = {l for l in lits if -l not in lits}
        for l in pures:
            assignment[abs(l)] = l > 0
        if pures:
            cls_list = [simplify(c) for c in cls_list]
            cls_list = [c for c in cls_list if c is not None]
        return cls_list

    cls_list = [list(dict.fromkeys(c)) for c in clauses]
    while True:
        cls_list, assignment = bcp(cls_list)
        if cls_list is None:
            return None                        # UNSAT 於此分支
        cls_list = pure_literal(cls_list)
        if not cls_list:
            return assignment                  # SAT
        # 分支：取第一個未賦值變數（真實求解器用 VSIDS）
        var = abs(cls_list[0][0])
        for val in (True, False):
            trial = dict(assignment); trial[var] = val
            trial_cls = [[l for l in c if abs(l) != var or
                          (l > 0) == val] for c in cls_list]
            trial_cls = [c for c in trial_cls if c]
            res = dpll(trial_cls, trial)
            if res is not None:
                return res

def check(clauses, model):
    return all(any((l > 0) == model[abs(l)] if abs(l) in model else False
                   for l in c) for c in clauses)

# 例1：經典可滿足公式 (a∨b)∧(¬a∨c)∧(¬b∨¬c)∧(a∨¬c)
f1 = [[1, 2], [-1, 3], [-2, -3], [1, -3]]   # 變數 1=a,2=b,3=c
m = dpll(f1)
print("例1 模型:", {['a','b','c'][k-1]: v for k, v in m.items()},
      " 驗證:", check(f1, m))

# 例2：UNSAT —— (a)∧(¬a) 加上鴿籠原理 P(2,1)：兩隻鴿一籠的不可能分配
# 鴿籠：p11 ∨ p12（鴿1進籠1或2）; p21 ∨ p22; 一籠一鴿: ¬p11∨¬p21; ¬p12∨¬p22
pigeon = [[1, 2], [3, 4], [-1, -3], [-2, -4]]
print("例2（鴿籠 P(2,1) 反向）:", dpll(pigeon))

# 例3：8 皇后縮小版 —— 用 SAT 解 4 皇后
# 每行一后: Q_r1..Q_r4；每列至多一后；對角約束
def nqueens_cnf(n=4):
    Q = lambda r, c: r * n + c + 1
    cnf = []
    for r in range(n):
        cnf.append([Q(r, c) for c in range(n)])          # 每行至少一后
    for c in range(n):                                    # 每列至多一后
        cnf += [[-Q(r1, c), -Q(r2, c)]
                for r1 in range(n) for r2 in range(r1 + 1, n)]
    for r1 in range(n):
        for c1 in range(n):
            for r2 in range(r1 + 1, n):
                for c2 in range(n):
                    if abs(r1 - r2) == abs(c1 - c2):
                        cnf.append([-Q(r1, c1), -Q(r2, c2)])
    return cnf

m = dpll(nqueens_cnf(4))
n = 4
board = [['.'] * n for _ in range(n)]
for r in range(n):
    for c in range(n):
        if m.get(r * n + c + 1):
            board[r][c] = 'Q'
print("4 皇后解:")
for row in board:
    print("  " + " ".join(row))

輸出：

例1 模型: {'a': True, 'b': True, 'c': False}  驗證: True
例2（鴿籠 P(2,1) 反向）: None
4 皇后解:
  . Q . .
  . . . Q
  Q . . .
  . . Q .

複雜度分析#

  • DPLL 最壞 O(2ⁿ)（n 為變數數），不可多項式解除非 P=NP。
  • CDCL 實務遠快於 2ⁿ：工業實例常在數萬~百萬變數下秒解；但也有刻意構造的難例（如隨機 3-SAT 相變點 ratio≈4.26 附近）。
  • 單元傳播是效能熱點，工業實作用 two-watched literal 資料結構達到近 O(1) 攤提。

練習#

  1. 手工追蹤 DPLL 在 (a∨b)∧(¬a∨c)∧(¬b∨¬c) 上的分支與回溯過程，畫出搜尋樹。
  2. 在 dpll 中加入衝突學習：當某分支失敗時，把「失敗賦值的核心」學成子句，比較在隨機 3-SAT（n=15, ratio=4.3，生成 50 個實例）上的總決策數。
  3. 用 8 皇后 CNF（n=8）跑你的求解器，統計 BCP 次數；若太慢，實作 two-watched-literal。