強力なSATソルバーテクノロジーは、悪名高いCollatz仮説で機能します。ただし、この可能性はそれほど高くありません。
過去数年間、Mariin Hijulは、SATソルバー（満足度を表すSAT）と呼ばれるコンピューター化された証明検索テクノロジーを使用して、数学的な問題の印象的なリストを克服してきました。2016年のピタゴリアントリプレット、2017年のSchurの5位、そして最近、「コンピューター検索は90年前の数学的問題に対処するのに役立った」という記事で、少し前に書いた7次元のKellerの仮説。
しかし今、カーネギーメロン大学のコンピューター科学者であるヒジュールは、さらに野心的な目標に目を向けました。それは、数学で最も難しい未解決の問題であると多くの人が考えているコラッツの推測です（そしておそらく最も簡単に定式化できます）。キユルがそのような試みをしていることを私から知った他の数学者は、それについて懐疑的でした。
「SATソルバーを使用してこの問題を完全に解決する方法がわかりません」と、コンピューター証拠の第一人者であるピッツバーグ大学のトーマス・ヘイルズは述べています。このテクノロジーは、本質的に、数学者が問題を個別の有限の問題に変えることによって、問題を解決するのに役立ちます。問題の中には、無限の数のオプションがあります。
しかし、ヘイルズは他の人たちと同様に、キユルを過小評価することを警戒していました。 「彼はSAT言語で問題を定式化する巧妙な方法を見つけるのが非常に得意です。彼はそれがとても上手です。」
スコットアーロンソンテキサス大学オースティン校のコラッツ推測でヒユルと協力して、次のように付け加えました。「マリンはハンマーを持った男、つまりSATソルバーであり、おそらく世界でこのハンマーの最も価値のある持ち主です。そして、彼はそれをほとんどすべてに適用しようとしています。」しかし、彼がコラッツの仮説を釘に変えることができるかどうかは、時が経てばわかるでしょう。
SATソリューションでは、提案ロジックを使用するコンピューターが理解できる言語で問題を再定式化し、コンピューターを接続して、これらのステートメントを真にする方法があるかどうかを判断する必要があります。これが簡単な例です。
あなたが育児を手配しようとしている親であるとしましょう。あなたの乳母の1人は火曜日と木曜日を除いて一週間働くかもしれません。もう1つは火曜日と金曜日以外です。 3番目-木曜日と金曜日を除く。あなたは火曜日、木曜日、金曜日にあなたの子供と一緒に座る必要があります。これは達成できますか？
これをテストする1つの方法は、乳母の制約を式に変換し、SATソルバーにフィードすることです。プログラムは、式が真である、つまり「満足」していることが判明するように、つまり、必要な3日間を取得できるように、乳母の間で日数を分配する方法を探します。成功した場合、そのような方法が存在します。
残念ながら、最も重要な数学的質問の多くをSAT言語に再定式化する方法はすぐには明らかではありません。しかし、時には予期しない方法で満足度の質問と言い換えることができます。
「タスクが巨大であるが有限の計算にいつ削減されるかを予測するのは難しいです」とアーロンソンは言いました。
Collatzの推測は、最初は乳母の問題とはまったく思えない数学の質問の1つです。彼女は次のことを提案します：任意の数（整数、ゼロ以外）を取ります。奇数の場合は3を掛け、1を足します。偶数の場合は2で割ります。その結果、新しい数値が得られます。同じルールを適用して続行します。この仮説では、開始番号に関係なく、最終的に1になり、その後、1、4、2、1のループでスタックすることが予測されます。
そして、この仮説がほぼ100年間使用されてきたという事実にもかかわらず、数学者はそれを証明することに近づいていません。
しかし、これはキユルを止めませんでした。 2018年、彼とアロンソンは、大学の同僚でありながら、国立科学財団からSATソルバーをコラッツの推測に適用するための助成金を受け取りました。
任意の数を取ります。奇数の場合は3を掛け、1を足します。偶数の場合は2で割ります。その結果、新しい数値が得られます。同じルールを適用して続行します。 1にならない数字を見つけられますか？自分で試すことができます。
まず、コンピューター科学者のアーロンソンは、コラッツ仮説の別の定式化、いわゆるを思いついた。コンピュータの操作を容易にする「代替ルールシステム」。
置換ルールシステムでは、文字A、B、Cなどの文字のセットを操作します。これらを使用してシーケンスを形成します：ACACBACB。これらのシーケンスを変換するためのルールもあります。 ACに出会ったら、それをBCに置き換えるというルールがあります。他の人は航空機をAAAに置き換えることができます。変換を定義するルールはいくつでも設定できます。
コンピュータ科学者は一般に、特定のJVが常に終了するかどうかを知る必要があります。つまり、どの行から開始し、どの順序でルールを適用するかに関係なく、その行が最終的にルールを適用できない状態になるというのは本当ですか？
アーロンソンは、コラッツの仮説と同様に、7つのシンボルと11のルールを備えたSPを考案しました。彼のJVが常に終了することを証明できれば、それによって仮説が正しいことを証明できます。
Collatzの推測をSATソルバーの問題に変えるために、AaronsonとHiyulは、行列または数値の配列を含む別のステップを踏まなければなりませんでした。 SP内の各シンボルに一意のマトリックスを割り当てる必要がありました。このアプローチ（SPが作業を終了しているという証拠を探す一般的な方法）により、マトリックス乗算による数値変換について推論することができます。 SPで7つのシンボルを示す7つのマトリックスは、11のルールの相互の対応を反映して、一連の制約全体を満たす必要がありました。
「まず、これらの制約を満たす行列を見つけようとします」と述べています。カーネギーメロン大学の博士課程の学生であるEmreYolchuは、Hijulでこの問題に取り組んでいます。 「成功すれば、実行が停止することを証明できます」。したがって、Collatzの仮説は正しいです。
SATソルバーは、これらの制約を満たすマトリックスの存在の問題に答えることができます。 AaronsonとHijulは、最初に小さな2x2マトリックスでSATソルバーを実行しました。彼らは実用的な選択肢を見つけられませんでした。次に、3x3マトリックスを試しました。そして再び役に立たない。彼らは、それらが見つかることを期待して、マトリックスのサイズを増やし続けました。
ただし、適切なマトリックスを検索する複雑さはサイズとともに指数関数的に増大するため、このアプローチは無期限に進化することはできません。 Hijulは、最近のコンピューターは12x12より大きいマトリックスを処理できないことを示唆しています。
「マトリックスが複雑になりすぎると、問題を解決できなくなります」と彼は言いました。
Hijulはまだ検索の最適化に取り組んでおり、SATソルバーがますます大きな行列をチェックできるように検索をより効率的にしようとしています。彼女と彼女の同僚は、彼らの現在の発見を要約した記事に取り組んでいますが、彼らはほとんどアイデアがなく、おそらくすぐに-少なくともしばらくの間、あきらめなければならないでしょう。
結局のところ、SATソルバーの魅力は、別のケースをチェックする方法、別の乳母に電話する方法、少しでも検索を延長する方法しかわからない場合、おそらく探しているものを見つけることができるということです。この意味で、キユルの主な利点は、SATソルバーの経験ではなく、結果の追求に対する彼の愛情である可能性があります。
「私はただの楽観主義者です」と彼は言いました。「運が良かったと感じることが多いので、どこまで行けるか試してみます。」