充足可能性ソルバ (SAT ソルバ) の原理
Hiromi ISHII

2024-03-10
Tsukuba Computer Mathematics Seminar 2024

充足可能性ソルバ (SAT ソルバ) の原理
充足可能性ソルバ (SAT ソルバ) の原理

本日の話題：充足可能性問題と SAT ソルバ
充足可能性問題：与えられた命題論理式が （古典的に） 充足可能かどうかを判定する問題
古典命題論理式：命題変数 𝑃 , …, 𝑄 , …, を ∧（かつ）、∨（または）、→（ならば）、¬（でない）で結んで得られる論理式
古典的充足可能性 : 与えられた式を真とするような、 命題変数への真偽値∘（真）または ×（偽）の割り当てが存在するか？

充足可能性（SATisfiability）を略して SAT と呼ぶ。
NP- 完全：総当たりで解けるような任意の問題が SAT に帰着できる
本来 SAT は判定問題だが、具体的な求解まで含めて SAT と呼ぶ事が多い

色々な問題が SAT（やその拡張である SMT ソルバ）で解け、実用上も重要
充足可能性ソルバ (SAT ソルバ) の原理

1/27

SAT で解ける問題の例：論理パズル
問 (三人の島民 [1])

常に嘘だけをいう嘘吐きと、 本当のことだけをいう正直者だけが住む島
で、A, B, C 三人の島民に出会った。彼らのいうことには：
A：「B と C はどちらも正直者だ」
B：「A は嘘吐きで、C は正直者だ」
A, B, C はそれぞれ正直者か、嘘吐きか？

充足可能性ソルバ (SAT ソルバ) の原理

2/27

三人の島民：回答
𝐴,𝐵,𝐶 を「A が正直者」「B が正直者」「C が正直者」を表す命題変数とする
情報を命題論理式に変換して (PA) ∧ (PB) を充足する解を求めればよい：
𝐴⟷𝐵∧𝐶

(PA)

𝐵 ⟷ ¬𝐴 ∧ 𝐶(PB)

真理表を書いてみると、全員嘘吐きだとわかる。
𝐴

𝐵

𝐶

(PA)

(PB) (PA) ∧ (PB)

𝐴

𝐵

𝐶

(PA)

(PB) (PA) ∧ (PB)

∘
∘
∘
∘

∘
∘
×
×

∘
×
∘
×

∘
×
×
×

×
×
∘
∘

× ∘
× ∘
× ×
× ×

∘
×
∘
×

×
∘
∘
∘

∘
×
×
∘

×
×
×
×

充足可能性ソルバ (SAT ソルバ) の原理

×
×
×
∘

3/27

SAT で解ける問題の例：数独
簡単な例として、4 × 4 の小さな数独の問題を SAT で解くことを考える。
𝑖, 𝑗, 𝑘 ≤ 4 に対し命題変数 𝑃 = を用意する （𝑑いうきもち）。

= 𝑘と各マスには 1, 2, 3, 4 のいずれかの数字一つを入れる。
𝑃= ∨ 𝑃= ∨ 𝑃= ∨ 𝑃=
≤

≤

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑑

𝑃 = ⟶ ¬𝑃 =∧≤≠

充足可能性ソルバ (SAT ソルバ) の原理

4/27

SAT で解ける問題の例：数独 （続）各行、各列、各 2 × 2 の小ブロックには各数字 1, …, 4 が一つずつ入る。
「各行」は次のように書ける（「各列」も 𝑖, 𝑗 の役割を入れ換え同様）：(𝑃 = ∨ 𝑃 = ∨ 𝑃 = ∨ 𝑃 = )≤≤演習問題：「一意性」の条件が要らない理由を考えてみよう。
演習問題：「各ブロック」の条件を書き下してみよう。

あとは盤面の情報を 𝑃 = の and で与えれば個別の問題を解ける！

充足可能性ソルバ (SAT ソルバ) の原理

5/27

SAT で解ける問題の例：命題論理の定理自動証明
SAT ソルバは定理の自動証明にも使える
定理 (古典命題論理の完全性定理および健全性定理 (Gödel))任意の古典命題論理式 𝜑 に対し、𝜑 がどんな真偽値の割り当てに対しても真であることと、𝜑 が証明可能であることは同値である。
系 (証明可能性の特徴付け)

任意の古典命題論理式 𝜑 が証明可能である必要十分条件は、¬𝜑 が充足可能でないことである。
¬𝜑 が充足可能でない事がわかれば、𝜑 が証明できたことになる！
充足可能性ソルバ (SAT ソルバ) の原理

6/27

SAT で解ける問題の例： SMT ソルバへ
SAT だけでも強力だが、更に述語論理（∀ とか ∃ とかを入れたやつ）に拡張した SMT（SAT Modulo Theories）ソルバの研究も盛んに行われている
代表的なソルバ： Z3, CvC5, etc.

SMT で扱える理論の例：線型計画法、整数計画問題、同値関係、配列、etc.
数独なんかは配列の理論とかを使ったほうが綺麗
工学的にもこれらはかなり重要
定理証明系で人間が手で書きたくない補題の自動証明にも使える

SMT は SAT ソルバを外部の理論ソルバと協業させこれらの問題を解く
SAT を如何に速く解くかが SMT の実装にも重要

Disclaimer: 今回は SMT の話はしません

充足可能性ソルバ (SAT ソルバ) の原理

7/27

SAT ソルバの原理
SAT ソルバの原理

SAT は 「難しい」論理パズルの解法で見たように、すべての命題変数の有り得る真偽値の割り当てを総当たりして、真理表をつくれば原理的には解ける
これは命題変数の数を 𝑛 とすると 2 通りの場合分けが必要になる
もっと効率的な方法はないか？

実は「総当たりで解ける問題」は全て SAT に帰着できる（SAT は NP- 完全である）ことが知られている
𝑃 ≠ NP 予想が正しければ、本質的に効率的な解法は存在しない

本質的に速くなくても実用的な問題に対し十分速い手法が研究されている
以下ではその中でも主流な CDCL 法の原理を簡単に紹介（参考文献 [2–5]）
SAT ソルバの原理

8/27

連言標準形 （CNF）
SAT ソルバは連言標準形 (CNF) と呼ばれる形の論理式を扱うことが多い
CNF: (𝑃 ∨ ¬𝑄 ∨ 𝑅) ∧ (𝑄 ∨ ¬𝑅) ∧ (𝑅) ∧ (𝑆 ∨ ¬𝑇 ) みたいな論理式
定義 (CNF の定義)

1. 命題変数 𝑃 とその否定 ¬𝑃 を合わせてリテラルと呼ぶ。 以下、 リテラルを表すメタ変数を
𝑙, 𝑙 などと書く。
2. 0 個以上のリテラルを「または」で繋いだもの 𝑙 ∨ … ∨ 𝑙 を節と呼ぶ。以下、節を表すメタ
変数を 𝐶, 𝐶 などと書く。
3. 0 個以上の節を「かつ」で繋いだ 𝐶 ∧ … ∧ 𝐶 の形の論理式を連言標準形（Conjunctive Normal Form, CNF）と呼ぶ。
注意：空の節は矛盾に、空の CNF は恒真に対応する。

任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

𝑛∨𝑛 ∧ (¬𝑛 ∨ 𝑛 ∨ 𝑅) ∧ (¬𝑛 ∨ 𝑛 ) ∧ (¬𝑅 ∨ 𝑛 )

𝑛

¬

𝑛

∧

𝑅

∧ (¬𝑛 ∨ ¬𝑛 ) ∧ (𝑛 ∨ 𝑛 )∧ (¬𝑛 ∨ 𝑃 ) ∧ (¬𝑛 ∨ 𝑄) ∧ (¬𝑃 ∨ ¬𝑄 ∨ 𝑛 )𝑃

𝑄任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

𝑛∨𝑛 ∧ (¬𝑛 ∨ 𝑛 ∨ 𝑅) ∧ (¬𝑛 ∨ 𝑛 ) ∧ (¬𝑅 ∨ 𝑛 )

𝑛

¬

𝑛

∧

𝑅

∧ (¬𝑛 ∨ ¬𝑛 ) ∧ (𝑛 ∨ 𝑛 )∧ (¬𝑛 ∨ 𝑃 ) ∧ (¬𝑛 ∨ 𝑄) ∧ (¬𝑃 ∨ ¬𝑄 ∨ 𝑛 )𝑃

𝑄任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

𝑛∨𝑛 ∧ (¬𝑛 ∨ 𝑛 ∨ 𝑅) ∧ (¬𝑛 ∨ 𝑛 ) ∧ (¬𝑅 ∨ 𝑛 )

𝑛

¬

𝑛

∧

𝑅

∧ (¬𝑛 ∨ ¬𝑛 ) ∧ (𝑛 ∨ 𝑛 )∧ (¬𝑛 ∨ 𝑃 ) ∧ (¬𝑛 ∨ 𝑄) ∧ (¬𝑃 ∨ ¬𝑄 ∨ 𝑛 )𝑃

𝑄任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

𝑛∨𝑛 ∧ (¬𝑛 ∨ 𝑛 ∨ 𝑅) ∧ (¬𝑛 ∨ 𝑛 ) ∧ (¬𝑅 ∨ 𝑛 )

𝑛

¬

𝑛

∧

𝑅

∧ (¬𝑛 ∨ ¬𝑛 ) ∧ (𝑛 ∨ 𝑛 )∧ (¬𝑛 ∨ 𝑃 ) ∧ (¬𝑛 ∨ 𝑄) ∧ (¬𝑃 ∨ ¬𝑄 ∨ 𝑛 )𝑃

𝑄任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

𝑛∨𝑛 ∧ (¬𝑛 ∨ 𝑛 ∨ 𝑅) ∧ (¬𝑛 ∨ 𝑛 ) ∧ (¬𝑅 ∨ 𝑛 )

𝑛

¬

𝑛

∧

𝑅

∧ (¬𝑛 ∨ ¬𝑛 ) ∧ (𝑛 ∨ 𝑛 )∧ (¬𝑛 ∨ 𝑃 ) ∧ (¬𝑛 ∨ 𝑄) ∧ (¬𝑃 ∨ ¬𝑄 ∨ 𝑛 )𝑃

𝑄任意の命題論理式は CNF で表せる
定理 (命題論理式の CNF への変換)

任意の命題論理式 𝜑 は同値な CNF 𝜑を持つ。

de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数 𝑛 を導入し、各節のサイズが高々 3 の CNF（3-CNF）に変換できる
論理式 ¬(𝑃 ∧ 𝑄) ∨ (𝑅 ∧ 𝑆) の CNF への変換例：

𝑛∨𝑛 ∧ (¬𝑛 ∨ 𝑛 ∨ 𝑅) ∧ (¬𝑛 ∨ 𝑛 ) ∧ (¬𝑅 ∨ 𝑛 )

𝑛

¬

𝑛

∧

𝑅

∧ (¬𝑛 ∨ ¬𝑛 ) ∧ (𝑛 ∨ 𝑛 )∧ (¬𝑛 ∨ 𝑃 ) ∧ (¬𝑛 ∨ 𝑄) ∧ (¬𝑃 ∨ ¬𝑄 ∨ 𝑛 )演習問題：他の結合子の変換規則を考えてみよう。

𝑃𝑄

DPLL: CDCL の祖先
CDCL の基礎は Davis–Putnam–Logemann–Loveland (DPLL) アルゴリズム
基本的な考え方： CNF の節やリテラルを削れるまで削ってから場合分け充足された節は削除できる → 節が一つもなくなれば充足可能！
偽なリテラルがあれば、節から削除できる → 空な節ができたら充足不能！

以下の規則に従って CNF を変形する：
単位節伝播：リテラル一つだけの節 𝑙 があれば 𝑙 ≡ ⊤ とし ¬𝑙 を削除
純リテラル：肯定または否定のみ出現するリテラル 𝑙 があれば 𝑙 ≡ ⊤ としそのリテラルを含む節を削除（コスト面から実装しない事が多い）
Decide：他規則が適用できないならリテラルを一つ選び場合分け真偽を仮決めし継続。失敗したら巻き戻し (Backtrack) 否定で確定し継続

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する

SAT ソルバの原理

12/27

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する(1, 2) (3, 4) (5, 6) (2, 5, 6)

SAT ソルバの原理

∣

12/27

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する(1, 2) (3, 4) (5, 6) (2, 5, 6)− Dec 1 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)

SAT ソルバの原理

∣
∣1

12/27

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する(1, 2) (3, 4) (5, 6) (2, 5, 6)∣− Dec 1 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1− Unit 2 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1 2

SAT ソルバの原理

12/27

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する(1, 2) (3, 4) (5, 6) (2, 5, 6)∣− Dec 1 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1− Unit 2 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1 2− Dec 3 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣ 1 23

SAT ソルバの原理

12/27

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する(1, 2) (3, 4) (5, 6) (2, 5, 6)∣− Dec 1 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1− Unit 2 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1 2− Dec 3 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣ 1 23− Dec 5 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣ 1 23 5

SAT ソルバの原理

12/27

DPLL の動作例
¬𝑃1 ∨ 𝑃2 ∧ 𝑃3 ∨ 𝑃4 ∧ ¬𝑃5 ∨ ¬𝑃6 ∧ ¬𝑃2 ∨ ¬𝑃5 ∨ 𝑃6 を DPLL で解いてみよう（[2] の例）。
今後は CNF しか出て来ないので、(1, 2) (3, 4) (5, 6) (2, 5, 6) と略記する(1, 2) (3, 4) (5, 6) (2, 5, 6)∣− Dec 1 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1− Unit 2 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣1 2− Dec 3 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣ 1 23− Dec 5 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣ 1 23 5− Unit 6 ⟶(1, 2) (3, 4) (5, 6) (2, 5, 6)∣ 1 23 5 6

SAT ソルバの原理

12/27

Backtrack しまくる DPLL の動作例
(1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)− Dec [1-4] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣∣ …4− Unit [5-11] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ … 4 … 11

− Unit 12 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ … 4 … 11 12− Bktrk ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ …4− Dec [5-7] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ …4…7− Unit [8-11] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ … 4 … 11

− Bktrk ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ …4…7− ⋯ ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ … 4 … 11

− Bktrk ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ …4…6− ⋯ ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ … 4 … 11

− Bktrk ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ …4…5− Bt on 7, 8, 10, 11 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣ … 5 7 8 10 11

CDCL: Conflict-Driven Clause Learning
単純総当たりより DPLL は賢いが、Backtrack で得られる情報が少ない
折角 Backtrack でいったん真偽値が確定しても、 更に Backtrack すればその情報は消えてしまう

Backtrack は一段階ずつしか戻らない
場合分けが入れ子になっている場合、実は直近の場合分けよりもっと早くに矛盾が起きていても延々と一段階ずつ Backtrack してしまう

矛盾からに過程を辿っていって矛盾の原因となった「理由」を見付け。学
習節として CNF に追加してそこまで一気に巻き戻そう (Backjump) ！
これが矛盾からの節学習 (Conflict-Driven Clause Learning, CDCL)SAT ソルバの原理

14/27

CDCL: どういう学習節が望ましいか？
学習節が元々の入力の帰結であること
任意のタイミングで Backjump が起き得る
いつでも使えるように、仮定が本質的には増えていてはならない「すぐに使える」学習節であること
Backjump した直後に、新しい情報が得られないと意味がない
特に、巻き戻した段階で単位節になっているようにしたい

なるべく小さいほうがよい
単位節や矛盾が比較的すぐ出るようにしたい

含意グラフを考えるとこれらを満たす学習節を得られる
SAT ソルバの原理

15/27

CDCL：含意グラフ
これまでに真偽を割り当てたリテラルを頂点として持つ有向グラフ
単位伝播で真になったリテラルへ、根拠となったリテラルから辺を伸ばす
単位伝播＝「他のリテラルが真にならなかったので最後の一つを真にする」「根拠」：つまり、真偽を確定させた節に含まれる他のリテラルの否定
ただ一つのリテラルを持つ単位節のリテラルや、場合分けリテラルの場合入次数はゼロ

以下は最初の (1, 2) (3, 4) (5, 6) (2, 5, 6) に対する含意グラフの例
黒丸はこれよりも前の場合分けで仮置きされたリテラル

3

5

6

1

2

6

赤丸は互いに矛盾したリテラル
SAT ソルバの原理

16/27

CDCL：含意グラフと学習節 1 - カットと矛盾原因
含意グラフを conflict side と reason side の二つの集合にカットすると、矛盾への原因が得られる
直接矛盾した頂点は必ず conflict side に入れる
現在の場合分けの起点以前のものは全て reason side に入れる
それ以外のリテラルはどちらに割り当ててもいい

このとき、reason side のリテラルは conflict side の原因になっている
特に conflict side に向かう辺を持つ reason side の頂点があれば十分
3

5

6

reason side

conflict side1

2

SAT ソルバの原理

6

17/27

Cut と学習節の例：多段 Backtrack の例の序盤(1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)
1
5
3

4

2
8

7
6

Cut 𝐴

12
10

9

Cut 𝐵

11

12

Cut 𝐶

Cut A: (1, 2, 3, 4) → 3 の場合分け直後へ飛び、4 が単位節伝播
Cut B: (2, 7, 8) → 2 の場合分け直後へ飛ぶが何もわからない
Cut C: (2, 10) → 2 の場合分け直後へ飛び、10 が単位節伝播
単位節になっているものとなっていないものの違いは何か？

単位節と UIP
Cut に対応する学習節が単位節になるのは、 一意相互作用点 （UniqueInteraction Point, UIP）と呼ばれる頂点の直後で Cut した時
頂点 𝑙 が UIP である ⟺ グラフから 𝑙 を取り除くと、直近の決定リテラルから少なくとも一方の矛盾頂点へのパスが消える（「必ず通る点」）

前の例では 4, 7, 10 が UIP で、Cut 𝐴, 𝐶 が頂点 4, 10 の直後の Cut に相当「学習節が単位節になる」ためには UIP で切ればよい（逆もまた真）決定リテラル自身も UIP なので、少なくとも一つ UIP は存在する
矛盾に一番近い UIP、1-UIP の Cut がよいことが経験的に知られている [6]前の例では、(2, 10) に対応する 10 で切った Cut 𝐶 が 1-UIP
conflicting side が増えるほど必要な仮定も増えそうなので、直感的ではある
SAT ソルバの原理

19/27

1-UIP 学習節の生成と導出規則
含意グラフは概念上でわかりやすいが、直接実装する必要はない
矛盾節に導出規則 (Resolution) を単位節になるまで繰り返し適用すればよい
定理 (導出規則)

以下の導出規則は古典論理の派生規則：𝑐 ∨ 𝛷, ¬𝑐 ∨ 𝛹𝛷∨𝛹
古典的に 𝑐 ∨ 𝛷 は ¬𝑐 → 𝛷 と、¬𝑐 ∨ 𝛹 は 𝑐 → 𝛹 とそれぞれ同値
更に排中律があるので 𝑐 ∨ ¬𝑐 が成り立つから、結局 𝛷 ∨ 𝛹 が結論できる
SAT ソルバの原理

20/27

導出の繰り返しで 1-UIP 学習節を作る
1. 矛盾した二つの節の矛盾リテラルに導出規則を適用
2. 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用「単位節になる」＝最後の場合分け以後の命題変数が一つになる

学習節の導出の例：

SAT ソルバの原理

21/27

導出の繰り返しで 1-UIP 学習節を作る
1. 矛盾した二つの節の矛盾リテラルに導出規則を適用
2. 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用「単位節になる」＝最後の場合分け以後の命題変数が一つになる

学習節の導出の例：
1
5
3

4

2
8

7
6

12

(2, 10, 12)12(11, 12)10
9

11

SAT ソルバの原理

21/27

導出の繰り返しで 1-UIP 学習節を作る
1. 矛盾した二つの節の矛盾リテラルに導出規則を適用
2. 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用「単位節になる」＝最後の場合分け以後の命題変数が一つになる

学習節の導出の例：
1
5
3

4

2
8

7
6

12

(2, 10, 12)(2, 10, 11)

10
9

11

12

(11, 12)
SAT ソルバの原理

21/27

導出の繰り返しで 1-UIP 学習節を作る
1. 矛盾した二つの節の矛盾リテラルに導出規則を適用
2. 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用「単位節になる」＝最後の場合分け以後の命題変数が一つになる

学習節の導出の例：
1
5
3

4

2
8

7
6

12

(2, 10, 12)(2, 10, 11)

10
9

11

12

(10, 11)(11, 12)
SAT ソルバの原理

21/27

導出の繰り返しで 1-UIP 学習節を作る
1. 矛盾した二つの節の矛盾リテラルに導出規則を適用
2. 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用「単位節になる」＝最後の場合分け以後の命題変数が一つになる

学習節の導出の例：
1
5
3

4

2
8

7
6

12

(2, 10, 12)(2, 10, 11)

10
9

11

12

(10, 11)(2, 10)(11, 12)
SAT ソルバの原理

21/27

導出の繰り返しで 1-UIP 学習節を作る
1. 矛盾した二つの節の矛盾リテラルに導出規則を適用
2. 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用「単位節になる」＝最後の場合分け以後の命題変数が一つになる

学習節の導出の例：
1
5
3

4

2
8

7
6

12

(2, 10, 12)(2, 10, 11)

10
9

11

12

(10, 11)(2, 10)(11, 12)

根拠となる節で導出を繰り返す事が、「原因」を手繰っていく事に対応
SAT ソルバの原理

21/27同じ例の CDCL の動作
長い例で学習節ありの Backjump がどう振る舞うか見てみよう(1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)− ⋯ ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12)∣∣ … 4 … 11 12− Bkjmp ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2)∣1 2− Unit 10 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2)∣ 1 2 10− Dec [3-4] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2)∣ 10 … 4− Unit [5-8] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2)∣ 10 … 8− Bkjmp ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ 1 2 10− Unit 7 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ …7− Dec [3-4] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ …4− Unit [5-6] ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ …6− Dec 8 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ …8− Unit 9 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ …4 …68 9− Dec 11 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ … 11− Unit 12 ⟶ (1, 2, 3, 4, 5) (3, 4, 6) (5, 6, 1, 7) (7, 8) (2, 7, 9) (8, 9, 10) (10, 11) (11, 12) (10, 2, 12) (10, 2) (2, 7, 10)∣ 1 … 12

Backjump 二回だけですんなり解けている！

CDCL：更なる最適化手法
現代の CDCL では以下のようなテクニックで効率化が図られている：
監視リテラル：単位節または矛盾節の検出方法の効率化
観察：単位節・矛盾節確定するのは、リテラル数が 2 以下になったときだけ
そこで、節ごとに最大 2 つのリテラルを監視リテラルとして指定
監視リテラルの真偽が確定したときだけ、その節の状態を確かめて単位節・矛盾節の検出を行えばよい！

変数選択ヒューリスティクス：場合分けする変数と真偽には任意性がある
どのリテラル、値を選ぶかで性能が大きく変わる
時間減衰する優先度をつかう VSIDS など変数選択の指標が提案されている選択の指標に関しては、例えば Liang らの論文 [7] が詳しい

CDCL：更なる最適化手法 （続）リスタート：履歴の破棄
辿った履歴によって簡単にとけたり、逆に永遠に解けなかったりする
そこで矛盾が起きたら一定間隔で状態を破棄し、ゼロから解きなおす
学習節は捨てず、間隔はだんだん長くするので、完全性は担保される
リスタート間隔のヒューリスティクスは Wu らの論文 [8] が詳しい

忘却：増えすぎた節の枝刈りをする
矛盾のたびに学習節が増えるので、節数が爆発しがち
そこで、適切な指標の下で優先度の低い学習節を定期的に削除削除するのは学習節だけなので、完全性に影響しない
SAT ソルバの原理

24/27

実装、 まとめ実装、 まとめCDCL 型 SAT ソルバの実装
MiniSat[9] (http://minisat.se) がシンプルかつ高速で、実装の参考になる
herbrand[10]: MiniSAT や参考文献を基に私が Haskell で実装してみたもの
https://github.com/konn/herbrandHaskell を使って実装
それでも GC は無効化されないのでまだまだ遅い
メモリまわりの管理を MiniSat を参考に改築したい

実装、 まとめ

25/27

まとめ
SAT ソルバは古典命題論理式の充足可能性を判定するプログラム
NP- 完全なので本質的に難しい
CDCL: 矛盾するごとに学習節を作り、必要なところまで一気に巻き戻す
監視リテラルや Restart など、色々なヒューリスティクスが提案されている

CDCL は述語論理上の理論に一般化した SMT ソルバの基礎でもある
私の動機： Presburger 算術 （整数計画法） と未解釈関数つき同値関係の理論の組合せソルバを実装したい
整数計画法のインクリメンタルでバックトラック可能で完全なソルバが必要
CVC4 [11] のサイトなどを見てみたがパッと見付からずよい文献をご存知の方おしえてください
実装、 まとめ

26/27

参考文献
[1] レイモンド・スマリヤン , “スマリヤンの決定不能の論理パズル ゲーデルの定理と様相論理 ,” 白揚社 , 2008.
[2] Aleksandar Zeljić, "CS357: Advanced Topics in Computer Science". Course Material. Stanford University. 2019. https://web.stanford.edu/class/cs357/.
[3] 鍋島秀和 and 宋剛秀 , “高速 SAT ソルバーの原理 ,” 人工知能 , pp. 68–68, vol. 25, no. 1, 2010, https://www.jstage.jst.go.jp/article/jjsai/25/1/25_68/_arti-

cle/-char/ja/.
[4] 岩沼宏治 and 鍋島秀和 , “SMT：個別理論を取り扱う SAT 技術 ,” 人工知能 , pp. 86–86, vol. 25, no. 1, 2010, https://www.jstage.jst.go.jp/article/
jjsai/25/1/25_86/_article/-char/ja/.
[5] Enuba Torlak, “A Modern SAT Solver”. Course Material. 2003. https://courses.cs.washington.edu/courses/cse507/17wi/lectures/L02.pdf.
[6] L. Zhang et al., “EffEfficient Conflict Driven Learning in a Boolean Satisfiability Solver,” in Proceedings of ICCAD-01, November 2001, pp. 279–279.
[7] J. H. Liang et al., “Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers,” in Hardware and Software: Verification and Testing, N. Piterman, Eds., Cham: Springer International Publishing, November 2015, pp. 225–225.
[8] H. Wu, “Randomization and Restart Strategies,” Master's Thesis, University of Waterloo, pp. 1–1, 2006.
[9] Niklas Eén and Niklas Sörensson. MiniSat. http://minisat.se/.
[10] Hiromi ISHII. herbrand . https://github.com/konn/herbrand.
[11] Clark W. Barrett, et al. "CVC4". in Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. pp. 171-177. https://doi.org/10.1007/978-3-642-22110-1_14. https://cvc4.github.io/publications.html.