帽子の色あてパズルを Alloy で解く

どこが元ネタなのかよくわかりませんが、数日前に帽子の色をあてるゲームで誰が回答できるか、というパズルが流行ってたようですね。確かこんな問題でした。

白か黒の帽子をかぶった A, B, C, D の4人の子供が並んでいる。
A と B, C, D の間には仕切りがあり互いに見えない。B, C, D はこの順に並んでおり C は B が、D は B と C が見える。
全員は帽子が白黒合計2つずつであることと、お互いの位置関係は知っている。
A と C が黒、B と D が白の帽子をかぶっている時、最初に自分の帽子の色を答えられるのは誰か。

いやまあ答は C なんですが、今 Alloy という形式手法の言語を勉強していまして、これはどうやらパズルを解くのにはもってこいのツールであるようですので練習がてらこのパズルを Alloy を使って解いてみようと思った次第です。

まず最初にそれぞれが自分の直接見えている子の帽子の色をみて自分の帽子の色を言いあてることができるか(というか、できないこと)を証明するモデルを書きました。
https://gist.github.com/1743472#file_puzzle_1.alloy

enum Cap { Black, White }

abstract sig Children {
  cap:    one Cap,
  visible: set Children
  }

one sig A extends Children {} {
  visible = none
  cap = Black
  }
one sig B extends Children {} {
  visible = none
  cap = White
  }
one sig C extends Children {} {
  visible = B
  cap = Black
  }
one sig D extends Children {} {
  visible = B + C
  cap = White
  }

fact {
  #cap.Black = 2 and #cap.White = 2
  }

pred CanAnswer(c: Children) {
  #(c.visible :>cap.Black) = 2 or #(c.visible :> cap.White) = 2
  }

run {
  no c: Children | CanAnswer [c]
}

見えてる範囲に白か黒の帽子が2つあればあとは反対の色の帽子しかありえないから回答できる、というのをがちがちに書いたのが CanAnswer という述語です。でも A, B, C, D の誰もそれを満たさないので、これだけだと誰も回答できないことになります。
つまり「誰もすぐには回答できない」ということと、お互いの可視関係の知識をヒントとして利用しないといけないわけなので、そういうルールを追加してやらないといけません。というわけで小一時間ほどうーんと唸って書いたのがこちらです。

https://gist.github.com/1743472#file_puzzle_2.alloy

// 帽子の色
enum Cap { Black, White }

abstract sig Children {
  cap:    one Cap,        // かぶっている帽子の色
  visible: set Children   // 見える他の子供
  }

// A, B, C, D の条件
one sig A extends Children {} {
  visible = none
  cap = Black
  }
one sig B extends Children {} {
  visible = none
  cap = White
  }
one sig C extends Children {} {
  visible = B
  cap = Black
  }
one sig D extends Children {} {
  visible = B + C
  cap = White
  }

fact {
  #cap.Black = 2 and #cap.White = 2
  }

// c の帽子の色の合計のいずれかが num なら真
pred CountCapNumber (c: Children, num: Int) {
  #c :> cap.Black = num or #c :> cap.White = num
  }

// 前をみた瞬間に答えられるか
pred すぐに回答できる (c: Children) {
  CountCapNumber [c.visible, 2]
  }

// 他の子の回答(ができないこと)を待って答えられるか
pred 少しして回答できる (c: Children) {
  // すぐに回答する子はいない
  no a: Children | すぐに回答できる [a]
  // 答えられない誰かが自分を見ているなら、共通して見える子の帽子の色が
  // 1=(2-1)なら回答できる
  some a: Children | c in a.visible and CountCapNumber [c.visible & a.visible, 1]
  }

pred 回答できる {
  some c: Children |
    すぐに回答できる [c] or 少しして回答できる [c]
  }

run 回答できる

なんか急に述語に日本語を使っていますが、途中で日本語をつかってもいい & 使ったほうが結果が見やすいことに気がついたので方針を変更してます。
「少しして回答できる」という述語に誰もすぐに回答できない場合にそれをヒントとして回答できる条件を記述しています。これを使ってモデル図を表示させるとこうなります。

やったね、C が回答できるってわかったよ。
……なんかちょっと虚しいですね。正直「少しして回答できる」の条件は ad hoc すぎるというか、そこまでわかってたらもう問題解けてるだろという気がしないでもないので、もうちょっと関係式に基づいた書き方ができるといいかなと思うのですが、わたしの今の Alloy 力ではかないませんでした。
でもですね、この A, B, C, D のシグネチャの制約の cap の色を割り当ててるところをコメントアウトすると、任意の帽子の色の組み合わせの時に誰が最初に回答できるかというのが列挙できるんですよ。たとえばこんな結果が得られます。

うん、C か D だってことは知ってた……。

もうちょっと先に進めるとすると、たとえば最初の帽子の色の組み合わせだと C が回答した瞬間に今度は B が自分の帽子の色を推定できるんですよね。では D が(すぐに)回答できた場合は何が起きるのか? などというのをモデリングしようと思うと、もっと根本的にモデルの書き方を変更しないといけないような気がしています。よくわかっていないのですが Alloy は 1階論理しか扱えないので、こういう他の人の回答がそのまま知識になるという問題をモデリングしようとすると工夫が必要なのだと思います。誰か Alloy エキスパートが現われてずばっと解いてくれないかなぁ。