rw3sat.js

rw3sat.js

function random_walk_3_sat(f, n, rr) {        // W1
    var ff = f.split(/\s*and\s*/).map(function (c) {
        return {
            toString: function () { return c; },
            eval: Function("x", "return " + c.replace(/\bor\b/g, "||") + ";")
        };
    });
    for (var r = 0; r < rr; r++) {
        var x = random_walk_3_sat_w4(n);    // W4
        for (var k = 0; k < 3 * n; k++) {
            if (ff.every(function (c) {return c.eval(x);})) {    // W7
                return "充足可能である";
            }
            var c = random_walk_3_sat_w10(ff, x);    // W10
            var idx = parseInt(c.toString().match(/\d+/g).sample());    // W11
            x[idx] = !x[idx];    // W12
        }
    }
    return "おそらく充足不可能である";
}
function random_walk_3_sat_w4(n) {
    var result = [];
    for (var i = 0; i < n; i++) {
        result.push(Math.random() < 0.5 ? false : true);
    }
    return result;
}
function random_walk_3_sat_w10(a, x) {
    return a.filter(function (c) { return !c.eval(x); }).sample();
}
Array.prototype.sample = function () {
    return this[Math.floor(Math.random() * this.length)];
}

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 ');

//console.log(random_walk_3_sat(f, 4, 3));
//alert(random_walk_3_sat(f, 4, 3));
print(random_walk_3_sat(f, 4, 3));