2019-01-07

充足可能性問題(SAT)

このページでは、充足可能性問題(SAT)というNP完全な問題をイジングモデルによって表現する方法について述べます。

問題の定式化

$N$個の論理変数$x_1, x_2, \ldots, x_N$を取ります。 各$x_i$は0か1の値を取る変数です。 論理変数またはその否定$x_1, x_2, \ldots, x_N, \bar{x}_1, \bar{x}_2, \ldots, \bar{x}_N$のことを”リテラル(literal)”と呼ぶことにします。 また、いくつかのリテラル$y_{i_1}, \ldots, y_{i_k}$の論理和からなる論理式$y_{i_1}\lor \ldots \lor y_{i_k}$のことを”節(clause)”と言います。 さらに、幾つかの節の論理積からなる論理式$C_1 \land \ldots C_m$のことを”連言標準形(CNF、Conjugate Normal Form)”といいます。

ここでは、特にCNFに対する充足可能性問題CNF-SATを考えます。 CNFに対する充足可能性問題とは、与えられたCNFに対して、そのCNFを1にするような各論理変数$x_i$への0か1の割り当てが存在するかどうか判定する問題を言います。

特に、CNFを構成する各節が、ちょうど3つのリテラルから成り立っているときCNFを3-CNFと言います。 理論計算機科学における重要な事実として、任意のCNFは多項式時間で3-CNFに変換できます。 したがってCNF-SATの代わりに3-CNFを入力とする充足可能性問題3-SATを考えて構いません。 そこで、ここでは3-SATについて考えることにします。

イジングモデルへの変形

3-SATは多項式時間でMIS(最大独立集合問題)に帰着されます。 3-SATを解くときはMISに帰着してから、MISを代わりに解いてあげれば良いでしょう。 その帰着は以下のようになります。

与えられた3-CNFを$\Psi = C_1 \land \ldots \land C_m$とします。 各節は以下のような3つのリテラルからなる節です。 $$ C_i = y_{i1} \lor y_{i2} \lor y_{i3} $$ $\Psi$をもとに、MISの入力となる無向グラフを以下のようにして構成します。

各節$C_i$に対して3つの頂点$i1, i2, i3$を作ります。 そして、それら3つを互いに辺で繋ぎます。 こうして全部で$3m$個の頂点からなる$m$個の三角形ができました。 次に、これらの三角形を繋いでいきます。 異なる二つの3角形$(i1. i2. i3)$$(j1, j2, j3)$に対して、それらの中にある頂点$i1$$j1$が繋がれるとは、対応するリテラルが以下の関係式を満たすときです。 $$ y_{i1} = \bar{y_{j1}} $$ こうして三角形を作り、それらを繋いで得られるグラフを$G$としましょう。 この$G = (V, E)$を入力としてMISを解き、MISの解で得た頂点集合の要素数と元の3-SATの節の数が一致した場合、元の3-SATは充足可能であることが分かり、MISの解を元の3-SATの解に変換することができます。

以下の図に3-SAT:$(a|b|c)\&(\overline{a}|\overline{b}|c)$を解く手順を示します。 まず、$C_1=(a|b|c)$から頂点$a,b,c$を作り、互いに辺でつなぎます。 次に、$C_2=(\overline{a}|\overline{b}|c)$から頂点$\overline{a},\overline{b},c$をつくり、互いに辺でつなぎます。 このとき、$a$$\bar{a}$は同時にTrueになることはないので辺をつなげます。$b$$\bar{b}$も同様です。 このようにして得たグラフに対してMISを解くと図の右側のようなMISの解を得ます。 図のMISの解では頂点$a$と頂点$\bar{b}$が選択されています。 これは元の3-SATで$a=True,b=False$を選んだことを表し、このとき実際に元の3-SATがTrueであることが確認できます。 ちなみに、MISの問題を解くエネルギー関数は以下のようにして構築されます。 $$ H = H_A + H_B = A \sum_{uv \in E} x_u x_v - B \sum_{v \in V} x_v $$

エネルギー関数の最小化により充足可能性問題が解けるのは何故か

エネルギー関数の最小化によりMISが解けることは既知とします。

MISを解くことで3-SATが解けることは以下のようにして示すことができます。 MISを解くことで得られた独立集合を考えましょう。 MISの入力である無向グラフは、もとの3-CNFの$m$個の節に対応する$m$個の三角形が繋がれたグラフです。 そして、各三角形の頂点のうち少なくとも1つは独立集合の元として選ばれています。 したがって、肯定に対応するリテラルが選ばれているなら対応する論理変数の値を1にして、否定に対応するリテラルが選ばれているなら0にするという割り当てを行えば、3-SATの解となる割り当てを構成することができます。 したがって、3-SATが解けたことになります。

参考文献

A. Lucas, “Ising formulations of many NP problems”(open access).