日々の流転

λ. 『笑わない数学者』のビリヤードの問題をAlloyで

先日、笑わない数学者―MATHEMATICAL GOODBYE (講談社文庫)(森 博嗣) の劇中に登場した5つのビリヤードの玉のパズルを Mathematical Goodbye. -笑わない数学者からの挑戦状- クイズ＆パズルの部屋「Quizzical Days.」 というところで見た知人に、解の一意性について聞かれた。

昔読んだときには、まじめに考えた気がするけど、また考えるのは面倒なので Alloy Analyzer に解かせてみることに。以下がAlloyで書いたモデル。

sig Ball {
   num : one Int,
   next : one Ball,
}

fact {
   all b : Ball | int 1 <= int b.num && int b.num <= int 15
   all b1 : Ball | all b2 : Ball {
      b1.num=b2.num implies b1=b2
      b2 in b1.^next
   }
   #Ball = 5
}

sig Cnt {
   ball : one Ball,
   val  : one Int,
   next : lone Cnt
}

fact {
   all c1 : Cnt {
      (no c2 : Cnt | c1=c2.next) implies c1.val = c1.ball.num
      all c2 : c1.next {
         c2.ball = c1.ball.next
         c2.val = int c1.val + int c2.ball.num
      }
      no c2 : c1.^next | c1.ball = c2.ball
   }
}

pred show() { }
run show for 5 Ball, 0 Cnt, 6 int

pred goal() {
   all n : Int |
      (int 1 <= int n && int n <= int 21) implies
         some c : Cnt | c.val=n
}
run goal for 5 Ball, 25 Cnt, 6 int

残念ながら解けなかったけどね。

なお、一意性の証明はぐぐればどこかで見つかるでしょう(投げやり

2009-03-01 追記

これを書いたときは Alloy の sum の構文について知らなかったので地道に足し算をしていたが、sumを使うようにしたら、ちゃんと解けた。あと、Alloyでパックマン - らくがきえんじんで「sig ... in ...」という構文について知ったので、それも使ってみている。

abstract sig Ball {
  num : one Int,
  next : one Ball
}
one sig B1, B2, B3, B4, B5 extends Ball {}
fact {
  all x : Ball | 1 <= x.num && x.num <= 15
  #(Ball.num) = 5
  next = B1->B2 + B2->B3 + B3->B4 + B4->B5 + B5->B1
}

pred connected[S : set Ball] {
  all x, y : S | y in x.*((next + ~next) & (S -> S))
}

sig s01, s02, s03, s04, s05, s06, s07, s08, s09, s10,
    s11, s12, s13, s14, s15, s16, s17, s18, s19, s20,
    s21 in Ball { }
fact {
  B1.num = 1
  connected[s01] && sum s01.num = 01
  connected[s02] && sum s02.num = 02
  connected[s03] && sum s03.num = 03
  connected[s04] && sum s04.num = 04
  connected[s05] && sum s05.num = 05
  connected[s06] && sum s06.num = 06
  connected[s07] && sum s07.num = 07
  connected[s08] && sum s08.num = 08
  connected[s09] && sum s09.num = 09
  connected[s10] && sum s10.num = 10
  connected[s11] && sum s11.num = 11
  connected[s12] && sum s12.num = 12
  connected[s13] && sum s13.num = 13
  connected[s14] && sum s14.num = 14
  connected[s15] && sum s15.num = 15
  connected[s16] && sum s16.num = 16
  connected[s17] && sum s17.num = 17
  connected[s18] && sum s18.num = 18
  connected[s19] && sum s19.num = 19
  connected[s20] && sum s20.num = 20
  connected[s21] && sum s21.num = 21
}

pred show { }
run show for 5 Ball, 6 int

実行結果

Executing "Run show for 6 int, 5 Ball"
   Solver=minisat(jni) Bitwidth=6 MaxSeq=4 Symmetry=20
   33024 vars. 430 primary vars. 114895 clauses. 365ms.
   Instance found. Predicate is consistent. 10741ms.

ここで、次の解を計算させると逆周りになった解が出てきて、さらにその次の解を計算させると今度は解無しになる。ので、解の一意性も確認できた。