アカウント名:
パスワード:
到達した状態を管理するのにもメモリが大量に必要になります。
ルービックキューブについてなら、このパズルの本質は各キューブの配置と移動のさせ方のみであり、モデルはそのままルービックキューブ本体であると言える。 実物と同じ振る舞いをするものはエミュレータと呼ばれる。
この場合は「ルービックキューブをエミュレートして解法を探索した」と表現すべきかと。
この paper で導入している Cayley graph や coset、automorphism はモデルではないということでしょうか。全通りをエミュレートしたのではなく、A* algorithm のように (推定値のままなので途中まで A* で、厳密には A* (optimal) ではない) 途中までの upper bound を見積もって 26 という数字を出しています。
現代では天気予報つったら「シミュレート」に決まっていますが、いつの日か天気予報を「エミュレート」できるようになるのでしょうか。 それはつまり「地球」をエミュレートするということですが...地球エミュレータ? ~以下妄想~ 森羅万象をエミュレート。 ちょっと早送りすれば天気予報も楽々的中。地震雷火事戦争、常に事前予想して回避・解決。 不可避の天変地異が判明し、エミュレート環境を宇宙に打ち上げて脱出。 以降、「あちら側」が人類の「世界」となる。 天変地異が起こったら、設定変更してスナップショットからやり直し。 戦争が起こっても、スナップショットからやり直し。 受験に失敗したら、スナップシ(略 彼女に振られたら、ス(ry 極超並列多重結合演算の果て、ついにエミュレータ群がダウンし、「世界」は終わった。 ...こんなSF小説出てたりして。
しかるに、総当りで全検索したのであればそれは模擬ではないでしょ?
ルービックキューブの世界選手権に出ている人たちの実感は何手くらいなのでしょうね。
最後のひと工夫でさらに3手縮めているところがミソのようですがまだ理解できていません。
最後のひと工夫 (三手縮める) は Kociemba の Cube Explorer で brute force をかけました、ということでしょう。Section 7.3 のまんまです。
Kunkle達はこれをしなかったそうです。
リンク先 (cubezzz.homelinux.org) には
I already told this Daniel Kunkle and he agreed with this.
追実験はそう難しくないはずなので、近いうちにちゃんとした 26 手の証明は完成されると期待したいんですが、それよりも現時点で 26 手の証明がされたというのは誤報なので、これがどう修正されていくかが気になります。
Brute force では 25 手の証明までこのまま一気にされそうな勢いですが、やっぱりアルゴリズム面での工夫と breakthrough がないと面白くないですね。まだ新規参入者のつけいる余地はあるということですか。
四色問題については、「四色問題の証明の『正しさそのもの』を計算機が対話的に検証する」という取り組みがなされています。
同様の手法により、『「ルービックキューブは26手以内で揃う」の証明は正しかった」ことを計算機で実証する人も現れるでしょう。
# 科研費をこのネタで申請するのでAC
数学方面の人だとこの辺り詳しいと思いますが。
「シミュレーションした」と「総当たりした」は,全然違うことだと言いたかったのですが. シミュレーションすることは,証明するための必要条件でも十分条件でもありません.
総当りで証明した →納得 シミュレーションで総当りし、証明した →納得 シミュレーションで証明した →「シミュレーションで○○して証明した」、の○○が何かちゃんと言ってくれよ。 ということでした。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
身近な人の偉大さは半減する -- あるアレゲ人
シミュレーションでは証明にならない (スコア:0)
Re:シミュレーションでは証明にならない (スコア:3, 参考になる)
Re:シミュレーションでは証明にならない (スコア:2, すばらしい洞察)
Re:シミュレーションでは証明にならない (スコア:1)
全て揃った状態を、木構造のルートとして、
次の一回の90度回転操作でできる状態をその子として、
また、次の一回の・・・・・・・・・・・・・・・・・・・・、
を繰り返せば、26回目の操作までに全ての状態が出現する。
証明終わり。
ところで、ルービックキューブが取り得る状態の数っていくらだ?
6^54-回転対称分だから・・・・
ううっ、出直します。
Re:シミュレーションでは証明にならない (スコア:2, 興味深い)
(回した後に回転面を床につければ同じ状態になる)
回す方向は鏡面とすると、無視して考えられる。
最初の一手目は「完成形から一回回した状態」の一パターンしかないので、
完全に揃ってる状態ではなく、一手目を木構造のrootにできるかもしれない、などと思ったり。
#書いた後に不安になってきた。いいのかな?(笑
取り得る状態 (スコア:1)
立方体の合同変換が 6×4 = 24 だから、54!/24 が取り得る状態数。
何か見落としてるような気がするなー。 そうだ、角のcubeは角にしか来れないんだった!
しからば、角のcubeは 8、辺中央のcubeは 12、面中央のcubeは 6
というわけで 8!×12!×6!/24 が取り得る状態数。(ホントにこれで良いのかな?)
実を言うと、ルービックキューブに触ったこともないもんね。
the.ACount
Re:取り得る状態 (スコア:1)
ルービックキューブに触った経験から言うと、
角の1ピースだけが 90度回転するとか、辺の1ピースだけが 向きが反転するとかいった状態は起こらないようです。
Re:取り得る状態 (スコア:0)
よって、エッジとコーナーだけを考えれば良く、位置関係に関しては分解を許せば 12! x 8! 通りありますが、
そのうち半分(奇置換となるもの)は存在しないことが証明可能で他は存在するので、12!x8!/2通り。
エッジの向き(位置は同じでも裏返る場合もある)は、分解を許せば 2^12通りですが、裏返りは実は奇数個にならないことが
分かっているので、2^11通り。コーナーの向きは分解を許せば3^8通りですが、回転数の合計のmod3が0になることが分か
っているので、3^7通り。
よって、 12! x 8! x 2^10 x 3^7 = 43252003274489856000通りで、alchematon氏のコメントにある数字で正しいです。
Re:シミュレーションでは証明にならない (スコア:1, 興味深い)
到達した状態を管理するのにもメモリが大量に必要になります。
逆に不揃いから揃える方向ならば、6面が揃ったというチェックは簡単に実装できます。
また初期状態の全パターンは再帰を使えば簡単に生成できるのでメモリコストは少しですみます。
その各状態から26手まで総当りですが、26手を総当りで試して、26手以内に6面揃えばその初期パターンは26手以内であると確認されるので打ち切れます。
これも再帰を使えば26手までは十分試せるでしょう。
これである初期状態から26手総当りを行っても6面が揃わなければ26手以内では揃わない初期状態があると証明できます。
#どっちにしても計算量は膨大ですね
Re:シミュレーションでは証明にならない (スコア:1)
ルービックキューブの状態を一意で密なハッシュ値であるidに変換できれば
(つまり全ての状態に0から始まる一意なIDが付けられれば)、解を根とする木構造を深さ26までの
深さ優先探索で総当りしながら、たどり着いたノードの状態のハッシュをメモリにキャッシュして、
適当にたまったところでHDDのidビット目に1を上書していけば、最後に全ての状態に対してビットが
立っているか確認するだけでいいので。
ってなわけで問題は結局、
って部分に集約されるのではないかと。
全ての状態に対して到達しているかしていないかを1bitで表したとしても、約5エクサバイト
(43,252,003,274,489,856,000bit)の補助記憶領域が必要な訳で、メモリほど高速である
必要がないのでHDDでOKって事を考えても現実的かは微妙な容量ですね。
ただ、不揃いから揃える場合の初期状態数(43,252,003,274,489,856,000)と、それぞれそこから
下手すると深さが26の木を辿らなきゃいけないって事を考えれば(解からなら1回辿るだけでOK)、
解から辿った方が現実的なやり方だと思います。
Re:シミュレーションでは証明にならない (スコア:2, 参考になる)
(というか逆方向を取る時点で枝切りされる)
Re:シミュレーションでは証明にならない (スコア:0)
Re:シミュレーションでは証明にならない (スコア:0)
Re:シミュレーションでは証明にならない (スコア:2, 参考になる)
天気予報は気象モデルを作ってごにょごにょするので、シミュレートしていると言える。
ルービックキューブについてなら、このパズルの本質は各キューブの配置と移動のさせ方のみであり、モデルはそのままルービックキューブ本体であると言える。
実物と同じ振る舞いをするものはエミュレータと呼ばれる。
この場合は「ルービックキューブをエミュレートして解法を探索した」と表現すべきかと。
元論文を読みましたか? (スコア:1)
この paper で導入している Cayley graph や coset、automorphism はモデルではないということでしょうか。全通りをエミュレートしたのではなく、A* algorithm のように (推定値のままなので途中まで A* で、厳密には A* (optimal) ではない) 途中までの upper bound を見積もって 26 という数字を出しています。
内部構造まで再現すべき (スコア:1, すばらしい洞察)
よって、表面のパズル性だけを取り出したモデルはしょせんモデルであり、シミュレーションの名で呼ばれるべきでしょう。
エミュレート(妄想系オフトピ) (スコア:1)
現代では天気予報つったら「シミュレート」に決まっていますが、いつの日か天気予報を「エミュレート」できるようになるのでしょうか。
それはつまり「地球」をエミュレートするということですが...地球エミュレータ?
~以下妄想~
森羅万象をエミュレート。
ちょっと早送りすれば天気予報も楽々的中。地震雷火事戦争、常に事前予想して回避・解決。
不可避の天変地異が判明し、エミュレート環境を宇宙に打ち上げて脱出。
以降、「あちら側」が人類の「世界」となる。
天変地異が起こったら、設定変更してスナップショットからやり直し。
戦争が起こっても、スナップショットからやり直し。
受験に失敗したら、スナップシ(略
彼女に振られたら、ス(ry
極超並列多重結合演算の果て、ついにエミュレータ群がダウンし、「世界」は終わった。
...こんなSF小説出てたりして。
May the music be with you.
Re:エミュレート(妄想系オフトピ) (スコア:0)
下駄の事?
Re:シミュレーションでは証明にならない (スコア:0)
私自身は、ここで「エミュレータ」という言葉を使うのは違和感があります。
エミュレータというのは「本物と置き換え可能」程度の強い意味があると思います。
人間にとってみれば、計算機内のメモリの内容が変化するだけでは、
本物のルービックキューブと同じようには遊べません。
また、たとえエミュレータと呼べるとしても、それはシミュレータと呼べないこととは別ではないでしょうか。
Re:シミュレーションでは証明にならない (スコア:0)
あくまで模擬であって、実際とは違うからシミュレーションだろう。
しかるに、総当りで全検索したのであればそれは模擬ではないでしょ?
元コメントはそういう意味だと思うんだが・・・
Re:シミュレーションでは証明にならない (スコア:1, おもしろおかしい)
Re:シミュレーションでは証明にならない (スコア:2, おもしろおかしい)
Re:シミュレーションでは証明にならない (スコア:0)
たとえば総当りでなく10通り程度の実験だったら、それは模擬?
Re:シミュレーションでは証明にならない (スコア:0)
ないのかな?総当りでやってたならば示されてしまってるということに
もなりそうなんだけど.
枝刈りの仕方とかからまだ言えないのかしら.
Re:シミュレーションでは証明にならない (スコア:0)
他にもっと効率のよいアルゴリズムがあるのかもしれません。
つまり、総当りというのは初期状態のことであって、経路では ないのです。
ルービックキューブの世界選手権に出ている人たちの実感は何手くらいなのでしょうね。
Re:シミュレーションでは証明にならない (スコア:3, 参考になる)
こっちのページ [physorg.com]には論文へのリンクがあります。これから読んでみます。
ちなみに世界選手権でいちばんメジャーな解法である「LBL法」では平均56手くらいです。
自分で解きながら数えたこともありますがおおむね50~60手くらいです。
最小手数を競う競技もあります。
紙と鉛筆だけを使って1時間以内に見つかった解の手数を使います(公式ルール [jrca.cc]内のArticle E参照)。
公式世界記録 [worldcubeassociation.org]では28手、非公式記録 [speedcubing.com]では21手というのが今日現在の記録のようです。
Re:シミュレーションでは証明にならない (スコア:3, 参考になる)
そこまでの最大手数、そこからの最大手数の和を計算したそうです。
最後のひと工夫でさらに3手縮めているところがミソのようですがまだ理解できていません。
Wikipediaの記事 [wikipedia.org]では、ルービックキューブの最短手数探索法について、
Thistlethwaiteによる4段階法、Kociembaによる2段階法が解説されています。
CoopermanとKunkleの方法は、同じように表記すれば、
G0=<L,R,F,B,U,D>
G1=<L2,R2,F2,B2,U2,D2>
と部分問題を設定した場合に相当します。
CoopermanとKunkleはcosetの要素全体に対して総当たり的に到達可能手数をさがしています。
このような方法だと、必ずG1を通るような経路しか計算していないので、手数のupper boundしか得られません。「G1を通れば26手で解ける状態」にも、G1を一度も通らないようなより短い手数が存在する可能性が残ります。
高田馬場から東京まで、東西線を必ず使うとして、大手町へ出るとか九段下へ出るとか、全部の場合を調べて遅くとも何分で着く、とはわかった。しかし東西線を使わない場合(JRだけとかタクシーとか)は調べていない、というような感じ。
Re:シミュレーションでは証明にならない (スコア:2, 参考になる)
最後のひと工夫 (三手縮める) は Kociemba の Cube Explorer で brute force をかけました、ということでしょう。Section 7.3 のまんまです。
26手以下という証明はできていなかった (スコア:1)
この中で、レベル3までのcosetとレベル12と13のハーフターン部分群要素の積について、brute forceのかけ方が足りなかったことが、Herbert Kociembaの指摘 [homelinux.org](コメントを見るにはログインが必要)によってわかったそうです。彼らはレベル3のcoset 23個と624個の部分群要素の積、約1.4万個を作成してCube Explorerにかけました。論文の方法ではレベル13のcosetについては、3+13つまり16手以内であることしか証明できないので、実際に最適解を求めてみて14手以内だった、上限を2手縮めた、と主張してたわけです。
23も624も、ともに対称性を使って要素数を減らした結果の数え上げなので、積を計算するときには少なくとも片方は48通りに回転させなければなりません。Kunkle達はこれをしなかったそうです。
そんなわけで、「ルービックキューブは26手以内で揃う」という証明は未完成です。計算し忘れた分の中に14手以内で解けない状態がもし見つかったら、この論文では証明できなかったことになります。もちろん追加でCube Explorerを回してみたら、全部14手以内で解けるかもしれません。しかしそれよりは、論文のSection 6に示されている方法で調べた方が早く結果がわかるかもしれません。
Re:26手以下という証明はできていなかった (スコア:1)
リンク先 (cubezzz.homelinux.org) には
とあるので、そのうち Kunkle から何かコメントがあるかもしれませんね。追実験はそう難しくないはずなので、近いうちにちゃんとした 26 手の証明は完成されると期待したいんですが、それよりも現時点で 26 手の証明がされたというのは誤報なので、これがどう修正されていくかが気になります。
Brute force では 25 手の証明までこのまま一気にされそうな勢いですが、やっぱりアルゴリズム面での工夫と breakthrough がないと面白くないですね。まだ新規参入者のつけいる余地はあるということですか。
Re:シミュレーションでは証明にならない (スコア:1)
Re:シミュレーションでは証明にならない (スコア:1)
Re:シミュレーションでは証明にならない (スコア:0)
Re:シミュレーションでは証明にならない (スコア:2, 参考になる)
バグの可能性も否定できないので、数学による証明が待たれます。
Re:シミュレーションでは証明にならない (スコア:2, 参考になる)
数え上げが数学ではない。という論調が見受けられますが、それは間違いです。
事実が証明できるなら、それは数学です。
エレガントではない、エレファントな解法だ。ってことで好まれないことは事実ですが。
それに、背理法や帰納法だって、最後に待っているのは数え上げでしょ?
かのガウスも、この手の数値実験を好んでいた。といわれています。
Re:シミュレーションでは証明にならない (スコア:1, 興味深い)
四色問題については、「四色問題の証明の『正しさそのもの』を計算機が対話的に検証する」という取り組みがなされています。
同様の手法により、『「ルービックキューブは26手以内で揃う」の証明は正しかった」ことを計算機で実証する人も現れるでしょう。
# 科研費をこのネタで申請するのでAC
Re:シミュレーションでは証明にならない (スコア:0)
数学ではないでしょうけど。
実際、どんなねらいがあってこんなことやったのだろうか…。
Re:シミュレーションでは証明にならない (スコア:0)
数学方面の人だとこの辺り詳しいと思いますが。
Re:シミュレーションでは証明にならない (スコア:1)
「シミュレーションした」と「総当たりした」は,全然違うことだと言いたかったのですが. シミュレーションすることは,証明するための必要条件でも十分条件でもありません.
Re:シミュレーションでは証明にならない (スコア:1)
Re:シミュレーションでは証明にならない (スコア:0)
そんな主張は誰もしていないと思うけど……。
Re:シミュレーションでは証明にならない (スコア:0)
どう考えても、君の言いたいことが伝わらない。
「総当たりした」・・・全ての組み合わせについて試行した。
「シミュレーションした」・・・実際にキューブを操作せずに数値計算で代用した。
「シミュレーションした」って語に「総当りせずに代表例だけに絞った」なんて意味はありません。
ここまで書いて気がついたが、もしかしてシミュレーション全てがモンテカルロシミュレーションだとか思ってるとか。
Re:シミュレーションでは証明にならない (スコア:0)
「単に総当りで調べたというだけなのでは?」と書いたら、
「単に総当りでシミュレーションするだけでは証明にならない」と言っていると
思うのが普通でしょう。
Re:シミュレーションでは証明にならない (スコア:1)
総当りで証明した →納得
シミュレーションで総当りし、証明した →納得
シミュレーションで証明した →「シミュレーションで○○して証明した」、の○○が何かちゃんと言ってくれよ。
ということでした。
Re:シミュレーションでは証明にならない (スコア:0)
Re:シミュレーションでは証明にならない (スコア:0, オフトピック)
そのとおりだと思います。証明としてスマートではないだけです。
私は2年に1度の頻度で必ず(といっていいほど)確率の問題が
出題される大学の試験で、出題された確率の問題をすべて数え上げて
回答しました。試験時間の1/3を費やしたけど、確実に完答出来た
甲斐はありました(合格した)
#全二百数十通りあったけどね。
Re:シミュレーションでは証明にならない (スコア:0, 余計なもの)
http://ja.wikipedia.org/wiki/%E5%9B%9B%E8%89%B2%E5%95%8F%E9%A1%8C [wikipedia.org]