A. Lucas, Front. Phys. (2014) 掲載例題の実装と解説 ー 充足可能性問題 (SAT)¶
本サンプルコードでは、論文 A. Lucas, "Ising formulations of many NP problems", Front. Phys. (2014) で紹介されている『充足可能性問題 (SAT)』に Fixstars Amplify を用いて取り組みます。同論文に紹介されている他の NP 完全・NP 困難な問題も以下で解説しています（カッコ内は論文内で問題に対応する節番号）。
- グラフの分割問題（2.2節）
- 最大クリーク問題（2.3節）
- 厳密被覆問題（4.1節）
- 集合パッキング問題（4.2節）
- 最小頂点被覆問題（4.3節）
- 充足可能性問題（SAT）（4.4節）
- 最小極大マッチング問題（4.5節）
- グラフ彩色問題（6.1節）
- クリーク被覆問題（6.2節）
- 整数長ジョブスケジューリング問題（6.3節）
- ハミルトン閉路問題（7.1節）
- 有向帰還頂点集合問題（8.3節）
- 最小帰還辺集合問題（8.5節）
- グラフ同型性判定問題（9節）
3-SAT 問題¶
$N$ 個の論理変数 $x_1, x_2, \ldots, x_N$ に対して、これらとその否定 $\bar{x_1}, \bar{x_2}, \ldots, \bar{x_N}$ のうちいくつかの論理和 (or) をとったものを 節 といいます。例えば、以下は節のひとつです。
$$ x_1 \lor \bar{x_2} \lor x_3 $$
3-SAT 問題とは、3 つのリテラル（$x_i$ または $\bar{x_i}$ のことです）からなる節がいくつかあるとき、$x_1, x_2, \ldots, x_N$ のそれぞれに $0$ または $1$ を代入することで、すべての節の値が $1$ となるようにできるかどうかを判定する問題です。
例えば、
$$ (x_1 \lor \bar{x_2} \lor x_3) \land (x_2 \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \bar{x_4}) \land (x_2 \lor x_3 \lor x_4) $$
は 3-SAT 問題であり、$x_1 = 1$, $x_2 = 1$, $x_3 = 1$, $x_4 = 0$ とすると 4 つの節がすべて $1$ となります。
ここでは、Fixstars Amplify を用いて 3-SAT 問題の解を探索するプログラムを作成します。定式化は A. Lucas, Front. Phys. (2014) の 4.4 節のものに沿って行います。
問題の作成¶
本サンプルプログラムでは、3-SAT 問題の例題として、
$$ (x_1 \lor \bar{x_2} \lor x_3) \land (x_2 \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \bar{x_4}) \land (x_2 \lor x_3 \lor x_4) $$
を扱います。
コード中では、論理変数 $x_1, x_2, \ldots, x_N$ はインデックス $1, 2, \ldots, N$ で、それらの否定 $\bar{x_1}, \bar{x_2}, \ldots, \bar{x_N}$ は負の数 $-1, -2, \ldots, -N$ で表現することにします。節はリテラルのタプルとして表現し、3-SAT 問題は節のリストで表します。
N = 4 # 論理変数の数
problem = [(1, -2, 3), (2, -3, 4), (-1, -2, -4), (2, 3, 4)]
定式化¶
以下、論理変数の数を $N$、節の数を $M$ とします。上で実装した今回の問題設定では、$N=4$, $M=4$ となります。
定式化の方針¶
$3 \times M$ 個のバイナリ変数 $q$ を用意し、それぞれの節に現れる各リテラルと対応させます。つまり、$q_{i, j}$ は、$i$ 番目の節に現れる $j$ 番目のリテラルに対応します。
ここで、リテラルとバイナリ変数の値同士を対応させるのがすぐに思いつく方法ですが、この方法で定式化すると最終的に不等式制約の導入により、補助変数が必要になります。補助変数の利用は必ずしも悪いことではありませんが、使わないに越したことはないため、今回は別の方法での定式化を考えます。
以下の問題を考えます：
(問題☆) ： 3-SAT 問題のそれぞれの節について、その節に現れるリテラルのうち 1 つだけに印をつけます（↓参照）。印をつけた $M$ 個のリテラルの中に、ある論理変数 $x_i$ とその否定 $\bar{x_i}$ が両方現れることがないようにできるでしょうか?
$$ \text{印をつけた例：}\:\:(\boxed{x_1} \lor \bar{x_2} \lor x_3) \land (\boxed{x_2} \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \boxed{\bar{x_4}}) \land (\boxed{x_2} \lor x_3 \lor x_4) $$
実は、もしこの (問題☆) が解けるとすると、3-SAT 問題も解けることになります。というのも、以下のようにすれば、(問題☆) の解から 3-SAT 問題の解を導くことができるためです。
- 3-SAT 問題の解の導出
$i = 1, 2, \ldots, N$ それぞれについて、(問題☆) の解において印がついているリテラルの中から、$x_i$ または $\bar{x_i}$ であるものを探します（そのようなものは複数あるかもしれませんが、(問題☆) の条件より、$x_i$ と $\bar{x_i}$ の両方に印がついていることはありません）。$x_i$ に印がついているときは $x_i = 1$ とし、$\bar{x_i}$ に印がついているときは $x_i = 0$ とします。どの $x_i$ または $\bar{x_i}$ にも印がついていないときは、 $x_i$ は $0$ と $1$ のどちらにしても構いません。
このようにして決めた論理変数 $x$ が 3-SAT 問題の解となっていることは簡単に分かります。 また、3-SAT 問題に解が存在するならば、その解において $1$ と等しくなるリテラルを各節ごとに 1 つ選んで印をつけることで (問題☆) の解を構成できるので、3-SAT 問題に解が存在するにもかかわらず 問題 (☆) には解が存在しない、ということが起こりえないことも分かります。
したがって、3-SAT 問題の代わりに (問題☆) を解けばよいです。
(問題☆) を定式化します。 $3 \times M$ 個のバイナリ変数 $q$ を各リテラルと対応させた上で、バイナリ変数は、対応するリテラルに印がついているかどうかを表すことにします。印がついていれば $1$ 、ついていなければ $0$ です。
たとえば、以下の式で四角で囲ったリテラルに印がついているとき、$q$ は次の表のようになります。
$$ (\boxed{x_1} \lor \bar{x_2} \lor x_3) \land (\boxed{x_2} \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \boxed{\bar{x_4}}) \land (\boxed{x_2} \lor x_3 \lor x_4) $$
| $q$ | 1 番目のリテラル | 2 番目のリテラル | 3 番目のリテラル |
|---|---|---|---|
| 1 番目の節 | 1 | 0 | 0 |
| 2 番目の節 | 1 | 0 | 0 |
| 3 番目の節 | 0 | 0 | 1 |
| 4 番目の節 | 1 | 0 | 0 |
また、この $q$ から 3-SAT 問題の解を復元すると、$x_1 = 1$, $x_2 = 1$, $x_4 = 0$ となります。復元方法は、前述の通り、$x_i$ に印がついているときは $x_i = 1$、$\bar{x_i}$ に印がついているときは $x_i = 0$、$x_i$ または $\bar{x_i}$ にも印がついていないときは、 $x_i$ は $0$ と $1$ のどちらでも良い、です（つまり、$x_3$ は $0$ または $1$ のどちらでも構いません）。
目的関数¶
(問題☆) は、条件をみたす印のつけ方を 1 つ見つける問題なので、目的関数は $0$（無し）です。
制約条件¶
$q$ に対応する印の付け方が (問題☆) の解となるためには、以下がみたされる必要があります。
- 条件 1：各節について、その節に現れる論理変数と対応するバイナリ変数のうち、ちょうど 1 つが $1$ である。
- 条件 2：各 $i$ について、$x_i$ と対応するバイナリ変数と $\bar{x_i}$ と対応するバイナリ変数がともに $1$ となっていることはない。
条件 1 は、$q$ の各行に関する one-hot 制約であり、以下のように表されます。
$$ \sum_{k = 0}^{N-1} q_{i, k} = 1 \quad \text{for} \quad i \in \{0, 1, \ldots, M-1\} $$
また、条件 2 は、以下のように表されます。
$$ q_{i, k} q_{j, l} = 0 $$
ここで、上式において、$(i, j, k, l)$ は、$q_{i, k}$ に対応するリテラルが $q_{j, l}$ に対応するリテラルの否定となるようなインデックスです。
実装¶
上で作成した問題と定式化を使って、実際に問題を解いてみましょう。最初に、Fixstars Amplify SDK の BinarySymbolGenerator を使って
$3\times M$ のバイナリ変数 $q$ を作成します。
from amplify import VariableGenerator
M = len(problem) # number of clauses
gen = VariableGenerator()
q = gen.array("Binary", shape=(M, 3))
次に、条件 1 に対応する制約条件を作成します。前述の通り、条件 1 は、$q$ の各行についての one-hot 制約です。2 次元の多項式配列の各行についての one-hot
制約を一度に生成するには、one_hot 関数の axis パラメータに 1 を与えればよいです。
from amplify import one_hot
constraint1 = one_hot(q, axis=1)
条件 2 に対応する制約条件を作成します。条件 2 は、$x_i$ と対応する $q$ の要素と、$\bar{x_i}$ と対応する $q$ の要素が両方 $1$
であってはならないという条件でした。$q_{i, k}$ に対応するリテラルは problem[i][k]
で取得でき、その絶対値が論理変数のインデックスを表し、その符号が否定であるかどうかを表しています。したがって、ある 2 つのリテラルが互いに否定であるかどうかは、その 2 つの
problem 同士を足して $0$ になるかどうか、と同一です。
from amplify import equal_to, sum as amplify_sum
constraint2 = amplify_sum(
equal_to(q[i, k] * q[j, l], 0)
for i in range(M)
for k in range(3)
for j in range(M)
for l in range(3)
if problem[i][k] + problem[j][l] == 0
)
作成した制約条件をまとめて組合せ最適化モデルを構築します。
from amplify import Model
model = Model(constraint1 + constraint2)
クライアントを設定して、Fixstars Amplify Annealing Engine (AE) で実行します。
from amplify import FixstarsClient, solve
from datetime import timedelta
client = FixstarsClient()
# client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx" # ローカル環境等で使用する場合は、Fixstars Amplify AE のアクセストークンを入力してください。
client.parameters.timeout = timedelta(milliseconds=1000) # タイムアウトは 1000 ms
# 求解を実行
result = solve(model, client)
解が見つかったかどうかを確認します。Amplify SDK は制約条件をみたす解を自動でフィルターするので、result
が空でなければ、制約条件をみたす解が見つかったと分かります。
if len(result) == 0:
print("解が見つかりませんでした。")
else:
print("解が見つかりました。")
最後に、マシンが出力した (問題☆) の解を 3-SAT 問題の解に変換します。
import numpy as np
x = np.zeros(
N + 1
) # 3-SAT 問題の解のデフォルト値。x が 1-origin なので余分に1個作っておく
values = q.evaluate(
result.best.values
) # decode メソッドにより、決定変数と同じ形に解を整形
ones = np.argwhere(values == 1) # 1 となっている q の要素を検索
for i, k in ones:
if problem[i][k] > 0:
x[problem[i][k]] = 1
print(x[1:])
