LoginSignup
2
1

More than 5 years have passed since last update.

@antimon2(Shunsuke GOTOH)in有限会社来栖川電算

「充足可能性問題(3-SAT)を解く乱択アルゴリズム」 by Julia for v1.0

Last updated at Posted at 2018-08-12

TL;DR

  • 「過去に Qiita で書いた Julia 記事のコードを最新 v1.0 で動くものにリライトしよう」という超個人プロジェクトの第1弾
  • Julia v0.3.5（3年以上前！）→ Julia v1.0.0 へのポーティング例

前置き

元ネタは、結城浩氏著の「数学ガール 乱択アルゴリズム」。
新しい言語を覚えるとき、慣れるために「充足可能性問題（3-SAT）を解く乱択アルゴリズム」（p.353）を実装するという癖をつけています1。

ということで「勉強開始約1ヶ月の Julia ( http://julialang.org/ ) で実装してみました」というのが、元記事。
その時実装したものを、最新の Julia v1.0.0 で動作するように修正してみた、というのがこの記事になります。

開発環境・動作確認環境

  • Mac OSX 10.11.62
  • Julia v0.3.5 → v1.0.0

コード

まずは元記事のコードを再掲：

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

このコードは（ひょっとしたら）Julia v0.3.x でしか動かない（かもしれません（未確認））です。少なくとも V0.6.4/v0.7.0/v1.0.0 では動作しません。

Julia v1.0.0 で動作するよう、リライトしたものが以下になります。
主な変更箇所に「# ←ココ！(N)」みたいなコメント入れておきました。

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

解説

まず初めに。
リライト後のコードは、Julia v0.7/v1.0 でないと動作しません。
上に挙げた「主な変更箇所」ごとに解説します。

(1) using Random

対象：Julia v0.7/v1.0

Julia v0.7 以降は、乱数を扱う各関数は標準添付モジュール Random 内に移動になりました。よって using Random と書かないと random() 関数や bitrand() 関数が使えません3。
なお、v1.0 以降の必須要件は実はココだけで、逆にこの行をコメントアウトすれば、リライト後のコードは v0.6 でも動作します（v0.6.4 で動作確認済）。

(2) struct キーワード

対象：Julia v0.5 以降

Julia v0.4 までは、型宣言は type 〜 end または immutable 〜 end でした。前者が「通常の型（＝変更可能な型）」、後者が「変更不可能（immutable）な型」でした。
Julia v0.5 以降、型宣言は struct 〜 end または mutable struct 〜 end に変更になりました。前者が「構造体（＝immutable な型）」、後者が「変更可能（＝mutable）な構造体」です。
つまり、もし今まで古い Julia で type 〜 end と書いていたら mutable struct 〜 end に、immutable 〜 end と書いていたら struct 〜 end に書き直す必要があります4。

(3) 外部コンストラクタ

対象：???

これは個人的な感想かもしれませんが。
昔は所謂「外部コンストラクタ」（＝型定義外に記述した、その型のインスタンスを生成する関数）を「型名と同じもの」として定義するのが面倒だったり直感的でなかった時代があった気がします。なので「外部コンストラクタは、型名と同じで小文字にした関数名を使用する」のがコーディングスタイルとして良さげかな？ということで、そのようなコードを書いていました5。

それがマイナーバージョンアップを繰り返すうちに、もしくは私が Julia を深く知るうちに、「あれ、ひょっとして、なんか型名と同じ関数を定義するのが直感的でやりやすくなったかも？」「てかむしろ最近の Julia ってそゆのを推奨してるんじゃね？」と思うようになって、今では積極的に外部コンストラクタも型名と全く同じ名前で定義するようにしています。

(4) ⊻

対象：Julia v0.6 以降

⊻は Julia の「排他的論理和」演算子 です。
v0.5 までは $ でした（例によって移行期間中である v0.6 では両方使用可能でした）。
⊻ は、Julia の REPL で \xor（または \veebar）と入力して Tab キーを押すと変換できます。

ちなみに、C言語 や Python などよくある言語で排他的論理和の演算子としてよく使われるのは ^ ですが、Julia ではこれは「冪乗演算子」です（Python の ** にあたるもの）。

(5) bitrand()

対象：Julia v0.4 以降

これはかなり昔に既に移行（関数名変更）していたわけですが。
その昔 randbool(n::Int) という関数がありました。文字通り「Bool型の値を乱択した配列を返す」関数だったわけですが、その戻り値は Array{Bool} ではなく BitArray という特殊な型6でした。これは false/true を 0/1 としてビット表現に置き換えて容量節約をしたものです7。
それで「名が体を表してない」ということで名称変更になった模様です。

（オマケ）Generator 内包表記

対象：Julia v0.5 以降

ここは書き換えずに元のままでも動作します。
ただ今回のような、any() や all() と言った関数に各要素に関数を適用した結果を渡すような場合は、Julia v0.5 以降に導入された「Generator 内包表記」を利用することが推奨されます。理由は以下の2点：

  • 記述が直感的で分かりやすい
  • 内部処理が最適化されやすい

おそらく後の方に出てくる filter(c -> !issatisfied(c, x), f.clauses) も、内包表記を利用して書き換えた方が見た目にもパフォーマンス的にも良くなるかも。そこも余力があってうまく書き換え成功したら、この記事を加筆修正したいと思います。

感想

さすがに3年前のコードはそのままでは動作しませんでしたが、割と機械的な追記・置換で動くものは書けるな、というのが実感。

Julia v1.0 怖くないよー

  1. 同じような記事を書く度に毎回コピペしてましたこの文章。 ↩

  2. まだ El Capitan… 最近 Docker が動かなくなったので落ち着いたら High Sierra に上げる予定。秋には Mojave が来るらしいけれどそれまでは持ちそうにない感じ… ↩

  3. より正確には、v0.7 ではまだ Deprecated Warning が出るだけで using Xxxx を書かなくても使える場合もあります。v1.0 では完全に移行したので using Xxxx を書かないと使えません。 ↩

  4. ちなみに移行期間中（＝v0.5.x の時代）はどちらの書式も許されていて、短い方で「変更可能な型は type 〜 end、変更不可能な型は struct 〜 end で書けばいいや」なんて考えてた時期もありました…楽しちゃダメですね ↩

  5. 元記事であのようなコードを書いたのも、私が Julia を本格的に勉強し始めた頃だし、色々とよく分かってなかった部分もあるかもしれません。あと他言語の外部コンストラクタのお作法に影響されてたのだったかも（記憶が曖昧）。 ↩

  6. なお BitArray <: AbstractArray{Bool} であり、「Bool型の配列」として普通に扱えます。コード内に敢えて ::AbstractArray{Bool, 1} と書いてある箇所は、::BitArray{1} でも良かったわけですが、「仕様上 Array{Bool, 1} でも BitArray{1} でもどちらが来ても動作する」ようにするために敢えてそう書きました。 ↩

  7. ちなみに Julia の Bool 型のサイズは1バイトです。よって要素数が8のArray{Bool,1}は8バイトを占有しますが、同じ要素数8でもBitArray{1}ならば1バイトしか占有しません。 ↩

2
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
2
1