アインシュタインパズル - 教えて！アロイ人！

アインシュタイン式論理脳ドリル

まず最初に、本屋で見かけたこんなパズルに挑戦してみましょう。

問題をそのままコピーしてしまうと著作権的にアレなので、内容を変えています。

1. キツネを見たのははじめ
2. 白が好きなのは黒が好きな人の左隣
3. ライオンを見た人は右端
4. なつこは赤が好きな人の右隣
5. かづみはゆうこの隣
6. 緑が好きな人は真ん中
7. たくやは茶色が好きな人の二つ左
8. カメを見た人は黒が好き
9. ミズスマシを見た人はゆうこ

以上のヒントを元に、下のマトリクスを埋め、

	－左－	－－－	真ん中	－－－	－右－
名前
好きな色
見たもの

トラを見たのは誰でしょう、というような問題に答えることがパズルの目的になります。各マスには、上の文中の色がついた言葉が入ります。

というわけで、これを見て、どんなものをAlloyに入力すると、どんな出力が得られるのか、をとりあえず見てみましょう。

Alloyでどう書く？

abstract sig World {
  name : one Name,
  color : one Color,
  animal : one Animal,
  left : lone World,
  right : lone World
}

one sig LL, LC, CC, RC, RR extends World {}
enum Name {はじめ,なつこ,かづみ,たくや,ゆうこ}
enum Color {白,黒,赤,茶,緑}
enum Animal {キツネ,カメ,ミズスマシ,ライオン,トラ}

fact {
  all n : Name | n in World.name  
  all c : Color | c in World.color  
  all m : Animal | m in World.animal  
}

 fact {
  left = ~right
  RR.right = none
  RR in RC.right
  RC in CC.right
  CC in LC.right
  LC in LL.right
  LL.left = none
}

fact {
  -- rule 1
  one a : World | はじめ = a.name and キツネ = a.animal
  -- rule 2
  one disj a, b : World |  白 = a.color and 
                          黒 = b.color and
                          a = b.left
  -- rule 3
  one a : World | ライオン = a.animal and a.right = none
  -- rule 4
  one disj a, b : World | なつこ = a.name and 
                         赤 = b.color and
                         a = b.right
  
  -- rule 5
  one disj a, b : World | かづみ = a.name and
                         ゆうこ = b.name and
                         (a = b.left or b = a.left)
  -- rule 6
  one a : World | 緑 = a.color and
                 a.left.left.left = none and
                 a.right.right.right = none
  -- rule 7
  one disj a, b : World | たくや = a.name and
                         茶 = b.color and
                         a = b.left.left 
  -- rule 8
  one a : World | 黒 = a.color and カメ = a.animal
  -- rule 9
  one a : World | ゆうこ = a.name and ミズスマシ = a.animal
}

pred show() {}
run show

実行結果

上のプログラムを実行すると、以下のような解が提示されます。

これを見ると、トラを見たのが「たくや」だということがわかります。

意味分からないですよね

ふ～ん・・という感じでしょうか。

とにかくさっぱり意味が分からないと思うので、上のソースを１行ずつ説明していくことにしましょう。

パズル世界の記述１

まず最初に、このパズルが取り扱う世界がどんなものかを記述します。考えなくていいものは整理し、パズルの要素だけを抜き出します。

abstract sig World {
  name : one Name,
  color : one Color,
  animal : one Animal,
  left : lone World,
  right : lone World
}

ここでは、アインシュタインパズルの回答を構成する表を定義しています。この表にモノが埋まったものが、このパズルの世界の全てですので、ここから定義を始めます。

最初のabstractは（抽象的な）という英語で、この後で定義するものが、具体的なモノではないことを示しています。
次のsigは「signagure（シグネチャ）」の略で、「こんなものがありますから覚えてくださいね」と、Alloyにお願いする言葉です。
１行目の最後にあるのは、Worldとありますが、これが世界に僕が付けた名前です。大文字で始まる何かの単語であればなんでもかまいません。
このWorldは、上の表の縦の列１列分を表します。

その次に続くのが、このWorldが持っている属性の一覧です。

• nameは、Name（後で定義します）のうちのどれか一つ（one）です。
• colorは、Color（後で定義します）のうちのどれか一つ（one）です。
• animalは、Animal（後で定義します）のうちのどれか一つ（one）です。
• leftは、このWorldの左隣の他のWorldですが、もしかするとないかもしれません(lone）。
• rightは、このWorldの右隣の他のWorldですが、もしかするとないかもしれません(lone）。

これが、以下のように五つ並んだものが、このパズルの表となります。

one sig LL, LC, CC, RC, RR extends World {}

上の宣言は、LL,LC,CC,RC,RRという名前のWorldが、一つずつ存在するということを意味しています。今のところは「存在」だけが示されていて、並び順は決められていません（後で定義します）。
最初にWorldを宣言した際はabstracctを付けていましたが、今回は付けていません。ここで出た五つのものが、具体的に存在することが明らかになった最初のものです。

マス目に入るものの記述

次に、Worldの中に入るものを宣言します。先ほど（後で定義します）と書いたName、Color、Animalをここで宣言します。

enum Name {はじめ,なつこ,かづみ,たくや,ゆうこ}
enum Color {白,黒,赤,茶,緑}
enum Animal {キツネ,カメ,ミズスマシ,ライオン,トラ}

fact {
  all n : Name | n in World.name  
  all c : Color | c in World.color  
  all m : Animal | m in World.animal  
}

最初の行は、Nameというものは「はじめ、ななこ、かづみ、やくや、ゆうこ」のうちのどれかである、ということを示しています。
2行目、３行目も同様に、ColorとAnimalが何であるかを宣言しています。

次の「fact」は、それに続く括弧に入っているものが「絶対に曲げられない事実である」ということを示しています。
次の「all n : Name | n in World.name」という記述が一番なじみにくいように感じられるかもしれませんが、この行をそのまま日本語に表すならば、
「全ての名前は、Worldであるもの（LL,LC,CC,RC,RRのいずれか）のnameに含まれる。」
ということになります。名前もWorldも五つずつしかありませんから、こう書いてしまうと、この時点ではどれがどれに対応しているかは分からないけど、名前とWorldが１対１で対応することになります。
ColorとAnimalについても同様です。

世界の横方向の順序性を定義

次に、五つ定義した世界を横に１列に並べてやる必要があります。五つのものを左から「LL,LC,CC,RC,RR」と並べたいのです。そのための記述が以下のものです。

 fact {
  left = ~right
  RR.right = none
  RR = RC.right
  RC = CC.right
  CC = LC.right
  LC = LL.right
  LL.left = none
}

factは、先ほども出たように、この括弧の中が「ゆるぎない事実」であることを指しています。
中身の１行目「left = ~right」ですが、これは、Worldのleftとrightというのが、丁度逆になっている関係であることを宣言しています。つまり、RCのrightがRRなら、RRのleftは必ずRCである、という関係を示しています。
次に、RRの右には何もない、という記述が続きます（RR.right = none）。
そして、RR=RC.right、RC=CC.rightという風に、要素を次々と右につないでいきます。最後に、LLの左に何もないことを示せばこの作業は完了です。

お疲れ様でした。ここまでで、このパズルの世界観についての記述は終わりました。続いて、問題文をAlloyの言葉に翻訳していきます。

条件１

ソースの中に「--rule 1」とあるのは単なるコメントです。

• キツネを見たのははじめ

one a : World | はじめ = a.name and キツネ = a.animal

上の文を、Alloyに分かるように書いたものが下の記述です。
「マス目に入るものの記述」で見たのと少し似た表現ですが、これをあえて文にするなら

• あるWorld(これを仮にaとする）が必ず一つ存在して、そのaのnameは「はじめ」で、なおかつそのanimalは「キツネ」である。

という意味になります。aがどれかは分からないけど、どれかはこの条件を満たすと言っているのです。

条件２

• 白が好きなのは黒が好きな人の左隣

one disj a, b : World |  白 = a.color and 
                         黒 = b.color and
                         a = b.left

次は少しややこしいです。先ほどは一つのWorldの条件を示していましたが、今度は二つのWorldにまたがった条件を設定しています。

• 等しくない二つのWorld(これを仮にa, bとする）が必ず存在して、そのaのcolorは「白」で、なおかつbのcolorは「黒」で、しかもaはbの左である。

「等しくない」を表しているのが、「disj」です。

条件３

• ライオンを見た人は右端

one a : World | ライオン = a.animal and a.right = none

少し見慣れてきましたか？今度は

• あるWorld(これを仮にaとする）が必ず一つ存在して、そのaのanimalは「ライオン」で、なおかつその右には何もない（右端）。

という意味です。

条件４

• なつこは赤が好きな人の右隣

one disj a, b : World | なつこ = a.name and 
                         赤 = b.color and
                         a = b.right

条件２と同じですね。

条件５

• かづみはゆうこの隣

one disj a, b : World | かづみ = a.name and
                         ゆうこ = b.name and
                         (a = b.left or b = a.left)

「隣」という表現が出てきましたが、これはつまり、「aの右がbであるか、またはbの右がaである」という意味ですので、上のようにかけます。

条件６

• 緑が好きな人は真ん中

one a : World | 緑 = a.color and
                 a.left.left.left = none and
                 a.right.right.right = none

「真ん中」という条件はどう書けばいいのか・・・と迷った結果、「aの左の左の左は何もなく、かつaの右の右の右は何もない」としました。
これが真ん中を意味するのは分かりますね？

条件７

• たくやは茶色が好きな人の二つ左

one disj a, b : World | たくや = a.name and
                         茶 = b.color and
                         a = b.left.left 

二つ左、という条件をどう書くかは、ここまで読んできた人なら分かりますね？aはbの左の左です。

条件８

• カメを見た人は黒が好き

one a : World | 黒 = a.color and カメ = a.animal

条件１と同じですね。

条件９

• ミズスマシを見た人はゆうこ

  one a : World | ゆうこ = a.name and ミズスマシ = a.animal

これも条件１と同じですね。

おしまいに

pred show() {}
run show

最後についているこの２行は「以上を満たすもがどんなものなのか見せて！」という命令です。この前まではAlloyはずっと我々の話を聞いているだけでしたが、この２行を受け取ることで、答えを探し始めます。

これで完了！

どうでしたか？問題文をAlloyに分かるように翻訳する作業は、問題文の中にある論理を冷静に見つめて、それを厳格に書き起こしていくという作業になります。ちょっと大変かも知れませんが、Alloyにはもっとたくさんの文法があり、その表現力はここで上げたものよりもはるかに大きくて、ややこしいことを厳格に、しかも手短に表現する力を持っています。
こうして、問題文の世界と条件を入力してやれば、後はその条件を満たす世界がどんなものか、Alloyが探し出してきてくれます。複数見つかればそれらを順に見せてくれます。
見つからなければ「そんな条件を満たす状態は見つからなかった」と教えてくれますが、これには注意があります。これはあくまで「見つからなかった」だけであって「存在しない」「ありえない」ということを保証してているわけではないということです。ここだけは忘れないでください。

（文責：片山 功士）

今日： - 人
昨日： - 人
トータル： - 人