トップ «前の日記(2010-06-17) 最新 次の日記(2010-06-26)» 月表示 編集

日々の流転


2010-06-21 [長年日記]

λ. The ICFP Programming Contest 2010

今年もThe ICFP Programming Contest 2010 に参加していた。期間は日本時間の 6/18(金) 21:00 から 6:21(月) 21:00 までの72時間。 チーム名はいつもの Team Sampou というチーム名で、メンバーもいつものようなメンバー。

やっていたことを簡単に時系列にまとめておく。

6/18(金) 夜

とりあえず、問題は読んだものの、サーバーが重く、ログインしようとしても Internal Error とか言われるので、ログインは諦める。 Ternary Streams を考えるのはまだ無理そうなので、回路記述の構文について考える。

最初は、以下のサンプルで、最初と

  • 最後以外の各行がノードで、
  • 同じ「数字(L|R)」の箇所同士がワイヤーで結ばれていて、
  • 両側の端点がともにXになっている、X18L0#X7Lが外界を表す「external gate」

なのかと思った。 だけど、それだとLとR、そして最初と最後の「19L」の意味がわからない。

19L:
12R13R0#1R12R,
14R0L0#4R9L,
9R10R0#3L8L,
2L17R0#5L9R,
15R1L0#10R13R,
3L18R0#6L15L,
5L11R0#13L12L,
19R16R0#11R8R,
2R7R0#11L10L,
1R3R0#18L2L,
8R4L0#16L2R,
8L7L0#15R6R,
6R0R0#14L0L,
6L4R0#14R0R,
12L13L0#17L1L,
5R11L0#16R4L,
10L15L0#17R7R,
14L16L0#18R3R,
9L17L0#19R5R,
X18L0#X7L:
19L

ログインできるようになったので、自分で色々書いて食わせてみるも、inconsistent input connection ではねられてしまうので、諦めて寝る。

6/19(土)

午前中は歯医者に行くなどする。 そういえば去年もICFPC中に歯医者に行ったなぁ。

0#の部分がゲートの種類を表しているのではないかと思い、その部分を変更してみるも、unknown kind of node というエラーに。このエラーメッセージからするとノードの種類は色々あるのか? と疑うも成果なし。

池上さんが以下の記述で inconsistent input connection でエラーにならず、this is an illegal prefix でエラーになるのを発見するも、結局構文は分からず。

0L:
X0R0#X0R:
0L

午後は某所でオフラインミーティング。 問題を説明して議論しているうちに、nobsunが回路の記述の正しいフォーマットに気づく。0#の左側の「数字(L|R)」は入力が何行目のノードのどちらの出力からきたかで、右側の「数字(L|R)」は出力が何行目のノードのどちらの入力に繋がっているかを表しているのね。そして、0#の左側のXは環境からの入力を表し、右側のXは環境への出力を表すと。 Task Description では外界がひとつのゲートとして抽象化されている的なことが書いてあったのに……しくしく。

それに基づいてinconsistent input connection でエラーにならず、this is an illegal prefix でエラーになる幾つかの小さな例を作る。

[打ち合わせの様子の写真]

そして、上の写真中の4つの回路(1),(2),(3),(4)をサーバーに食わせたときの出力列をもとに、

  1. 逆方向のワイヤの初期値
  2. ゲートの関数
  3. サーバで回路に与えている入力

の3つを同時に求めることに。 これは色々試行錯誤したが、最終的には制約をAlloyに突っ込んだ(solve-op.als)ら、すべてを一意に決定してくれた。これだけで一意に決まる自信はなかったので、ちょっと驚いた*1

[Alloyの出力]

というわけで、逆方向のワイヤの初期値は 0 で、ゲートの関数は以下のような関数。サーバでの入力は 01202101210201202 。

op|  0     1     2
--+-----------------
0 |(0,2) (2,2) (1,2)
1 |(1,2) (0,0) (2,1)
2 |(2,2) (1,1) (0,0)

ゲートの関数がわかったので、Task Description の回路をオートマトンArrowで実装し、サーバで与えている入力を与える。これをサーバの出力と比較することで、遅延が発生するワイヤは、下に書いてあるノードから上に書いてあるノードへとつながるワイヤであって、その逆ではないことを得た。そんでもって、そのオートマトンArrowで実装した回路に Task Description で指定された入力を与える事でキーをゲット。

キーをゲットしたは良いものの、ゲートの関数が意味不明すぎて、これでどうやってキーを出力する回路を組んだら良いかさっぱりわからず。 多分、これを組み合わせて色々なプリミティブを実装するんだろうなぁ、と思いつつ、みんなでご飯を食べにいき解散。

ここまでの成果: Circuit.hs

帰りの電車の中でも色々試してみるが、心持ち電車が空いているなぁ、と思ったら、ワールドカップの日本戦か。

長い一日だった。

6/20 (日)

Alloyを使ったプリミティブの合成の試みと、ゲートの性質を考える事を、並行して行う。

Alloyを使った試みでは、入力を複数回使うことを許して組み合わせ回路を合成すると、色々できるけれど、入力を複数回使う事を許さないと何も面白いものは作れないということに気づき、挫折。 そこで、まずは入力を複製する回路を合成する事を考えるけれど、これも小規模な組み合わせ回路の範囲では存在せず、やっぱり挫折。

やっぱり順序回路を考えないとダメかぁ、などと思いつつ、ゲートの関数opの性質を考えていて、第一出力に着目すると、fst (op (x,y)) = (x-y) `mod` 3 になっていることに気づく。 さらに、少し遅れて、第二出力に着目すると、snd (op (x,y)) = (x*y+2) `mod` 3 だということに気づく。

この時点で既に夕方 orz

ゲートの関数がこういう風に表せるということが分かるとだいぶ考えやすくなって、特定の値を特定の値へと変換するだけの簡単な順序回路を幾つか作ってみる。 ただし、入力を複製したり、出力を捨てて定数にしたりといった回路は作れなかった。 というあたりで量子計算を量子回路で書いているのを連想したりする。

……とかグダグダ考えているうちに、出力したいデータを s = s1 s2 ... sn とすると、

[図]

というような回路を考えて、

  • s1 = f1(0)
  • s2 = f1(f2(0))
  • sn = f1(…fn(0)…)

を満たすように、f1,…,fnを決めれば良いと言うことに気づく。 例えば、fiとして状態を持たず入力をインクリメントする回路を適当な回数繰り返すようなものを使うことにすれば、絶対に作れる。

で、入力をインクリメントするような回路を作ったと思って、それを使ってオートマトンArrowを使って回路を構成してみたんだけど、実際に動かしてみると答えが合わない。 調べてみると、状態を持たずに入力をインクリメントする回路を作れてなくて、状態を持って変な動作をする回路になってしまっていた。 しょうがないのでで手で無理やり辻褄をあわせて、キーを出力する回路を作れた。

オートマトンArrowを使って書いたのを、手で回路記述言語に落とすのはやる気が起こらなかったので、ここまでを一般化・自動化して、任意の3進列を回路へエンコードするプログラムが書いた。

ここで、さあサーバーにsubmitするぞと思ったら、サーバーさんがお亡くなりに……orz

しばらくしたら、投稿出来て…… やたっ! 通った!!

You have submitted fuel for car 219 with size 54. A special comment for you:
circuit output starts with
   11021210112101221
this is a legal prefix
Congratulations.
You have submitted a circuit that produces the key prefix.

というところでこの日は終了。

6/21(月)

車と燃料のデータがどう3進列にエンコードされているのかを調べる。 これは一人で作業していて、かなりめげそうになった。

車の方のエンコーディングは複雑そうなのに対して、燃料の方はタンクの数だけ非負係数の行列が並んでいるだけだろうから、[[[N]]]で表現されていると考えるのが自然だろう、と思い色々な3進列を生成してはサーバーに投稿してみる。最初はまったく規則性が見えず途方にくれていたけれど、長い事やっているうちにエラーにならなかった入力のプリフィックスとメッセージ中の「for 1 tanks」、「using 1 ingredients of air」、それから「dimension mismatch」「fuel coefficients missing for tank 1」「c_{1,1} must be >= 1」といったメッセージの間に規則性があることに気付く。

この時点で気付いていた対応
prefixtankingredientmessage値の予想
000dimension mismatch[]
1010dimension mismatch[[]]
11011dimension mismatch[[[]]]
111011c_{1,1} musb be >= 1[[[0]]]
1111011fuel coefficient missiong for tank 1[[[n]]]

これでなんとかなりそうな気がしてきた。 で、これをもとに考えていたのだけど、どうしても思いつけなかった。 リストというからには常識的に考えて再帰的な構造になっているはず*2だが……

かなりの時間をかけてもどうしても思いつけなかったので、さきほどはエラーにならない入力をあまり作れてなかった2を含むtritsについてもエラーにならない入力を色々作ってみて、prefixと結果の関係の分析を続ける。 それで、リストが全然再帰的な構造になっていなかった事に気付く。これはさっきは気付けなかったわけだ。 で、最終的には以下のように符号化されてそうだと推定するところまでは行ったが、この時点でもう既に夕方 orx

class Trits a where
 toTrits :: a -> [Int]

instance Trits Int where
 toTrits 0 = [0]
 toTrits _ = undefined

instance Trits a => Trits [a] where
 toTrits xs =
   case length xs of
     0 -> [0]
     1 -> 1 : concatMap toTrits xs
     2 -> [2,2,0] ++ concatMap toTrits xs
     3 -> [2,2,1,0] ++ concatMap toTrits xs
     4 -> [2,2,1,1] ++ concatMap toTrits xs
     5 -> [2,2,1,2] ++ concatMap toTrits xs
     6 -> [2,2,2,2,0] ++ concatMap toTrits xs
     _ -> undefined

このまま分析を続ける手もあったけど、それよりは思い、簡単そうな車に、この範囲であてずっぽで作った燃料を供給してみる。 タンクが1個の車はそれでも通るし、タンクが2個のやつも少しだけ通った。

車が多すぎて供給できる車を探すのが大変なので、さすがにこれは自動化プログラムを書くべきと思ったが、そこまでは手が回らなかった。 そして、車のフォーマットの解析もしないとなぁ。とか思っているうちに終了。

フォーマットの解析が終わって、始めて制約を解く本質的な勝負に入れたはずなのに、結局そのスタート地点にも立てずに終了したという感じ。楽しかったけど、やっぱり悔しい。

関連

*1 どうでも良いけど、Alloy の Evaluator は出力をコピペできなくてマジひどい。

*2 これが誤り