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

前置き

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

今回は、今後仕事で使うかもしれない² Scala で。
とりあえず FP in Scala 読書会³ にも1回参加したしその本も5章までは読んだので、その勉強成果みたいなのも兼ねて。

開発環境・動作確認環境

環境1（自宅Mac）：
- Mac OSX 10.11.6
- java v1.8.0_92
- Scala v2.11.8 / Scala v2.12.0-M4⁴
環境2（会社PC）：
- Windows 10 Pro
- java v1.8.0_92
- Scala v2.11.8
環境3（動作確認）：
- ideone.com
- java v1.8.0_51
- Scala 2.11.7

コード

例1：とりあえず書いてみた初期版

とりあえず「他言語で培った関数型プログラミングの基礎知識」と「クラスベースのオブジェクト指向プログラミングの定石」をベースに、少しだけ「Scala 特有の書き方（覚えたから使ってみたかった）」のエッセンスを加えて『とにかく動くもの』を目指した結果がこちら。

rw3sat_oo.scala

// rw3sat_oo.scala

import scala.util.Random

object Main {
  class Literal(val index: Int, val flag: Boolean) {
    def apply(x: Seq[Boolean]) = this.flag ^ x(this.index)
  }
  object Literal {
    def apply(index: Int, flag: Boolean) = new Literal(index, flag)
  }

  class Clause(val literals: Seq[Literal]) {
    def apply(x: Seq[Boolean]) = this.literals.exists(_(x))
  }
  object Clause {
    def apply(literals: Literal*) = new Clause(literals)
  }

  class CNF(val clauses: Seq[Clause]) {
    def apply(x: Seq[Boolean]) = this.clauses.forall(_(x))
  }
  object CNF {
    def apply(clauses: Clause*) = new CNF(clauses)
  }

  def sample[A](a: Seq[A]): A = a(Random.nextInt(a.length))

  def w4(n: Int): Seq[Boolean] = for (_ <- 0 until n) yield Random.nextBoolean  // W4

  def rw3sat(f: CNF, n: Int, r: Int): String = {
    @annotation.tailrec
    def loop(k: Int, r: Int, x: Seq[Boolean]): Option[Seq[Boolean]] = 
      (f(x), k, r) match {
        case (true, _, _) => Some(x)                                // W7,W8
        case (_, 0, 0) => None                                      // W17
        case (_, 0, _) => loop(n * 3, r - 1, w4(n))                 // W15,W16
        case _ => {
          val c = sample(f.clauses.filterNot(_(x)))                 // W10
          val index = sample(c.literals).index                      // W11
          val x2 = x.updated(index, !x(index))                      // W12
          loop(k - 1, r, x2)                                        // W13,W14
        }
      }

    loop(n * 3, r, w4(n)) match {                               // W2,W3,W5,W6
      case Some(x) => "Satisfiable with [" + x.mkString(",") + "]"   // "充足可能である"
      case _ => "Probably Unsatisfiable"    // "おそらく充足不可能である"
    }
  }

  def main(args: Array[String]): Unit = {
    val p1 = Clause(Literal(0, false), Literal(1, false), Literal(2, false))
    val p2 = Clause(Literal(3, false), Literal(1, false), Literal(2, true ))
    val p3 = Clause(Literal(0, true ), Literal(3, false), Literal(2, false))
    val p4 = Clause(Literal(0, true ), Literal(3, true ), Literal(1, false))
    val p5 = Clause(Literal(3, true ), Literal(1, true ), Literal(2, false))
    val p6 = Clause(Literal(0, true ), Literal(1, true ), Literal(2, true ))
    val p7 = Clause(Literal(0, false), Literal(3, true ), Literal(2, true ))
    val p8 = Clause(Literal(0, false), Literal(3, false), Literal(1, true ))

    val f = CNF(p1, p2, p3, p4, p5, p6, p7, p8)
    // val f = CNF(p1, p2, p3, p4, p5, p6, p8)
    println(rw3sat(f, 4, 3))
    // => Probably Unsatisfiable
  }
}

ideone.com での動作確認。

コードそのものは、以前書いた同じ関数型の Egison版や Elixir版をだいたいそのまま翻訳した感じになっています。
今回も対応する仮想コードの行番号を記述（行末の # W4 とか）しておいたので書籍をお持ちの方はそれと対比して見ていただけると良いと思います。
一応、Scala 固有の箇所を自分の言葉で解説してみます（ツッコミ大歓迎）。

3,27,29行目。乱数周りは素直に scala.util.Random パッケージを利用。
- 副作用を伴う擬似乱数ですが、それとIO以外の部分に関しては純粋関数型プログラミングを心がけています⁵。
6-25行目。class 定義を利用した Literal, Clause, CNF の各定義。
- それぞれの定義で、class Xxx のすぐあとに object Xxx とあります。クラス名と同名のオブジェクトを「コンパニオンオブジェクト」と呼び、そのクラス固有の処理等を記述できるようになっています。特にその中に apply メソッドを定義すると、Xxx() のようにクラス名だけで（new を頭につけないで）呼び出すことができて、Factory Method とか外部コンストラクタの用途で使えます。今回もそのように利用（特に Clause とか CNF で、リスト（Seq）で渡さなくても可変個引数で渡せばOKなようにしています）。
- あと class 定義内にも def apply(～) がありますが、こちらも「val x = new Xxx() な x に対して、x(～) と書くことができる（x.apply(～) と同じ意味になる）」というもの。Python の def __call__(～): と類似。
27行目。def sample[A](～: Seq[A]): A の [A] は、型ジェネリクスの表記。Java だと <T> T sample(List<T> ～) みたいな感じ、Julia だと function sample{T}(～: AbstractVector{T}) みたいな。
型パラメータは、Aから順に大文字アルファベット1文字を使用するのが Scala 流だそうです。
29行目。for (yyy <- zzz) yield xxx は、Scala のリスト内包表記。yield がなければ普通の for ループ、あればそれぞれの結果を要素とするリスト（正確には Seq？）を返す、という違いがある模様。Elixir の「for は comprehension（only）」よりも個人的には分かりやすい。
32行目。@annotation.tailrec は、以降に続く関数が「末尾再帰」であることを示す annotation。これがついていると、末尾再帰出ない場合にコンパイル時にエラーが出るらしい⁶。
Scala は非純粋関数型言語⁷ であり、手続型言語によくみられる制御構造としての for や while といったループも存在しますが、せっかくなので今回も（純粋）関数型プログラミングを目指して⁸ループは関数の再帰で実現。その方がきれいなので⁹。
46-49行目。Scala もパターンマッチ構文持ってます。なかなか便利。自分でパターンをある程度構築できることも含めて Scala の match は結構魅力的。
↑のマッチ式でも利用している、Option/Some/None¹⁰。値があるときは Some(x) でくるんで、ないときは None を返す。そのまま match で受け取れる。Scala での定石のようで、標準ライブラリも基本的にこれを利用（例：Map[A,B]のget()メソッドはOption[B]を返す）。

例2：もうちょっと Scala らしくしてみた第2版

Scala らしくというか、「クラスベースオブジェクト指向っぽさ（というかJavaっぽさ）がどうも違和感あるからできれば排除したい」と思いまして。
あとパターンマッチももう少し活用できないか、と。
といった工夫をしてみたコードがこちら。

rw3sat.scala

// rw3sat.scala

import scala.util.Random
// import scala.language.implicitConversions

object Rw3sat {
  type Literal = (Int, Boolean)
  object Literal {
    def apply(index: Int, flag: Boolean): Literal = (index, flag)
    def unapply(l: Literal) = Some(l)
  }

  type Clause = Seq[Literal]
  object Clause {
    def apply(literals: Literal*): Clause = literals
  }

  type CNF = Seq[Clause]
  object CNF {
    def apply(clauses: Clause*): CNF = clauses
  }

  trait IsSatisfied[+A]
  case object Satisfied extends IsSatisfied[Nothing]
  case class Unsatisfied[A](x: A) extends IsSatisfied[A]
  // implicit def isSatisfiedToBoolean[A](v: IsSatisfied[A]): Boolean = v match {
  //   case Satisfied => true
  //   case Unsatisfied(_) => false
  // }

  def eval(l: Literal)(x: Seq[Boolean]): Boolean = {
    val Literal(i, b) = l
    b ^ x(i)
  }
  def eval(c: Clause)(x: Seq[Boolean]): Boolean = 
    c.exists(eval(_)(x))
  def eval(f: CNF)(x: Seq[Boolean]): IsSatisfied[CNF] =
    f.filterNot(eval(_)(x)) match {
      case Nil => Satisfied
      case fs => Unsatisfied(fs)
    }

  def sample[A](a: Seq[A]): A = a(Random.nextInt(a.length))

  def w4(n: Int): Seq[Boolean] = for (_ <- 0 until n) yield Random.nextBoolean  // W4

  def rw3sat(f: CNF, n: Int, r: Int): String = {
    @annotation.tailrec
    def loop(k: Int, r: Int, x: Seq[Boolean]): Option[Seq[Boolean]] = 
      (eval(f)(x), k, r) match {
        case (Satisfied, _, _) => Some(x)                           // W7,W8
        case (_, 0, 0) => None                                      // W17
        case (_, 0, _) => loop(n * 3, r - 1, w4(n))                 // W15,W16
        case (Unsatisfied(fs), _, _) => {
          val c = sample(fs)                                        // W10
          val Literal(index, _) = sample(c)                         // W11
          val x2 = x.updated(index, !x(index))                      // W12
          loop(k - 1, r, x2)                                        // W13,W14
        }
      }

    loop(n * 3, r, w4(n)) match {                               // W2,W3,W5,W6
      case Some(x) => "Satisfiable with [" + x.mkString(",") + "]"   // "充足可能である"
      case _ => "Probably Unsatisfiable"    // "おそらく充足不可能である"
    }
  }

  def main(args: Array[String]): Unit = {
    val p1 = Clause(Literal(0, false), Literal(1, false), Literal(2, false))
    val p2 = Clause(Literal(3, false), Literal(1, false), Literal(2, true ))
    val p3 = Clause(Literal(0, true ), Literal(3, false), Literal(2, false))
    val p4 = Clause(Literal(0, true ), Literal(3, true ), Literal(1, false))
    val p5 = Clause(Literal(3, true ), Literal(1, true ), Literal(2, false))
    val p6 = Clause(Literal(0, true ), Literal(1, true ), Literal(2, true ))
    val p7 = Clause(Literal(0, false), Literal(3, true ), Literal(2, true ))
    val p8 = Clause(Literal(0, false), Literal(3, false), Literal(1, true ))

    val f = CNF(p1, p2, p3, p4, p5, p6, p7, p8)
    // val f = CNF(p1, p2, p3, p4, p5, p6, p8)
    println(rw3sat(f, 4, 3))
    // => Probably Unsatisfiable
  }
}

ideone.com での動作確認。

基本的な流れは例1 と同じ。特に終盤のループ呼び出し・結果戻し部分と main() は全く同一。
変更箇所を少し詳しく解説（ツッコミ大歓迎）。

7-21行目。Literal,Clause,CNFをクラスをやめてただの型エイリアスに変更。
このときもコンパニオンオブジェクトが定義できるので、外部コンストラクタは先の例とまったく同じ仕様のものを定義。
- 10行目。Literal のコンパニオンオブジェクト内に def unapply(～) というのが定義してありますが、これは抽出子（extractor）の定義。これが定義してあると、パターンマッチのケースパターン（Constructor パターン）として利用できたり、32行目や56行目のように（一部の）フィールドを他の変数に束縛できたりします。これで「オブジェクト指向っぽさ」が1つ減らせる！
23-25行目。「満たされているかどうか」も1つの型（=trait IsSatisfied[+A]）として表現。「満たされている」は case object、「（～に関して）満たされない」は（～にあたる部分をフィールドとして保持するような）case class として表現（それぞれ case object Satisfied extends IsSatisfied[Nothing], case class Unsatisfied[A](x: A) extends IsSatisfied[A]）。
- case object/case class は、そのままマッチ構文の case 式に渡せる。特に case class の方は、デフォルト実装で apply や unapply が定義される。
  Scala で何か（複合）データ型を考えるときはまず「case class にできないか？」を考える、これが常道のようです。その意味では今回の Literal は case class でも良かったですね。
4,26-29行目。↑で定義した IsSatisfied型を Boolean に暗黙変換するための implicitメソッドの定義。せっかく覚えたから使ってみたかっただけ。でも結局使われることがなくなったのでコメントアウトで残しておいただけです(^-^;
31-41行目。例1ではクラスのインスタンスメソッド def apply(～) で定義していたものを外出ししたもの。
ただし CNF に対しては↑で定義した IsSatisfied型を返すようにしてみました。
関数名同じで戻り値の型が違うのが微妙にいやらしいけれどとりあえずやっつけで¹¹。
54-55行目。規定回数ループ内で充足解が見つからなかった際の処理も少し変更。というかパターンマッチ case Unsatisfied(fs) で、「充足しないClauseのリスト（Seq）」がfsという変数に束縛されるので、そこから sample するだけでOK、ということ。例1では「（充足解でないなら）CNFから充足しないClauseをfilterしてそこからsample」という流れだったのをワンクッション減らしたわけです（と同時にここでもオブジェクト指向っぽさを1つ排除！）。

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

感想

個人的に JVM言語は少し避けて通ってきた過去があり、Scala も本当に最近になってまともに触り始めたのですが、言語としては面白いですね。パターンマッチもけっこう柔軟だし自分で case も定義できる（def unapply()）し。
仕事とは関係なく、道具として、純粋関数型プログラミングの一つの選択肢として、これからも付き合っていけそう。とりあえず Stream が使えるから、あれとかアレとかは近いうちに試すつもり。
ただ、欲を言うなら、コンパイルがもっと速いともっとうれしい……。

参考

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

Ruby版: https://gist.github.com/960956
JavaScript版: https://gist.github.com/966408
CoffeScript版: https://gist.github.com/1000913
R版: https://gist.github.com/2811277
Python版: https://gist.github.com/2818831
Haxe版: https://gist.github.com/4148331
Egison版: http://qiita.com/antimon2/items/c55a31a1bbd1f98360f0
Julia版: http://qiita.com/antimon2/items/96e3bd6e452e03cf98db
Elixir版: http://qiita.com/antimon2/items/d6b4a4ceb1b48549b32f

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

もう何度目かの序文コピペ。 ↩
というか周りみんな使ってるし社内ツールが Scala で実装されてたりするしなんか乗っておかないと置いてかれるっぽいので。。。 ↩
ちなみにこの勉強会の主催者が今会社で隣に座っています。 ↩
自宅の Scala 環境は scalaenv/sbtenv で構築。 ↩
FP in Scala 本の第6章で、状態をやりとりすることで副作用を伴わない純粋関数型の擬似乱数の話も出てきますが、まぁそれはそれとして。 ↩
なおコンパイル時に末尾再帰最適化が走るらしく、関数が末尾再帰になっているとコンパイル時にジャンプ（通常のループ？）に変換してくれる模様。その挙動自体は @annotation.tailrec とは無関係（なくても最適化は走る、ということ）らしいです。 ↩
この表現に何本かマサカリガ飛んできそうな気もしますがとりあえず様子見(^-^; ↩
先述の通り擬似乱数生成と IO は目をつぶってください。 ↩
個人の感想です。 ↩
Haskell の Maybe/Just/Nothing と考え方は同じ（モノとして同一とは言っていない）。 ↩
なおこの場合、関数名を同じままで戻り値を揃える（＝一方は def eval(c: Clause)(〜): IsSatisfied[Clause]、他方は def eval(c: CNF)(〜): IsSatisfied[CNF]）と、error: double definition: 〜 and 〜 have same type after erasure: (c: Seq, 〜) というようなエラーになってしまいます。implicit val を利用したり一方の引数を名前渡し（def eval(c: => CNF)〜）にしたり、といったHack を利用する必要があるみたいです（ちょとめんどくさい）。 ↩