[ICFP] ICFP Programming Contest 2010 参加記

pure pure code ++ というチームで参加していました。今回は問題がとても面白かったと思います。楽しめました。チームのメンバは http://twitter.com/nya3jp/status/16604202811 の6人。6人目のメンバーはトンちゃんでしょうか。
http://www.icfpcontest.org/2010/ コンテストのページはこちら。
http://icfpcontest.org/icfp10/score/teamAll 順位表はこちら。
上位5チームはリストには表示されないようです。pure pure code ++ は表示されていないので5位以内ということみたいです。上位5チームのの点数とチーム名が非表示なので自分のチームが一体何位なのか全くわからないのですが、それなりの手応えはあります。発表まで順位が分からないようにとのことなので、点数などの公表は控えておきます。

問題の詳細は、http://icfpcontest.org/2010/task/
mr_konnさんによる日本語訳 http://d.hatena.ne.jp/mr_konn/20100618/icfp2010task

大まかな内容は次のような感じです：

• 車と燃料を作って期間内になるべくたくさん儲けよう
• 車は一定時間ごとに利益を生む。車から生じた利益は燃料の供給元で（だいたい）山分けされる
• 車のエンジンは行列の制約式として表され、それを満たす燃料（行列）を供給できる
• つまり、なるべく他のチームに燃料を作られない車を作って、なるべく他のチームの車の互換燃料を作った人が勝ち

当時の様子を書いて行きます。

一日目

開始直前

京都からやって来るchunさんが乗り物酔いと闘いながらbitbucketのプライベートレポジトリなどを用意してくれる。私はhgの使い方を勉強するなど。普通にコミットする分には適当に何とかなりそう。とても緊張してくる。

21時

いよいよ開始。英語と格闘するが殆ど理解出来ない。やばい。チーム名がぴゅあぴゅあこーどに決まる。

23時頃

全く問題読みに貢献できないまま、大まかな解読が終わる。車と燃料を作るようだが、それぞれは詳細秘密の3進表記で表される。さらに燃料は3進表記そのままではなくて、それを生成する回路で送信する必要がある。それももちろん詳細は秘密ですって、なんぞそれ。リバースエンジニアリングゲーか。リバースエンジニアリングならまかせろー、って感じでもないが、とりあえず回路の仕様を頑張って調べる。

0時頃

とりあえず適当な回路を投げて反応を見てみる。うえーい、全然わからん。悶々としていると、phoenixさんが表埋められそうと言ってサクサクと表が埋まっていく。何が起こっているんだ。とりあえず私は並行して回路シミュレータを書く事にした。これも問題の仕様がよくわからず、どういう条件で信号が遅延するのか曖昧なまま書いていたが、なんとかなった。

1時頃

シミュレータが出来る頃、表も完成していた。シミュレータに入力を突っ込んで鍵を生成してみる。鍵はできたが合ってるかどうか全然わからない。入力をパススルーする回路がなんだか私には良く分からないが作られて、入力が得られる。それを元に検算、シミュレータのバグが取れて、正しい鍵が得られる。

4時頃

素子の挙動と出力すべきキーとサーバの入力（の先頭17文字）は分かったが、果たして如何にしてキーを出力するのか？入力から出力への簡単な回路があるか少し考えてみたが、さっぱり分からない。それも分からないが、本番の燃料投入では17文字以上出力しなければならない。それは即ち不明な入力に対してこちらの意図した列を出力しなければならないということ。入力に対してキーを出力する簡単な回路を見つけても意味がないことに気付く。入力非依存で指定した列を出力できる回路を生成できなければいけない。

5時頃

nyaさんとphoenixさんが謎の技法により定数回路などをさくさくと作り上げていく。若者の人間離れというのを目の当たりにする。私は他にできることがないので、それらを組み合わせてジェネレータを作ることに。Haskellで書かれたとってもぴゅあぴゅあ（グローバル変数を書き換えまくる）なコードが完成した。この時の回路はパススルー回路と定数加算回路を逆順でつないだだけの単純なもので、1tritあたり約16gateも消費するお粗末なものだった。しかし、結局最後までこれと大差のないコードが使われることになる。6時半ごろ、ついに最初の得点が入る。他の人は寝ていたようなので、一人で盛り上がる。すでに8チームほどがサブミットした後だっただろうか。ちょっと出遅れたと思った。

9時頃

phoenixさん邸へ移動。任意の列を送れるようになったので、まずは燃料を何とかしようということに。適当な列をひたすら投げまくる。システムのエラーメッセージがどう見てもParsecのエラーです。これはHaskellで書かれているな。どうやら3進コードの最初のところにタンク数が入っているらしいことが分かる。そして数のエンコード方法が大体分かってくる。燃料は3次元配列になっていると睨んでいろいろ突っ込んでみるが、これがなかなかうまくいかない。dimension errorとひたすら言われるが、車と燃料の仕組みを理解せずにやっていたので、そもそも何のdimensionなのか分からない。

昼過ぎ

相変わらず進展せず。ぼちぼち鍵車以外の車が解かれ始めて焦る。あまりにも解読が難航しすぎて眠い眠い。この頃サーバーの反応をWikiにまとめていたが、とても面倒だったので、nyaさんがサブミットして入力と結果を保存するコマンドラインツールとCGIを作り始める。これによってサブミット作業がとても楽になる。CGIは今後継続的に更新されていき、欲しい機能がいつの間にか実装される神インフラとなる。

15時頃

あまりにも眠かったので1時間ほどうとうとしていると、なんと車と燃料のフォーマットと整数のエンコードがすべて分かったという。そ、そんなバカな？yuizumiさんとphoenixさんが人間離れを起こしたらしい。どうやら解読が難航していたのは、リストの長さを表す整数と、行列の成分を表す整数のエンコードが異なっていたせいらしかった。車が読めるようになったので、いまさらになって車のお勉強をする。分かったような分からんような。1次元の2を突っ込むと解けてしまう車が幾つかあるというのが分かったのでサブミット。実は試行錯誤の最中にもなぜか解けている車があったが、ようやくちゃんと理解して送れた。

17時頃

問題の全貌がようやく理解できて、ICFPにはありがちな、遠い遠いスタートラインにようやく立てた。さて、問題が分かったが、これは非線形の整数計画問題なのか？答えが出せるのかこれは？私には全然分からないが、簡単に解けるならこんなの問題になるはずがないということは恐らく間違いない。chunさんが1次元の解をブルートフォースで見つけるプログラムを書いて、いくつかの車に対してトリビアルでない燃料を投入することができるようになった。

18時頃

もしかして：やることがない？何をやったらいいのか分からない。

19時頃

高次元に対応するにはブルートフォース以外の方法が必要だ。焼きなましとか。焼きなましならまかせろー、バリバリ。Marathon Matchで培った焼きなまし技術を今こそ活かすとき。

20時頃

焼きなましソルバ完成。しかし、全然解いてくれない。極稀に解ける車もあったが、これでは話にならない。焼きなましで上手くいく類の問題ではなかったのか。はたまたプログラムがバグっているのか。焼きなましを信じてこのままやっていいのか。

20時40分頃

一頻り弄って、やっぱり焼きなましでは無理でした。と報告した矢先にひどいバグが見つかる。[0-1)の乱数が欲しい場所でrand()と書いていた。なぜこれで解けていた問題があるのかは謎だ。ともかく、これを直すと結構な数の車を解けるようになった。方針は間違っていなかったのか。Lightning Division終わるまでしばしのサブミット祭り。

二日目

21時

Lightning Division終了。濃密な一日であった。この時点で5位に入っていたようだが、6位との間をふらふらしていたので、そんなに良い順位ではないだろう。ご飯を食べながら明日以降の作戦会議。一つはゴルフ。ゴルフは最大で収入が2倍近く変わる可能性があるのでおそらく重要だろうと言う事。もう一つは車の製造。gusさんが作っているそうなので、それを完成させてもらう方向で。最後にソルバの強化。ソルバは車の耐久試験にも使われることになるだろうから、車の強度にとっても重要。ご飯を食べて帰宅。眠すぎて電車の中で立っているのが辛かった。

0時

帰宅。回路ジェネレータに明らかな無駄があったので取り急ぎ修正。回路規模が半分ほどになって、おそよ1tritあたり8ゲート。眠気の限界に達する。

11時30分

再びphoenixさん宅へ。昼食後作業。まず私のすることはソルバの強化。焼きなましに用いるスコアとして、満たしている制約式の数を用いていたが、これは離散的過ぎるし、ひとつの制約式を満たすのが完全にランダムでしか見つけられないので良くない。それぞれの制約式が満たされている度をうまく0-1の値にすることにする。まず最初に、行列の要素のうち満たされているものの個数を入れることにした。とても単純だが、これだけでもかなり性能向上した。次に各要素がどれぐらい条件に反しているかを考慮するようにする。試行錯誤していろいろ式を試してみるが、この問題は行列を乗算するので係数は非常に大きくなる傾向にあって、故に、ずれている分のlogをとって、さらにそれを0-1に正規化することにした。

昼ごろ

車の量産体制が整ったようで、少しずつ車が出荷されていく。解かれないかどきどき。ソルバの自動化が行われ始める。ポンコツ車が結構な割合で出荷されてくるので、まず決め打ちのいくつかの行列を突っ込んでみて、次にブルートフォースを走らせて、ダメだったら焼きなましソルバを走らせるような感じ。

9時頃

20台ほどの車が出荷される。最初の方に出荷した数台以外は解かれていないようだ。良かった。私とchunさんはひたすらソルバの改良をする。それに加えて焼きなましが漏らす巨大整数を入力しないと解けないタイプの問題をみんなで各個撃破。このころにはかなりの車を解けるようになっており、相当の収入が得られるようになっていた。最盛期のぴゅあぴゅあこーど＋＋：ご飯を食べている間に+100点なる発言がなされてから夕食に行ったら実際には+200点だったり、http://twitter.com/wata_orz/status/16615142451 を見てにやにやしたりするなどする。

三日目

0時頃

最終日に向けて私は泊り込みで作業。焼きなましソルバの性能がほぼ完成を迎え、ランダム生成系をほぼ全て廃車にできるようになり、残りの手動生成系を各個撃破した結果、2種類の車を残しほぼ解けるようになった。解けないものの1つは1日目の終了時点頃に投稿された3000番台〜4000番台の車で、一見普通のランダム生成に見えるが、他のとどこかが違うのか何故か解けない。右辺が左辺よりも大きいのでおそらく解の存在する領域がとても狭いのだと思うが、それにしても他の類似の車はさくさく解けるのでこれは大変な謎だった。もう一つが巨大整数を必要にしているように見えるが手計算では規則性のつかめない問題（45076番など）。同じタイプの車で番号が若くてサイズの小さい試作機のようなのがあったので、もしかしたらと思って焼きなましにかけてみると2x2行列の比較的小さい解が得られた。この解を元に式の意味をphoenixさんと考えていると、紆余曲折の末、これは巨大整数の素因数分解を要求していることがわかった。行列の積で任意の数をエンコードできるとか…。作るのは簡単だけど解くのは難しいのは：素因数分解というのはまあそうだけど、それを実際に制約式にエンコードして出荷してくるというのは脱帽だった。

4時頃

一応素因数分解はどこかで走らせることに。サイズとしては10^100程度で、これが初めて素因数分解されたのは1990年頃らしいが、果たしてそのころのスパコンに今のPCが追いついているのだろうか。サーバが重くなりすぎて結果が返ってくるのに2分ぐらいかかるようになる。この調子で最終日大丈夫なのかと心配。車のサイズが100文字までになったというtwitter上の噂。なんぞそれ。そんな仕様変更があったら今回一気にクソゲー化だ。そんなこんなでなるほど4時じゃねーのを見届けて寝る。

10時頃

寝ている間に新車カタログの仕様変更があって、車のスクレイプができなくなっていた模様。ひどい…。早速対応してもらうが、これでロスした点数は少なくないだろう。とりあえず夜のうちに増強されたのか、サーバはずいぶん軽くなった。車100文字制限も撤回された模様。車の出荷も再開。私は自動ソルバをくぐり抜けた車を焼いていく作業の繰り返し。車の投稿スピードが上がってきてだんだん辛くなってくる。素因数分解は結局無理っぽいので諦める。

12時頃

ご飯を食べながら。今朝から新しく提供されるようになった車リストに供給された燃料のサイズが乗っているらしく、それを見ると他のチームの燃料は相当小さいらしい。1文字1-2ゲートのチームもいる。これは結構まずいのではないか。やはりゴルフもやるべきか。

昼頃

CGIに2-5チームしか解いてない車のうち自分たちの解けた車の数を表示する機能がついた。それによると、2チームしか解いていない車の実に9割以上がうちが解いたものだということが判明した。にわかには信じがたい数であったが、リストをダウンロードしなおして眺めてみるに本当にそのようだ。それを元に収入を見積もると、200程度はあると出た。これは恐ろしい数だ。しかも2チームの車のうち約半数がうちの燃料の方がサイズが小さいらしい。これはどういう事か？つまりゴルフの必要性は少なくなったということだ。100チームの中でトップを取るのは2チームの中でトップをとるより遥かに難しいが、100チームの中でトップを取ることの意味は殆ど無い。そこを目指すよりsolved 1の車を解いていったほうが遥かに効率が良い。車の生産も終わり、全体の方針としては、後はひたすら出てくる新車をスクラップにしていくという事になる。

改めてリストを見ると、鍵生成は6ゲートでできるらしい。それと2のみの行列を出すコードは7ゲートでできるらしい。結構多くのチームがそれで提出している。これが分かったところで任意の列を生成することはできないだろうから得点にはほとんど影響がないが、7ゲートの方は割とたくさんの車に供給できるので、見つけたら収入が10点ぐらいは増えるかもしれない。たくさんの人がサブミットしてるなら簡単な回路かもしれないので、適当に考えてみるがよくわからず。yuizumiさんが全探索組んで6ゲートの回路が発見される。ちょっと嬉しい。しかし出てきた回路を見ても、意味はさっぱりわからない。7ゲートの回路は探索が終わらなくて見つからず。無念。

夕方頃

もはや車をひたすら潰すのみ。潰せども潰せども車はやってくる。終わりに近付いて新車の入荷するペースも加速度的に上がってくる。しかし思い出出荷のような簡単に解けるのががほとんどで、CGIをリロードするたびに数十という単位で車が減っていく。デフォルトパラメータの自動焼きなましソルバで生焼けになってしまった車を手動でじっくり焼きなます。ひたすら焼きなます。入荷する車は、ポンコツ、簡単に焼ける、硬いがパラメータをうまく選んでじっくり時間をかければ焼ける、手動で簡単に解ける、のおおよそ4種で、前者二つは自動的に消えて、手動が必要なものに対しては各個スペシャルソルバを作成し、硬いが焼けるものに関してはchunさんが膨大なコンピュータリソースにものを言わせて超並列で焼いていく。このころにはソルバのさらなる性能向上により3/4000番台の車も頑張れば焼けるにカテゴライズされていたので、これも超並列で頑張って、最終的には30台程度はスクラップにすることができた。それにしてもあんなに初期に出た割にはなんという硬い車だったのだろう。十分に役割を果たしたに違いない。

終了直前

全員総出でひたすら車を潰し続ける。無限プチプチにも似た楽しさがあったが、さすがに何時間もやり続けるとしんどい。8時頃、まだ1時間もあるのか、などの声も。それでもなんとか、できるだけの車を潰しきって時間終了。完走することができた。

反省・感想

とにかくとても楽しかった。問題がとても良かったと思う。前半のリバースエンジニアリング部分は蛇足にも見えるが、個人的にはそういうのも楽しめた。行列いじるだけではなんだかICFPという感じがしないような気もするし。参加者同士の問題の出し合いというのはICFPでは新しかったと思う。解けない車が出てきて、そのアイデアに驚嘆したり、さらにゴルフもあり、非常に盛りだくさんだった。独りでやっていたらやることが多すぎて相当厳しかったかもしれないが、そういう意味では、チームに恵まれて十分に楽しめたと思う。nyaさんの強力なインフラとgusさんの車製造のおかげで私は燃料製造に集中することができた。インフラと車がどうなってるのかは今でもよく分かっていない。今回良かったのはとにかくきちんと平行に作業が進んで、個々のタスクもほぼ間違った方向に行かなかった事だと思う。

後日談

http://icfp.gnumaniacs.org/2010/06/21/whats-this-thing-with-cars-and-fuels/

公式ブログに解説記事のようなものがアップされた。曰く、

• 車は本当は "relative termination problem in string rewriting" と呼ばれる問題で
• 燃料はそれを解く方法。"matrix interpretation"と呼ばれるもの

　　　　　　　　　ナ ゝ　　　ナ ゝ　/　 　 十＿"　 　 ー;=‐　　　　　　　　　|! |!
　　　　　　　　　　cト　　　　cト　/＾､_ﾉ　 | ､.__　つ　 （.__ 　 ￣￣￣￣ 　 ・ ・
ミﾐ:::;,!　　　　　　u　　　　　　　｀ﾞ"~´　　　ヾ彡::l／VvVw、 ,yvヾNヽ　　ゞヾ　 ,.　,.　,.　、､ヾゝヽr＝ヾ
ﾐ::::;/　　￣ﾞ`ｰ-.､　　　　　u　　;,,;　　　j　　 ヾk'!　' l　/ 'ﾚ ^ヽﾍ＼　　 ,rﾞゞﾞ-"､ノ /　l!　!ヽ ､､　|
ミ/　　　　J　　　ﾞ`ｰ､　　　"　;, ;;;　,;;　ﾞ　　u ヾi　　　 ,,./　,　,､ヾヾ　　 | '-- ､..,,ヽ　 j　 !　| Nヾ|
'"　　　　　　　_,,.. -─ゝ.､　　　;, "　;;　　　_,,..._ゞｲ__／/〃 i.! ilヾゞヽ　 | ､　 .r．　ヾ-､;;ﾉ,.:-一'"i
　　j　　　　／　　 ,.- ､　 ヾヽ、　;; ;;　_,-＜　　/／_,,＼' "' !|　:l ﾞi !_,,ヽ.l　`ー─--　 ｴｨ' (． 7 /
　　　　　　:　　　　' ・丿　　￣≠Ξｲ´,-､　ヽ /ｲ´ r．　`ー-'ﾒ ,.-´､　　i　　　　 u　　ヾ｀`ー' ｲ
　　　　　　 ＼_　　　 _,,......::　　　´ﾞi､　`¨　/　i　ヽ.__,,... '　 u ﾞl´.i･j.冫,ｲﾞl　 ／ ｀`-､..-　ノ　:u l
　　　u　　　　　￣￣　　彡"　　　、ヾ￣｀`ﾐ::.l　　u　　　j　　i､｀ー'　.i /　/､._　　　　｀'y　　 /
　　　　　　　　　　　　　　u　　　　　　｀ヽ　　ﾞ:l　　 ,.::- ､,,　,.　ノ　ﾞ u　!　/_　　￣　ー/　u　/
　　　　　　　　　　　_,,..,,_　　　　,.ｨ､　 ／　　　|　 /__　　 ｀`- ､_　　　 l　l　 ｀`ｰt､_　/　　／
　　ﾞ　　　u　　,.／´　"　 ｀`- ､_Ｊ　r'´　 u　丿　.l,...　｀ー一''/　　　ノ　 ﾄ ､,,_____　ﾞ/　／
　　　　　　　 ./＿_　　　　　　　　ｰ７　　　　/、　l　　 'ﾞ　ヽ/　 ,. '"　　＼｀ｰ--- ",.::く､
　　　　　　　/;;;''"　￣￣ ───/　　ﾞ　 ,::'　 ＼ヾﾆ==＝'"／ ｀- ､　　　ﾞー┬ '´　/　＼..,,__
、　　　　　 .i:⌒`─-､_,....　　　　l　　　／　　　　 ｀ー┬一'　　　　　 ヽ　　　 :l　 ／　 , '　｀ソヽ
ヾヽ　　　　 l　　　　　 `　 ｀ヽ、 l　 .／　　ヽ　　　　　 l　　　　　　　　　）　　,; ／　　　,'　　　　'^i 

…て、知らんがな。どうやら我々は分からぬうちになんだか与り知らない問題に挑戦させられていたようです。で、このコンテストによって

• 互換 matrix interpretations を見つける新しいアイデア
• 新しいhard termination problem

が作られるはずだったと。

• 実際に、これらの両方で成功したと考えている

まじかー。うちはひたすら焼きなましただけだけどな。

さて如何様にして、参加者と主催者は科学の発展に貢献しようとしたのか？

• good fuel producerなコンテストチームは、来る [termination competition] の "relative termination of string rewriting" 部門に、そのソルバーをエントリーすることが促される。

まあぶっちゃけどうなんでしょう。こんな急造のものが戦えるんでしょうか。good fuel producer なのはおそらく確かなんですけど。

• 運営は難しい車を、来る termination competition のベンチマークとしてサブミットしていた

そのへんのテストは通過していたわけですか。

• コンテストチームは、そのアイデアとアルゴリズムを [Workshop on Termination] にサブミットできる。

なんか大層な話になってきましたな。

もしあなたがパズル好きなら：

• Car { chambers = [ Chamber { upper = [0,1], mode= Main, lower = [1,0] } ] } に供給できる燃料が存在しないことを証明できるか？

難しいですね。

• コンテストの各車が linear derivational complexity を持つことを証明できるか？

linear derivational complexity ってなんだろう。

まとめ

俺達はようやくのぼりはじめたばかりだからな このはてしなく遠い relative termination of string rewriting 坂をよ…

未完