Alloyでパズル (3) シマウマのパズル

5381 ワード
形式手法 AlloyAnalyzer どう書く どう書く テキストリンク

きのう Qiita でパズルを検索して出てきた [Prologで論理パズル] グリッドパズル；シマウマのパズル をやってみた。
やったと言っても、解き方を考えないので問題文を言い換えただけに近い。

問題

そのまま引用、長い。

家が5軒一列に並んで建っている。
5軒の家はそれぞれ違う色に塗られていて、住んでいる人はそれぞれ生まれた国、飼っているペット、飲み物、履物の種類が違う。

  • スコットランド人は赤い家に住んでいる。
  • ギリシャ人は犬を飼っている。
  • コーヒーを飲むのは緑色の家の人。
  • ボリビア人はお茶を飲む。
  • 緑色の家はクリーム色の家のすぐ右隣りにある。
  • 革靴を履いている人はカタツムリを飼っている。
  • 厚底靴を履くのは黄色の家の人。
  • 牛乳を飲むのは真ん中の家の人。
  • デンマーク人は左端の家に住んでいる。
  • 革サンダルを履いている人は、キツネを飼っている人の隣の家に住んでいる。
  • 厚底靴を履いている人はの家は、ウマを飼っている家の隣。
  • スリッパを履いている人はオレンジジュースを飲む。
  • 日本人はビーチサンダルを履いている。
  • デンマーク人は青い家の隣に住んでいる。

さて、水を飲むのは誰？また、シマウマを飼っているのは誰？

リスト

Alloy の場合は、問題をなるべく素直に記述するだけで終わりなのであまり難しいところはない。
日本語で書かれた問題文をどのくらい違和感なく記述できるかに注目してほしいくらい。
「家が５軒一列に並んで建っている」の表現は少々特殊だが、読むぶんには問題ないだろう。
（House1の右はHouse2、House2の右はHouse3、.. と１文で書いている）
enum の値は参照先のものをそのまま拝借した。

puzzle3.als
// シマウマのパズル
// https://qiita.com/Soichir0/items/daa0b9df8a2500ae0a04

// 家が5軒一列に並んで建っている
// 5軒の家はそれぞれ違う色に塗られていて、住んでいる人はそれぞれ生まれた国、
// 飼っているペット、飲み物、履物の種類が違う
enum Color {Blue, Green, Red, Yellow, Cream}
enum Nationality {Denmark, Japanese, Bolivian, Scottish, Greece}
enum Pet {Snails, Dog, Horse, Fox, Zebra}
enum Drink {Tea, Orange, Milk, Coffee, Water}
enum Footwear {Leather, Slipper, LeatherS, BeachS, Platform}

abstract sig House {
    color: disj Color,                      // それぞれの色は違う
    left,right: lone House                  // 左右にはたかだか１軒の家がある
}
one sig House1,House2,House3,House4,House5 extends House {}
fact 家は一列に並ぶ {
    right = House1->House2 + House2->House3 + House3->House4 + House4->House5
    left = ~right       // 左は右の反対
}

sig Person {
    house: disj House,                      // それぞれ別の家に住んでいる
    nationality: disj Nationality,          // それぞれの国籍は違う
    pet: disj Pet,                          // それぞれのペットは違う
    drink: disj Drink,                      // それぞれの飲み物は違う
    footwear: disj Footwear                 // それぞれの履物は違う
}

fact {
    nationality.Scottish.house.color = Red  // スコットランド人は赤い家に住んでいる
    nationality.Greece.pet = Dog            // ギリシャ人は犬を飼っている
    drink.Coffee.house.color = Green        // コーヒーを飲むのは緑色の家の人
    nationality.Bolivian.drink = Tea        // ボリビア人はお茶を飲む
    color.Green = color.Cream.right         // 緑色の家はクリーム色の家のすぐ右隣りにある
    footwear.Leather.pet = Snails           // 革靴を履いている人はカタツムリを飼っている
    footwear.Platform.house.color = Yellow  // 厚底靴を履くのは黄色の家の人
    drink.Milk.house = House3               // 牛乳を飲むのは真ん中の家の人
    nationality.Denmark.house.left = none   // デンマーク人は左端の家に住んでいる
    // 革サンダルを履いている人は、キツネを飼っている人の隣の家に住んでいる
    footwear.LeatherS.house in pet.Fox.house.(left+right)
    // 厚底靴を履いている人はの家は、ウマを飼っている家の隣
    footwear.Platform.house in pet.Horse.house.(left+right)
    footwear.Slipper.drink = Orange         // スリッパを履いている人はオレンジジュースを飲む
    nationality.Japanese.footwear = BeachS  // 日本人はビーチサンダルを履いている
    // デンマーク人は青い家の隣に住んでいる
    nationality.Denmark.house in color.Blue.(left+right)
}
// 問題：水を飲むのは誰？ シマウマを飼っているのは誰？

run {} for exactly 5 Person

「〜は」の位置に=を移動してnationality.Scottish = house.color.Redとしても大丈夫。
見た通り、家の色を比較するか人を比較するかの違いになる。
「真ん中の家」は「３軒左にも３軒右にも家がない」とも書けるが、長いので単に House3 とした。

結果

水を飲むのはデンマーク人、シマウマを飼っているのは日本人だった。
Evaluator でdrink.Water,pet.Zebraなどと打ってそれが何を示すか確認することもできる。
特定のPersonからpetやdrinkを引くだけでなく、逆にpet.Dogやdrink.WaterからPersonを引けるのが面白いところ。
　　

解説：わかった気になるドット結合

どうやってdrink.Water.nationalityはDenmarkにたどり着くのか、Evaluator で出た各段階を切り貼りで解説を。
まずdrinkは、Person->Drinkの一覧を意味する（sig Person {drink: Drink}より）
ドット結合では左辺と右辺の共通行をつなぎ、当てた列自体は消す。
そのためdrink.Waterの時点で左辺Waterの行から最右列を消したPerson$0だけが残る。
そこへ右からnationalityを当てると、右辺Person$0行の最左列が消えたDenmarkが残る。
　　
ついでに、２項関係の場合は~で列反転できるので、(~nationality).drinkで国籍別飲み物一覧が得られる。
　　
なお、ドットに接する左右の列が異なる型だった場合、共通する行がないため単に空集合となる。
だいたいこのくらいの理解でよろしいかと。
結果、逆引きだからと言ってコストが高いということはない。

参考