SAT ソルバーの原理

最初に全体像

SAT ソルバーは、命題論理式 \(F\) について「\(F\) を真にする変数割当が存在するか」を判定するアルゴリズムです。入力は多くの場合、連言標準形 CNF（conjunctive normal form）で与えられます。

古典的 DPLL は「単位伝播・純リテラル消去・分岐・バックトラック」による完全探索です。CDCL は DPLL を基礎にしつつ、衝突から新しい節を学習し、非時系列バックトラックで探索空間を飛び越える現代 SAT ソルバーの中核です。

1. SAT 問題の形式化

1.1 変数、リテラル、節、CNF

SAT の判定問題は次です。

ここで \(\alpha\models x\) は \(\alpha(x)=1\)、\(\alpha\models\neg x\) は \(\alpha(x)=0\) を意味します。節 \(C\) はその中の少なくとも 1 つのリテラルが真なら真、CNF \(F\) は全節が真なら真です。

1.2 部分割当と三値評価

探索中の割当は全変数ではなく部分割当 \(\alpha:V\rightharpoonup\{0,1\}\) です。未割当を \(\bot\) ではなく「未定義」として扱うと、各リテラル・節は三値的に評価されます。

1.3 制限・簡約 \(F|_\alpha\)

部分割当 \(\alpha\) のもとで式を簡約する操作を \(F|_\alpha\) と書きます。実装では必ずしも式を物理的に書き換えませんが、概念上は次です。

1. 真になった節は CNF から削除する。
2. 偽になったリテラルは節から削除する。
3. 空節 \(\Box\) が出たら矛盾。
4. 全節が消えたら充足。

上式では第 1 節 \((x\lor y)\) は真で消え、第 2 節 \((\neg x\lor z)\) では \(\neg x\) が偽なので消え、単位節 \((z)\) が残ります。

1.4 CNF への変換：Tseitin 変換

一般の命題式を CNF に単純分配で変換すると指数的に大きくなる場合があります。SAT 実務では Tseitin 変換を用い、部分式ごとに新しい補助変数を導入して、元式と充足可能性が同値な CNF を線形サイズで作ります。

例として、部分式 \(z \leftrightarrow (a\land b)\) は次の CNF で表せます。

重要なのは「論理的同値な CNF」ではなく「充足可能性を保存する CNF」で十分なことです。補助変数の存在量化を考えれば、元式 \(G\) と Tseitin CNF \(T(G)\) について

が成り立ちます。

2. DPLL：単位伝播つき完全バックトラック探索

DPLL は Davis–Putnam–Logemann–Loveland 手続きの略称です。SAT を解く古典的かつ根本的なアルゴリズムであり、現代 CDCL ソルバーも DPLL の探索状態・単位伝播・分岐という骨格を継承しています。

2.1 DPLL の状態

DPLL の状態は概念的には次の組で表せます。

ここで \(F\) は固定の CNF、\(\alpha\) は現在の部分割当です。実装ではさらに、割当順序を表すトレイル、分岐レベル、各割当の理由を持つことがあります。ただし純粋な DPLL では理由節を CDCL ほど本格的には使いません。

2.2 DPLL の 4 つの基本操作

操作 A：単位伝播（unit propagation）

単位伝播は論理的には含意です。\((\neg x\lor y\lor z)\) は \((x\land\neg y)\to z\) と等価なので、\(x=1,y=0\) の下では \(z=1\) が強制されます。

操作 B：純リテラル消去（pure literal elimination）

例えば未充足部分に \(p\) は出るが \(\neg p\) が出ないなら、\(p=1\) として \(p\) を含む全節を満たして構いません。なぜなら \(p=1\) は他の節を偽にする方向には作用しないからです。ただし現代 CDCL では純リテラル消去は探索中に常用されないことも多く、前処理や特殊用途で使われます。

操作 C：分岐（decision / split）

単位節も純リテラルもなく、まだ未割当変数が残っているなら、ある変数 \(x\) を選び、\(x=1\) または \(x=0\) を仮定して探索します。

この同値性が DPLL の分岐の根拠です。変数選択ヒューリスティックは性能を大きく左右しますが、完全性には影響しません。

操作 D：バックトラック

ある枝で空節 \(\Box\) が生じたら、その枝は失敗です。直近の未探索分岐に戻り、反対値を試します。両方の値が失敗すれば、さらに前の分岐へ戻ります。

2.3 DPLL の標準擬似コード

DPLL(F, α):
    # F: CNF, α: partial assignment

    while exists a unit clause C under α:
        let ℓ be the only unassigned literal in C
        α := α ∪ {ℓ = true}
        if some clause is false under α:
            return UNSAT

    if every clause is satisfied under α:
        return SAT with model α

    if some clause is false under α:
        return UNSAT

    optionally apply pure literal elimination:
        for each pure literal ℓ:
            α := α ∪ {ℓ = true}

    choose an unassigned variable x

    if DPLL(F, α ∪ {x = true}) == SAT:
        return SAT
    else:
        return DPLL(F, α ∪ {x = false})

実装では「式を毎回コピーして簡約する」方式は単純ですが遅く、トレイルと監視リストで状態を差分管理します。ただし DPLL の数学的意味は上記で完全に表現できます。

2.4 DPLL を推論規則として書く

DPLL は状態遷移系としても表せます。\(M\) をリテラル列、つまり現在のトレイルとします。\(F\) は固定 CNF です。

2.5 手計算例

次の CNF を考えます。

1. 最初に unit 節はありません。\(a=1\) を決定します。
2. \((\neg a\lor c)\) が unit になり、\(c=1\) が伝播します。
3. \((\neg c\lor d)\) が unit になり、\(d=1\) が伝播します。
4. \((\neg d\lor b)\) が unit になり、\(b=1\) が伝播します。
5. 全節が真になり SAT です。モデルの一例は \(a=b=c=d=1\) です。

2.6 DPLL の停止性・健全性・完全性

理由は、各分岐で未割当変数が少なくとも 1 つ割り当てられ、探索木の深さは高々 \(n\) だからです。単位伝播・純リテラル消去も未割当変数を減らすため無限ループしません。

SAT 側は全節が満たされたことを直接確認して返すため明らかです。UNSAT 側は、単位伝播と純リテラル消去が充足可能性を保存し、分岐が \(x=1\) と \(x=0\) の完全な場合分けであることから従います。

これは変数数に関する帰納法で示せます。\(n=0\) では空 CNF か空節で即判定できます。\(n>0\) では、未割当変数 \(x\) について \(F|_{x=1}\) と \(F|_{x=0}\) の少なくとも一方が SAT なら \(F\) は SAT、両方 UNSAT なら \(F\) は UNSAT です。DPLL はこの完全な場合分けを実行します。

2.7 DPLL の計算量

最悪の場合、DPLL は \(2^n\) 個の割当を調べる必要があります。SAT は NP 完全問題なので、多項式時間で常に解く既知の一般アルゴリズムはありません。ただし、実際の問題では単位伝播、学習、ヒューリスティックにより巨大な探索空間が劇的に削減されます。

3. CDCL：Conflict-Driven Clause Learning

CDCL は DPLL を拡張し、衝突から学習節を導出し、探索を非時系列に戻すアルゴリズムです。現代の完全 SAT ソルバーの中核はほぼ CDCL です。

3.1 CDCL の状態

CDCL の典型的状態は次です。

トレイルの各要素は、実装上はおおむね次の構造体です。

AssignmentEntry = {
    variable: Var,
    value: Bool,
    level: Int,
    reason: Clause | null  # null means decision literal
}

3.2 決定レベルとトレイル

決定レベルは、何回目の意思決定に依存する割当かを表します。レベル 0 は入力の単位節や前処理だけから強制される割当です。新しい decision literal を置くたびにレベルが 1 増え、その後の単位伝播は同じレベルに属します。

上の \(a@2^d\) は「\(a\) はレベル 2 の決定リテラル」、\(b@2^{C_1}\) は「\(b\) はレベル 2 で節 \(C_1\) により伝播した」という意味です。

3.3 CDCL メインループ

CDCL(F):
    L := ∅
    τ := empty trail
    decision_level := 0

    while true:
        confl := BooleanConstraintPropagation(F ∪ L, τ)

        if confl != null:
            if decision_level == 0:
                return UNSAT

            learnt, backjump_level := AnalyzeConflict(confl, τ)
            L := L ∪ {learnt}
            Backjump(τ, backjump_level)
            Enqueue(asserting literal of learnt, reason = learnt)

        else:
            if all variables are assigned:
                return SAT with model τ

            ℓ := PickBranchLiteral()
            decision_level := decision_level + 1
            Enqueue(ℓ as decision, reason = null)

DPLL との核心的な差は、AnalyzeConflict、learnt clause、Backjump の 3 点です。

3.4 Boolean Constraint Propagation（BCP）

CDCL の BCP は、現在の割当で unit になった節を検出し、強制リテラルをトレイルに追加します。BCP の結果は次のどれかです。

素朴にすべての節を毎回走査すると遅いため、現代ソルバーではほぼ必ず 2-watched literals を使います。

3.5 2-watched literals：BCP 高速化の本質

各節で 2 つのリテラルを「監視」します。節 \(C\) が長さ \(k\) であっても、監視中のリテラルが偽になったときだけその節を調べます。監視リテラルの不変条件は次です。

節 \(C=(\ell_1\lor\ell_2\lor\cdots\lor\ell_k)\) で \(\ell_1,\ell_2\) を監視しているとします。\(\ell_1\) が偽になったとき、\(\ell_3, \dots,\ell_k\) の中に偽でないリテラルがあればそこへ監視を移します。なければ、もう一方の監視リテラル \(\ell_2\) の値により次が決まります。

2-watched literals が強力なのは、バックトラック時に監視位置を巻き戻す必要がないことです。割当を取り消すと false だったリテラルは undef に戻るため、「偽でない 2 つをできるだけ監視する」という条件は壊れにくく、前向き伝播だけで管理できます。

3.6 含意グラフ

CDCL は衝突時、トレイル上の「どの割当がどの節によって生じたか」をグラフとして見ます。これが含意グラフです。

含意グラフは明示的に巨大グラフとして保存されるとは限りません。実装では各伝播リテラルの reason clause をトレイルに持つだけで、必要な部分を衝突解析時に辿れます。

3.7 分解能と学習節

CDCL の学習節は、分解能推論で導出されます。分解能の基本形は次です。

ここで \(A,B\) はリテラルの選言です。もし \(F\models A\lor x\) かつ \(F\models B\lor\neg x\) なら、\(F\models A\lor B\) です。したがって、分解能で得た学習節を追加しても元の充足可能性は変わりません。

3.8 asserting clause と backjump level

CDCL で特に重要なのは、学習節をasserting clauseにすることです。現在の決定レベル \(d\) で、学習節の中にレベル \(d\) のリテラルがちょうど 1 つだけ残るように解析すると、より低いレベルへ戻った直後、その節が unit になり、残ったリテラルの反対を強制できます。

学習節を

とし、\(\ell^*\) だけが現在レベル \(d\)、他の \(\ell_i\) はより低いレベルだとします。このとき backjump level は通常、他のリテラルの決定レベルの最大値です。

ただし \(r=0\) なら \(b=0\) です。レベル \(b\) まで戻ると、\(\ell_1, \dots, \ell_r\) はすべて偽のまま残り、\(\ell^*\) だけが未割当になるため、\(C_L\) は unit になり \(\ell^*\) が伝播します。

3.9 UIP と 1-UIP

1-UIP 学習は、実用上非常に標準的です。学習節が短くなりやすく、backjump 後すぐ有効な伝播を生みやすいためです。

AnalyzeConflict(conflict_clause C, trail τ):
    learnt := C

    while number_of_literals_at_current_level(learnt) > 1:
        choose a literal ℓ in learnt whose variable was assigned last
        R := reason(ℓ)              # reason clause that implied ℓ
        learnt := Resolve(learnt, R, variable(ℓ))

    asserting_literal := the only literal in learnt at current level
    backjump_level := maximum level among other literals in learnt
    return learnt, backjump_level

「最後に割り当てられた現在レベルのリテラル」を選ぶと、トレイルを逆向きに辿るだけで 1-UIP 節が得られます。

3.10 MiniSat 風の衝突解析の見方

実装では、毎回節全体を集合演算で作り直すより、マーク配列 seen[var]、カウンタ pathC、一時節 out_learnt を使って効率的に 1-UIP 節を作ります。概念的には次です。

analyze(confl):
    learnt := [⊥ placeholder]
    pathC := 0
    p := null
    idx := trail.size - 1
    clause := confl

    repeat:
        for each literal q in clause:
            if q.var not seen and level(q.var) > 0:
                seen[q.var] := true
                if level(q.var) == current_level:
                    pathC := pathC + 1
                else:
                    learnt.push(q)

        repeat:
            p := trail[idx]
            idx := idx - 1
        until seen[p.var]

        clause := reason(p)
        seen[p.var] := false
        pathC := pathC - 1

    until pathC == 0

    learnt[0] := complement(p)
    backjump := max(level(lit.var) for lit in learnt[1:])
    return learnt, backjump

この p が 1-UIP に対応し、complement(p) が学習節の asserting literal になります。

3.11 CDCL が完全である理由

CDCL は DPLL と同じく完全です。学習節は元の式から含意されるので、解を消しません。backjump は時系列順でないものの、学習節が反対枝や同じ矛盾を禁止するため、論理的に不要な領域を飛ばしているだけです。有限個の節しか存在しない有限変数上では、同じ完全割当を無限に繰り返さないように設計された CDCL は停止し、SAT または UNSAT を返します。

より証明論的には、CDCL は分解能証明を探索していると見なせます。UNSAT の場合、最終的に空節 \(\Box\) を導出する分解能証明が得られます。SAT の場合、全変数割当が衝突なしに完成し、モデルが得られます。

4. 実装・工学的技法

4.1 DIMACS CNF

SAT ソルバーの標準的な入力形式は DIMACS CNF です。変数は正整数、否定リテラルは負整数、各節は 0 で終わります。

p cnf 3 2
1 -2 0
2 3 -1 0

これは \((x_1\lor\neg x_2)\land(x_2\lor x_3\lor\neg x_1)\) を表します。

4.2 リテラルの整数エンコード

実装ではリテラルを整数で表すと高速です。典型例は変数番号 \(v\) と符号 bit \(s\in\{0,1\}\) を使い、

と符号化する方法です。補リテラルは XOR 1 で得られます。

neg(lit) = lit ^ 1
var(lit) = lit >> 1
sign(lit) = lit & 1

この表現では、watch list、activity 配列、割当配列を連続メモリに置けるためキャッシュ効率が良くなります。

4.3 伝播キュー

CDCL では、トレイルのうちまだ伝播処理していない位置を qhead で管理します。

propagate():
    while qhead < trail.size:
        p := trail[qhead]
        qhead := qhead + 1
        for each clause C watching ¬p:
            update watches or return conflict
    return null

新しくリテラル \(p\) が真になると、偽になった補リテラル \(\neg p\) を監視している節だけを調べればよい、というのが watch list の要点です。

4.4 分岐ヒューリスティック：VSIDS

変数選択は性能に直結します。VSIDS 系の考え方では、最近の衝突に関わった変数の activity を上げ、時間とともに decay します。直感的には「最近矛盾を起こした制約の周辺を優先して決める」戦略です。

on conflict with learnt clause C:
    for each variable x in C:
        activity[x] += var_inc
    var_inc *= 1 / decay

pickBranchVariable():
    return unassigned variable with maximum activity

activity は優先度付きキューや heap で管理されます。値が大きくなりすぎる場合は全体を rescale します。

4.5 位相選択と phase saving

変数を選んだ後、それを true にするか false にするかも重要です。phase saving は、過去にその変数が持っていた値を次回の decision でも使う戦略です。多くの実問題では局所的に一貫したモデル候補があり、phase saving は再探索を安定させます。

4.6 restart

restart は、学習節を保持したままトレイルをレベル 0 まで戻す操作です。探索を最初からやり直すように見えますが、学習節が増えているため同じ探索ではありません。

4.7 学習節データベース削減

CDCL は衝突のたびに節を追加するため、放置するとメモリも BCP コストも増大します。そこで、役に立たない学習節を定期的に削除します。

4.8 節最小化

衝突解析で得た学習節には冗長リテラルが含まれる場合があります。節最小化は、あるリテラルが他のリテラルから理由節を通じて導けるなら削除する技法です。

のような関係があれば、\(\ell_3\) の必要性を解析できます。実装では reason graph のレベル集合や再帰的マークにより近似的・効率的に判定します。

4.9 前処理・インプロセッシング

SAT ソルバーは探索前または探索中に式を簡約します。代表的なものは次です。

• unit propagation at level 0：トップレベル単位節を先に伝播。
• subsumption：\(C\subseteq D\) なら \(D\) は冗長なので削除可能。
• self-subsuming resolution：節を分解能で短縮。
• bounded variable elimination：変数を分解能で消去。ただし節数爆発を制限。
• blocked clause elimination：充足可能性を保存する冗長節削除。
• equivalence detection：同値変数や XOR 構造を検出。

4.10 UNSAT 証明と proof logging

産業応用では「UNSAT と出た」だけでは不十分で、検証可能な証明が必要になることがあります。CDCL は学習節を分解能で導出しているため、DRAT、LRAT、FRAT などの証明ログ形式で外部チェッカに検証させられます。

SAT の場合はモデルを検証すればよいので容易です。UNSAT は全探索の正当性を示す必要があり、proof logging が重要になります。

5. DPLL と CDCL の比較

付録：記法・擬似コード・実装チェックリスト

A.1 記法一覧

A.2 実装チェックリスト

A.3 よくある誤解

参考文献

以下は本レポートの背景にある代表的資料です。DPLL の原典、CDCL の初期体系化、Chaff による実装上のブレークスルー、MiniSat 系の簡潔な実装思想を中心に挙げます。

1. Martin Davis, George Logemann, Donald Loveland, “A machine program for theorem-proving,” Communications of the ACM, 1962. CACM page
2. Martin Davis, Hilary Putnam, “A Computing Procedure for Quantification Theory,” Journal of the ACM, 1960.
3. João P. Marques-Silva, Karem A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers, 1999. PDF
4. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik, “Chaff: Engineering an Efficient SAT Solver,” DAC 2001. PDF
5. Niklas Eén, Niklas Sörensson, “An Extensible SAT-solver,” SAT 2003 / MiniSat line of work.
6. Niklas Sörensson, Niklas Eén, “MiniSat v1.13 — A SAT Solver with Conflict-Clause Minimization,” SAT Competition 2005 poster. PDF