SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme

あなたは、巨大な三次元のジグソーパズルを解こうとしているところだと想像してください。しかし、これは夕焼けや猫の写真ではありません。それは、2つの数字のグリッドを掛け合わせるために設計された数学的な機械です。コンピュータサイエンスや数学の世界では、これは「行列積（マトリックス・マルチプリケーション）」と呼ばれます。何十年もの間、数学者たちはこの機械を作るための最も効率的な方法を追い求めてきました。彼らは、この仕組み全体を機能させるために必要な、最小限の基本的で小さな構成要素（「乗算」と呼ばれます）の絶対的な数はいくつかを知りたいと考えています。

これらの構成要素をレゴブロックだと考えてください。長い間、誰もが3x3の乗算マシンを作るには23個のブロックが必要であることを知っていました。大きな疑問は、「では、22個だけで作れるのか？」ということでした。この答えを見つけるために、研究者たちはこの問題を、ビデオゲームや数独の本にあるような巨大な論理パズルへと変貌させました。彼らは、数学のルールをコンピュータがチェックできる形式にエンコードし、「SAT」問題（充足可能性問題）と呼ばれるものを作り上げました。もしコンピュータが、ルールを破ることなくすべてのスイッチを「オン」にする方法を見つけられれば、そのパズルは解けたことになります。もしコンピュータが「不可能」と言えば、おそらく22個のブロックでは足りないということになります。この論文は、私たちの現在のコンピュータの限界と、これらの数学的機械に対する理解をテストするために設計された、こうした特定の論理パズルの集合について掘り下げています。

---

「不可能」ではなかった偉大なパズル

デジタル探偵であるニック・パラディノス（Nick Palladinos）は、他の誰もが諦めてしまった10個の論理パズルのセットに対して、新鮮な視点で再検討を行うことにしました。「チャレンジ2」として知られるこれらのパズルは、非常に具体的で厳格なルールを持つ他の研究者たちによって作成されました。パズルの作成者たちは、これらは解くのが「不可能」であると考えていました。彼らは、ルールがあまりにも厳しいため、23個のレゴブロックのどの組み合わせを用いてもマシンを組み立てることは不可能だと信じていたのです。それは、「ここに鍵のかかった箱がある。この鍵を開けることは絶対にできない」と言われ、周囲の全員がただ頷いて立ち去ったような状態でした。

しかし、パラディノスは大きなハンマーで無理やり鍵を開けようとしたわけではありません。代わりに、彼は鍵そのものを観察し、決定的なことに気づきました。ルールは、人々が思っていたほど厳格ではなかったのです。

パズルの作成者たちは、「ポジティブ」な指示を使ってルールを書いていました。彼らは、「ここにはこの特定のブロックがなければならない」とか「あそこにはあのブロックがなければならない」と言いました。しかし、「そして、これらのブロックに他のブロックを触れさせてはいけない」ということを言い忘れていたのです。結局のところ、最終的なマシンが正しく機能する限り、余分なブロックを追加することは数学的に可能です。「不可能」とされたパズルは、実は単に、誰かが「箱が実はもう少し大きくなれる」という事実を無視して、パズルのピースを小さすぎる箱に押し込もうとしていたために、扉が開くのを待っていただけだったのです。

シフトとスワップの魔法

では、パラディノスはどうやってこれらを解いたのでしょうか？ 彼は「対称性」を用いた巧妙なトリックを使いました。ルービックキューブを想像してみてください。キューブ全体をひねったり回転させたりしても、色は移動しますが、キューブ自体は同じ物体です。パラディノスは、自分が作っている数学的な「マシン」も同様の性質を持っていることに気づきました。彼は、動作する解（行列を正しく掛けることができる23個のブロックのセット）を取り出し、「GL(3, 2)群作用」と呼ばれる特別な数学的なダンスを用いて、パーツをひねったり、回転させたり、シャッフルしたりすることができました。

これは、部屋の家具を配置換えするようなものです。ソファを左に動かし、ランプを右に動かし、ラグを中央に置くことができます。部屋は依然として部屋であり、家具は依然として機能しますが、レイアウトは異なります。パラディノスは、既知の動作する解を取り出し、これらの数学的な「ひねり」を加えました。そして、これらのシャッフルされた新しい家具のレイアウトが、トリッキーなパズルが要求する特定の「スロット」に適合するかどうかを確認するためのマッチングゲームを行いました。

すると、どうでしょう？ 見事にフィットしたのです！

実際、パラディノスは単に一つの解を見つけただけではありません。彼は、不可能だと思われていたすべてのパズル（全10個）に対して解を見つけ出しました。彼は、これらの「解けない」はずの公式が、実は「充足可能（satisfiable）」であることを証明したのです。コンピュータは単に推測したのではなく、あらゆるルールをチェックしました。この論文は、これらすべての「チャレンジ2」のファイルにおいて、23個の構成要素を配置してマシンを機能させる有効な方法が存在することを裏付けています。「不可能」というラベルは、ルールの誤解によるものであり、真の数学的な障壁ではなかったのです。

「ゴースト」ブロックと完璧な解

この論文は、第3の課題である「チャレンジ3」にも取り組みました。これは異なる問いを投げかけています。「23個のブロックを使ってマシンを作れるか。ただし、そのうちの特定の1つのブロックを『ゴースト』にできるか？」数学的に言えば、これは23個の構成要素のうち1つが「タイプ3カウント」がゼロであるべきであることを意味します。これは、これらのマシンによく現れる特定のパターンに、そのブロックが参加しないようにするという、少し凝った言い方です。

パラディノスは、これも成し遂げました。彼は動作する解からスタートし、極めて精密なスワップ（入れ替え）を行いました。彼は、特定の役割を果たしている2つのブロックを取り出し、それらを、同じ仕事をするものの見た目が異なる別の2つのブロックと交換しました。このスワップは非常に巧妙で、特定のパターンを一切引き起こさない「ゴースト」ブロックを作り出しました。彼は、23個のブロックを用いて3x3行列積マシンを構築でき、かつそのうちの1つがその特定のパターンから完全に自由である（トリガーしない）ことを証明しました。

最終チェック

誰もが「コンピュータに運良く当たっただけではないか」と言えないように、パラディノスは超厳格なチェッカーを構築しました。彼は、全21個のパズル（チャレンジ1から10個、チャレンジ2から10個、およびチャレンジ3から1個）の全26,541個の変数（スイッチ）のリストを生成しました。そして、元のパズルのルールと新しい解を読み込み、2,461,316個の論理節（クローズ）のすべてをチェックする別のプログラムを実行しました。

結果はどうだったでしょうか？ 失敗はゼロでした。すべてのルールが満たされていました。解決策は実在し、検証されており、再現可能です。適切なソフトウェアさえあれば、誰でも同じコードを実行して、約9秒で全く同じ答えを得ることができます。

これが意味すること（および意味しないこと）

では、最大の教訓は何でしょうか？ この論文は、「不可能」とされたパズルが実は解けるものであったことを示しています。ルールは、パズル作成者が考えていたほど厳格ではなかったのです。これは、数学やコンピュータサイエンスにおいて、最も困難なことは解を見つけることではなく、問題が思っているほど壊れていないことに気づくことである、ということを思い出させてくれます。

しかし、注意点があります。この論文は、「F2」と呼ばれる特定の数学的世界（数値が1+1=0となるような世界）におけるパズルを解いたものです。これは、私たちが22個のブロックのマシンを作れることを証明したわけではありません。22個のブロックのマシンを求める旅（チャレンジ4）は、依然として未解決のままです。また、この論文は、これらの解がエンジニアリングで使用される複素数のような、現実世界のあらゆる種類の数学で機能することを保証するものでもありません。あくまで、記述された特定の論理パズルを解いたものなのです。

しかし、書かれたパズルに関しては、結論は明白です。「不可能」は、実は「可能」でした。扉はロックされていたのではなく、ハンドルを回すための正しい鍵が必要だっただけなのです。