うそつきのパズル その３ - 教えて！アロイ人！

論理パズル「出しっこ問題」傑作選　小野田 博一

今回は、本を変えて、といっても著者は変わっていないのですが「論理パズル「出しっこ問題」傑作選」からの問題をとりあげてみます。「史上最強の～」は、同じ系統の問題を沢山集め、難度がだんだん上がっていくような構成ですが、この「出しっこ問題」は、色々な系統の論理パズルを集めた、バラエティに富んだ本ととなって、単に読み物として読んでも楽しめます。

亜美の家

A,B,Cと一列に並んだ三軒家があり、そのうちの二つはそれぞれ亜美と佐助の家です。
「佐助の家はBではありません」と亜美が言いました。二人が隣り合って住んでいるのなら、この発言は真実、そうでないならウソです。亜美の家はどれ？
という問題です。

今回は趣向を変えて、この問題を題材にし、Alloy上でどのように作業をしていくかを見てもらうことにします。

パズルを記述していく作業

これまで解いてきたパズルの解を得るソースを見て、僕がそれを問題文を見ながらサクサクと書き、Enter一発で解を得たと考えているかも知れませんが、全くもってそんなことはありません。実際の作業は試行錯誤の連続なのです。Alloyのいいところは、この「試行錯誤に寛大」なところにあります。

開いたばかりのAlloy Analizerの画面は真っ白で何も入力されていません。ここにパズルの世界を入力していくわけですが、これまでに出てきたようなレベルのパズルでは、大体次のような流れで作業を進めることになります。

1. パズルのステージに登場するモノや人を定義と、どんな属性を持っているかを書く。
2. それらのモノや登場人物の間に成り立っていないといけない条件を書く。
3. 発言などの、最終的にパズルのネタとなっている中心的な条件を書く。

場や登場人物、属性の定義

今回のパズルでは、家が三軒（A,B,C）と、人物が二人（アミとサスケ）が出てきますので、まずそれを記述します。

abstract sig House {
  live : lone Name
}

enum Name {アミ, サスケ}
one sig A, B, C extends House {}

家には、0人か1人（lone）の人が住んでいて、家は3軒、人は二人定義できました。
で、この程度できたら、とりあえず動かしてみるのです。動かすにはrunの行が必要でしたら、

run {}

を加えて、画面上のExecuteボタンをクリックします。

すると、右側の領域に「Instance found ････」という表示が出るはずです。これは、この条件を満たす状態が見つかったということです。この状態でExecuteの隣にあるShowボタンをクリックしてみましょう。

こんな感じの図が表示されたかと思います。全く同じではないかもしれませんが。

この図を見ると、とりあえず家が３件、人が二人いるところまでは伝わっているようです。さらに上の「Next」をクリックすると、次の候補を表示してくれます。

どんどんクリックしていくと、色々な状態を表示してくれます。

ただ、家が全く独立していて、隣同士という概念がありませんし、一人の人が複数の家に住むことも容認されてしまっています。

関係の記述

このままでは困るので、家が隣同士ということはどういうことか、人が家に住むということはどういうことかをわかってもらえるような記述を追加していきます。
まずは、家の関係を追加しましょう。最初に書いたHouseの定義に少し追加して、

abstract sig House {
  live : lone Name,
  tonari : some House
}

とします。これで家の隣に家がある関係を表現できました。someというのは「1個以上」の関係を表していて、この場合家Bには隣家が二つ必要でしたから、lone（0か1）では表現できないため、登場したものです。あと、liveの行とtonariの行の境目にカンマが必要になりますので注意してください。
これでまた実行してみましょう。

こんな図が出てきました。誰も家に住んでないのはともかくとして、家の順番が変ですし、何より家Aの隣に家Aがあることになっています。こんな変なことにならないよう、制約を追加していきます。。

fact {
  tonari = ~tonari
  B in A.tonari
  C in B.tonari
  not A in C.tonari
  no a : House | a in a.tonari
}

1行目は、「隣という関係はお互い様」であること、つまり「家Aの隣が家B」なら、「家Bの隣が家A」も必ず成り立つ、ということを示す記述です。Alloyではとても重要な書き方なので抑えて置いてください。アインシュタインパズルにも出てきていました。
2行目と3行目は、Aの隣がB、Bの隣がCという、家の並びの順番を指定しているものです。in、というのは、ちょっと違和感があるかもしれませんが「部分集合」を表しています。tonariというのは１個以上の家の集まりですから、=で結ぶのではなく、「その中に含まれる（in）」と書く必要があります。
4行目は、「Cの隣はAでない」という制約です。これがないと、A,B,Cが三角形に並んでしまい、パズルの前提に合わなくなります。
最後の行は、「どの家も、自分の隣の集合の中に自分自身は入っていない」という制約です。

これで家がきれいに並んだはずです。実行してみましょう。

縦に並んでしまいましたが、きれいに並んでいるのでよしとしましょう。
他の例を見るためにNextをクリックしていくと、こんな図が出てきます。

サスケが２件の家に住んでいる上、アミが家なき子になっています。次はここに手をつけましょう。
先ほどのfactに、以下の2行を追加します。

all n : Name | n in House.live
no disj a, b : House | a.live = b.live

1行目は、「全ての人は、どこかの家に含まれる（Houseを全部並べて、そのliveの中身を全部取り出すと、どの名前もどこかに入っている）」という意味の記述です。これで家なき子がいなくなるはずです。
2行目は、「どの2件の家を見ても、その2件の住人が同じ人であるということはない」という制約です。

これを追加して実行すると、

というような、一つの家に一人入っていて、住んでない家が１件、という構成だけになります。
これで、パズルの大きな世界観を構築することができました。

ここまでやってから、パズルのことを考えます。

パズルのネタを記述する。

パズルの中心になる言葉は、
「佐助の家はBではありません」と亜美が言いました。二人が隣り合って住んでいるのなら、この発言は真実、そうでないならウソです。
でしたね。これを頑張って一息に書いたのが以下の記述です。

one disj a, b : House | (a.live = サスケ and b.live = アミ and b in a.tonari) <=> サスケ != B.live

ある２件の家a,bについて、aにサスケが住んでおり、bにアミが住んでいて、aとbが隣なら、サスケはBに住んでいない（隣同士ならウソ）。逆に、隣同士でないなら、サスケはBに住んでいるということなので、これは両含意で記述しています。

実行してみましょう。

さらにNextで、

が表示されます。もう一度Nextをクリックすると「もうない」と言われますので、該当するのはこの二つだけのようです。両方をよく見ると、どちらもアミは家Bに住んでいることになっていますので、これが答えとなります。

見栄えの調整

このAlloyの図は、まぁ言いたいことはわかるのですが、住んでいる人をわざわざ家と同じように四角で囲って表示するのも大げさですし、かえって分かりにくくなっているような気もします。調整してみましょう。

この画面で、「Theme」をクリックすると、左のほうに設定画面が出てきますので、左下のrelationsの「live」をクリックし、上の「Show As Arcs」を何度かクリックしてOffにしてやります。さらに、そ#image(ami12.gif)
の下の 「Show As Attribute」をクリックし、Onにしてやります。
さらに、中央付近の「sig Name」をクリックしてから、上の「Show」をまた何度かクリックして「Off」にしてやります。

最後に、図の上の「Close」をクリックすると、名前が属性として表示されるようになり、すっきりと見やすくなります。これ以前のパズルで出てきた図は、実はこうしてからキャプチャしていたのでした。

おわり

Alloyを前にした解までの道のりが分かっていただけたかと思います。全体的な流れとしては、まずモノとその数（決まっているなら）を定義します。そうすると、Alloyはそれらのものを勝手に配置したりつなげたりしますので、その図を見ながら、不都合な関係を切るべく、一つ一つ条件を追加しながら状態を追い込んでいき、「変な状態にはならないが、正常な範囲では自由な状態」にしてから、最後に問題文を与えて「正常な状態の中で、問題文の条件を満たす状態だけに絞り込む」というような作業になります。
前述した「史上最強の論理パズル」に載っている問題の多くは、このプロセスで解けるはずです。ぜひ本を買って自分で問題を選び、手を動かして取り組んでみてください。ここを読むだけでは決して得られない手ごたえを感じることができるでしょう。
なぜ「買って」とお願いしているのかというと、２問も引用してしまったので、これを読んだ人に買ってもらわないと著者に申し訳ないと感じてしまっているからです。ブルーバックスだからそう高くもないです。損はさせません。本当いうと、全部の問題に対応するAlloyソースをここに載せたいくらいです。それぐらい、「史上最強の論理パズル」は初歩の「Alloyの筋トレ」に向いた本です。

全ソース

abstract sig House {
  live : lone Name,
  tonari : some House
}

enum Name {アミ, サスケ}
one sig A, B, C extends House {}

fact {
  tonari = ~tonari
  B in A.tonari
  C in B.tonari
  not A in C.tonari
  no a : House | a in a.tonari
  all n : Name | n in House.live
  no disj a, b : House | a.live = b.live
}

fact {
  one disj a, b : House | (a.live = サスケ and b.live = アミ and b in a.tonari) <=> サスケ != B.live
}

run {}

（文責：片山 功士）

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