乱択アルゴリズムに挑む(その 4)

一通り道具は揃ったはずなので、とりあえずプログラムっぽく整えてみる。

import java.util.*;

class ThreeSatisfiabilityProblem {
    public static void main(String[] args) {
        boolean [] x = new boolean[4];
        boolean [] p = new boolean[8];
        boolean sat;

        // 各 clause に使用されている変数の index
        int [][] index = {
            {0, 1, 2},
            {1, 2, 3},
            {0, 2, 3},
            {0, 1, 3},
            {1, 2, 3},
            {0, 1, 2},
            {0, 2, 3},
            {0, 1, 3}
        };

        for(int r = 0; r < 10; i++) {
            // ラウンドの初めにランダムで真偽値を決める
            for(int i = 0; i < x.length; i++) {
                x[i] = randomBool();
            }

            // 3 * (変数の数) 回のランダムウォーク
            for(int i = 0; i < 3 * x.length; i++) {
                // 個々の命題の真偽値を求める
                p[0] = x[0] || x[1] || x[2];
                p[1] = x[3] || x[1] || !x[2];
                p[2] = !x[0] || x[3] || x[2];
                p[3] = !x[0] || !x[3] || x[1];
                p[4] = !x[3] || !x[1] || x[2];
                p[5] = !x[0] || !x[1] || !x[2];
                p[6] = x[0] || !x[3] || !x[2];
                p[7] = x[0] || x[3] || !x[1];

                // 充足可能性を調べる
                sat = p[0];
                for(int j = 1; j < p.length; j++) {
                    sat = sat && p[j];
                }

                // 充足可能であればランダムウォークループを抜け、
                // そうでなければ充足されていない clause 中の
                // ランダムに選んだ一つの変数の真偽値を反転する
                if(sat) {
                    break;
                } else {
                    // 充足されていない clause の index を List に格納
                    List<Integer> list = new ArrayList<Integer>();
                    for(int j = 0; j < p.length; j++) {
                        if(!p[j]) {
                            list.add(j);
                        }
                    }

                    // List から一つランダムに index を取り出す
                    int m = list.get((int)(list.size() * Math.random()));

                    // p[m] に使われている変数からランダムに
                    // 一つ取り出し真偽値を反転する
                    int n = index[m][(int)(index[m].length * Math.random())];
                    x[n] = !x[n];
                }
            }

            // 充足可能であればそのラウンドで終了
            if(sat) {
                break;
            }
        }

        // 結果表示
        if(sat) {
            System.out.println("充足可能です。");
            // 充足可能な割り当ての表示
            for(int i = 0; i < x.length; i++) {
                System.out.print(" x[" + i + "] = " + x[i]);
            }
        } else {
            System.out.println("おそらく充足不可能です。");
        }
    }

    static boolean randomBool() {
        boolean b;
        int i = (int)(2 * Math.random());

        if(i == 0) {
            b = false;
        } else {
            b = true;
        }

        return b;
    }
}

ここで「おそらく充足不可能です。」の出力がポイント。各ラウンドごとに 個の真偽値の組み合わせの集合の上を 回ランダムウォークするが、全ての真偽値の組み合わせを試せるわけではないので、充足可能な組み合わせを見逃している恐れがある。なので「おそらく」が付くわけだ。見逃し確率を十分低く押さえる(この例では 5% 以下)ために、ラウンド数は 10 回と設定した。3-SAT の乱択アルゴリズムを用いた解法は概ねこんな感じになる。今回は 3-SAT に絞って乱択アルゴリズムを取り上げたが、乱択アルゴリズムは他にも同書に載っている例としてクイックソートのピボットをランダムに選ぶアルゴリズムなどがあり、さまざまな場面で使われる。実に興味深い。

追記 : アルゴリズムを微妙に間違えていたので修正。

最後にお約束の参考書籍紹介。

数学ガール/乱択アルゴリズム (数学ガールシリーズ 4)