5.1 3-SAT與布爾可滿足性#

概念說明#

布爾可滿足性問題（SAT, Satisfiability）是計算理論中第一個被證明為 NP-complete 的問題，堪稱「NP-complete 之王」。問題敘述很單純：給定一個由布林變數、AND、OR、NOT 組成的邏輯公式，問是否存在一組變數真假值的指派，使整個公式為真。

實務上最常用的形式是 CNF（合取範式）：公式是一堆子句（clause）的 AND，每個子句是若干個文字（literal，即變數或其否定）的 OR。例如：

(x1 ∨ ¬x2) ∧ (¬x1 ∨ x3) ∧ (x2 ∨ x3 ∨ ¬x4)

當每個子句恰好包含 3 個文字時，這個特例稱為 3-SAT。3-SAT 依然是 NP-complete（Cook-Levin 定理之後由 Karp 經化約證明），這個「恰好三個」的限制看似讓問題變簡單，實則不然——三個文字已足以表達任意的邏輯約束，這也是為什麼 3-SAT 成為化約時最受歡迎的「源頭問題」：把 3-SAT 化約到你的問題，通常比從一般 SAT 出發容易得多。

一個有 n 個變數、m 個子句的 3-SAT 實例，暴力解法是列舉所有 2ⁿ 種指派，逐一檢查是否滿足所有子句，時間為 O(2ⁿ · m)。截至今日，沒有人找到多項式時間的演算法；但另一方面，現代 SAT 求解器（見 7.3 節）在工業實例上動輒能處理百萬變數，這是理論與實務之間耐人尋味的落差。

演算法步驟#

讀入子句列表，每個子句是三個文字的集合，文字以整數編碼（正數 i 代表 xi，負數 -i 代表 ¬xi）。
對每個子句，檢查變數是否同時出現正負兩種文字——若是，此子句恆真，可移除（化簡）。
使用回溯法：選一個未指派的變數，先後嘗試賦值 True 與 False。
每次賦值後檢查是否有子句的三個文字全部為假——若是，立刻回溯（剪枝）。
若所有變數都有指派且無子句被違反，回報 SAT；若所有分支皆失敗，回報 UNSAT。

Python 程式碼範例#

from itertools import product

def sat_brute_force(num_vars, clauses):
    """暴力列舉所有指派，O(2^n * m)"""
    for values in product([False, True], repeat=num_vars):
        assign = {i + 1: values[i] for i in range(num_vars)}
        if all(any(assign[abs(l)] == (l > 0) for l in clause)
               for clause in clauses):
            return assign
    return None

def sat_backtracking(num_vars, clauses):
    """回溯法＋剪枝：發現子句全假立刻回溯"""
    assign = {}

    def clause_state(clause):
        """回傳 'sat' / 'conflict' / 'open'"""
        has_true = has_unassigned = False
        for l in clause:
            v = assign.get(abs(l))
            if v is None:
                has_unassigned = True
            elif v == (l > 0):
                return 'sat'
        if has_unassigned:
            return 'open'
        return 'conflict'

    def solve(i):
        if i > num_vars:
            return dict(assign)
        for val in (True, False):
            assign[i] = val
            if all(clause_state(c) != 'conflict' for c in clauses):
                result = solve(i + 1)
                if result is not None:
                    return result
            del assign[i]
        return None

    return solve(1)

clauses = [[1, -2], [-1, 3, 2], [-3, 4], [2, -4, 1]]
print(sat_brute_force(4, clauses))    # 找到一組滿足指派
print(sat_backtracking(4, clauses))   # 剪枝後通常更快

複雜度分析#

暴力法：2ⁿ 種指派 × 每次檢查 O(m)，總計 O(2ⁿ·m)。
回溯法：最壞情況仍是 O(2ⁿ·m)，但剪枝在多數實例上大幅縮短搜尋樹。
空間複雜度：O(n + m)，只需儲存指派與子句。
理論下界：在指數時間假設（ETH）下，3-SAT 無法在 2^o(n) 時間內解決。

練習#

將公式 (x1 ∨ x1 ∨ x2) ∧ (¬x1 ∨ ¬x1 ∨ ¬x2) 寫成 Python 的子句列表，並用程式判斷是否可滿足，找出所有滿足指派。
修改 sat_backtracking，加入「單元傳播」（unit propagation）：當某子句只剩一個未指派文字時，直接強制賦值。比較修改前後在隨機 3-SAT 實例上的節點數。
寫一個亂數產生器，生成 n = 10、m = 43 的隨機 3-SAT 實例（子句/變數比約 4.3 是相變區），統計 20 次實驗中可滿足的比例。