ひとり勉強会 RSSフィード

2009-02-09

充足と恒偽のあいだ

|  充足と恒偽のあいだを含むブックマーク

あるいは、ランダムなSAT問題の答えを分ける不思議な数字、4.27。

調べたり実験したりしてたら面白くなってきたので、まとめておきます。

3-SAT?

3-SAT は、「「「変数か、変数を NOT した式」を3個 OR で繋げた式」を何個か AND で繋げた式」が与えられたときに、「式全体の値が true になるように変数の値を決めることができるか?」を判定する問題です。NP完全問題の代表例として有名です。たとえば

(x1 || x2 || x3) && (!x1 || !x2 || !x3) && (x1 || !x3 || !x4)

この論理式は、x1=true、x2=false、x3とx4は適当に決めれば全体は true になるので、答えは "SATISFIABLE (充足可能)" です。

一方で、ちょっと人工的ですが、

(x1 || x1 || x1) && (!x1 || !x1 || !x1)

これは、x1 を true にしても false にしても全体は false なので、"UNSATISFIABLE (充足不可能)" が答えになります。

ランダム生成

3-SAT問題の論理式をランダム生成した場合、答えが "SATISFIABLE" になる確率と、"UNSATISFIABLE" になる確率、どちらが高いでしょうか?

ちょっと考えると感覚的にはなんとなくわかると思うのですが、3-SAT の論理式の場合、条件を && で繋いでいくので、長い論理式であればあるほど制約がきつくなって "UNSATISFIABLE" になりやすくなります。

  • 式が短いほうが SATISFIABLE になりやすい
  • 式が長いほうが UNSATISFIABLE になりやすい

逆に、式が長くても、たとえば10000項の論理式であっても、その中に変数が20000種類含まれていたら、変数の値を調整できる部分が大きいので、巧いことやって式をtrueにする抜け道が見つけやすくなります。

  • 変数の数が少ない方が UNSATISFIABLE になりやすい
  • 変数の数が多い方が SATISFIABLE になりやすい

…と、傾向としては、こうなりそうです。

Phase Transition!

面白いのは、この傾向は、どうも「なりやすい」というレベルではなく、ある点を境にかなり急激に変化するらしい。この手の問題の "Phase Transition" と呼ばれているそうです。

  • (式の長さ / 変数の数) ≦ 4.0 だとほぼ確実に SATISFIABLE
  • (式の長さ / 変数の数) = 4.27 付近で半々
  • 4.5 ≦ (式の長さ / 変数の数) だとほぼ確実に UNSATISFIABLE

(※ここでは、"式の長さ" は && で繋ぐ単位である (? || ? || ?) の個数を指しています。)

実験してみました。変数の数20で式の長さ3.0〜6.0倍まで色々変えてみたもの(赤)と、変数の数50で式の長さを3.0〜6.0倍まで色々変えてみたもの(青)。解くのは PicoSAT に頑張ってもらいました。それぞれの点で100回ランダム生成した問題を解いてSATISFIABLEだった率を集計してます。

f:id:hzkr:20090209120004p:image

まだ問題サイズが小さすぎるのか、3.5〜5.0の辺りまであいまいな部分が広がっていますが、かなり傾向は見て取れます。"Experimental results on the crossover point in random 3-SAT" という論文に200変数の場合の実験結果が載っていて、かなり綺麗なグラフになっています。以下に引用します。

f:id:hzkr:20090209122446p:image

逆に言うと、4.27付近は「SATISFIABLEかUNSATISFIABLEか全く予想がつかない」ので、SATを解くアルゴリズムにとってとても難しいゾーンということになります。上に引用したグラフにありますが、ヒューリスティックを駆使して効率的にSATを解くアルゴリズムは、式長/変数数比がこのゾーンの外ならとても効率的にSATを解けるらしいです。この4.27ゾーンだけが鬼門

実験だけではなく、"A new upper bound for 3-SAT" によると、問題サイズを大きくしていくと、理論的に3.52以下はほぼ確実にSATISFIABLE、4.4898以上はほぼ確実にUNSATISFIABLEとなることが証明されていて、この理論値の幅はじわじわと狭められていっているそうな。

CC0
To the extent possible under law, the person who associated CC0 with this work has waived all copyright and related or neighboring rights to this work.

Connection: close