LoginSignup
0
0

More than 5 years have passed since last update.

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

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

Last updated at Posted at 2015-08-22

前置き

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

ということで。前々回の Egison版、前回の Julia版 に続いて、Ruby ライクな言語の中で最近特に Hot な（気がする）Elixir で書いてみました。
ideone.com にも採用されて Playground 的に動作確認もできますし2。

開発環境・動作確認環境

  • 環境1：
    • Mac OSX 10.9.5
    • Erlang/OTP 17 3
    • Elixir 1.0.5 3
  • 環境2（動作確認）：

コード

rw3sat.ex
# rw3sat.ex
# http://ideone.com/3PzRUG

defmodule RW3SAT do
  :random.seed :os.timestamp

  defp sample(xs) do
    # ref: http://c4se.hatenablog.com/entry/2015/04/20/101926
    Enum.at(xs, :random.uniform(Enum.count xs) - 1)
  end

  defmodule Literal do
    defstruct index: 0, flag: false
  end
  defp literal(index, flag), do: %Literal{index: index, flag: flag}

  defmodule Clause do
    defstruct literals: []
  end
  defp clause(literals), do: %Clause{literals: literals}

  defmodule CNF do
    defstruct clauses: []
  end
  defp cnf(clauses), do: %CNF{clauses: clauses}

  defp satisfied?(l = %Literal{}, x) do
    if l.flag, do: !Enum.at(x, l.index), else: Enum.at(x, l.index)
    # l.flag xor Enum.at(x, l.index)
  end

  defp satisfied?(c = %Clause{}, x) do
    Enum.any?(c.literals, &(satisfied?(&1, x)))
  end

  defp satisfied?(f = %CNF{}, x) do
    Enum.all?(f.clauses, &(satisfied?(&1, x)))
  end

  defp w4(n) do                                                       # W4
    for _ <- 1..n, do: sample([false, true])
  end

  defp rw3sat_loop(_, _, _, _, _, true) do                            # W7
    "充足可能である"                                                  # W8
  end

  defp rw3sat_loop(_, _, 0, 0, _, _) do
    "おそらく充足不可能である"                                        # W17
  end

  defp rw3sat_loop(f, n, 0, r, _, _) do
    x = w4(n)
    rw3sat_loop(f, n, n * 3, r - 1, x, satisfied?(f, x))          # W15,W16
  end

  defp rw3sat_loop(f, n, k, r, x, _) do
    c = f.clauses |> Enum.filter(&(!satisfied?(&1, x))) |> sample     # W10
    %{index: i} = sample(c.literals)                                  # W11
    x2 = for j <- 0..n-1 do                                           # W12
      if i == j, do: !Enum.at(x, j), else: Enum.at(x, j)
    end
    rw3sat_loop(f, n, k - 1, r, x2, satisfied?(f, x2))            # W13,W14
  end

  def rw3sat(f, n, r) do
    x = w4(n)
    rw3sat_loop(f, n, n * 3, r, x, satisfied?(f, x))          # W2,W3,W5,W6
  end

  def main do
    p1 = clause([literal(0, false), literal(1, false), literal(2, false)])
    p2 = clause([literal(3, false), literal(1, false), literal(2, true )])
    p3 = clause([literal(0, true ), literal(3, false), literal(2, false)])
    p4 = clause([literal(0, true ), literal(3, true ), literal(1, false)])
    p5 = clause([literal(3, true ), literal(1, true ), literal(2, false)])
    p6 = clause([literal(0, true ), literal(1, true ), literal(2, true )])
    p7 = clause([literal(0, false), literal(3, true ), literal(2, true )])
    p8 = clause([literal(0, false), literal(3, false), literal(1, true )])

    f = cnf([p1, p2, p3, p4, p5, p6, p7, p8])
    # f = cnf([p1, p2, p3, p4, p5, p6, p8])
    rw3sat(f, 4, 3) |> IO.puts
    # => おそらく充足不可能である
  end

end

RW3SAT.main

ideone.com での動作確認4。

コードそのものは、最近書いた Julia版 や Egison版 をだいたいそのまま翻訳しただけです。それらと比較していただければ難しいことは無いと思います。
もちろん今回も対応する仮想コードの行番号を記述（行末の # W4 とか）しておいたので書籍をお持ちの方はそれと対比して見ていただけると良いと思います。
一応、Elixir っぽいと思われる部分を自分の言葉で解説してみます（ツッコミ大歓迎）。

  • 5行目、9行目。Elixir での乱数の扱いはこの書き方がデファクトスタンダードのようです。
    :random は、Erlang OTP (stdlib) の random モジュールを表す Atom。最近よくある言語と違い乱数シードは自動で適当に設定はされないので、現在日時（ミリ秒）等を渡してシード設定してやる必要があるようです。
    なお乱数シードの設定は、プログラム実行の中でどこかで1回だけ実行すれば良いわけですが、それも踏まえて敢えて「モジュール定義の先頭行」でそれを実施しています。そのモジュールを解釈するときその1回だけ実行されるわけなので。
  • Literal、Clause、CNF は、モジュール内にネストした構造体として定義。literal、clause、cnf という private 関数で外部コンストラクタ（っていう言い方を Elixir で言うのか未確認）定義して生成を簡略化（というより他言語での記述に合うようにしてみた）。
  • 17〜38行目。パターンマッチを利用した関数の多重定義（っていう言い方を Elixir で以下略）。
    Elixir の（Erlang 由来の？）パターンマッチもなかなか面白い(^-^) 代入も実はパターンマッチの特別な場合とか、なんか楽しい(^-^) パターンが自分で構築できたらもっと良いのにとか思う。
  • 28, 29行目。上は if 式（正確には if はマクロ）をインラインで3項演算子的に利用した記述。下は、それを xor を利用したショートハンドに置き換えようと試みた書き方。Elixir は xor 廃止されたんですね、エラーが出てびっくり。便利なのになー。
  • 33, 37, 58行目。&(〜) というのは無名関数（lambda）のシンタックスシュガーのようです。&1,&2,… が渡される仮引数。
    Ruby で Proc オブジェクト等をブロックとして引数に渡す &block という書き方と、Clojure 等で見られる #2(〜 %1 %2) みたいな lambda の書き方のミックス、でしょうか。
    なお、曖昧さが問題なければ () は不要でこのコードの場合は &satisfied?(&1,x) と書いても動作するようです。
  • 41行目。Elixir のリスト内包表記。
    Python の [sample([False, True]) for _ in range(n)] に相当。
    なんか見た目（手続き型言語でよく見られる普通の）ループの書式なんですけれど、式の結果はリスト。個人的には少し紛らわしいです。まあ慣れの問題かな？
  • 44〜64行目。Elixir には言語仕様としてのループは存在しません、Haskell とか Egison とかもちろん Erlang とかのように、ループは再帰で実現。
    また先ほど触れたように、パターンマッチで（同じ個数の引数を持つ関数でも見た目個別に多重に）定義できるので、このような宣言的な書き方をすることで極力条件分岐を表に出さずに済みます。
    その仕様に徹底的にこだわって、ループに関しては if による条件分岐を一切なくしてみました。どうでしょう？
  • 58行目。|> はパイプライン演算子。関数を次々と適用していく、他言語にもよく見られる言語仕様。Ruby のメソッドチェインとの対比をしていた記事をどこかで見かけた気がします。
  • 59行目。これもパターンマッチの一例。右辺は %Literal{} になるので、index と flag の2つのフィールドを持つわけですが、そこで左辺を %{index: i} とすることで、右辺の index フィールドの値と左辺の i がマッチングされて、結果的に i にその値が代入される仕組み。
    これだけだと i = sample(c.literals).index と書いても目的は達成されるのですが、もし flag フィールドの値も取り出したければ %{index: i, flag: f} = 〜 と書くことで両方一気に取得できる、と。これ便利♪ 使いこなせたらいろいろハッピーになれそう(^-^)

んー、やっぱ書いてみると盛りだくさんだー。

なお（毎度恒例ですが）、Elixir の技術情報的な内容以外（3-SAT そのものについて等）は、書籍や、私や他の方の過去の実装例（記事末尾↓参照）を参考にしてください。

感想

どこかで見かけたけれど、「Elixir は文法は Ruby に似せているけれど、触れば触るほど Ruby とは別言語。むしろ結局 Erlang」まさにこれ。
軽い気持ちで触れようと思ったら結局「軽く」じゃ済まなくなってきてます。本腰入れて勉強するかとっとと見切りを付けて今勉強中のモノに集中するかしないと。

ただ、あともう1つ、以前他言語で書いたものを Elixir に移植したもの5があるので、余裕があったらそれも後日記事にするかもしれません。

参考

私が過去に実装した他言語での実装例

その他の実装例・関連記事

Elixir/Erlang の技術情報

  1. 以上、何度目かのコピペ。 ↩

  2. 利用可能になったのは約1ヶ月前ですが、今日 (2015/08/22) 現在まだ不具合が残っているらしく、2回に1回くらい RuntimeError が出ます。Erlang 側のエラーのようです。もうちょとちゃんとしてほしい ideone.com。 ↩

  3. Homebrew で普通にインストール。特に難しいことなかったので導入記事書きません。 ↩

  4. ideone.com で動作確認したいがために、1ファイルで収まるようにこのような書き方をしています。mix コマンドでプロジェクトを作ったりテスト駆動開発したりとか今回はしていません。コマンドラインでの実行は elixir rw3sat.ex。 ↩

  5. というか以前個人的に某所で出題したややこしい処理を実装する問題を Elixir で自分で解いてみた話（で分かる人には分かるかも）。 ↩

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