TRICK 2015 に入賞しました - λx. x K S K ＠はてな

TRICK というのは Transcendental Ruby Imbroglio Contest for rubyKaigi の略で， Ruby を使って狂ったプログラムを書くというコンテストで，今回が 2 回めだそうです．今年の 9 月の FTD 2015 (日本ソフトウェア科学会大会の併設イベント) で TRICK 2015 のことを知り，遠藤さんから「なにかネタがあったら投稿しませんか」というお話をいただいたので，参加させていただきました．思いついたネタとしては 3 つほどあって，実は 3 つとも投稿できる状態にはなっていたのですが， 1 つは完成度的にいまいちだったので投稿を断念し，残りの 2 つを投稿しました．どちらか一方でも審査員の目に留まれば…と思っていたのですが，なんと 2 位と 5 位という非常にありがたい評価をいただきました．ただ，企業の大合併とは違うので 2 位と 5 位を合わせたからといって 1 位に勝ることはありません．実際，1 位の作品には到底及ばなそうです．

入賞された皆さんが続々と自分の作品を解説記事を公開しているので，私も自分の 2 作品について解説しておきます．とはいっても，言いたいことはすべて remarks.markdown の中にあるので，詳しく知りたい方はそちらをご覧ください (各作品へのリンク先にあります)．

第 5 位最短 SAT ソルバ

SAT 問題は，「¬A ∧ (B∨A)」のような論理式に対し，それを真にする変数A, Bの真偽値割当て (この論理式なら A=偽, B=真) を見つける問題で，その問題の難しさは変数の個数に対して NP 完全であることが知られています．奇しくも，第 4 位の作品が NP 完全の問題の一つである数独を解くプログラムになっていますが，この作品は見た目も面白くて確かにこれには負けるなぁという感じです．

で，その SAT 問題を解くプログラムは SAT ソルバと呼ばれ，さまざまな分野に応用されています (元々は定理の自動証明が目的だったようです)．その求解速度を競う SAT Competition という世界大会が毎年開催されています．今回提出した作品のこだわりの 1 つは，この世界大会にも参加できるような入出力仕様に則って作成したところです．もちろん，性能的には既存のプログラムに太刀打ちできるものではありませんが…．

入力は連言標準形 (CNF) という「論理和の内側には論理積が現れない形」の論理式に限定されていて， SAT Competition では以下のような DIMACS CNF 形式で与えられます：

c
c This is a sample input file.
c
p cnf 3 5
 1 -2  3 0
-1  2 0
-2 -3 0
 1  2 -3 0
 1  3 0

この入力は，論理式

(L1 ∨ ¬L2 ∨ L3) ∧ (¬L1 ∨ L2) ∧ (¬L2 ∨ ¬L3) ∧ (L1 ∨ L2 ∨ ¬L3) ∧ (L1 ∨ L3)

に相当します． c で始まる行はコメントで，p cnf 3 5 は変数が 3 つ，論理和で繋げられた式 (以下，節とよぶ) が 5 つであることを表します． 0 は節の終わり，1 以上の整数は変数， - は否定を表します．この論理式を真にする真偽値割当ては，L1=真，L2=真，L3=偽なので，

s SATISFIABLE
v 1 2 -3

を出力することが，SATソルバに求められていることです．複数の解がある場合はそのうちの 1 つを出力するだけでかまいません．解が存在しない場合は，

s UNSATISFIABLE

と出力します．既存の SAT ソルバの中には，minisat や nanosat や picosat というそのプログラムの小ささも売りにしたものがありますが，今回 TRICK に提出した作品は外部ライブラリも一切使わず 194 バイトという大きさで実現することに成功しました．名付けて yoctosat といったところでしょうか．

さて，その SAT ソルバは以下の一行プログラムで， DIMACS CNF 形式の文書をそのまま(拡張された)正規表現へ変換することで実現しています：

_='s %sSATISFIABLE';puts eval$<.read.gsub(/.*p.*?(\d+).*?$|\d+/m){$1?%w[?-* +'=-'=~/#{'(-?)'* }-*=(?=]*$1:$&>?0?"\\#$&$|":'$)(?='}+')/x?[_%p%i=0,[*$~].map{|x|x>?-?:v:eval(x+?1)*i-=1}*" "]:_%:UN'

具体的には，上の入力例に対しては以下のような Ruby プログラムが生成されます：

  '-'*3+'=-' =~ 
  /#{'(-?)'*3}-*=(?=
   \1$| -\2$|  \3$| $)(?=
  -\1$|  \2$| $)(?=
  -\2$| -\3$| $)(?=
   \1$|  \2$| -\3$| $)(?=
   \1$|  \3$| $)(?=
  )/x

=~ の左辺の文字列は，---=- で変数の個数分の - と =- から成ります．右辺の正規表現は (-?)(-?)(-?)-*= で始まっているため，後方参照として使用される \1, \2, \3 はそれぞれ - か空文字列のどちらかを表すことになり，それが変数の真偽値割当てに対応します．それに続く正規表現は，左辺の残りの - (ハイフン) 1 文字にマッチしなければいけません． (?=\1$|-\2$|\3$) がマッチするには，

\1が -
\2が空文字列
\3が -

のいずれかが成り立っている必要があります．これは，L1∨¬L2∨L3 が真となるためには，

L1 が真
L2 が偽
L3 が真

のいずれかが成り立つ必要があることに対応します． DIMACS CNF 形式の変数名が数値であることや否定が - で表現されていることをうまく利用して，正規表現への変換を簡単にしています．また，上の正規表現には x フラグが付いているために空白や改行が無視されることもポイントです．各節の最後にある |$ はあってもなくても結果は変わりませんが，正規表現への変換を簡単にするために追加されています．さらに，(?=...)は先読み正規表現でマッチした文字列を消費しないため，それ以降のすべての (?=...) も - にマッチする必要があります．これは，すべての節が真になるような真偽値割当てを見つけなければならないことと一致するわけです．なお，このアイデアは Abigailさんによる Perl での正規表現を元にしていますが， DIMACS CNF 形式に合わせるための工夫や先読み正規表現を利用している点が異なります．今回の Ruby による SAT ソルバはコードの短縮が主な目的なので，このような細かい工夫が必要でした．他のゴルファーと力を合わせればきっともっと短いコードが実現できたかもしれませんが，私には 194 バイトが限界でした．

この作品は「役に立ってはいけない」という TRICK が満たすべき条件に反しているのではないかと不安だったのですが，実際のところあまり役に立ちません．理由が 2 つあります． 1 つは Ruby の正規表現における制約です．変数が 200 個を超える場合，正規表現に \200 のような後方参照が必要になりますが， Ruby ではこの正規表現は \200 という 1 文字にマッチしてしまいます．ただし，3 桁でも 8 以上の数字が混じっている場合には後方参照として機能します．これは \ddd が 1 文字と認識されるのは ddd が 8 進数で 3 桁の数値だけであるためです．ちなみに，最初の桁が 1 の場合にも後方参照として機能するようです．詳細は remarks.markdown をご覧ください．もう 1 つの理由は，変数が 30 個くらいになっただけで現実的な時間で解が求まらないという致命的な点です．こちらの方が実用的な SAT ソルバとしては問題ですね．つまり，変数が 3 桁以上で問題になるような上述の制約についてそもそも気にする必要はなかったわけです．全然役に立たない SAT ソルバを作ってしまってすみません．ところで，上の制約って Ruby の仕様として知られていることなんでしょうか…？

第 2 位コラッツ列生成プログラム

コラッツの予想とは，どんな非負整数も HOTPO 操作を繰り返すといずれ 1 にたどりつくというものです． HOTPO は Half-Or-Triple-Plus-One の略で，「偶数なら半分にする，奇数なら 3 倍して 1 を足す」という操作のことです．その昔，ポカリスエットのホットで Hot Po という商品がありましたが，それとは全く関係ありません． 2⁶⁰ ぐらいまでの整数に対しては正しいことが計算によって確かめられているそうですが，現在も未解決の問題の 1 つです．角谷問題とか，シラキュース問題とか，いろんな名前がついている有名な問題です． 3 から始めると，

3 → 10 → 5 → 16 → 8 → 4 → 2 → 1

27 から始めると，

27 → 82 → 41 → 124 → 62 → 31 → 94 → 47 → 142 → 71 → 214 → 107 → 322 → 161 → 484 → 242 → 121 → 364 → 182 → 91 → 274 → 137 → 412 → 206 → 103 → 310 → 155 → 466 → 233 → 700 → 350 → 175 → 526 → 263 → 790 → 395 → 1186 → 593 → 1780 → 890 → 445 → 1336 → 668 → 334 → 167 → 502 → 251 → 754 → 377 → 1132 → 566 → 283 → 850 → 425 → 1276 → 638 → 319 → 958 → 479 → 1438 → 719 → 2158 → 1079 → 3238 → 1619 → 4858 → 2429 → 7288 → 3644 → 1822 → 911 → 2734 → 1367 → 4102 → 2051 → 6154 → 3077 → 9232 → 4616 → 2308 → 1154 → 577 → 1732 → 866 → 433 → 1300 → 650 → 325 → 976 → 488 → 244 → 122 → 61 → 184 → 92 → 46 → 23 → 70 → 35 → 106 → 53 → 160 → 80 → 40 → 20 → 10 → 5 → 16 → 8 → 4 → 2 → 1

このように HOTPO 操作を繰り返して得られる数列はコラッツ列と呼ばれ，予想の付かない数列で 1 にたどりつくことから，プログラミング教育の現場でも while 文の練習として使われることもあるようです． Ruby の場合 (教科書的に書くなら)

x = ARGV[0].to_i
puts x
while x > 1
  if x % 2 == 0 then
    x = x / 2
  else
    x = 3 * x + 1
  end
  puts x
end

となりますが，今回 TRICK に提出したプログラムはこれと同等のものです．

実際に提出したプログラムがこちらです：

%%%while eval '_=%%r%%(.)...\1=%%=~[%%%%,,,,,%%%s  ?=]*%%%%%%#"]*%%%%3x+1?%%'.% %%",%*p(_||=eval($**%%%))

何が評価されたか本当のところは審査員の皆様に尋ねてみないと分かりませんが，算術演算を一切使わずに文字列処理によって HOTPO 操作を実現したところでしょうか． % がやたらと多いですが，これは文字列リテラルや正規表現リテラルの % 記法 (%%...% や %r%...%) を多用しているためです．慣れれば読むことは難しくありません (たぶん)．このプログラムを作成する際，

この % 記法と % 演算子を列べれば % だけからなる式が作れるんではないだろうか…？しかも，% の個数が 4 * k + 3 のときだけ意味のある式になる！これは大発見だ！ TRICK に使えるかも！

などと浮かれていたのですが，いろいろ調べてみたらそんなことは既に知られていて前回の TRICK に使われていたようです． TRICK の投稿規定にも過去の入賞作品をよく調べろって書いてありましたね．危うく二番煎じとなるところでした．と，話が逸れましたが，上述のプログラムの基本的なアイデアは「ある文字列を偶数回繰り返すのと奇数回繰り返すのとでは意味の違う式を作る」というもので，その「ある文字列」というのが ", です．具体的には，「n が偶数なら半分に，奇数なら 3*n+1 に」という HOTPO 操作を，

n = (/(.)...\1=/ =~ eval('[",,,,,"'+ '",'*n + '  ?=].join#"].join("3x+1?")'))

という式で実現しています (上のプログラムはこれを読みにくくしたものです)． eval 式で生成された文字列に対して正規表現 /(.)...\1=/ でマッチングを行い，マッチした位置が n に代入されます． " が偶数個か奇数個かによって最後の " が文字列の終了を表すか開始を表すかという意味が変わるため，この結果 eval 式が返す文字列が変わるというカラクリです． n が偶数のときは，上の eval 式の引数が

⇒ '[",,,,,"'+ '",' + '",' + '",' + ... + '",' + '  ?=].join#...'
⇒ '[",,,,,"",",",...",  ?=].join#...'

と評価され，最後の " は文字列の終了を表します．ここで，",,,,,""," の部分に違和感を感じる方がいらっしゃるかもしれません．私もこのプログラムを作成する前は知らなかったのですが， Ruby ではダブルクオートやシングルクオートによる文字列リテラルを列べて書いてもよいようで， "ab""cd" は "abcd" と同等だそうです．したがって，",,,,,""," は ",,,,,," を表します． join の後ろの #以降はコメントとして eval の際には無視されます． ", を n 個連結すると ",", が n/2 個続くことになるので，上の式の評価結果は ",,,,,...,=" となります．先頭の ",,,,," を含めると , の個数は 5 + n/2 となり，正規表現 /(.)...\1=/ がマッチするのは末尾の ,,,,,= ですので，その位置は n/2 番めとなるわけです．

n が奇数のときはどうでしょう． eval 式の引数は

⇒ '[",,,,,"'+ '",' + '",' + '",' + '",' + ... + '",' + '  ?=].join#"].join("3x+1?")'
⇒ '[",,,,,"",",",",...,",  ?=].join#"].join("3x+1?")'

と評価され，最後の ", は文字列の開始になるため， ...join#" までの文字列が配列の最後の要素になります．この文字列の配列を 3x+1? という文字列を結合するので，最終的には

",,,,,,3x+1?,3x+1?,...,3x+1?,  ?=].join#"

という文字列になります．配列の要素は (n+1)/2 個なので，eval によって間に3x+1? が (n-1)/2 個入った文字列が得られます．この文字列に，正規表現 /(.)...\1=/ がマッチするのは末尾の方にある ?, ?= であり，その前には先頭の ,,,,, と , が (n+1)/2 個と 3x+1? が (n-1)/2 個 (このうち最後の1個の末尾の ? はマッチの開始位置) あるので，マッチする位置は 5+(n+1)/2+(n-1)/2*5-1 = 3*n+1 となるわけです．ただし，これは n が 3 以上の奇数の場合です． n = 1 のときは配列の要素が 1 つであり 3x+1? が入らないため，正規表現 /(.)...\1=/ にはマッチしません．その結果，n が nil となり while 文が終了するわけです．

ここまでの説明を呼んでお気づきになった方もいらっしゃると思いますが，このプログラムに出てくる 3x+1 は基本的にはどんな文字列でもかまいません (= が含まれるとややこしくなりますが)．今回の作品で 3x+1 という文字列を選んだのは，コラッツ予想が 3x+1 問題とも呼ばれるためです．実はここに自分のハンドル名でも入れようとか思っていたのですが，投稿規定に反するということでやめました (この規定に反してしまった人(主催者?)もいたようですが…)．

おわりに

説明を書いてみたら remarks.markdown とほとんど同じことを書いてしまった気がします．日本語で読む人も多いと思いますので，一応意味はあるのかもしれません．もちろん TRICK の性質上，こんなものを読んでも何も得られないわけで，意味なんてないはずですが，話のネタにでもなれば幸いです．今回初めての参加でしたが，次回もネタがあれば参加してみたいですね．何としても 3 連覇は阻止しないといけませんから．

第 5 位 最短 SAT ソルバ

第 2 位 コラッツ列生成プログラム

おわりに

第 5 位最短 SAT ソルバ

第 2 位コラッツ列生成プログラム