「SATで挑む平面彩色問題：研究環境構築記録～第1回：数学に詳しくない僕が研究環境を作ろうと思った理由～」

はじめに

僕は数学に詳しいわけではありません。
むしろ苦手です。
大学や研究機関で専門的に数学をやってきたわけでもなければ、グラフ理論や離散幾何に関する体系的な訓練を受けてきたわけでもありません。

正直なところ、研究というものを自力でやれるほどの能力は現状ないわけです。

しかしながら、数学の考え方というものには惹かれるものがあり、苦手なりに学んでいきたいと考えています。

その中で、特に僕が興味を持ったのは、視覚的に表現できる分野です。
それが、平面彩色問題、より具体的にはHadwiger–Nelson problem でした。

未解決問題に取り組むにはあまりにも実力がないのは理解しています。
ですが、面白そうだと思ったことをそのままにしておくのはもったいないと思いました。

そこで、個人的に細々と研究したいなと思った次第です。
そして一応記録を残していれば何かと面白いかと思い、ここに書いていこうと思います。

• 何を問題として扱っているのかを理解
• それを計算機で検証できる形に落とし込み
• 自分で実験できる状態を作る

まず、その入口までたどり着くことを目標にしました。

その第一歩が、今回のシリーズで書いていく研究環境の構築です。

このシリーズでは、数学の研究環境を整えていった過程を順番に記録していきます。今回はその第1回です。

そもそも僕が興味を持った対象は何か

この問題に興味を持ったきっかけは、「平面を何色で塗り分けられるか」という問題を思い出したことです。
昔、ドラマで「4色問題」が扱われていた記憶があり、当時は研究するほどの興味はありませんでしたが、なんとなく記憶に残っていました

• 地図のように区切られた領域があり
• 隣り合う領域どうしが同じ色にならないように塗り分ける

という、いわば「面を塗る問題」ですね。

ところが、Hadwiger–Nelson problem は少し違うものになります。

調べていくうちに分かってきたのは、この問題では「面」を塗るのではなく、平面上の各点に色を割り当てるということでした。しかも禁止される条件も、「近い点は同じ色にしてはいけない」ではなく、距離がちょうど1の2点だけが同色禁止というルールです。

平面を点の集合と考え、その点は面積を持たず、そして条件に従い塗り分ける。
ふと単位円の組み合わせをイメージしたりしましたが、どうもそれだけで表現できるものでもなさそうです。

この時点で、僕の直感はかなり混乱しました。
ですが、だからこそ面白そうだなと思ったのです。

分からなかったことを分からないままにしないために

まだ分からないことだらけです。

• この問題は4色問題とどう違うのか
• 「点に色をつける」とはどういう意味か
• 平面全体を扱う問題なのに、なぜグラフの話になるのか
• unit distance graph とは何なのか
• SATを使うとはどういうことなのか

僕はこの問題を、ChatGPTに相談しながら進めることにしました。
というかChatGPTがあるからこそ、研究しようなどと思えたということです。
ただし、それは「答えを丸投げする」という意味ではありません。

• 自分がどこで分からなくなるのか
• どこを勘違いしているのか
• どう説明されると理解しやすいのか

そういうことを対話の中で明らかにしていきたいと思います。

なぜ「まず環境を作る」のか

問題の輪郭が少し見えてきたところで、次に考えたのは「では自分はこの問題にどう関わるのか」ということです。

ここで僕が感じたのは、これは紙とペンだけで真正面から殴りにいくには重すぎる、ということ。
もちろん数学の問題なので理論的理解は必要なのだが、それと同時に、今回僕が関わりたいと思った方向はかなり明確でした。

それは、計算機を使って検証可能な形で問題に触れることです。
理論への理解が乏しくても、実験が個人でできるということが重要だと思いました。

この問題について調べる中で、近年の進展は単に「考えて分かった」というより、

• グラフを作り
• 彩色条件を論理式として記述し
• SATソルバーで充足可能性を判定し
• 必要なら証明ログまで検証する

という流れの上に乗っていることが分かってきました。

つまり、いきなり難しい数学の議論に突っ込むよりも先に、まずは

• Linux 環境
• Python
• SAT 関連ツール
• 検証のための実行環境

を整え、「問題を実験できる状態」を作り、そこから色々条件を変えて研究を進めたいと思ったのです。

グラフ理論への理解が乏しい今、それでも研究に触れられる環境が欲しいなと。

今回のシリーズは何を書くのか

これから数回にわたり、環境構築の記事を書きたいと思っていますが、一応説明を。

これは、専門家が整理した完成版の解説ではなく。
また、「最短で構築する手順書」でもありません。

むしろ逆で、これは

• 数学に詳しくない僕が
• 興味をきっかけに
• ChatGPTに相談しながら
• 何をして
• どこでつまずき
• 何が起こり
• どう考えを変え
• 最終的にどう構築したか

を、できるだけそのまま残していく記録です。
この記事の価値は「きれいに成功したこと」ではなく、むしろ、

• 分かっていなかったこと
• 途中で誤解していたこと
• 実際に失敗したこと
• 方針を変えたこと

まで含めて書くことに意味があると思っています。

実際、この環境構築は最初から順調だったわけではありません。
途中ではかなり大きなトラブルも起きており、あとから見ると「あそこでの判断が分かれ目だった」と思う場面も多い。

そういう意味でも、このシリーズは「成功談」ではなく、試行錯誤の全体記録として読んでもらうのがいちばん近いかと思います。

この記事を誰に向けて書くのか

このシリーズは、同じような立場の人に向けて書いている。

たとえば、

• 数学の専門家ではないけれど興味を持った人
• 研究という言葉にひるみつつも、実際に何か始めたいと思っている人
• LinuxやSAT環境を使ってみたいが、何から手をつけてよいか分からない人
• うまくいった話だけでなく、失敗も含めて参考にしたい人

には、ある程度役に立つのではないかと思っています。
少なくとも僕自身にとっては備忘録として機能します。

実際に行った環境構築の概要

最終的には、Ubuntu仮想環境上に、

• Python
• PySAT
• CaDiCaL
• DRAT-trim

などを使って、論理条件をSATとして記述し、充足可能性やグラフ彩色の検証を試せるところまで到達しました。

つまり今から書くのは、「これからどうするか」ではなく、どうやってそこまで辿り着いたかの振り返りです。

そこまでには色々問題も起こったので、それを書いていくこととします。

おわりに

数学が苦手だが、考え方には興味があり、研究もしてみたい。
そんな考えを、なんとか実行に移せる環境があり、かつそれができる対象を見つけられたと思っています。

次回は、Linux環境として最初に WSLを選んだ理由 について書いていきます。

次回は、【なぜWSLを選択したのか】について書きます。