ルービックキューブは26手以内で揃う!
http://slashdot.jp/articles/07/06/05/0527229.shtml
「コンピュータによる全パターンを網羅した証明」ってさ、モゾモゾする部分が、
「そのアルゴリズムに間違いはないのか」
「プログラムの時点でバグは存在していないのか」
って点だよね。これを検証するのが大変で。追証しにくいんだよね。
だから、「エレガントな解法」が好まれるんだと思う。
パターンは限られている「閉じた環境」だから、なんらかの「完全解」があるのは理解できるわけだけど。