もっとシンボリックに「充足可能性問題(3-SAT)を解く乱択アルゴリズム」 by Julia v1.0

TL;DR

• Julia なら、こんなにシンボリックな（≒直感的に書けてしかも速い）プログラムも書けるんですよ！

初めに

先日の記事（「充足可能性問題(3-SAT)を解く乱択アルゴリズム」 by Julia for v1.0）は、「3年前に書いた Julia（当時 v0.3.x）のコードを最新の Julia v1.0.0 で動くようにする」ことが目的だったもの。
今回は、「もし今同じものを1から Julia v1.0.0 で書くなら、実装にもっと手間を加えて、その代わりにそれを『使う側』はもっともっと直感的に書けるようにするかも」というコンセプトで、さらに書き直してみた結果を紹介します。

テーマは、「もっとシンボリックに」。

開発環境・動作確認環境等

• Mac OSX 10.11.6
• Julia v1.0.0

具体的にやりたかったこと

やりたかったのは以下の2つ：

• (x₁ ∨ x₂) ∧ (x₄ ∨ ¬x₃) のような論理式を直接記述したい
• 変数の数は固定パラメータなので、rw3sat() 関数に引数として渡すのをやめたい

先にちょっとだけ解説します。興味が無い方は 実装例 に飛んでください。

(x₁ ∨ x₂) ∧ (x₄ ∨ ¬x₃) のような論理式を直接記述したい

元々、一番最初に参考にした maehrm さんの Ruby 版 では、命題論理式を "( x[0] or x[1] or x[2]) and (!x[3] or !x[1] or x[2])" のような、Ruby で直接評価もできるような文字列 で与えていました。
私も過去に書いた他言語版では、同様に「その言語の eval() 関数（またはメソッド）に渡せる文字列を与える」タイプの実装（例：Ruby版（先の maehrm さん版を少し弄ったもの）、R版、Python版）や、「その文字列を独自に解釈または変換して目的の CNF（内の各 Clause）を取得して処理する」タイプの実装（例：JavaScript版、Haxe版）をやってたりしました。

3年前に Julia 版を書くにあたって、この方針を採らなかったのは、以下のような理由によるもの：

• せっかくしっかりとした 型システム があるのだから、それを有効に使いたい（というか 多重ディスパッチ を試したい）
• Julia にも eval() あるけれど、「文字列 ▷ parse → 式 ▷ eval → 値」って微妙に回りくどいし eval() 一歩間違えば危ないし絶対遅い、Julia の高速性 が活かせるコードにしたい

ということで あのようなコード になり、あのコードがその後実装した（主に）関数型言語による実装¹（例：Elixir版、Scala版）のベースになってたりもします²。

でもあのコード、やっぱ機械的なんですよね。各関数（コンストラクタ）の組合せでデータ構造を直接的に表現（もしくは具現化）する、それも悪くはないんですけれど、以前のような直感性が失われているのは気になってたのです。「やっぱ論理式みたいに見える記述方法で入力を与えたい」って。

でも、今なら言える。型（データ型）定義による実装方針を保持したままで、かつ論理式のような（というか 論理式そのものの見た目の）コードを書くことが出来る ようにできるのです。そう、Julia なら。
（詳細はこの後の実装例を参照のこと）

固定パラメータを関数に引数として渡すのをやめたい

今までの私の全ての実装例で共通していたのが、これ。
最初に「コレとコレとコレとコレ」と変数（Literal）を決めて、その（3つ以内の）組合せ（or 条件）で節（Clause）を作り、その組合せ（and 条件）で作ったのが CNF（3SAT）。
それを満たす変数の（実際の値の）組合せが存在するかどうか、というのが、目的の「3SAT問題」。それを探索する関数 rw3sat() 関数を記述する、というのが目的。
この関数に渡すのは、だから、CNF と試行回数だけで良いはずなんです。変数の個数は、関数のパラメータではなく、CNF を組み立てるときに必要なんだし、その時の個数を記憶しておいてそこから取り出せば良い（というかそうすべき）もののはず。
これ、前々から少し引っかかってたことなんです。

でも今まで、rw3sat() 関数の2番目の引数に与えていたのは、それが一番手っ取り早い実装だったから³。

ただ、これを「文字通り固定パラメータとして暗黙的に持たせて、それを効率良く取り出して利用する方法」があるんです。そう、Julia なら。
（詳細はこの後の実装例を参照のこと）

コード

ということで、今回の成果物⁴です。

所々に # ↓ Point (N) のようなコメントを入れてあります。

Rw3sat.symbolic.jl

# Rw3sat.symbolic.jl
using Random

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

#             ↓ Point (1)
struct Literal{N}
    index::Int
    not::Bool
end

# ↓ Point (2)
¬(l::Literal{N}) where {N} = Literal{N}(l.index, !l.not)

issatisfied(l::Literal, x::AbstractArray{Bool, 1}) = l.not ⊻ x[l.index]

# ↓ Point (3)
struct LiteralSymbol{N} <: AbstractVector{Literal{N}} end
LiteralSymbol(N::Int) = LiteralSymbol{N}()
Base.size(::LiteralSymbol{N}) where {N} = ((N::Int),)
Base.length(::LiteralSymbol{N}) where {N} = N::Int
function Base.getindex(x::LiteralSymbol{N}, idx::Int) where {N}
    if idx < 1 || idx > N
        throw(BoundsError("attempt to access $(N)-element LiteralSymbol at index [$idx]"))
    end
    Literal{N}(idx, false)
end

#            ↓ Point (1)
struct Clause{N}
    literals::Array{Literal{N}, 1}
end
# Clause(ls::Literal...) = Clause([ls...])
# ↓ Point (4)
Clause(literals::Array{Literal{N}, 1}) where {N} = Clause{N}(literals)
Clause(literal::Literal{N}) where {N} = Clause{N}([literal])
Clause(clause::Clause) = clause

# ↓ Point (5)
const ClauseOrLiteral{N} = Union{Clause{N}, Literal{N}}

# ↓ Point (2)
∨(c1::Clause{N}, c2::Clause{N}) where {N} = Clause([c1.literals; c2.literals])
∨(x1::Literal{N}, x2::Literal{N}) where {N} = Clause([x1, x2])
∨(c1::ClauseOrLiteral{N}, c2::ClauseOrLiteral{N}) where {N} = Clause(c1) ∨ Clause(c2)

issatisfied(c::Clause, x::AbstractArray{Bool, 1}) = any(issatisfied(l, x) for l=c.literals)

#         ↓ Point (1)
struct CNF{N}
    clauses::Array{Clause{N}, 1}
end
# CNF(cs::Clause...) = CNF([cs...])
# ↓ Point (4)
CNF(clauses::Array{Clause{N}, 1}) where {N} = CNF{N}(clauses)
CNF(clause::Clause{N}) where {N} = CNF{N}([clause])
CNF(literal::Literal{N}) where {N} = CNF{N}([Clause(literal)])
CNF(cnf::CNF) = cnf

# ↓ Point (5)
const Proposition{N} = Union{CNF{N}, Clause{N}, Literal{N}}

# ↓ Point (2)
∧(c1::CNF{N}, c2::CNF{N}) where {N} = CNF([c1.clauses; c2.clauses])
∧(c1::Clause{N}, c2::Clause{N}) where {N} = CNF([c1, c2])
∧(c1::ClauseOrLiteral{N}, c2::ClauseOrLiteral{N}) where {N} = Clause(c1) ∧ Clause(c2)
∧(p1::Proposition{N}, p2::Proposition{N}) where {N} = CNF(p1) ∧ CNF(p2)

issatisfied(f::CNF, x::AbstractArray{Bool, 1}) = all(issatisfied(c, x) for c=f.clauses)

#                     ↓ Point (1)
function rw3sat(f::CNF{N}, rr::Int) where {N}
    for r = 1:rr
        x = bitrand(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

# ↓ Point (3)
強, 正, 美, 優 = LiteralSymbol(4)
# ↓ Point (2)
p₁ = 強 ∨ 正 ∨ 美
p₂ = 優 ∨ 正 ∨ ¬美
p₃ = ¬強 ∨ 優 ∨ 美
p₄ = ¬強 ∨ ¬優 ∨ 正
p₅ = ¬優 ∨ ¬正 ∨ 美
p₆ = ¬強 ∨ ¬正 ∨ ¬美
p₇ = 強 ∨ ¬優 ∨ ¬美
p₈ = 強 ∨ 優 ∨ ¬正

f = p₁ ∧ p₂ ∧ p₃ ∧ p₄ ∧ p₅ ∧ p₆ ∧ p₇ ∧ p₈
# f = p₁ ∧ p₂ ∧ p₃ ∧ p₄ ∧ p₅ ∧ p₆ ∧ p₈
# ↑ Point (2)

#               ↓ Point (1)
println(rw3sat(f, 3))

解説

上述のコード内に挙げた各 Point ごとに解説します。

Point (1) Julia の型パラメータ

Julia の型には型パラメータを設けることができます。
この型パラメータに、整数値を設定することも出来ます⁵⁶。

これを利用して、CNF（やそれらを構成する Clause, Literal、および Literal を半自動生成する目的で今回新たに定義した LiteralSymbol）に型パラメータ N を持たせています。この N が、変数の個数です。

型パラメータは、その型を受け取る関数で where {N} のように宣言することで、定数（扱いの変数？）のようにその関数内で自由に参照できます⁷。

しかもうまく実装すれば、コードを利用する側はその型パラメータの存在を意識するのは最初の1回だけ（実装によってはまったく無意識的に埋め込む方法もアリ）。今回の場合は、最後の方に各リテラルを宣言するときの 強, 正, 美, 優 = LiteralSymbol(4) という箇所に変数の個数 4 が明示的に出てくる以外、全く出てきません！

やりたかったことその2「固定パラメータは関数の引数に渡さない」が見事に実現できました！

Point (2) Julia の独自演算子の定義

Julia は、一部の記号について、通常の関数定義の方法で関数として定義すると、そのまま演算子として利用できるようになります。
実際、四則演算を初めとする標準の演算子のほとんどは、関数として定義されています⁸。

そして、論理演算でよく使われる数学記号である、¬（論理否定）、∨（論理和）、∧（論理積）は、Julia において「演算子として利用できる記号」になっています。
しかも¬はきちんと「単項演算子として利用できる」ように内部実装されています！

なのでこれらを（今回のコードのように）適切に実装すると、コード中に (x₁ ∨ x₂) ∧ (x₄ ∨ ¬x₃) のような論理式がそのまま記述できます！

今回は「Literal の論理否定 ¬ は Literal（$\forall l \in Literal,, \neg l \in Literal$）」「Literal または Clause の論理和は Clause」「Literal または Clause または CNF の論理積は CNF」という定義をしています。
よってコード最後の方の、p₁〜p₈（例：p₁ = 強 ∨ 正 ∨ 美）は Clause, f（f = p₁ ∧ p₂ ∧ p₃ ∧ p₄ ∧ p₅ ∧ p₆ ∧ p₇ ∧ p₈）は CNF となっています。

とにかくこれで、やりたかったことその1「論理式をそのまま記述したい」が見事に実現できました！

Point (3) 独自の配列型の宣言

(1) でもちらっと触れましたが、今回 Literal を半自動生成する目的で、LiteralSymbol という型も新たに用意しました。
使い方は先ほど示したコードに書いてある通り、

# ↓ Point (3)
強, 正, 美, 優 = LiteralSymbol(4)

と記述すると、

『Literal（変数）のシンボルを4つ用意して、それぞれ 強, 正, 美, 優 という名前にする』

という意味になります。

以降はこれらの変数を使って論理式を記述するだけでOK！

仕組みは、配列のインデックス参照の仕組みをそのまま利用しているだけです。詳しくはコードを覗いて見てください。
あと「もしこれを定義せずに 強, 正, 美, 優 それぞれを個別の（ただし同じ CNF で利用する4つの）Literal として宣言するには、どう記述すれば良いか」てのを考えてみてください。やっぱり機械的な作業が必要になってくるのが分かると思います。

なお struct LiteralSymbol{N} <: AbstractVector{Literal{N}} end と宣言していますが、setindex!() 関数は多重定義していないので、配列と言っても代入は出来ません、参照だけです、そもそも struct だから immutable だし⁹。

Point (4) 外部コンストラクタ、もしくはコンバータ

前回の記事でも「型定義外に型名と同じ関数を定義することで外部コンストラクタ」という話はしたと思います。
「型名と同じ名前の関数」には、実はもう1つの役割があります。それは「コンバータ（変換器）」です。

Julia には暗黙キャストは存在しません。ある型から別の型に変換する場合は、互換性がありそうな型であっても、内部的に全て変換関数や変換ルール（promote_rule）の定義が記述されています。
+ 演算子は1つしかなくても、それで数値同士ならどんな型同士でも演算できるのは、Julia が内部で premote_rule や変換器を細かく記述して、+ 演算子（関数）をうまく多重定義しているからです。

同様なことを、今回少しだけ実施しています。promote_rule を定義するほど複雑じゃなかったので、少しだけ手抜きして、変換器として「Literal の Clause への変換」「Clause の CNF への変換」「Literal の CNF への変換」を定義して、「ClauseまたはLiteralどうしの論理和演算∨は、両オペランドをClauseに変換してから実施する」「CNFまたはClauseまたはLiteralどうしの論理積演算∧は、両オペランドをCNFに変換してから実施する」という実装をしています。

Point (5) Union Type の 型パラメータ付型エイリアス

Julia では 型エイリアス を定義するには、const キーワードを利用します¹⁰。
この時、型パラメータ付のエイリアス型も定義できちゃいます。

今回は「Clause{N}型、もしくはLiteral{N}型」を表す Union Type として ClauseOrLiteral{N} という型エイリアスを、「CNF型、Clause{N}型、もしくはLiteral{N}型」を表す Union Type として Proposition{N} という型エイリアスを宣言しています。

ちなみに Proposition{N} の方ですが、これ、共通の Abstract Type にしても良かったですね。その場合、先に

abstract type Proposition{N} end

と記述しておいて各型の宣言時に

struct Literal{N} <: Proposition{N}
    〜
end

のように記述することになります。

今回は取り敢えずやっつけで Union Type にしましたが、もっと型の数が多いときは、どのように実装すべきかきちんと型設計をして決めた方が良いでしょうね。

最後に

最初に『しかも速い』と言っておきながら、速度（パフォーマンス）はまだ十分に確認していません。
取り敢えずこのコードをそのまま1ファイルに記述してコマンドラインから実行しても、速度最適化をきちんとしていないし JIT コンパイルの時間も含まれてしまうので、そこまでの速度を実感できないかもしれません。
そのあたり、きちんと検証までいけたらこの記事に追記・修正したいとは思います。

取り敢えず、Julia ってちょっとした工夫を取り入れていろんなことが出来るんだ、ってことだけでも伝わったら良いな、と。
Julia 楽しいよー

1. マサカリ投げられないように補足しておくと正確には、「関数型プログラミングが得意な言語による、なるべく関数型プログラミングを意識した実装」です。 ↩

2. より正確には、やはり関数型パラダイムを持つ Egison で実装した例の方が先にあって、旧 Julia版 はその時のデータ型定義（Literal とは「整数値（＝インデックス番号）とBool値（肯定か否定か）からなるタプル」、Clause とは「Literal のリスト」、CNF とは「Clause のリスト」）と、「あるBool値の列がそれら全条件を満たすものかの判定方法」を移植したものになっていたりもするわけですけれど。 ↩

3. ちなみにクラスベースオブジェクト指向設計をしていれば、それは「rw3sat() メソッドを擁するオブジェクトのインスタンス変数（もしくは設計方針によってはクラス変数？）」に持てばよさそうな気がします…いやそれでも色々と他の整合性とか面倒なことになりそうな気もする…。 ↩

4. 見て分かるとおり、結局「1から書き直した」コードではなく「元のコードを大幅に加筆修正した」ものになっています。 ↩

5. 例えば標準では、Array{T, N} という型は「要素の型がTで次元数がNの配列型」です。つまり型パラメータNは整数値です。 ↩

6. 型パラメータに設定できるものは、型と整数値以外にも、(1)Symbol値（:a とか）、(2)isbits() に渡して true が返る値（整数値はここに含まれる、他には実数値・関数等）、(3)それらのTuple値（(Int,1,:a,+) とか）。 ↩

7. 実装レベルに近い話をすると、そのように宣言された型パラメータを参照している箇所は、中間表現では Expr(:static_parameter, 1) のようになっています。つまり文字通り「1番目の静的パラメータ」ですね。 ↩

8. 代入演算子（=）、論理演算子（&&,||）などは例外で、関数としては定義されていません（⇔所謂オーバーロードで動作を変えることが許されていません）。 ↩

9. コレ別に <: AbstractVector{Literal{N}} 要らなかったんですけれどね、実は。「こんな感じでオレオレ配列型だって簡単に定義できるんですよ」っていう例も兼ねて今回は敢えて。 ↩

10. 昔は typealias というキーワードがあって、これを利用して型エイリアスを定義していました。 ↩