五角ミノ十二面体

英語でquintominal dodecahedraというクイズである. 十二面体のクイズといえば, Hamilton順路が有名だが, これは全然別だ. 今年4月に新型コロナで死去したJohn Conwayが1958年頃考えたらしい.

Conway他の書いた"Winning Ways Vol.4"の表紙に下のような興味ある図があった.


正五角形の5辺を5色(例えば赤青橙緑黒)で塗ると, 回転, 裏返しは同じと見た時, 12通りの五角形が得られる. (5!/5/2=12) 図の下にある12の五角形だ. この一組をquintomino(「五角ミノ」と訳すのは如何?)という. 一方, 正十二面体は12の正五角形か構成されるから, 辺が同じ色になるように, 各面に五角ミノを1枚づつ貼れるかというのが問題である.

Winning Waysの表紙は, 12の五角ミノにIを除いてAからMまで名をつけ, 解答を描いたものである. 各五角ミノの色の配置は以下の通り.

A=01234 B=01243 C=01324 D=01342 E=01423 F=01432
G=02134 H=02143 J=02314 K=02413 L=03124 M=03214

答をいうとこれは可能であり, 等価性を考慮すると3通りの解があるという. 表紙の3つの絵はAを底面にしたその3通りを示している.

KnuthのTAOCP, 第4巻, 第5分冊はDancing Linksが話題で, 膨大な数の演習問題があるが, その中にquintominal dodecahedron問題を解けというのがあった(ex 7221-136)ので, 挑戦してみたというのが今回のブログである.

正十二面体は下左のようなもので, こういう立体の絵では扱いにくいから, 通常は下右のような形相図(高木貞治 数学小景)を使う. 数学小景には正十二面体を床に置き, 上面の正五角形の少し上の光源で照すと, こういう影ができると書いてある.


正十二面体には, 頂点(青)と辺(赤)と面(緑)に番号を付けたが, 同じ番号を面0を底にした形相図に付けると下のようになる. 右端は面にも番号を付けたものだ. 0番の面がないのは, それは周囲の大きい五角だからだ.


ペントミノのとか8クィーンのような, ピースを置けるかどうかの問題は, 現在置いてあるピースの状態と, これから置くピースの集合を引数として受取り, あるピースがさらに置けるなら, その状態と今残るピースを新しい引数にして自分を再帰呼出しする関数を書くと解けるのが普通である.

以下のSchemeのプログラムもその方針で出来ている. colorsは12の五角ミノのリスト. facesは各々の面を作る辺の番号のリストである. allcsは色のリストを回転したり裏返したりしたもののリストを作る.

(define colors '
((0 1 2 3 4)(0 1 2 4 3)(0 1 3 2 4)(0 1 3 4 2)(0 1 4 2 3)
 (0 1 4 3 2)(0 2 1 3 4)(0 2 1 4 3)(0 2 3 1 4)(0 2 4 1 3)
 (0 3 1 2 4)(0 3 2 1 4)))
(define faces '
 ((0 1 2 3 4)(0 5 6 7 8)(1 9 10 11 5)(2 12 13 14 9)(3 15 16 17 12)
  (4 8 18 19 15)(7 20 21 22 18)(6 11 23 24 20)(10 14 25 26 23)
  (13 17 27 28 25)(16 19 22 29 27)(21 24 26 28 29)))
(define (allcs cs)
 (let ((ccs '()))
  (do ((i 0 (+ i 1))) ((= i 5))
   (set! ccs (cons cs ccs))
   (set! cs (append (cdr cs) (list (car cs)))))
  (set! cs (reverse cs))
  (do ((i 0 (+ i 1))) ((= i 5) (reverse ccs))
   (set! ccs (cons cs ccs))
   (set! cs (append (cdr cs) (list (car cs)))))))  

状態stateは辺の番号順の30の色のリストで, 先頭には最初の五角ミノAを固定し, 未定の25の場所は()にする. 数のリストである状態を数字列に変換したり, 逆に変換したりするのがcompressとexpandである.

(define (compress col)
  (list->string (map (lambda (n) (integer->char (+ n 48))) col)))
(define (expand col)
  (map (lambda (n) (- (char->integer n) 48)) (string->list col)))
(define state (append '(0 1 2 3 4) (make-list 25 '())))

次のtryが再帰呼出しの関数で, 状態stateと残りの五角ミノrestを受け取る. matchはその状態でposの場所がcolの色と一致しているか()かであれば真を返す. 要するに置けるということである. fillcはposの場所をcolの色にした新しい状態を返す. 新しい状態は再帰呼出しから戻るときに捨てるから, 置いたピースを戻す仕事はしない.

ifから後がtryの本体で, 残りの五角ミノがなければ((length(rest))=0なら)解があったとして出力する. 五角ミノの1個をとってcolとし, 残りをnewrestにし, 今度置く面をposにし, colを回転, 反転してcolsにし, そのそれぞれcについて置けるようなら再帰呼び出しする.

(define count 0)
(define (try state rest)
 (define (match state col pos)
  (every (lambda (c p) (let ((d (list-ref state p)))
   (or (null? d) (= d c)))) col pos))
 (define (fillc state col pos)
  (let ((newstate (list-copy state)))
   (for-each (lambda (c p)
    (list-set! newstate p c)) col pos) newstate))
 (if (= (length rest) 0)
  (begin (display (compress state)) (newline)
   (set! count (+ count 1)))
  (for-each (lambda (n)
   (let* ((col (list-ref colors n))
     (newrest (delete n rest)) 
     (pos (list-ref faces (- 12 (length rest))))
     (cols (allcs col)))
    (for-each (lambda (c)
     (if (match state c pos)    
      (try (fillc state c pos) newrest))) cols))) rest)))

Aが置いてあるので0を除き, restを(1 2 ... 11)としてtryを呼ぶと60個数の解が次のように得られる.

(newline)
(try state (range 1 12))
(display count)

"012343421042143042321400312301"
"012343421402013214300141324302"
"012343421420130204031343214201"
"012344231023134204031240413201"
"012344231320410012234101334402"
"012342431340401201031242330241"
"012342431430031214031242304210"
"012342431430130240031422341120"
"012342431430130204032141324102"
"012342431430130024231042314021"
"012342431403103204031242014231"
"012343241024134042321203001143"
"012343241024143240301020314321"
"012343241024143042320211304310"
"012343241024143042233010114032"
"012343241024413012321200341304"
"012343241420103042321204310341"
"012342341034431021231300224401"
"012342341340140042321202413301"
"012342341430130204032314112204"
"012342341304041241300212134203"
"012344312032431021314200124403"
"012344312320410102034321234401"
"012344312302014124300241423301"
"012342143034134240100232310241"
"012342143340041241102033402231"
"012342143304401012120232334410"
"012342143304014214100232331204"
"012342143304041241013122034023"
"012342143304041241100323224301"
"012342143304041142200132334102"
"012342143403031241100232443201"
"012343412042413120300241320341"
"012343412402103024310241324310"
"012343412402013142300421342301"
"012343412402013124033241024031"
"012343412402031124300243124103"
"012343412420013124302041304321"
"012344132032431012134020342014"
"012344132032431120034210324410"
"012344132032431021130244320041"
"012344132032134024134200321104"
"012344132023431021132404003421"
"012344132302401021134203024431"
"012342413340410102022431332401"
"012342413430130204013242114203"
"012342413403013124200341224301"
"012343142042431021133200423401"
"012343142024143042312100314302"
"012343142402013124300214321304"
"012344213023413102024231004431"
"012344213320401102024233140134"
"012344213320410102023241443301"
"012344213320410120204031334421"
"012344213320014142024231330041"
"012344213320140240014231334210"
"012344123032431201014130324402"
"012344123023143042124300214301"
"012344123320410102023414231403"
"012344123302041241100434332201"

後ではこの文字列のリストをallsolsとして使う.

ところで, Conwayの解は3通りであった. 上の60個の中には, 色の置換えについて等価のものが沢山あるということだ. 次に等価を発見する作業をやってみよう.

上の最初の解"012343421042143042321400312301"は形相図に書き入れてみると, 下左のようになる. その3と4を交換すると中の図になる. 周囲は01234ではなくなるが, よく見ると下の五角形(面の番号1)の周囲が01234である. そこで辺の接続関係を保ったまま, これが周囲(面0)に来るように図を書き直すと右のようになる. この列を圧縮したのが"012343421420130204031343214201"で, 先程の解の2番目であった. だからこの2つの解は等価であった. これを上の全ての解のすべての置換について実行し, 同じになったものをまとめると3通りになる.


以下はそのプログラムだ.

repはcolのprm0をprm1で置き換える. つまりcolの(0 1 2 3 4)を(0 1 2 4 3)で置き換える(3と4を交換する).

  (define (rep prm0 prm1 col) ;col expanded form
 (define (pair as bs)
  (if (null? as) as
   (cons (list (car as) (car bs))
    (pair (cdr as) (cdr bs)))))
 (define (subst ps ls)
  (if (null? ls) ls
   (cons (cadr (assoc (car ls) ps))
    (subst ps (cdr ls)))))
 (subst (pair prm0 prm1) col))

(0 1 2 3 4 3 4 2 1 0 4 2 1 4 3
0 4 2 3 2 1 4 0 0 3 1 2 3 0 1))
は
(0 1 2 4 3 4 3 2 1 0 3 2 1 3 4
0 3 2 4 2 1 3 0 0 4 1 2 4 0 1)
になって左と中の絵に対応する.

remapは置き換えた色のリストを, (0 1 2 3 4)が先頭になるように(面0になるように)位置を変更した辺のリストを作る. newposとしよう. これを基本位置という. つまり右の絵にする. これは多少面倒だ.

まず後述の関数newfaceを置換後の色のリストに使うと, colorsに対応する五角ミノがいる位置が得られる. このリストをnewcolとすると, newcolは

((0 8 7 6 5) (0 1 2 3 4) (28 25 13 17 27)
 (28 29 21 24 26) (9 1 5 11 10) (22 29 27 16 19)
 (9 2 12 13 14) (23 26 25 14 10) (23 11 6 20 24)
 (15 19 18 8 4) (22 21 20 7 18) (15 16 17 12 3))

これを見ると五角ミノ(0 1 2 3 4)は(0 1 2 3 4)にいたのに(0 8 7 6 5)に, (0 1 2 4 3)は(0 8 7 6 5)にいたのに(0 1 2 3 4)に, (0 1 3 2 4)は(1 9 10 11 5)にいたのが(28 25 13 17 27)に, (0 1 3 4 2)は(22 29 27 16 19)にいたのに(28 29 21 24 26)にいった.

newposを作る方針は次のようだ. 基本位置に来る五角ミノの現在位置を設定する. (0 1 2 3 4)は(0 8 7 6 5)にいたので, newposは(0 8 7 6 5 ...)となる(左の絵).


先頭の(0 8 7 6 5)の0と1の位置にある0の辺と8の辺の隣の面を探す. つまり(cdr newcol)中の0と8を持つリストを探すと(0 1 2 3 4)と(15 19 18 8 4)が見付かるが, これらに共通の4が辺0と8から別れるもう1本の辺と分る. これはnewposの5の位置なので, そこに4を置く.

(0 8 7 6 5 4 ...) まで判明した(中の絵). すると後は判明した場所を隣同士にもつ五角ミノを探す作業を続ける.

まずnewposの(0 5)の位置の(0 4)を持つ五角ミノ, (0 1)の位置の(0 8)を持つ五角ミノを探すと (0 1 2 3 4)と(15 19 18 8 4)が見付かるので, それらの入る(6 7 8)の位置に(2 3 4), (11 10 9)の位置に(15 19 18)が入り, 右の絵になる. 以後同様にして各辺が決る. (consfの下請け関数cfsが担当する.)

(define (remap newcol)
 (compress (map (lambda (n) (list-ref newcol n))
  (consf (newface newcol)))))
(define (newface col)
 (define (sel ps ls)
  (map (lambda (p) (list-ref ls p)) ps))
 (append-map (lambda (c)
  (filter (lambda (f) (equal? c (sel f col)))
   (apply append (map (lambda (a) (allcs a)) faces))))
     colors))

(define (consf col)
 (let ((newpos (append (car col) (make-list 25 '()))))
  (define (csf a b c d e)
   (define (ls n f m)
    (list-set! newpos n (list-ref f m)))
   (define (search a b)
    (car (filter (lambda (c) (subset? (list a b) c))
     col)))
   (define (reshape a b l)
    (define (left a l)
     (cadr (member a (cons (car l) (reverse l)))))
    (if (= b (left a l)) (set! l (reverse l)))
    (let ((p (elemindex a l)))
     (append (drop p l) (take p l))))
   (let* ((fa (list-ref newpos a))
     (fb (list-ref newpos b))
     (ff (reshape fa fb (search fa fb))))
    (ls c ff 2) (ls d ff 3) (ls e ff 4)))
  (let* ((f (car col)) (f0 (car f)) (f1 (cadr f))
    (g (car (filter (lambda (a) (member f0 a))
     (cdr col))))
    (h (car (filter (lambda (a) (member f1 a))
     (cdr col))))
    (n (car (intersection g h))))
   (list-set! newpos 5 n)
   (csf 0 5 6 7 8) (csf 1 5 11 10 9) (csf 2 9 14 13 12)
   (csf 3 12 17 16 15) (csf 4 15 19 18 8)
   (csf 7 18 22 21 20) (csf 6 11 23 24 20)
   (csf 10 14 25 26 23) (csf 13 17 27 28 25)
   (csf 16 19 22 29 27)
   newpos)))

prmは(0 1 2 3 4)の順列. prem0はその先頭(0 1 2 3 4). equivは等価の解をまとめたリストのリスト. doループで実行が始まる.

doループではallsolsから解を1個とりcolとし, equivの表のどれかに既にあればなにもしない. どれにもないなら, そrwれを1個もつリストをequivに追加し, そのリストをeqlistとする. colを120通りの色の置換えをし, 置き換えたnewcolがqlistになければ追加する.

(define prm (permutation (range 0 5)))
(define prm0 (list-ref prm 0))
(define equiv '())
(do ((j 0 (+ j 1))) ((= j 60))
 (let* ((col (list-ref allsols j)))
  (if (every (lambda (a) (not (member col a))) equiv)
   (begin (set! equiv (cons (list col) equiv))
    (let ((eqlist (filter (lambda (a) (member col a))
       equiv)))
     (do ((i 1 (+ i 1))) ((= i 120))
      (let ((newcol (remap (rep prm0 (list-ref prm i)
        (expand col)))))
       (if (not (member newcol (car eqlist)))
        (set-cdr! (last-pair (car eqlist))
         (list newcol))))))))))

それぞれの等価グループの長さを出力し, 各グループを昇順に並べ替え出力する.

(display (map length equiv))
(define (formprint ls)
 (for-each (lambda (a) (display a) (newline)) ls))
(for-each (lambda (a) (newline)
 (formprint (sort a string<?))) equiv)

(20 10 30)
012342143034134240100232310241 ;20 taocp B
012342143304041241013122034023
012342143304401012120232334410
012342143340041241102033402231
012342341034431021231300224401
012342341340140042321202413301
012342341430130204032314112204
012342431340401201031242330241
012342431430130240031422341120
012343241024134042321203001143
012343241024143042233010114032
012344123023143042124300214301
012344123032431201014130324402
012344123320410102023414231403 ;winning C
012344132023431021132404003421
012344132032431012134020342014
012344213320140240014231334210
012344213320401102024233140134
012344231023134204031240413201
012344231320410012234101334402

012342413403013124200341224301 ;10
012343142402013124300214321304 ;taocp C
012343412042413120300241320341
012343412402013124033241024031
012343412402013142300421342301
012343412402031124300243124103
012343412402103024310241324310
012343412420013124302041304321
012343421402013214300141324302
012344312302014124300241423301 ;winning A

012342143304014214100232331204 ;30
012342143304041142200132334102 ;winning B
012342143304041241100323224301
012342143403031241100232443201
012342341304041241300212134203
012342413340410102022431332401
012342413430130204013242114203
012342431403103204031242014231
012342431430031214031242304210
012342431430130024231042314021
012342431430130204032141324102
012343142024143042312100314302
012343142042431021133200423401
012343241024143042320211304310
012343241024143240301020314321
012343241024413012321200341304
012343241420103042321204310341
012343421042143042321400312301
012343421420130204031343214201
012344123302041241100434332201
012344132032134024134200321104
012344132032431021130244320041
012344132032431120034210324410 ;taocp A
012344132302401021134203024431
012344213023413102024231004431
012344213320014142024231330041
012344213320410102023241443301
012344213320410120204031334421
012344312032431021314200124403
012344312320410102034321234401

Winningやtaocpについてはまた述べる.