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

おはようございます。

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

本記事で「(a∨b∨c）∧(￢b∨￢c∨d)=T」という形で書いている箇所がありますが、正確には「元の2つの節（論理式）の積が恒真になる」という意味ではありません。正しくは、(a∨b∨c) と (¬b∨¬c∨d) を b で解消（resolution）したときに得られる解消節が

(a∨c∨¬c∨d)=T

というトートロジーになり、結果として「解消しても有効な新しい節が増えない（解消節は捨てられる）」場合がある、という現象です。以下の本文はこの意味に読み替えてください。また、ここで述べているのは前処理（DP/VE的な変数消去）が入力分布によって効きやすい可能性であり、最悪ケースのSATが多項式時間で解けるという主張ではありません。

今回は、前回に引き続き、

(a∨b∨c) と (￢b∨￢c∨d) を b で解消するとトートロジー解消節が得られる（捨てられる）

という事を利用して、SAT表現で部分的に{{a,b,c},{notb,notc,d}}のような節がある場合、探すためのコストは81/4の定数倍となりますが、（VE：変数消去の手続きとして見たときに）新たな有効節を増やさずに当該変数を含む節を削除できる場合をもう少し詳しく考察します。

例）

{{{a,b,c},{not b,not c,d},{e}}} について、b を消去（VE）する局面を考えると、

{a,b,c} と {not b,not c,d} から b に関する解消節は {a,c,not c,d} となりますが、これは {T}（トートロジー）なので追加不要です。したがって（b を含む節を削除できる手続きのもとで）残りは {{e}} だけになります。

まず、モノトーンの場合普通のサーキットであれば、前回の節までで考察したように、オーダーは

size(C)=2^(p-1)/m^2≧n^(8・k^(1/2))

より決まります（参照：モノトーンそしてmP≠mNP その11（http://peunp.blogspot.jp/2014/11/blog-post.html））

ところが、乱数を発生させずに、

(b を含む節) と (not b を含む節) の組で、b に関する解消がトートロジーになって捨てられる

となるものを探すということを考えますと、節集合Cの元の数|C|をn、節の中のブール変数の平均の数をmとおいて、総当たりで探すことになりますから、オーダーは単純に考えるとO(m^2*n^2)となり、候補を見つける作業自体は多項式で表わすことができるようになります。発生確率も4/81と比較的高いことから、乱数で元を発生させたようなホワイトノイズがSATの節にある場合は、こうした「解消しても節が増えない（捨てられる）変数消去」が多く見つかり得て、前処理として式を著しく縮められる可能性があります。つまりNTMで適当にデータを作成して処理するというような場合ほとんどの場合ホワイトノイズであると考えられますので、（入力分布によっては）実用上の計算量を大きく下げられるのではないのかと考えます。

※ただしこれは「一般のSATが最悪ケースで多項式時間で解ける」という意味ではなく、あくまで“前処理が効きやすい場合がある”という趣旨です。

さらに、乱数を発生させて探す場合にはオーダーは確率4/81の逆数の84/4に乱数発生のコストを加えたものを定数Aとすると、コストは最悪でもA（m^2）より大きくならず、即ちオーダーは（m^2）まで押さえられると思われます。

プログラムを用いた乱数を場合どれくらいの試行を行えば良いかを確認したのですが、例えば、n=1000,r=100の場合、81×100の試行で約56％、81×500で約98％まで節の数は減少し、81×800で99.7％、81×100で残りの節はほぼ0か1にまで減少しました。

検証用のプログラムはGitHubにアップロードしています。（実際はいくつかのバージョンがあるのですが、今回の検証用のプログラムだけアップロードします）。プログラムの解説は、今回のブログの目的から外れますので行いませんが、よろしければ、どうぞご確認下さい。

アドレスはこちら

https://github.com/Futarisizuka/SAT_term_compress_simulation