Alloyで論理パズルを解いてみる その5

roller-coaster.als

//問題:
//男子4人(雅之、宗彦、その他２人w)、女子4人(玲奈、香織、舞、美紀)の8人
//でジェットコースターに乗ることになった。ジェットコースターは２人掛け
//4つからなり、それぞれの車には男子、女子それぞれ一人ずつ乗った。
//
// 1. 香織の隣は雅之ではなく、2つ後の車に宗彦が乗った
// 2. 雅之は美紀より後ろ(直後とは限らない)に乗り、舞は雅之の後ろ(直後
//    とは限らない)に乗った。
//
// 玲奈は何番目の車に乗った?
//
// 出典: 新作論理パズル77 小野田 博一
open util/ordering [車]

abstract sig 男子 {}
abstract sig 女子 {}

one sig 雅之, 宗彦, モブ, モブ' extends 男子 {}
one sig 玲奈, 香織, 舞,    美紀 extends 女子 {}

sig 車 {
   に乗っている男子: one 男子,
   に乗っている女子: one 女子
}

fact 一人が乗れるのは一台だけ {
   all m: 男子 | one に乗っている男子.m
   all f: 女子 | one に乗っている女子.f
}

fact 香織の隣は雅之ではなく2つ後の車に宗彦が乗った {
  {c: 車 | c.に乗っている女子 = 香織}.に乗っている男子 != 雅之
  {c: 車 | c.に乗っている女子 = 香織}.next.next.に乗っている男子 = 宗彦   
}

fact 雅之は美紀より後ろに乗り舞は雅之の後ろに乗った {
   one c: {c: 車 | c.に乗っている女子 = 美紀}.^next | c.に乗っている男子 = 雅之
   {c: 車 | c.に乗っている男子 = 雅之}.next.に乗っている女子 = 舞
}

pred show {}
run show for 4