充足と恒偽のあいだ
あるいは、ランダムな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だった率を集計してます。
まだ問題サイズが小さすぎるのか、3.5〜5.0の辺りまであいまいな部分が広がっていますが、かなり傾向は見て取れます。"Experimental results on the crossover point in random 3-SAT" という論文に200変数の場合の実験結果が載っていて、かなり綺麗なグラフになっています。以下に引用します。
逆に言うと、4.27付近は「SATISFIABLEかUNSATISFIABLEか全く予想がつかない」ので、SATを解くアルゴリズムにとってとても難しいゾーンということになります。上に引用したグラフにありますが、ヒューリスティックを駆使して効率的にSATを解くアルゴリズムは、式長/変数数比がこのゾーンの外ならとても効率的にSATを解けるらしいです。この4.27ゾーンだけが鬼門。
実験だけではなく、"A new upper bound for 3-SAT" によると、問題サイズを大きくしていくと、理論的に3.52以下はほぼ確実にSATISFIABLE、4.4898以上はほぼ確実にUNSATISFIABLEとなることが証明されていて、この理論値の幅はじわじわと狭められていっているそうな。
