Zenn
Open11

CDCL (conflict-driven clause learning) アルゴリズムのSATソルバーを作る

termoshtttermoshtt

通常SATソルバと行った時は命題論理の充足可能性問題を解くアルゴリズムを指しますが、今回は論理学には深入りせずにブール論理の言葉で議論していきます。

ブール論理

ブール論理というのは集合 B = \{0, 1\} に対して、二項演算 \land (論理積)、\lor (論理和)、単項演算 \lnot (否定) 及び以下の性質を満たす代数構造です。

  • 結合則: a \lor (b \lor c) = (a \lor b) \lor c, a \land (b \land c) = (a \land b) \land c
  • 交換則: a \lor b = b \lor a, a \land b = b \land a
  • 吸収則: a \lor (a \land b) = a, a \land (a \lor b) = a
  • 分配則: a \lor (b \land c) = (a \lor b) \land (a \lor c), a \land (b \lor c) = (a \land b) \lor (a \land c)
  • 可補束: a \lor \lnot a = 1, a \land \lnot a = 0
  • 等冪性: a \lor a = a, a \land a = a
  • 有界性: a \lor 0 = a, a \land 1 = a, a \lor 1 = 1, a \land 0 = 0
  • 相補性: \lnot 0 = 1, \lnot 1 = 0
  • ド・モルガンの法則: \lnot (a \lor b) = \lnot a \land \lnot b, \lnot (a \land b) = \lnot a \lor \lnot b
  • 対合: \lnot \lnot a = a

この代数構造を含めてあらためて B と書くことにします。これらの演算のうち結合則・交換則・吸収則・分配則・可補則を満たす任意の台集合を持つ代数構造をブール代数と呼びますが、ブール論理はそのうち特に台集合を B = \{0, 1\} としているものです。

論理式と標準形

可換環に対して多項式を考えたように、ブール論理についても変数を導入し、その変数に対して論理積、論理和、否定を適用することで式を構成できます。これを論理式と呼びます。例えば変数を x_1, x_2, x_3 \in B として、(x_1 \land x_2) \lor x_3 という論理式を考えることができます。このような式は演算の組み合わせによって何通りにも作ることができるので、特に有限回の操作で作ることが出来る論理式全体を多項式環のように B[x_1, x_2, x_3] と書きましょう。この集合にもそのまま論理積・論理和・否定が定義されてブール代数となります。特に変数の無い場合 B[] は B と同一視できます。

1つの多項式に対して例えば x^2 - 1 と (x+1)(x-1) のように同じものを表す複数の表示がありますが、論理式にも同じことが言えます。多項式の場合に和を後に持ってきた x^2 - 1 の形式と積を後に持ってきた (x+1)(x-1) の形式があるように、論理式では \land を後に持ってきたものと \lor を後に持ってきたものがあります。これをそれぞれ連言標準形 (CNF, Conjunctive Normal Form) と選言標準形 (DNF, Disjunctive Normal Form) と呼びます。いずれも \lnot は \land と \lor より前に持ってきます。

SATソルバ

可換環R上の多変数多項式 f \in R[x_1, \ldots, x_n] を使った方程式 f(x_1, \ldots, x_n) = 0 を満たす (x_1, \ldots, x_n) \in R^n の事を方程式の解と呼びますが、同じように多変数の論理式 f \in B[x_1, \ldots, x_n] を使った「方程式」f(x_1, \ldots, x_n) = 1 を満たす (x_1, \ldots, x_n) \in B^n の事を充足解と呼びます。この充足解を求める問題をSAT (Satisfiability) と呼びます。SATソルバはこの問題を解くアルゴリズムのことを指します。

termoshtttermoshtt

論理式 f \in B[x_1, \ldots, x_n] が一つ与えられたとする。例えば x_1 = 1 と仮定してこれを f に代入したものを f(x_1 = 1) \in B[x_2, \ldots, x_n] のように書くことにしよう。

変数の代入に対して充足解がどうなるのかを考えてみよう。
もし f=1の充足解が無いとすると、当然 f(x_1 = 1) = 1の充足解も存在せず、逆にf(x_1=1)=1の充足解が求まったならそこにx_1 = 1を加えるとそれはf=1の充足解になる。x_1 は 0 か 1 しか値を取らないので、f=1の充足解を探す為に f(x_1 = 0) = 1 と f(x_1 = 1) = 1 の充足解を探す問題を解けばよいことが分かる。
これはB[x_1, \ldots, x_n]上の充足解が変数の一つ少ないB[x_2, \ldots, x_n]の充足解を求める問題に分解できること意味しており、一方一つしか変数の無い論理式に対しては充足解を求めることは自明なので、再帰的に問題を分割していけば充足問題は2^n個の自明な問題に分割でき、これは（計算量を考えなければ）常に解けることが分かる。

この原始的なアルゴリズムを単純な再帰として実装したものが brute_force である。決定変数の個数が精々30程度のごくごく小さい問題に対してはこれでも解けることが分かる。
https://github.com/termoshtt/cdcl/pull/5

なお各ステップにおいてどの変数を固定するのか？という問題がある。これはおそらく変数選択ヒューリスティックという分野が始まるはずだが、ここでは単に論理式に含まれる決定変数のうちIDが最も小さいものを選んでいる。

termoshtttermoshtt

次に単位伝搬を実装する。その前にもう少し用語を整理する。

リテラル

ある変数xによって f = x あるいは f = \lnot x でかける論理式をリテラルと呼ぶ。

節 (clause)

SAT問題では通常CNFになった論理式を扱う。CNFは次のようなAND (OR (NOT X))) の形になっている

f = \land_{i=1}^n \lor_{j=1}^m f_{ij}

なおANDとORがそれぞれ無い場合はそれぞれ n と m が 1 のケースと見なす（\land_{i=1}^1 f_i = f_1）。f_{ij}はリテラルである。

CNF系の論理式 f が1になるためにはANDで結合したすべてのサブ論理式 f_i = \lor_{j=1}^m f_{ij} が 1 になっている必要がある。この f_i を f の節 (clause) と呼ぶ。

例えば f_{11} = x, f_{12} = x とすると f_1 = x \lor x であるが、これは等冪則により簡略化してしまって f_1 = x として考える。このように簡略した後の式に含まれる決定変数の個数は一意に定まり、これを長さと呼ぶ。特に長さが 1 の節を単位節と呼ぶ。この時節はリテラルとして書ける。

単位伝搬

さてCNF形式の論理式 f = \land_{i=1}^n f_i の充足解を求める問題に戻ろう。もし f_1 が単位節 f_1 = x_1 であるとき、fが充足可能であるならば常にf_1も充足可能なのですなわちx_1 = 1である。つまり x_1 = 0 の分岐を探査する必要はなく、f(x_1 = 1) の充足可能性を調べれば十分となる。
これは探索する範囲が大幅に狭められることを意味する。

このように単位節によって割り当てられた変数を「含意（implication）」と呼び、一方探索の途中で仮定した変数の事を「決定（decision）」と呼んだりする（文献によって呼び方はわりとバラバラ）。

この含意のプロセスは伝搬する。例えば f_1 = \lnot x_1, f_2 = x_1 \lor x_2 だったとすると、最初にこの節を見たときは f_1 は単位節だが f_2 は単位節ではない。なのでまず f_1により x_1 = 0と含意する。すると f_2(x_1 = 0) = x_2なのでこれは単位節であり、よって x_2 = 1と含意出来る。これが単位節がなくなるまで繰り返すのが単位伝搬である。

このアルゴリズムは以下のPRで dpll として実装した
https://github.com/termoshtt/cdcl/pull/6

termoshtttermoshtt

ある二つの節f_1, f_2 \in B[x_1, \ldots, x_n]があって、特に

f_1 = x_1 \lor g_1, \space f_2 = \lnot x_1 \lor g_2, \space g_1, g_2 \in B[x_2, \ldots, x_n]

と書けるとする。この時に x_1 を「削除」した論理式 g_1 \lor g_2の事を「導出」と呼び f_1 \diamond f_2 と書く。これは任意の節 f_1, f_2 に対して x_1 に相当する変数が指定できれば存在し、存在すれば一意である。例えば二つ以上の組があるケース

\begin{align*} f_1 &= x_1 \lor x_2 \lor x_3, \\ f_2 &= \lnot x_1 \lor \lnot x_2 \lor x_4 \end{align*}

を考えると、これは x_1 を削除するのか x_2 を削除するのかの二通りがあり一意に決まらないように見える。しかしこの場合x_1を削除すると x_2 \lor \lnot x_2 = 1 なので

\begin{align*} (x_2 \lor x_3) \lor (\lnot x_2 \lor x_4) &= (x_2 \lor \lnot x_2) \lor x_3 \lor x_4 \\ &= 1 \lor x_3 \lor x_4 = 1 \end{align*}

同様に x_2 を消去しても x_1 \lor \lnot x_1 = 1 より 1 になる。つまりどっちの変数を消去してももう片方に由来して 1 になるので f_1 \diamond f_2 = 1 として一意に定まる。よってこの \diamond 記号にどの変数を削除するのかを追記する必要はない。

命題論理では A \to B は \lnot A \lor B と表現されるので、

\begin{align*} (A \to B) \diamond (B \to C) &= (\lnot A \lor B) \diamond (\lnot B \lor C) \\ &= \lnot A \lor C = A \to C \end{align*}

となることからもこの操作を導出と呼ぶ理由がうかがえる。

termoshtttermoshtt

導出の重要な性質は次の命題である

(f \land f_i \diamond f_j)(x) = 1なる x \in B^n に対して f(x) = 1 なのは明らかなので逆を示す。

x \in B^n が f(x) = 1 となると仮定しよう。この時全ての l \in [1, m] について f_l(x) = 1である。f_i \diamond f_j が存在するのだから、必要であれば f_i と f_j を入れ替えることにより、あるk \in [1, n]があって節 g_i, g_jによって

f_i = x_k \lor g_i, \space f_j = \lnot x_k \lor g_j

と書けるとしてよい。今 x \in B^n は固定してあるので x_k の値で場合分けする。

  • (x_k = 1 の場合) \lnot x_k = 0 なので f_j(x) = 1 であるためには g_j(x) = 1 でなければならない。よって (f_i \diamond f_j)(x) = (g_i \lor g_j)(x) = g_i(x) \lor g_j(x) = 1
  • (x_k = 0の場合) 同様に f_i(x) = 1 であるためには g_i(x) = 1 でなければならず、(f_i \diamond f_j)(x) = (g_i \lor g_j)(x) = g_i(x) \lor g_j(x) = 1

以上より (f_i \diamond f_j)(x) = 1 \square

節の集合が与えられ時にそれから導出される節を追加しても充足性が変化しないので、もし単位節x_k (あるいは\lnot x_k) が導出出来たら元の論理式の充足解は常にx_k = 1 (あるいはx_k = 0)であるし、0が導出出来たら元の論理式がUNSATであることが結論できる。
CDCLではこのように変数の方を順番に固定していくのではなく節の方を操作していく。

termoshtttermoshtt

これは次の形の方が使いやすい

証明は上の x_k の場合分けそのまま。上の命題はこれから直ちに導ける。

termoshtttermoshtt

充足性を保ったまま節を削除することもできる。その前に少し記法を整理する。

節 f はリテラル f_i によって常に f = \lor_{i=1}^l f_i と書ける。f_iのうち同じものは等冪則によって一つに削減されるので、全ての f_i は異なっているとしてよく、すると節はリテラルの集合として見做すことができる。特にこの時 f_i \in f と書く。

f(x) = 1 なる x \in B^n について、g(x) = 1は上の命題より明らか。逆を示す。

g(x^\prime) = 1となるx^\prime = (x_2, \ldots, x_n) \in B^{n-1}を一つ固定する。問題はx_1をどうやって復元するかである。i \in I_1 \cup \bar{I_1}についてg_iを次で定める：

\begin{align*} f_i &= x_1 \lor g_i &\text{for} \space i \in I_1 \\ f_i &= \lnot x_1 \lor g_i &\text{for} \space i \in \bar{I_1} \end{align*}

もし x_1 = 1 と決めるなら全てのi \in \bar{I_1} について g_i(x^\prime) = 1で無ければf_i(1, x^\prime) = 1と出来ず、x_1 = 0と決めるなら全てのi \in I_1 についてg_i(x^\prime) = 1となっていないと f_i(0, x^\prime) = 1と出来ない。
つまりある組 (i, j) \in I_1 \times \bar{I_1} があって g_i(x^\prime) = 0 かつ g_j(x^\prime) = 0であるならば f(x_1, x^\prime) = 1 となるように x_1 を定めることが出来ない。しかしg(x^\prime) = 1の仮定から全ての (i, j) \in I_1 \times \bar{I_1}の組について (f_i \diamond f_j)(x^\prime) = (g_i \lor g_j)(x^\prime) = 1なので g_i(x^\prime) = g_j(x^\prime) = 0となる組は存在しない。よって f(x_1, x^\prime) = 1となるように x_1をx^\primeから定めることが出来る。 \square

この操作によって充足性を維持したまま変数を一つ取り除くことができる。しかし節の数は p = \#I_1, q = \#\bar{I_1}とすると m - p - q + pq個になっており、最悪のケース p = q = m/2でm^2/4のように節の個数が変数を取り除く回数に対して指数的に増えてしまう事が分かる。

termoshtttermoshtt

以上で素朴なCDCLアルゴリズムを理解する準備が概ね整ったはず。

  • Clause Learningというのは導出節を追加する操作の事
  • 変数を削除するように導出節を追加するのでは節の数が爆発してしまうので不味い。つまり有益な節だけを学習する必要がある。
  • なのでDPLLの時のように変数に仮の値を割り当てていく探索を行いながら矛盾する節を探し、その矛盾した節から導出節を作る事にする。これで必要な節だけが学習できるという目算。

CDCLでは導出により増えていく節と変数の割り当てと同時に連携しながら管理していく必要がある。

Trail

矛盾した節を見つけたときにそれから導出節を作る必要があるので、どの節によって変数を固定することになったかの理由が必要となる。Knuth 4Bではこのデータ構造をTrailと呼んでいる。ここではTrailに何を保存する必要があるのかを議論して最後にTrailのデータ構造を示す。

変数の割り当て

ある変数に値を割り当てる操作は、真であるリテラルのリストにその変数のリテラルを追加することと対応するので、Trailではリテラルのリストを管理する。つまりリテラル l = x_1 がTrailに入っていれば x_1 = 1 と割り当てていて、 l = \lnot x_1 がTrailに入っていればx_1 = 0と割り当てている事に相当する。順々に変数を割り当てる操作はリテラルを順々にTrailに追加していく事に相当する。

単位伝搬

Trailにリテラルを追加する操作は二通りある。一つはDPLLの時の単位伝搬に相当する操作で、既にTrailにリテラル a_1, \ldots, a_kが存在していて、次の節 c がある場合、リテラル \lnot l を c を理由としてTrailに追加する。

c = l \lor \lnot a_1 \lor \cdots \lor \lnot a_k

この操作も同じように単位伝搬と呼ぶ。どの節から評価するか自由度があるが、そこは実装依存という事にしておく。

ここで重要となるのは、理由cに含まれているリテラルは既にTrailに入っている点である。つまりTrailに入っているリテラルの順序には意味がある。Trail内のリテラル l の理由にリテラル a が含まれているとき、lはaに直接依存しているという。

決定

もう一つは決定である。現在のTrailの状態において全ての節を確認して単位伝搬が行えない場合、既にTrailに含まれているリテラルと変数が被らない新しいリテラルをTrailに追加する。この時理由となる節は存在しない。どのようなリテラルを選ぶかは実装依存である。

Trailのリテラルには順序があるので、あるTrail中のリテラルを指定するとそれ以前にいくつ決定により追加されたリテラルが存在するかが一意に定まり、それを決定レベルと呼ぶ。例えば次のようになる：

step リテラル 理由 決定レベル
0 \lnot x_6 決定 1
1 \lnot x_9 決定 2
2 x_3 x_3 \lor x_6 \lor x_9 2
3 \lnot x_4 決定 3
4 x_5 x_5 \lor x_4 \lor x_6 3
termoshtttermoshtt

衝突

Trailにリテラルを追加したとき、ある節 c がTrailに含まれるリテラル a_0, a_1, \ldots, a_k を使って

c = \lnot a_0 \lor \lnot a_1 \lor \cdots \lor \lnot a_k

と書ける場合がある。この時Trailによって指定される変数の割り当てに対して、他の変数をどう指定してもこの節が 0 になることが結論できてしまう。これを衝突と呼ぶ。

もし決定レベル 0 で衝突が起こったならばそれは問題がUNSATである事を意味し、レベル 1 以上で発生した場合は問題がUNSATであるかどれかの決定が間違っているかのいづれかを意味する。

DPLLでは衝突が発生したとき最後の決定が間違っていたとしてバックトラックを行うが、CDCLでは衝突の理由を分析して導出節を追加し、さらにTrailの適切な地点まで一気に巻き戻す。

衝突節

上の設定における衝突節 c の分析に移ろう。現在のTrailの決定レベルを d とする。

まずTrailに変数を追加した後に必ず全ての節について衝突していない事を判定しており、衝突していた場合は処理を継続していない事を前提とすると（あとでそのようにアルゴリズムを定義するが、ここでは仮定とする）、a_0, \ldots, a_kのうちいずれかがTrailに最後に追加されたリテラルであることが分かる。適当に入れ変えることにより、このリテラルを a_0 であるとしてもよい。

続いて決定を行う前に全ての実行可能な単位伝搬を行っていると仮定すると、最後の決定の前の段階で節 c が単位伝搬の対象になっていない事から、a_0, \ldots, a_k のうち少なくとも二つのリテラルが現在の決定レベル d に属していることが分かる。片方は a_0 なので、やはり適当に並べ替えて a_1 がそうであるとしてよい。

するとa_0は現在の決定レベルにおいてa_1より後に追加されていることからa_0の理由は決定ではない（a_1は決定かもしれない）ので理由の節が存在し、それをc_0と書く。これは次の形をしているはずである：

c_0 = a_0 \lor \lnot b_1 \lor \cdots \lor \lnot b_l

ただし b_1, \ldots, b_lは a_0 以前にTrailに追加されたリテラルである。

つまりa_0をTrailに追加する直前の段階で c と c_0 が存在していて、その時のTrailではa_0をどう決めてもこの両方を満たすことは出来ないという事である。どうしてこのような状況になっているのだろうか？a_0 と \lnot a_0 以外の c と c_0 に含まれる全てのリテラル a_1, \cdots, a_k, b_1, \ldots, b_l が全てTrailに含まれているから、すなわち c \diamond c_0 が 0 だからである。よってこの導出節を新たに追加し、これが 0 になる前の状態まで戻ればよさそうである。

バックジャンプ

ではどこまで戻ればいいのだろうか？上での議論から既にc \diamond c_0 には少なくとも一つ現在の決定レベルのリテラル a_1 が含まれていることが分かっているが、もしこれが一つだけならこの導出節は一つ前の決定レベルにおいて単位伝搬に使えたはずである。
上での仮定「決定を行う前に全ての実行可能な単位伝搬を行っている」を維持することを考えると、もしこの導出節を追加する場合、これが単位伝搬に使う事が可能だったところまで戻らないといけない。つまり a_2, \ldots, a_k, b_1, \ldots, b_l のうち決定レベルが最大のものが d^\prime だとすると、Trailのこの決定レベルの最後に戻って（以降のTrailを削除し）、c \diamond c_0 を追加し、これによって単位伝搬により a_1 をTrailに追加してアルゴリズムを再開する。この操作をバックジャンプと呼ぶ。

c \diamond c_0 が現在の決定レベルに属する二つ以上のリテラルを含む場合は、次のプロセスによって一つだけ含むようになるまで変形する。
a_1 の他にも現在の決定レベルに属するリテラルが存在するケースを考える。この時上の議論と同じように少なくとも一方のリテラルは決定ではないので理由となる節 c_1 が存在し、(c \diamond c_0) \diamond c_1 を考えることでそのリテラルを取り除くことができる。
現在の決定レベルには有限個しかリテラルが無いので、このプロセスは有限回で終了し、現在の決定レベルにおけるリテラルを一つだけ含む導出節 c^\prime を得る。この c^\prime を使って上のバックジャンプを実行する。