数学研究ログ 第010回「研究再開とUbuntu環境の確認」

Hadwiger–Nelson問題の研究を再開します――まずは以前の計算環境を確認しました

以前、Hadwiger–Nelson問題に取り組むため、VirtualBox上のUbuntuへPythonやSATソルバーなどを導入しました。
環境構築自体は完了していたものの、その後しばらく研究には取り組めていませんでした。

今回、ようやく時間を取れそうになったため、いきなり難しい問題へ進むのではなく、簡単なところから少しずつ再開することにしました。

僕はまだグラフ理論の初心者です。
そのため、当面の目標は新しい結果を出すことではなく、小さなグラフの彩色問題を自分の手で再現し、理論と計算の流れを理解することです。

序盤の目標を決めました

最初は、三角形や四角形といった小さなグラフを扱います。
具体的には、次のような流れを一通り実行できるようにしたいと考えています。

  1. グラフをデータとして表現する
  2. 彩色問題をSAT問題へ変換する
  3. SATソルバーで判定する
  4. 得られた彩色やUNSAT証明を検証する
  5. 入力、コマンド、結果、考察を記録する

最初の正式な実験は、三角形が2彩色できないことをSATで確認する予定です。
非常に小さな問題ですが、今後より大きな単位距離グラフを扱うための基本手順を確認するには適しています。

Ubuntuの起動に少し時間がかかりました

研究再開の最初の作業として、VirtualBox上のUbuntuを起動しました。ところが、以前よりも起動に時間がかかり、しばらく画面が進みませんでした。

単に処理が遅いのか、起動が止まっているのか判断しにくく、最初の躓きとなりました。

今回は複数回起動を繰り返すことで起動できました。
前回のログなどが影響していたのか、メモリ使用量が関係しているのかは分かりません。

大きな問題はなさそうですが、起動時にそういうこともあるというのは知っておくと少し安心かもしれません。

以前の研究環境は残っていました

Ubuntuへ入った後、以前作成した研究用ディレクトリを確認しました。

Pythonの仮想環境、PySAT、CaDiCaL、drat-trimなどは、そのまま残っていました。
また、環境構築時に作成した小さなテストプログラムも見つかりました。

一つは、三角形を3色で彩色するSAT問題です。
三角形は3彩色可能であるため、結果はSATになります。

もう一つは、ある命題とその否定を同時に要求する、非常に単純なUNSATテストでした。
ただし、保存途中のバックアップファイルには文字が一つ欠けており、そのままでは実行できない状態でした。

正式な研究用コードではなかったため、修正して再利用するのではなく、過去の動作確認記録として残すことにしました。
もしかしたらそのうち消すかもしれませんが。

古いテストと正式な実験を分けました

以前のテストファイルを、そのまま新しい研究用フォルダへ置いておくと、今後作成する正式な実験と区別しにくくなります。

そこで、環境構築時のファイルは専用の保管場所へ移動しました。
不要に見える小さなファイルでも、以前どこまで動作確認したかを知る手掛かりになります。

すぐに削除するのではなく、日付と用途が分かる形で保管しておく方が安全だと判断しました。

まあ、少し期間が空いてしまったので、最初はまた簡単なテストのようなものを行うとは思いますが。

Ubuntu側を計算専用に整理しました

Ubuntu側には、プログラム、グラフデータ、テスト、実験結果、CNF、UNSAT証明などを置くための基本的な作業場所を用意しました。

細かなフォルダ構成は今後変更する可能性がありますが、大きくは次のように役割を分けています。

  • プログラム本体
  • 自動テスト
  • 基本グラフのデータ
  • 単位距離グラフのデータ
  • 実験ごとの作業場所
  • CNFや証明ファイル
  • ソルバーの結果
  • 一時ファイル
  • 過去のファイルの保管場所

最初から完璧な構成を作ることよりも、プログラム、入力データ、実験結果を混在させないことを重視しました。

研究資料をどこに置くか迷いました

今回、特に迷ったのは、研究関係のファイルをWindowsとUbuntuのどちらへ置くかという点です。
プログラムをUbuntu上で実行する以上、すべてをUbuntuへまとめる方法も考えられます。

しかし、僕は文章の編集やファイル整理にはWindowsの方が慣れています。
研究ノート、考察、参考文献、ブログ記事までUbuntu側へ置くと、日常的な作業が不便になる可能性がありました。

そこで、役割を次のように分けることにしました。

  • Windows側は研究資料全体の本拠地
  • Ubuntu側は計算とプログラム実行の環境

研究ノートや考察はWindows側で管理し、CNFやUNSAT証明などの計算ファイルはUbuntu側へ置きます。
重要な結果については、Windows側の実験記録へ整理して残します。

基本は研究データを全てWindows側に置きたいのですが、Ubuntuでなくては動かしにくいデータなどはそちらに置こうかと。
一応相互にデータを共有できるフォルダも用意しているので、困ることはないかと考えています。

今回の到達点

今回の作業では、新しい計算実験そのものはまだ始めていません。
しかし、以前作った環境が残っていることを確認し、過去のテストと今後の正式な研究を分離できました。

また、Ubuntu側を計算環境として使い続ける方針も決まりました。
環境構築を終えた直後は、ソフトが動くことだけで満足しがちです。

実際に研究を再開しようとすると、ファイルの場所、過去の作業内容、何を正本とするかといった管理面が重要になることが分かりました。

次は、Windows側に研究資料を管理するための場所を作り、研究概要やロードマップ、実験記録の形式を整理します。