鯛焼ぷろじぇくと。Official Website 
目次
はじめに
ここまでのシリーズでは、研究環境を構築していく過程を順番に記録してきました。
第1回はこちら
その中で、Linux、仮想化、SAT、グラフ彩色など、さまざまな専門用語が登場しました。
正直なところ、僕自身もそれらを最初から十分に理解していたわけではありませんでした。実際には、調べながら使い、使いながら少しずつ意味を掴んでいったというのが実態です。
そこでこの記事では、ここまでのシリーズで登場した用語を、自分なりに整理しておきます。厳密な専門用語辞典というよりは、「今回の環境構築と研究の入口において、どういう意味で使っていたのか」を意識したまとめです。
Linux
LinuxはOSの一種です。Windowsと同じように、コンピュータ全体を動かすための基本的な仕組みです。
今回の環境構築では、SATソルバーや関連ツールがLinuxを前提としていることが多かったため、Linux環境を用意する必要がありました。僕の場合は、Windows上に仮想的なUbuntu環境を作る形で使いました。
Ubuntu
UbuntuはLinuxディストリビューションの一つです。簡単に言えば、Linuxを使いやすく整理した配布形態の一つです。
Linuxにはさまざまな種類がありますが、Ubuntuは利用者が多く、情報も豊富で、初心者でも比較的扱いやすいため選びました。
WSL
WSLは Windows Subsystem for Linux の略で、Windows上でLinux環境を動かす仕組みです。仮想マシンとは違い、Windowsの機能としてLinuxを扱う形になります。
今回、最初に選ぼうとしたのがこのWSLでした。一般的には便利で手軽な選択肢ですが、Windowsの機能と密接に関わるため、構成や状況によっては影響範囲が広くなることがあります。
ここに、WSLとVirtualBoxの違いを簡単に整理した図を入れます。
VirtualBox
VirtualBoxは仮想マシンを作成するソフトウェアです。仮想マシンとは、PCの中に仮想的な別のPCを作るような仕組みです。
今回の環境構築では、Windows上でVirtualBoxを使い、その中にUbuntuをインストールしました。これにより、Windows本体とある程度分離されたLinux環境を作ることができました。
仮想化
仮想化とは、実際のハードウェアとは別に、ソフトウェア上で仮想的な環境を作る技術です。
今回の場合は、VirtualBoxを使って仮想的なPCを作り、その中でLinuxを動かしました。仮想化によって、Windows本体を直接変更せずに実験環境を持つことができました。
Guest Additions
Guest Additionsは、VirtualBoxの仮想環境に追加で導入する機能です。これを入れることで、コピー＆ペーストの共有、マウス操作の改善、画面表示の最適化などが可能になります。
第7回でかなり苦戦した部分でもありましたが、実際に使える仮想環境にするには重要な要素でした。
Python
Pythonはプログラミング言語の一つです。文法が比較的分かりやすく、今回のように条件を書いて実験する用途にも向いています。
僕はこの環境で、SAT問題を組み立てたり、グラフ彩色の小さな実験を行ったりしました。
仮想環境（venv）
Pythonの仮想環境は、プロジェクトごとに必要なライブラリを分離して管理する仕組みです。これにより、他のPython環境と干渉せずに作業ができます。
今回も .venv を作成し、その中に必要なパッケージをインストールしました。環境を汚さずに管理するという方針にも合っていました。
SAT
SATは、与えられた論理条件をすべて同時に満たす真偽の割り当てが存在するかどうかを判定する問題です。日本語では充足可能性問題と呼ばれます。
例えば、
- x は真
- x は偽
という条件を同時に満たすことはできないため、この場合は解がありません。逆に、矛盾しない条件であれば、真偽の割り当てが存在します。
ここに、SATとUNSATの違いを示す図を入れます。
SAT と UNSAT
SATは「条件を満たす割り当てがある」ことを意味します。UNSATは「どんな割り当てでも条件を同時には満たせない」ことを意味します。
今回の研究では、グラフ彩色問題をSATとして書いた場合、SATならその色数で彩色可能、UNSATならその色数では彩色不可能という意味になります。
PySAT
PySATは、PythonからSATソルバーを扱うためのライブラリです。これを使うことで、論理条件をPythonコードとして記述し、その場でSAT/UNSATの判定を行えます。
今回の環境では、まずPySATを使って簡単な論理条件の確認や、グラフ彩色の最小例を試しました。
SATソルバー
SATソルバーは、SAT問題を実際に解くプログラムです。PySATはそれをPythonから呼び出しやすくするための仕組みであり、実際の判定はソルバーが行います。
CaDiCaL
CaDiCaLはSATソルバーの一つです。SAT問題を実際に解くエンジンであり、研究用途でも扱いやすいソルバーとして今回導入しました。
DRAT-trim
DRAT-trimは、SATソルバーが出力した証明ログを検証するためのツールです。特にUNSATの場合、「本当に解がないのか」を第三者的に確認するために使われます。
今回の段階では、まずツールが動くところまで確認しました。今後、UNSAT証明をきちんと扱う際に重要になるはずです。
グラフ彩色問題
グラフ彩色問題は、グラフの頂点に色を割り当てて、辺でつながった頂点が同じ色にならないようにする問題です。
今回の研究では、平面上の点の距離条件をグラフとして表現し、それを彩色問題として扱う方向で考えています。
Hadwiger–Nelson problem
Hadwiger–Nelson problem は、平面上の各点に色を割り当てるとき、「距離がちょうど1の2点は同じ色にできない」という条件のもとで、平面全体を塗るのに最低何色必要かを問う問題です。
この問題は長いあいだ、少なくとも4色必要で、7色あれば十分であることまでは分かっていました。つまり答えは長く 4・5・6・7 のいずれかとされていました。
その状況が大きく動いたのが2018年でした。Aubrey de Grey によって、4色では彩色できない有限の単位距離グラフが構成されました。これにより、「平面全体も4色では足りない」ことが示され、下限が4から5に引き上げられました。
現在、Hadwiger–Nelson problem の答えは 5・6・7 のいずれかであるとされています。つまり今の焦点は、5色で十分なのか、それとも6色以上必要なのか、という点にあります。
ここで、問題の基本構造を整理した図を入れます。
続いて、2018年の進展を含む位置づけの図を入れます。
僕がこの問題に惹かれた理由の一つは、こうした進展が純粋な理論だけでなく、有限グラフの構成や計算機による検証とも深く結びついている点でした。今回構築した環境も、まさにそうした方向に少しでも近づくためのものです。
グラフ彩色とSAT化
今回のシリーズの後半で実際に試したように、グラフ彩色問題はSAT問題として書き直すことができます。
具体的には、
- 各頂点がどの色を持つかを変数にする
- 各頂点は少なくとも1色を持つ
- 同時に複数色は持たない
- 辺でつながった頂点は同じ色を持たない
という条件を論理式として表現します。
この対応関係を図で見ると分かりやすいので、ここに図を入れます。
このようにして、彩色問題をSAT問題に翻訳することで、機械的な検証が可能になります。
おわりに
今回の環境構築では、多くの用語が登場しましたが、それらは単に知識として覚えるためのものではなく、実際に触って覚えていけたらと思います。
今後も新しい用語や概念は出てくると思いますが、その都度こうして整理しながら進めていこうと思います。必要であれば、この用語整理も今後行っていくと良いかもしれませんね。