ノンモノトーンで計算が減る場合 その2

おはようございます。今回からは少しまじめにお話しします。自分の考えをお話しするので緊張するのです。

【追記（2026年2月23日）】

本記事中で、(a∨b)∧(¬b∨c)=a∨c のように「=（同値）」として書いている箇所がありますが、正確にはこれは同値変形ではなく、解消規則（resolution）によって (a∨c) が導出される（含意される）という意味です。すなわち

(a∨b)∧(¬b∨c) ⊨ (a∨c)

が正しい関係です。したがって、元の2節を (a∨c) で“置き換えて節を消す”という操作は一般には正しくありません。以下の本文は「導出される節を冗長節として追加する」あるいは「DP/VE（変数消去）の手続きの一部として用いる」という文脈で読み替えてください。

今回ここで発表することは、すでに、「http://etsurohonda-blog.blogspot.jp/2011/11/pnp.html」や http://etsurohonda-blog.blogspot.jp/2011/11/pnp.html」などで発表しているのですが、改めてきちんと考察をしてまとめておこうということもありまして、身の程知らずにもここに書かせて頂きます。

基本的なアイディアをまず述べます。

(a∨b)∧(￢b∨c)

の括弧を外すことを考えると普通ならば

(a∨b)∧(￢b∨c)=a∧￢b∨a∧c∨b∧￢b∨b∧c

となり、計算量は増大するように思われますが、一般に（解消／導出の意味で）考えると

(a∨b) と (￢b∨c) から (a∨c) を導出できます（解消：resolution）。すなわち

(a∨b)∧(￢b∨c) ⊨ (a∨c)　（１’）

となり、（導出される節が短いので）計算の見通しとしては小さくできる可能性があります。

※ただし（追記にも書いた通り）一般には同値ではないため、(a∨b) と (￢b∨c) を (a∨c) に“置き換える”ことはできません。

さらに

(a∨b∨c)∧(￢b∨￢c∨d)

のような論理式は（１’）の考え方（解消）を応用すると、例えば b に関して解消して

(b∨(a∨c)) と (￢b∨(￢c∨d)) から

(a∨c)∨(￢c∨d) を導出でき、これを整理すると

(a∨c)∨(￢c∨d)

= a∨c∨￢c∨d

= a∨T∨d

= T

となります。

※ここで T になるのは「元の2つの節全体が恒真になる」という意味ではなく、「b で解消して得られる解消節（導出される節）がトートロジーになり、追加しても意味がない（捨てられる）」という意味です。

これをSATの節に応用して考察していきます。そのとき、以下の二つの考え方を用います

一つ目は、SAT表現における節において、各変数はブール変数であるため取りうる値は二値ですが、実際には項があるかないか、あれば真か偽かという事で、場合としては三通りの場合分けで考察します

二つ目は、たくさんの節集合がある場合に、適当な二つの節を持ってきる場合を考えます。はじめに論理式で説明したように、その節に同じ項があり、逆の値を持つときには（解消により）短い節を導出できたり、あるいは解消節がトートロジーになって捨てられる場合があります。例えば{{a,b},{not(b),c}}という節からは, {a,c} を導出できます（解消：resolution）。

※ただし、一般には {{a,b},{not(b),c}} と {{a,c}} が同値という意味ではありません（元の2節を {a,c} に置き換えるのは不可）。DP/VE（変数消去）の文脈では、必要な解消節を生成した上で当該変数を含む節を削除する、という形で使います。

そのため（入力の構造によっては）節が実質的に縮んだり、あるいはあとで説明しますが、解消節がトートロジーになって追加が不要になる場合もあり、計算量が減る可能性がある、という考え方です。以下はもう少し詳しく場合分けして考察していきます。

※以下はSAT表現で、節集合Ｃの元の数はr、節の各リテラルは元々はm個のブール変数であるとして以下考えていきます

（a）適当に取った二つの節に同じ項があり逆の値を持つ場合

上でも説明していますが、部分的に{{a,b},{not(b),c}} から {a,c} を導出できる場合のことです。この場合、ある節にbが含まれ別の節にnot(b)が含まれる確率を考えます。そうすると、確率は1/9となる事が分かります。また、その逆もあり得ますので、確率は二倍となり、その場合に（導出される節が短くなることによって）見かけ上減る計算量は、上の式の左辺の計算量は単純に3、これが {a,c} のような短い節の扱いでは1、という見積りになります。

（注：以前のブログでは逆もありうるということを考慮に入れていませんでしたので修正しています）

ここからが以前と違う結論になるのですが、探すコストが9/2であるのに対し減らせるコストが2、前後に他の項があれば4の場合もあります。すなわち減らせる計算量は最大でも4。場合減らすコストより一致する項を探すコストの方が大きくなるため、この場合はやるだけ無駄ということになります。

（※追記：ここで言っている「減る」は、あくまで“導出される節が短い／扱いやすい”という直感的なコスト見積りの意味です。一般に元の節を置き換えて消す、という意味ではありません。）

（a’）適当に取った二つの節に二つ同じ項があり一つは同じ値、もう一つは逆の値を持つ場合

この場合の例としては{{a,b},{a,not(b)}}から {a} を導出でき、かなり小さくなっていますが、変数が増えると{a}にあたる部分が複数の変数からなりすべて一致するとのは比較的まれな場合と考えられます。また、見かけ上は小さくなっていますが、{a}に相当する部分が複数の変数よりなる場合の計算のコストは(a)の場合とほぼ同様と考えられますので考察から除外しても問題ないと考えます。

（b）適当に取った二つの節に同じ項二つありそれぞれがあり逆の値を持つ場合

部分的に{{a,b,c},{notb,notc,d}}のような節がある場合です。この場合、探すためのコストは81/4の定数倍となりますが、この場合 b に関して解消すると、導出される解消節がトートロジーになり得ます（上で述べた現象です）。その結果、DP/VE（変数消去）として見たときに「追加すべき解消節が増えない」形になり、変数消去が非常に得になる可能性があります。

例）{{{a,b,c},{not b,not c,d},{e}}

（b を消去する局面を考えると、解消節は {a,c,not c,d}={{T}} となり追加不要、残りは {{e}} だけになります。）

そのため、この場合、節二つ分を計算する必要が無くなり、減らす事のできるコストは論理和と論理積の個数即ち、（(節Aの長さ-1)+（節Bの長さ-1)+1）となります。従って、節の長さ（節の中の変数の個数）が11に等数発生などのコストを上乗せし、上回る場合はこの手法は有効となります。

今回は以上ですが、次回、この方法であるならば、乱数を発生させて適当な節と変数に注目すれば確率4/81ではありますが、大きく計算量を減らすことができる、と言う点に着目してもう少し考察を深めてみたいと思います。