Rw3sat.hx

Rw3sat.hx

package ;

using Lambda;

@:final
class ArraySampling {
    public static function sample<T>(a : Array<T>) : T {
        return a[Std.random(a.length)];
    }
}
using Rw3sat.ArraySampling;

typedef Clause = {
    literal_indexes : Array<Int>,
    eval : Array<Bool> -> Bool
}

@:final
class Rw3sat {

    static function random_walk_3_sat(f : String, n : Int, rr : Int) : String { // W1
        var ff = ~/\s*and\s*/g.split(f).map(parseClause);
        for (r in 0...rr) {
            var x = random_walk_3_sat_w4(n);    // W4
            for (k in 0...(3*n)) {
                if (ff.foreach(function (c){ return c.eval(x); })) {    // W7
                    return "充足可能である";
                }
                var c = random_walk_3_sat_w10(ff, x);   // W10
                var idx = c.literal_indexes.sample();   // W11
                x[idx] = !x[idx];                       // W12
            }
        }
        return "おそらく充足不可能である";
    }

    static function parseClause(c : String) : Clause {
        var idxs = [];
        var hash = new IntHash();
        // 本来の使い方じゃないけど、正規表現の全てのマッチに渡って処理する関数が他にないので。
        ~/(!)?x\[(\d+)]/g.customReplace(c, function (m) {
            var idx = Std.parseInt(m.matched(2));
            idxs.push(idx);
            hash.set(idx, m.matched(1)!='!');
            return m.matched(0);
        });
        return {
            literal_indexes: idxs,
            eval: function (x : Array<Bool>) : Bool {
                var result = false;
                for (key in 0...x.length) {
                    if (hash.exists(key)) {
                        result = result || (hash.get(key) == x[key]);
                        if (result == true) break;
                    }
                }
                return result;
            }
        };
    }

    static function random_walk_3_sat_w4(n : Int) : Array<Bool> {
        var result = [];
        for (i in 0...n) result.push([false, true].sample());
        return result;
    }

    static function random_walk_3_sat_w10(a : List<Clause>, x : Array<Bool>) : Clause {
        return a.filter(function (c) { return !c.eval(x); }).array().sample();
    }

    static function main() : Void {
        var p1 = "( x[0] or  x[1] or  x[2])";
        var p2 = "( x[3] or  x[1] or !x[2])";
        var p3 = "(!x[0] or  x[3] or  x[2])";
        var p4 = "(!x[0] or !x[3] or  x[1])";
        var p5 = "(!x[3] or !x[1] or  x[2])";
        var p6 = "(!x[0] or !x[1] or !x[2])";
        var p7 = "( x[0] or !x[3] or !x[2])";
        var p8 = "( x[0] or  x[3] or !x[1])";
        var f = [p1, p2, p3, p4, p5, p6, p7, p8].join(' and ');

        trace(random_walk_3_sat(f, 4, 3));
    }

}