Parabola Journal

[日記]制約充足問題についてのゆるふわな話

 
この記事はMachine Learning Advent Calendar 2012の12日目の記事として書いています.最初スカスカだった気がするのですが,いつの間にかガチ勢に囲まれてしまった気がして既に文章書くだけで怖いのですが,気のせいでしょうか.今日はゆるふわな話として制約充足問題についてやりますなぜMachine Learning Advent Calendarで書くのかというと本人も謎なのですが,当時は枠が開いていたので…

制約充足問題について

制約充足問題(CSP: Constraint Satisfaction Problem) [Wikipedia]とは,その名前の通り「こんな感じの条件1.,条件2.,…を全部満たしてくれることは可能ですか〜?」というような問いに関わる問題のことを言います.もうすぐ衆議院選挙がありますが,選挙の投票をするときに「政策1についてはこういう立場で〜,政策2についてこういう立場で〜.....を全部満たす議員さんが自分の選挙区にいるかな〜」みたいなことをぼんやり考えるようなことをやります.もう少し真面目な問題例としては,数独とかnクイーンとかがあります.

ミニ数独の例


  • どの行も数字が重複してはいけない
  • どの列も数字が重複してはいけない
  • どのブロックも数字が重複してはいけない

数独を解く



例えば,全部総当りしますもちろん普通に考えたらこんなこと当然しなくていいです.しかし4×4ぐらいならこれでも問題ないような雰囲気が少しだけありますが,こんな無茶なことしているといつかお姉さんみたいになってしまう気がします.


もちろん,普通に考えて無駄なことをしないようにバックトラックすればよいのです.



列方向を考えるとき,列方向に数値が重複してはいけないという制約を知っているので,バックトラックをしているとき,こんなことを考えています.



これを制約の数だけ行うと,そもそもチェックしなければならない数字というのがちゃんと少なくなるはずです.普通に数独を解いているときと同じことを,毎回やってあげればよいのですね.そうすれば最初みたいな無駄なことをしないでいいので,答えの探索が大分簡単になります.



真面目な制約充足問題の定義,解放の真面目な話を知りたい場合は,もちろん真面目な資料を読むのが良いです.制約充足問題自体は一般にはNP完全問題らしいですが,多くの場合で高速に解くことが可能らしいです.実際に高速に解いてもらうには,CSPソルバーというツールを使うのが一般的であります.

CSPソルバー: 制約充足問題を解くための道具

上で簡単なミニ数独を考えましたが,実際に制約充足問題を解く場合,自分でプログラムを書かなくても,便利なライブラリやツールがちゃんと公開されています.今回はCSPソルバー: Sugarを後ろで使いつつ,表面的にはScalaで書けるというおいしいライブラリであるCoprisを使ってみます.Scalaやってる人向けに言えば,必要なjarファイルを落としてきてsbtで管理するディレクトリのlibに入れておけばとりあえず使えます.以下のソースは基本的にCoprisのサンプルコードを借りてきました.

import jp.kobe_u.copris._
import jp.kobe_u.copris.dsl._

object MiniSudoku {
  def main(args: Array[String]) = {
    val puzzle = Seq(
      Seq(4, 0, 3, 0),
      Seq(0, 3, 0, 0),
      Seq(0, 0, 2, 0),
      Seq(0, 2, 0, 3))

    // ブロックの幅と数字の数		
    val (m, n) = (2, 4)
		
    // 4×4のマスでx(0,0)からx(3,3)までを整数値を取るべき変数として用意
    for (i <- 0 until n; j <- 0 until n)
      int('x(i, j), 1, n)

    // 行・列は全て異なる(Alldifferent)という条件を追加(add)する
    for (i <- 0 until n) add(Alldifferent((0 until n).map('x(i,_))))
    for (j <- 0 until n) add(Alldifferent((0 until n).map('x(_,j))))

    // ブロック内は全て異なるという条件を追加する
    for (i <- 0 until n by m; j <- 0 until n by m) {
      val xs = for (di <- 0 until m; dj <- 0 until m) yield 'x(i+di, j+dj)
      add(Alldifferent(xs))
    }

    // 既にpuzzleに埋まっている数値があればそれと一致(===)しなければならない
    for (i <- 0 until n; j <- 0 until n if puzzle(i)(j) > 0)
      add('x(i,j) === puzzle(i)(j))

    // 見つかったら出力
    if (find) {
      for (i <- 0 until n)
        println((0 until n).map( j => solution('x(i, j))).mkString(" "))
    }
  }
}		


[info] Running MiniSudoku
4 1 3 2                  
2 3 1 4                  
3 4 2 1                  
1 2 4 3 


中身はブラックボックス(確かSATの問題にしてる気がした)だとしても,自分の望む条件を書いてあげると,その答えを可能な限り頑張って求めてくれるというのは凄くいい話ですね.

宣言型と手続き型のはなし

制約充足問題を解いたときのように,普通に探索を考えていけば,その処理を手続き型で書くことは難しくない問題もたくさんあります.実際にC++やJavaでプログラムを書くわけですし,パラダイムはどうであれ手続き的に問題解決を目指します.

制約充足問題を手続き型で考える
  • 解空間を全列挙して進んでみる:アカン
  • 効率的な枝刈りを考える:制約の伝搬をする
  • ヒューリスティックを入れる:知らん
  • 諦める:この問題は実は解けない(解がない)!
しかし,ある程度,問題がしっかりと研究されていくと,その問題をメタ的に記述し,解いてくれるソルバーが開発されていく場合があります.こういった内部の細かいことを気にすることなく,もしくはそういったものに極力悩まされることなく

制約充足問題を宣言的に考える
  • 解の満たすべき性質である制約を記述してソルバーに投げる
という短いステップで問題が解けてしまうかもしれません.


機械学習/データマイニングは宣言型的な解決が出来るようになるだろうか 宣言型な考え方,どうせソルバーに投げるなら手続き型だ!っていうあら探しはやめろ!!!!

ようやくMachine Learning Advent Calendarの周辺まで戻って来れた気がします.最近研究されているようなされていないような(どれぐらいかは不明)話として,データマイニングや機械学習の問題は宣言的に書けるのだから,宣言的に解けたら嬉しいよね,というテーマがあります.近年の統計的かつ数学的に非常に高度化した(少なくとも僕の目からそう見える)話からすると,お前はいったい何を言っているんだ?と思われるかもしれませんが,

「あ〜○○くん,ビッグデータ用意したから何か使えそうな結果頼む」


みたいなことをもし言われたらどうでしょうか.こういう抽象的な問いでデータを持っている人がやりたいことって,まさに宣言型の手法が合っているのではないか効率的に解けるどうこうでいじめてはいけない!!!!!!あとそういう現実的な話でいじめるのよくない!!! と,そう思うのです.

  • あるお店での売上データを持ってきた,○日以上継続して売れていて,売上のピークが1年に4回あるような商品セットを知りたい
  • 損失関数を最小化するような,モデルのパラメータが欲しい

宣言っぽいと言えるような,言えないような….

まとめ

この記事では制約充足問題の基本的な話をしました.オマケで機械学習やデータマイニングで宣言的な解き方が出来るようになったら面白い,というよりもただ使うだけの人からするとわかりやすいよね〜という話を本当はちゃんとやろうとしたのですが思っていたより筆が進まず…やりました.今回は制約充足問題を基本的な部分で使いましたが,他にもSAT使ったり,もっと確率的な話をするためにベイジアンネットみたいなことをベースでやったり,まぁいろいろな人がいるんだなぁと思っていただいたら嬉しいなぁと思います.なお書いている人はこういう研究を一切していない模様.

記事を書くためにお世話になった土下座すべき参考文献一覧

コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です