鯛焼ぷろじぇくと。Official Website 
このシリーズでは、数学の研究環境を整えていった過程を順番に記録しています。
前回は【環境を「使える状態」にする】について書きました。まだの方は、先にこちらからどうぞ。
目次
ここまでで環境は「使える状態」になりました
第7回までで、VirtualBox上のUbuntu環境は操作性も含めて安定し、実際に作業できる状態になりました。ここからは、その環境に対して研究で使うツールを導入していきます。
この段階での目的は明確でした。
- 論理条件をSATとして記述できること
- それを実際に解かせることができること
- 結果を確認できること
つまり、「問題を計算として扱える状態」を作ることです。
Pythonの動作を確認
まずは基本となるPythonの動作を確認しました。ターミナルで次のコマンドを実行しました。
python3 --version
問題なくバージョンが表示され、Pythonが使えることを確認。
同様に、pipやgitについても確認し、基本的な開発環境が整っていることを確認しました。
この段階で、「最低限の実行環境はすでに整っている」という認識を持ちました。
仮想環境を作成
次に、Pythonの仮想環境を作成しました。
これは、プロジェクトごとに依存関係を分離するためのものです。次のコマンドを実行しました。
python3 -m venv .venv
source .venv/bin/activate
仮想環境を有効化すると、プロンプトの先頭に「(.venv)」が表示されるようになりました。この状態でパッケージをインストールすれば、システム全体には影響を与えずに管理できます。
ここでも「分離する」という方針がそのまま活きていると感じました。
PySATを導入
続いて、SAT問題を扱うためにPySATを導入しました。これはPythonからSATソルバーを扱うためのライブラリです。次のコマンドでインストールしました。
pip install python-sat
インストールは特に問題なく完了しました。
その後、動作確認として簡単なコードを実行しました。
from pysat.solvers import Solver
with Solver() as s:
print("OK")
これが正常に動作したことで、PySATが正しく導入されていることを確認しました。
簡単なSAT問題を実行しました
次に、実際にSAT問題を解かせるテストを行いました。非常に単純な例として、
- x が真
- x が偽
という矛盾した条件を与えました。
from pysat.formula import CNF
from pysat.solvers import Solver
cnf = CNF()
cnf.append([1])
cnf.append([-1])
with Solver(bootstrap_with=cnf.clauses) as s:
print("SAT?", s.solve())
この結果は「False」となり、期待通り「充足不可能」であることが確認できました。
この時点で、「自分で条件を書いて、それを機械に判断させる」という流れが成立していることを実感しました。
CaDiCaLとDRAT-trimも確認しました
さらに、外部のSATソルバーであるCaDiCaLと、証明検証ツールであるDRAT-trimについても動作確認を行いました。
それぞれ実行ファイルとして動作し、ヘルプが表示されることを確認しました。これにより、
- ソルバーとしての実行
- 証明の検証
といった一連の流れを構築できる見通しが立ちました。
実際に彩色問題を試しました
ここまでの準備が整った段階で、簡単なグラフ彩色問題をSATとして記述し、実行してみました。
その結果、
- SATであるかどうか
- 実際の割り当て（どの頂点にどの色が割り当てられたか）
を確認することができました。
この時、単にプログラムが動いたという以上に、「問題を自分の手で扱えている」という感覚がありました。
ここまでで何ができるようになったか
最終的に構築した環境では、次のことが可能になりました。
- 論理条件をSATとして記述する
- 充足可能性を判定する
- 解（モデル）を取得する
- 外部ソルバーと連携する
- 証明の検証を行う
つまり、平面彩色問題を計算として扱うための基盤が整いました。
今後の展開について
この環境が整ったことで、今後は次のようなことに取り組めるようになります。
- 条件を変えた実験
- より大きなグラフの検証
- 問題の一般化
- 幾何的な構造との対応
また、グラフ生成や数式処理のために、将来的にはSageMathの導入も検討しています。ただし現時点では、まずSATによる記述と検証に集中する予定です。
このシリーズのまとめ
今回の環境構築は、最初から順調に進んだわけではありませんでした。
- WSLを選択しました
- OSが起動しなくなるトラブルが発生しました
- 方針を見直しました
- VirtualBoxに切り替えました
- 仮想環境を構築しました
- 操作性の問題を解決しました
- 最終的に研究環境を完成させました
この流れを通して感じたのは、環境構築は単なる準備作業ではなく、設計と判断の連続であるということでした。
おわりに
僕は数学に詳しいわけではありません。
それでも、この問題に興味を持ち、自分なりに扱えるところまで持っていくことができました。
今回構築した環境は、まだ入口に過ぎません。しかし少なくとも、「試すことができる状態」には到達しました。
ここから先は、この環境を使ってどこまで進めるかになります。このシリーズはここで一区切りとし、次は実際の検証や考察に進んでいこうと思います。
次回はSATで挑む平面彩色問題：研究環境構築記録で扱った用語についての解説を用意しています。