コンピュータ支援による証明が「パッキングカラーリング」問題を解決する

コンピュータ支援による証明が「パッキングカラーリング」問題を解決する

チリ大学の学部生だったベルナルド・スベルカソーは、コンピューターを使って数学をすることに対して否定的な見方をしていた。それは真の知的発見とは相反するものだと思われていたからだ。

「問題を解決するためにコンピューターを使うことに対しては、素晴らしい議論の理想的な美しさや優雅さに反するかのように、本能や直感的に抵抗感がある」と同氏は語った。

しかし2020年、スベルカソーは恋に落ち、よくあるように、彼の優先順位は変わった。彼が夢中になったのは、オンラインフォーラムで見かけたある質問だった。たいていの問題はざっと目を通すだけで忘れてしまうのだが、この質問は目に留まり、右にスワイプした。

「私が最初にしたのは、Facebook グループの投稿に「いいね!」をして、後で誰かが解決策を投稿したときに通知が届くようにすることだった」と彼は語った。

問題は無限の格子を数字で埋めるというものだった。結局のところ、それは思いつきで解けるような問題ではなかった。この問題を解決するために、スベルカソーはチリを離れ、カーネギーメロン大学の大学院に進学しなければならなかった。

そこで2021年8月、彼はマライン・ホイレ氏と幸運な出会いを果たしました。ホイレ氏は、膨大な計算能力を駆使して難解な数学問題を解くコンピューター科学者です。シュベルカソー氏はホイレ氏に、この問題に挑戦してみたいかと尋ねました。これが二人の共同研究の始まりとなり、今年1月には、15という一つの数字で要約できる証明が完成しました。

あらゆる可能な方法

2002年、クレムソン大学のウェイン・ゴダード氏と志を同じくする数学者数名が組合せ論の問題を考察し、一定の制約のもとで地図に色を付けるというこの分野の主流の問題に新たな展開を加えようとしていた。

最終的に彼らは、無限に続く方眼紙のようなグリッドから始まる問題にたどり着きました。目標は、グリッドを数字で埋め尽くすことです。ただ一つ制約があります。同じ数字が出現するたびに、その数字自体よりも大きな距離を置かなければならないのです。(距離は垂直方向と水平方向の距離を合計することで測定されます。この距離は、格子状の街路を移動する様子に似ていることから「タクシー」距離と呼ばれています。)1のペアは、タクシー距離が1である隣接するセルには配置できませんが、距離が2である対角セルには配置できます。

ベルナルド・スベルカソ

ベルナルド・スベルカソーは友人に、マインスイーパーのようなゲームを作ってもらい、考えられる解決策を素早く試すことができた。写真:エドワード・チェン

当初、ゴダードと共同研究者たちは、無限の格子を有限の数の集合で埋めること自体が可能かどうかを知りたかった。しかし、2008年にゴダードと4人の共同研究者がこの「パッキング彩色」問題をArs Combinatoria誌に発表した時点で、22個の数で解けることを証明していた。同時に、5個の数だけでは解けないことも分かっていた。つまり、問題の真の答え、つまり必要な最小の数はその中間にあるということだ。

研究者たちは実際に無限のグリッドを埋め尽くしたわけではない。そうする必要もなかったのだ。グリッドの小さな部分集合、例えば10×10の正方形を取り、そこに数字を詰め込み、その詰め込んだ部分集合のコピーを、床をタイルのコピーで覆うように、隣り合わせに並べられることを示すだけで十分だ。

スベルカソーがこの問題を初めて知ったとき、彼はペンと紙を使ってタイルを探し始めた。数字のグリッドを描き、線を引いて消して、また試す、という繰り返しだった。すぐにそのやり方に飽きてしまい、友人に頼んで、マインスイーパーに似た、組み合わせをより速くテストできるウェブベースのツールを設計してもらうことにした。さらに数週間作業を続け、グリッドに8つの数字を詰め込むことは不可能だと確信したが、それ以上のことは考えられなかった。タイルの形があまりにも多すぎて、数字を詰め込む方法もあまりにも多すぎたのだ。

問題は、後に明らかになるが、特定の数の集合でグリッドをカバーできないことを示すのは、カバーできることを示すよりもはるかに難しいということだ。「一つの方法が機能しないことを示すだけでなく、あらゆる方法が機能しないことを示す必要があるのです」とゴダードは述べた。

スベルカソーがCMUに着任し、ヒューレを説得して共同研究を始めさせた後、彼らはすぐにグリッドを15個の数字で覆う方法を発見した。また、12個の数字だけで問題を解く可能性も排除できた。しかし、彼らの勝利の喜びは長くは続かなかった。彼らは、それが長年存在していた結果を再現したに過ぎないことに気づいたのだ。2017年には既に、研究者たちは答えが13未満でも15以上でもないことを知っていたのだ。

マライン・ホイレ

マライン・ホイレ氏は、コンピューターのパワーを活用して数学の難問の解決を推し進めることに特化している。写真:カーネギーメロン大学

有名教授を自分の得意とする問題に取り組ませた大学院1年生にとって、それは不安を掻き立てる発見だった。「ゾッとしました。何ヶ月も前からこの問題に取り組んでいたのに、それに気づかなかったんです。しかも、マライン教授の時間を無駄にさせてしまったんです!」と、スベルカソーは研究を振り返るブログ記事に記した。

しかし、ホイレは過去の研究結果の発見に刺激を受けた。それは、他の研究者たちがその問題に取り組む価値があるほど重要だと認識していることを示し、得る価値のある唯一の結果は問題を完全に解決することだと確信させた。

「この問題に20年も取り組んできたことがわかって、状況は完全に変わりました」と彼は語った。

下品なものを避ける

ヒューレは長年にわたり、膨大な組み合わせの中から効率的な方法を見つけることでキャリアを築いてきました。彼のアプローチはSAT(satisfiability:満足可能性)解決と呼ばれています。これは、0か1の2つの結果を取り得るブール式と呼ばれる長い式を構築するものです。結果が1であれば、式は真であり、問​​題は満たされます。

詰め込み彩色問題では、式中の各変数は、特定のセルに特定の数字が配置されているかどうかを表します。コンピュータは、式を満たすように変数を割り当てる方法を探します。コンピュータがそれを実行できれば、設定した条件でグリッドを詰め込むことが可能であることがわかります。

残念ながら、パッキングカラーリング問題をブール式として単純にエンコードすると、数百万項に達する可能性があり、コンピューター、またはコンピューター群でさえ、その内部で変数を割り当てるさまざまな方法をすべてテストしながら永遠に実行できる可能性があります。

「この力ずくの計算を単純にやろうとすると、宇宙が終わるまでかかるでしょう」とゴダードは言った。「ですから、それを実現可能なレベルまで下げるには、クールな単純化が必要なのです。」

さらに、パッキング彩色問題に数字を追加するたびに、可能な組み合わせが倍増するため、問題は約100倍難しくなります。つまり、並列に動作するコンピュータ群が1日の計算で12を除外できるとしても、13を除外するには100日の計算時間が必要になります。

ヒュール氏とスベルカソー氏は、力ずくの計算手法をスケールアップすることは、ある意味では下品だと考えていました。「いくつか有望なアイデアがあったので、『クラスター上で48時間以内にこの問題を解けるようになるまで、アプローチを最適化しよう』という考え方を採用しました」とスベルカソー氏は語ります。

そのためには、コンピューティング クラスターが試行する必要がある組み合わせの数を制限する方法を考え出す必要がありました。

「彼らはただ解決したいのではなく、印象的な方法で解決したいのです」とコロラド大学コロラドスプリングスのアレクサンダー・ソイファー氏は語った。

ヒュールとスベルカソーは、多くの組み合わせが本質的に同じであることを認識しました。ダイヤモンド型のタイルを8つの異なる数字で埋めようとする場合、最初に置く数字が中央のマスから1つ上と1つ右であっても、1つ下と1つ左であっても問題ありません。どちらの配置も互いに対称的であり、次の動きを全く同じように制限するため、両方を確認する必要はありません。

数字が詰まったダイヤモンド形の多色のチェス盤模様

もしすべての詰め込み問題がチェス盤のパターン、つまり1の対角線グリッドが空間全体を覆う(チェス盤の暗い部分のように)ことで解けるなら、計算は大幅に簡素化されるだろう。しかし、この14個の数字が詰め込まれた有限のタイルの例のように、必ずしもそうではない。チェス盤のパターンは、左上に向かっていくつかの場所で破られる必要がある。(提供:Bernardo Subercaseaux、Marijn Heule)

ヒュール氏とスベルカソー氏は、対称的な組み合わせをコンピューターが同等とみなせるようにする規則を追加し、全体の探索時間を8分の1に短縮しました。また、ヒュール氏が以前の研究で開発した「キューブ・アンド・コンカー」と呼ばれる手法も活用し、より多くの組み合わせを並行してテストできるようになりました。あるセルに3、5、または7のいずれかの数字が含まれていることが分かっている場合、問題を分割し、3つの可能性をそれぞれ異なるコンピューターセットで同時にテストすることができます。

2022年1月までに、これらの改良により、HeuleとSubercaseauxは2日未満の計算時間を要する実験において、パッキング彩色問題の解答として13を除外することができました。これにより、14または15という2つの解答候補が残りました。

大きなプラス

14 を除外して問題を解決するために、Heule 氏と Subercaseaux 氏はコンピューター検索を高速化する追加の方法を見つける必要がありました。

当初、彼らはグリッド内の個々のセルに変数を割り当てるブール式を記述していました。しかし、2022年9月、セルごとに処理を進める必要はないことに気づきました。代わりに、プラス記号の形をした5つのセルからなる小さな領域を検討する方が効果的であることを発見しました。

彼らはブール式を書き直し、複数の変数が「このプラス形の領域内に7はどこかにあるか?」といった疑問を表すようにしました。コンピューターは、7が領域内のどこにあるのかを正確に特定する必要はありませんでした。7がそこにあるかどうかだけを判断すればよかったのです。この疑問に答えるには、はるかに少ない計算リソースしか必要としません。

「特定の場所ではなくプラスだけを表す変数を持つ方が、特定のセル内のプラスについて話すよりもはるかに優れていることがわかりました」と Heule 氏は言います。

プラス探索の効率性に助けられ、ヒュール氏とスベルカソー氏は2022年11月にコンピューター実験で14を除外した。この実験は、13を除外した実験よりも実行時間が短くて済んだ。両氏はその後4カ月をかけてコンピューターの結論が正しいことを確認した。これは、コンピューターが結論に達するのに要した時間とほぼ同じ時間だった。

「私たちが、とある雑誌にちょっとした疑問として投げかけたものが、結局、何ヶ月もかけて人々のグループにその解決方法を考えさせるきっかけになったと考えると、うれしかった」とゴダード氏は語った。

シュベルカソーにとって、それは研究者としてのキャリアにおける最初の真の勝利だった。数学の研究を初めて考えた時に理想としていたタイプの発見ではなかったかもしれないが、最終的には、それ自体が知的報酬をもたらすことを彼は発見した。

「黒板を渡されて、なぜ15なのか説明できるような、形式的な理解ではありません」と彼は言った。「しかし、問題の制約がどのように作用するのか、ここに6、あそこに7があるとどれだけ良いのかを理解することができました。直感的な理解がかなり深まったのです。」

オリジナルストーリーは、数学、物理科学、生命科学の研究の進展や動向を取り上げることで科学に対する一般の理解を深めることを使命とする、 シモンズ財団の編集上独立した出版物であるQuanta Magazineから許可を得て転載されました。