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

Rw3sat.jl

# Rw3sat.jl
using Random  # ←ココ！(1)

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

# ↓ココ！(2)
struct Literal
    index::Int
    not::Bool
end
# literal(index, not) = Literal(index, not)
# ↑ココ！(3)

# issatisfied(l::Literal, x::AbstractArray{Bool, 1}) = l.not ? !x[l.index] : x[l.index]
issatisfied(l::Literal, x::AbstractArray{Bool, 1}) = l.not ⊻ x[l.index]
                                                         # ↑ココ！(4)

# ↓ココ！(2)
struct Clause
    literals::Array{Literal, 1}
end
Clause(ls::Literal...) = Clause([ls...])
# ↑ココ！(3)

issatisfied(c::Clause, x::AbstractArray{Bool, 1}) = any(issatisfied(l, x) for l=c.literals)
                                                        # ↑ココ！（オマケ）
# ↓ココ！(2)
struct CNF
    clauses::Array{Clause, 1}
end
CNF(cs::Clause...) = CNF([cs...])
# ↑ココ！(3)

issatisfied(f::CNF, x::AbstractArray{Bool, 1}) = all(issatisfied(c, x) for c=f.clauses)
                                                     # ↑ココ！（オマケ）
function rw3sat(f::CNF, n::Int, rr::Int)
    for r = 1:rr
        x = bitrand(n) # W4
        #   ↑ココ！(5)
        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

# ↓ココカラ！(3)
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)
# ↑ココマデ！(3)

println(rw3sat(f, 4, 3))

Rw3sat.v03.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))