はじめに
SATはNP完全な問題として非常に有名な問題です。ブール変数${x_1, x_2, ..., x_n}$が与えられた際に、これらからなる命題論理式を真にする組合せがあるかどうかを判断するものです。
SATの中でも有名なものとして、CNF-SATと呼ばれるものがあります。これは、複数の節(Clause)の論理積を取った形のもので、節の中は論理和のみで構成されているものを指します。この形状に限定してもNP完全であることが知られています。例としては、以下のような式です。
(x_1 \lor x_2 \lor x_3) \land
(\lnot x_1 \lor \lnot x_2 \lor x_3) \land
(\lnot x_1 \lor x_2 \lor \lnot x_3) \land
(x_1 \lor \lnot x_2 \lor \lnot x_3)
例えば、適当に値を当てはめてみると、$x_1 = 1, x_2 = 0, x_3 = 0$のとき、真となります。
解があるかどうかを判定するだけであれば、一つ見つかったので、これで十分なのですが、場合によっては解が何個あるのかを調べたいことがあります。例えば、数独などのペンシルパズルを作成する場合、解が唯一に定まっているかどうかが気になります。
このような、SATの問題に対して、解が何個あるのかを求める問題を#SATと呼びます。この問題は#Pというクラスに属しており、他の多くのNP完全な問題に対する解の数え上げがこのクラスに属します。
今回の記事では、このCNF-SATに対する#SATをテンソルネットワークを用いて解く手法について、文献[1, 2]を参考に、実装してみます。
手法の概要
テンソルネットワークの要素として、変数を表すCOPY-tensorと、節を表すClause-tensorの二つを用意します。
各変数と対応する節をつなげたような形のネットワークを作ります。イメージ図は以下の通りです。
（文献[2] Figure 1より引用）
丸が変数、三角が節を表すテンソルです。このテンソルネットワークの縮約をとることで、#SATの解が得られます。
COPY-tensor
変数$x_i$が現れる節の数を$k$とします。変数$x_i$に対応するCOPY-tensorは、ランク$k$のテンソルで、すべての節に対して$x_i=0$もしくは$x_i=1$になるようにするのが役割です。式で表すと以下の形になります。
\lvert 0 \rangle ^ {\otimes k} + \lvert 1 \rangle ^ {\otimes k}
Clause-tensor
節に対応するテンソルで、節中に現れるいずれかのリテラルが1であるときに、1となるようにすることが目的です。$m$を節中に現れる変数の数、節を$ \phi (\mathbf{x})$と表現すると、以下の式で表されます。
\sum_{\mathbf{x} \in \{0, 1\}^{m}} \lvert \mathbf{x} \rangle \langle \phi (\mathbf{x}) \rvert \lvert 1 \rangle = \sum_{\mathbf{x} \in \{0, 1\}^{m}} \phi (\mathbf{x}) \lvert \mathbf{x} \rangle
計算量について
厳密な計算量については、ここでは触れませんが、計算量に影響が大きい要素について考えてみます。
まず、入力として出てくるテンソルのサイズについて考えると、多くの節に登場する変数があると、それだけCOPY-tensorが大きくなります。また、節の中のリテラルの数が多いほどClause-tensorが大きくなります。これらはサイズに応じて指数的に大きくなります。
また、テンソルネットワークの形状について考えると、一般に木に近い形であるほど、理論的に言えば木幅が小さいほど、縮約のコストは小さくなります。
今回のネットワークについて考えると、各変数に対して、出現する節に同時に出てくる変数が偏っているようなケースだと、木に近い形になります。逆に、多くの変数同士が関連していると、木幅が非常に大きくなります。
これは、感覚的にも一般的な手順でSATを解く場合の難易度とも一致しています。
このため、テンソルネットワークを用いた手法が既存手法の苦手ケースに対して、特別強いということはないのですが、#SAT問題をテンソルの積の計算に落とし込むことで、GPUを活用して高速で計算できたりする場合があります。実際、文献[2]では、数値実験によって、特定のクラスの#SATにおいて、既存手法よりも高速に計算ができたと報告されています。
実装
それでは実際に実装してみます。テンソルネットワークの計算には、googleのTensorNetworkライブラリ[3]を利用します。
今回使う環境は以下の通りです。
Python 3.13.7
---
numpy 2.3.2
tensornetwork 0.4.6
SATのインスタンスとして、冒頭にも掲載した以下の式を利用します。
(x_1 \lor x_2 \lor x_3) \land
(\lnot x_1 \lor \lnot x_2 \lor x_3) \land
(\lnot x_1 \lor x_2 \lor \lnot x_3) \land
(x_1 \lor \lnot x_2 \lor \lnot x_3)
テンソルの定義
COPY-tensorとClause-tensorを作るための関数を用意しておきます。
def make_copy_tensor(rank):
T = np.zeros([2]*rank)
T[(0,)*rank] = 1
T[(1,)*rank] = 1
return T
def make_clause_tensor(rank, clause):
# clauseは、notがかかっているところを1、それ以外を0としたtuple
T = np.ones([2]*rank)
T[clause] = 0
return T
引数の設定や、Clause-tensorの作り方はいくつか考えられると思いますが、今回は節の要素数分のtupleを入力として受け取り、notがかかっている部分を1、それ以外を0としたものを考えます。
今回、CNF-SATを考えているため、節全体がFalseになるのは、すべてのリテラルがFalseの時のみです。この時のみ0を返すようなテンソルを簡単に作るため、先述の入力形式を用いることにします。
本記事では密行列で定義していますが、出現回数の多い変数や、変数の多い節を扱う場合はメモリ量が指数的に増えていきます。実用的な計算では、節を分解したり、疎行列として扱ったりする工夫が必要です。
次に、それぞれの変数、節に対応するCOPY-tensorとClause-tensorを作っていきます。
今回は、規模も小さいので、一つずつ書いていますが、より大規模なものを解こうと思ったり、複数の問題で使い回すのであれば、なんらかフォーマットを定義しておいたほうがよいと思います。
copy_tensor = dict()
clause_tensor = dict()
# 変数の定義
# rankは各変数が節に出現する回数なので、今回は全部4
copy_tensor[0] = tn.Node(make_copy_tensor(4))
copy_tensor[1] = tn.Node(make_copy_tensor(4))
copy_tensor[2] = tn.Node(make_copy_tensor(4))
# 節の定義
# 今回は3-SATになっているので、すべてrankは3
# x_0 or x_1 or x_2
clause_tensor[0] = tn.Node(make_clause_tensor(3, (0, 0, 0)))
# not x_0 or not x_1 or x_2
clause_tensor[1] = tn.Node(make_clause_tensor(3, (1, 1, 0)))
# not x_0 or x_1 or not x_2
clause_tensor[2] = tn.Node(make_clause_tensor(3, (1, 0, 1)))
# x_0 or not x_1 or not x_2
clause_tensor[3] = tn.Node(make_clause_tensor(3, (0, 1, 1)))
次に、これらのノードをつなげていきます。
今回はどの節も$x_0, x_1, x_2$が同様に登場するので、同じような記述の繰り返しになりますが、節ごとに変数が違う場合はそれに応じた書き方にしてください。
# エッジ作成
# A or B or C
tn.connect(copy_tensor[0][0], clause_tensor[0][0])
tn.connect(copy_tensor[1][0], clause_tensor[0][1])
tn.connect(copy_tensor[2][0], clause_tensor[0][2])
# not A or not B or C
tn.connect(copy_tensor[0][1], clause_tensor[1][0])
tn.connect(copy_tensor[1][1], clause_tensor[1][1])
tn.connect(copy_tensor[2][1], clause_tensor[1][2])
# not A or B or not C
tn.connect(copy_tensor[0][2], clause_tensor[2][0])
tn.connect(copy_tensor[1][2], clause_tensor[2][1])
tn.connect(copy_tensor[2][2], clause_tensor[2][2])
# A or not B or not C
tn.connect(copy_tensor[0][3], clause_tensor[3][0])
tn.connect(copy_tensor[1][3], clause_tensor[3][1])
tn.connect(copy_tensor[2][3], clause_tensor[3][2])
最後に、これらをまとめて縮約をとります。
nodes = [
copy_tensor[0], copy_tensor[1], copy_tensor[2],
clause_tensor[0], clause_tensor[1], clause_tensor[2], clause_tensor[3],
]
result = tn.contractors.auto(nodes)
# 結果の表示
print(f"解の個数: {result.tensor}") # 4
今回、3変数なので、$2^3=8$通りの変数の割り当てが存在し、各節にすべての変数が1度ずつ出てくるので、各節に対し、Falseになる割り当てが1つずつ存在します。節の被りはないため、$8-4=4$が正解になります。どうやら正しく計算できていそうです。
試しに、Trueとなる割り当てが一つもないケースも試してみます。以下は2変数のSATで、すべての節のパターンを含んでいるため、必ずどこかの節がFalseになります。
(x_1 \lor x_2) \land
(x_1 \lor \lnot x_2) \land
(\lnot x_1 \lor x_2) \land
(\lnot x_1 \lor \lnot x_2)
copy_tensor = dict()
clause_tensor = dict()
# 変数の定義
copy_tensor[0] = tn.Node(make_copy_tensor(4))
copy_tensor[1] = tn.Node(make_copy_tensor(4))
# 節の定義
clause_tensor[0] = tn.Node(make_clause_tensor(2, (0, 0)))
clause_tensor[1] = tn.Node(make_clause_tensor(2, (0, 1)))
clause_tensor[2] = tn.Node(make_clause_tensor(2, (1, 0)))
clause_tensor[3] = tn.Node(make_clause_tensor(2, (1, 1)))
# エッジ作成
tn.connect(copy_tensor[0][0], clause_tensor[0][0])
tn.connect(copy_tensor[1][0], clause_tensor[0][1])
tn.connect(copy_tensor[0][1], clause_tensor[1][0])
tn.connect(copy_tensor[1][1], clause_tensor[1][1])
tn.connect(copy_tensor[0][2], clause_tensor[2][0])
tn.connect(copy_tensor[1][2], clause_tensor[2][1])
tn.connect(copy_tensor[0][3], clause_tensor[3][0])
tn.connect(copy_tensor[1][3], clause_tensor[3][1])
nodes = [
copy_tensor[0], copy_tensor[1],
clause_tensor[0], clause_tensor[1], clause_tensor[2], clause_tensor[3],
]
result = tn.contractors.auto(nodes)
# 結果の表示
print(f"解の個数: {result.tensor}") # 0
こちらも正しく解けていそうです。
まとめ
今回は#SATをテンソルネットワークを用いて解く方法を紹介しました。
テンソルネットワークを用いた計算は、メモリ使用量が大きくなりやすく、計算コストも高いことが多いです。また、SATは制約充足問題の最も基本的な形であり、非常に多くの研究が行われているため、実態として今回のようなアプローチが直接#SAT全体の高速化に寄与する可能性は低いと考えています。
一方で、特定の規模・クラスの問題において、テンソルネットワークベースのアプローチが有効であることなどが見えてくると、テンソルネットワークの縮約順の最適化が、特定のケースにおける#SATの求解の高速化につながってくることになり、面白そうだなと考えています。