管理メニュー

教えて！アロイ人！

リニアな状態遷移を持つパズル２

最終更新：

pleasealloy

- view
メンバー限定 登録/ログイン

危ない家族

今日、「論理パズル」というキーワードでネットサーフィン（死語？）をしていたら、面白い問題を見つけました。「危ない家族」という、前回とりあげた「川渡り」パズルの一種なのですが、宣教師のものより凝っていることと、何よりAlloyのモデルの再利用性の高さを示すために取り上げてみることにしました。


ある家族がいます。
この家族は舟を使って川の向こう岸へわたろうとしています。
舟は１艘(そう)しかなく、１度に２人まで乗ることができます。
家族は父、母、息子１、息子２、娘１、
娘２、メイド、犬の８人(犬も１人と数えます)であり、
またこの舟をこげるのは父か母かメイドの３人だけです。

さぁ、そしてこの家族、ぢつは！とっても危険な家族なんです。
まず父は、母がいないと娘を殺してしまいます。
また母は、父がいないと息子を殺してしまいます。
そしてきわめつけ。
犬は、メイドがいないと家族をみんな殺してしまいます。

誰も死ぬことなく川をわたりきるにはどうすればよいでしょうか？


宣教師の問題と違うところ

問題全体の構成は宣教師の問題とほぼ同一で、ソースのほとんどが流用できます。違うところと言えば、
  1. 登場人物の種類と数が多い
  2. 「安全」の条件がだいぶ違う
  3. ボートに乗れる人が限られている
ことぐらいですので、これに着目して書き換えていくことにしましょう。

まず、登場人物は、以下の6種8人です。 

one sig 父,母,メイド,犬 extends Person {}
sig 息子,娘 extends Person {}

fact {
  #息子 = 2
  #娘 = 2
}
この際、犬も「Person」です。

安全条件は、以下のようになります。 
pred 安全 [group : set Person] {
  all d : 娘 | (父 in group && d in group) => 母 in group
  all s : 息子 | (母 in group && s in group) => 父 in group
  (犬 in group => メイド in group) || (犬 = group)
}
  • 全ての娘について、父と一緒なら、母もいなければならない。
  • 全ての息子について、母と一緒なら、父もいなければならない。
  • 犬がいるならメイドもいなければならない。ただし犬しかいない場合は問題ない。
というようなものです。

最後に、ボートを漕げる人の条件を追加して完了です。 
pred 川を渡る [移動元, 移動先, 移動元', 移動先' : set Person] {
  (one a : Person |
    a in 移動元 &&
    a in (父 + 母 + メイド) &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a) ||
  (some disj a, b : Person |
    (a + b) in 移動元 &&
    (a in (父 + 母 + メイド) || b in (父 + 母 + メイド)) &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b))
}

一人でわたる場合、父か母かメイドでなければならない。（その一人は、父と母とメイドを合わせた集合の中にいなければならない）。
二人で渡る場合は、aかbが父か母かメイドでなければならない。
という条件を追加しました。
runで実行しましょう。forの後の要素の数と、状態の数を増やしておかなければなりません。 
run { last.あっち = Person } for 8 but 18 状態

実行結果

実行した結果、17手で解が見つかりました。Webで公開されているものと同じようです。ここまでたどり着くのに、ものの数分でした。実行時間も数秒です。一度「川渡り」の構成が出来てしまうと、ほとんど変更なく別の川渡りに対応できるのが強みです。

もっと危ない家族


このパズルには続編が公開されています。これもやってみましょう。
追加される条件は、
  • じっちゃんと赤ん坊登場
  • じっちゃんは親がいないと子供を殺してしまう
  • 息子と娘は、親がいないとあかちゃんを殺してしまう
なんとも大変な事態ですが、やってみましょう。

人の定義

人の種類が入り組んできたので、abstractのsigを追加して整理しました。 
abstract sig Person {}
abstract sig Child extends Person {}
abstract sig Parent extends Person {}

one sig 父,母 extends Parent {}
one sig メイド,犬,じっちゃん extends Person {}
one sig 赤ん坊 extends Child {}
sig 息子,娘 extends Child {}

「安全」の条件に追加するのは以下の2行です。 
all c : Child | some p : Parent | (じっちゃん in group && c in group) => p in group
all c : Child | some p : Parent | (赤ん坊 in group && c in group) => p in group
  • じっちゃんがと子供のどれかがいる場合は親もいなければならない。
  • 赤ん坊と子供のどれかがいる場合は親もいなければならない。
じっちゃんと赤ん坊は実は同じ条件なのですね。
あとは、川を渡れる人にじっちゃんを加えて完成です。 

a in (父 + 母 + メイド + じっちゃん) &&


(a in (父 + 母 + メイド + じっちゃん) || b in (父 + 母 + メイド + じっちゃん)) &&

実行してみましょう。 
run { last.あっち = Person } for 10 but 22 状態

実行結果

あえて掲載しませんが、21手でゴールとなるようです。ここまでもほんの数分です。

そして伝説へ・・・・

これほどまでに簡単に「川渡り」が解けるとなると、新しい問題を作りたくなってきます。コンピュータがなければ、新しい人物や条件を加えて、果たして解があるのか、何手が最短なのか、別解はないのかを確かめる作業を考えると気が遠くなりそうですが、Alloyを使うと試行錯誤にほとんど頭を使いません。

ばっちゃん登場

というわけで、次のような条件を加えてみました。
  1. ばっちゃんを加える
  2. ばっちゃんはじっちゃんと同じ危険（子供と一緒の場合親もいないといけない）
  3. ばっちゃんは、自分ではボートを漕げないが、じっちゃんと二人で乗るのだけは嫌（何があったの？）
というものです。

修正

修正には上の条件に対応する3行を修正、追加するだけです。
まずは人の定義に追加。 
one sig メイド,犬,じっちゃん,ばっちゃん extends Person {}
安全条件に追加。 
all c : Child | some p : Parent | (ばっちゃん in group && c in group) => p in group
川を渡る条件を追加。 
not ((a + b) = (じっちゃん + ばっちゃん)) &&

あとはrunの行をちょこっと変えて実行するだけです。 
run { last.あっち = Person } for 11 but 26 状態

実行結果

26より少ない状態では解が見つからなかったので、初期状態を除いた25手が最短解のようです。これを手で調べることを考えるとゾッとします。

結論

Alloyは、パズルを解くだけではなく、作成する際にも非常な武器になることが分かりました。もちろん、昨今のパズル作家は何らかの形でコンピュータを使って別解がないことなどを確認しているとは思いますが、Alloyはもしかすると今まで使っていたどんなツールよりも簡単かもしれません。

全ソース

危ない家族

open util/ordering[状態] as ord

abstract sig Person {}

one sig 父,母,メイド,犬 extends Person {}
sig 息子,娘 extends Person {}

fact {
  #息子 = 2
  #娘 = 2
}

sig 状態 {
  こっち: set Person,
  あっち: set Person,
  ボート : one Place  
}

enum Place {こっちにある, あっちにある}

fact {
  first.こっち = Person && no first.あっち
  first.ボート = こっちにある
  all s : 状態 | 安全[s.こっち] && 安全[s.あっち]
}

pred 安全 [group : set Person] {
  all d : 娘 | (父 in group && d in group) => 母 in group
  all s : 息子 | (母 in group && s in group) => 父 in group
  (犬 in group => メイド in group) || (犬 = group)
}

pred 川を渡る [移動元, 移動先, 移動元', 移動先' : set Person] {
  (one a : Person |
    a in 移動元 &&
    a in (父 + 母 + メイド) &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a) ||
  (some disj a, b : Person |
    (a + b) in 移動元 &&
    (a in (父 + 母 + メイド) || b in (父 + 母 + メイド)) &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b))
}

 fact 状態遷移 {
  all 今 : 状態, 次 : 今.next {
     今.ボート = こっちにある =>
        川を渡る [今.こっち, 今.あっち, 次.こっち, 次.あっち]
    else
       川を渡る [今.あっち, 今.こっち, 次.あっち, 次.こっち]
    今.ボート != 次.ボート
  }
}

run { last.あっち = Person } for 8 but 18 状態

もっと危ない家族

open util/ordering[状態] as ord

abstract sig Person {}
abstract sig Child extends Person {}
abstract sig Parent extends Person {}

one sig 父,母 extends Parent {}
one sig メイド,犬,じっちゃん extends Person {}
one sig 赤ん坊 extends Child {}
sig 息子,娘 extends Child {}

fact {
  #息子 = 2
  #娘 = 2
}

sig 状態 {
  こっち: set Person,
  あっち: set Person,
  ボート : one Place  
}

enum Place {こっちにある, あっちにある}

fact {
  first.こっち = Person && no first.あっち
  first.ボート = こっちにある
  all s : 状態 | 安全[s.こっち] && 安全[s.あっち]
}

pred 安全 [group : set Person] {
  all d : 娘 | (父 in group && d in group) => 母 in group
  all s : 息子 | (母 in group && s in group) => 父 in group
  (犬 in group => メイド in group) || (犬 = group)
  all c : Child | some p : Parent | (じっちゃん in group && c in group) => p in group
  all c : Child | some p : Parent | (赤ん坊 in group && c in group) => p in group
}

pred 川を渡る [移動元, 移動先, 移動元', 移動先' : set Person] {
  (one a : Person |
    a in 移動元 &&
    a in (父 + 母 + メイド + じっちゃん) &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a) ||
  (some disj a, b : Person |
    (a + b) in 移動元 &&
    (a in (父 + 母 + メイド + じっちゃん) || b in (父 + 母 + メイド + じっちゃん)) &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b))
}

fact 状態遷移 {
  all 今 : 状態, 次 : 今.next {
    今.ボート = こっちにある =>
        川を渡る [今.こっち, 今.あっち, 次.こっち, 次.あっち]
    else
        川を渡る [今.あっち, 今.こっち, 次.あっち, 次.こっち]
    今.ボート != 次.ボート
  }
}

run { last.あっち = Person } for 10 but 22 状態

もっともっと危ない家族

open util/ordering[状態] as ord

abstract sig Person {}
abstract sig Child extends Person {}
abstract sig Parent extends Person {}

one sig 父,母 extends Parent {}
one sig メイド,犬,じっちゃん,ばっちゃん extends Person {}
one sig 赤ん坊 extends Child {}
sig 息子,娘 extends Child {}

fact {
  #息子 = 2
  #娘 = 2
}

sig 状態 {
  こっち: set Person,
  あっち: set Person,
  ボート : one Place  
}

enum Place {こっちにある, あっちにある}

fact {
  first.こっち = Person && no first.あっち
  first.ボート = こっちにある
  all s : 状態 | 安全[s.こっち] && 安全[s.あっち]
}

pred 安全 [group : set Person] {
  all d : 娘 | (父 in group && d in group) => 母 in group
  all s : 息子 | (母 in group && s in group) => 父 in group
  (犬 in group => メイド in group) || (犬 = group)
  all c : Child | some p : Parent | (じっちゃん in group && c in group) => p in group
  all c : Child | some p : Parent | (ばっちゃん in group && c in group) => p in group
  all c : Child | some p : Parent | (赤ん坊 in group && c in group) => p in group
}

pred 川を渡る [移動元, 移動先, 移動元', 移動先' : set Person] {
  (one a : Person |
    a in 移動元 &&
    a in (父 + 母 + メイド + じっちゃん) &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a) ||
  (some disj a, b : Person |
    (a + b) in 移動元 &&
    (a in (父 + 母 + メイド + じっちゃん) || b in (父 + 母 + メイド + じっちゃん)) &&
    not ((a + b) = (じっちゃん + ばっちゃん)) &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b))
}

fact 状態遷移 {
  all 今 : 状態, 次 : 今.next {
    今.ボート = こっちにある =>
        川を渡る [今.こっち, 今.あっち, 次.こっち, 次.あっち]
    else
        川を渡る [今.あっち, 今.こっち, 次.あっち, 次.こっち]
    今.ボート != 次.ボート
  }
}

run { last.あっち = Person } for 11 but 26 状態

（文責：片山 功士）


今日： - 人
昨日： - 人
トータル： - 人
「リニアな状態遷移を持つパズル２」をウィキ内検索
最近更新されたページ
もっと見る
ウィキ募集バナー