「充足可能性問題(3-SAT)を解く乱択アルゴリズム」 by Julia ref: http://qiita.com/antimon2/items/96e3bd6e452e03cf98db

Rw3sat.jl

# Rw3sat.jl

sample(a::Array) = a[rand(1:end)]

immutable Literal
    index::Int
    not::Bool
end
literal(index, not) = Literal(index, not)

# issatisfied(l::Literal, x::BitArray{1}) = l.not ? !x[l.index] : x[l.index]
issatisfied(l::Literal, x::BitArray{1}) = l.not $ x[l.index]

immutable Clause
    literals::Array{Literal, 1}
end
clause(ls::Literal...) = Clause([ls...])

issatisfied(c::Clause, x::BitArray{1}) = any(l -> issatisfied(l, x), c.literals)

immutable CNF
    clauses::Array{Clause, 1}
end
cnf(cs::Clause...) = CNF([cs...])

issatisfied(f::CNF, x::BitArray{1}) = all(c -> issatisfied(c, x), f.clauses)

function rw3sat(f::CNF, n::Int, rr::Int)
    for r = 1:rr
        x = randbool(n) # W4
        for k = 1:3n
            if issatisfied(f, x)    # W7
                return "充足可能である"
            end
            c = sample(filter(c -> !issatisfied(c, x), f.clauses))  # W10
            idx = sample(c.literals).index  # W11
            x[idx] = !x[idx]    # W12
        end
    end
    return "おそらく充足不可能である"
end

p1 = clause(literal(1, false), literal(2, false), literal(3, false))
p2 = clause(literal(4, false), literal(2, false), literal(3, true ))
p3 = clause(literal(1, true ), literal(4, false), literal(3, false))
p4 = clause(literal(1, true ), literal(4, true ), literal(2, false))
p5 = clause(literal(4, true ), literal(2, true ), literal(3, false))
p6 = clause(literal(1, true ), literal(2, true ), literal(3, true ))
p7 = clause(literal(1, false), literal(4, true ), literal(3, true ))
p8 = clause(literal(1, false), literal(4, false), literal(2, true ))

f = cnf(p1, p2, p3, p4, p5, p6, p7, p8)
# f = cnf(p1, p2, p3, p4, p5, p6, p8)

println(rw3sat(f, 4, 3))