SATソルバー使おうぜ：オープンショップスケジューリング問題をZ3で解く
「難しい問題の解決」といえば、AIやディープラーニング、機械学習がトレンドとして何年も語られてきました。でも、それだけじゃない道もあるんです。今回は、ちょっと地味だけど頼りになるツール、SATソルバー を紹介します。
SATソルバーとは
SATソルバーは、SAT（ブール充足可能性問題、Boolean Satisfiability Problem） を解いてくれるプログラムです。簡単に言うと、「与えられた論理式を真にする変数の真偽値の割り当て」を探すツールです。たとえば、 (A || C) && (!A || B || !C) みたいな論理式を考えます。このような形はCNF（連言標準形）と呼ばれています。リテラル（A や !B）を1個以上 OR で繋げた「節（clause）」を、さらに AND で繋げた形のブール論理式です。SATソルバーは、通常このようなCNFの形をした論理式を相手にして、与えられたCNFを true にできるか、できる場合はどんな時か、を答えてくれます。
具体例に戻ると、この論理式は、A=true; B=false; C=false とすれば全体が true になります。MiniSATなどのSATソルバーは、このような真偽の割り当てを一つ見つけてくれます（複数ある場合も追加の手順を踏めば見つけられます）。もし組み合わせが全くない場合（例: !A && !B && (A || B)）は充足不可能（矛盾）と答えます。
CNFでない論理式も、Tseitin変換という方法でCNFに変換可能です。元の式に追加変数を導入して変形する必要がありますが、充足可能性（ true になる割り当てが存在するかどうか）に関しては同等なCNFを作れます。
それで？ 別にZennの記事に数学の話は期待してないんだけどなぁ…。いえいえ、ここからが本番です！この凄さを次に実例で示しますよ。
マシンへのオペレーションの割り当て（オープンショップスケジューリング問題）をZ3で解く
今回はこのSATを解くためのソルバーとして、Z3という、Microsoft Researchが開発しているPythonからサクサクと使えるSMTソルバーというものを使います。SMTソルバーでは、ブール論理（SAT）に加えて整数や実数などの制約も扱えますが、今回は純粋なブール論理の問題としてSATを解くためだけに使います。
さらに今回は「オープンショップスケジューリング問題」を具体的に解いていきます。解いた結果のリポジトリはこちらです。ざっくり言うとショップ（お店）にマシンとオペレーションがあって、どのマシンにどのオペレーションをどの順番でさせるかといった問題ですが、詳しい問題設定は後述します。
執筆時点で最新だったPython 3.13 + poetry 2.1.4を使います。
まずは、z3のソルバーをインストールします。
poetry new sat
cd sat
poetry add z3-solver
簡単な例を解く
最初に出した例、 (A || C) && (!A || B || !C) をZ3で解いてみるコードはこんな感じです。
実行すると…
% poetry run python "./src/intro.py"
Satisfiable
a = True
b = False
c = False
というわけで同じ結果が得られました。
本題のオープンショップスケジューリング問題を解く
オープンショップスケジューリング問題(以下OSP)に戻りましょう。形式的な定義に関しては参考文献のこちらに譲りますが、こういう問題です：
「あるお店には、n台のマシンがあります。これから仕事のため、m個のジョブを実行しなければなりません。ジョブはそれぞれさらに複数個のオペレーションに分割されています。オペレーションはどの順番で行っても構いません。ただし、それぞれのオペレーションには特定のマシンが必要ですが、同時に２つ以上のオペレーションで同じマシンを使うことはできません。さて、このお店がすべてのジョブを完遂するまでに必要な時間はどれほどで、どんな順番でオペレーションを行えばよいでしょう？」
大事なのは
- オペレーション同士を同時に実行しても構わない
- ただし、同じマシンが必要なオペレーションが同時には実行できない
- お店がすべてのジョブを完遂するまでに必要な時間（
makespan）と順番を決定する
の３点です。ややこしいです。
さて、今回は実際によくベンチマークとして使われているもののうちの１つ、gp03-01という問題を解きます。これは3つのマシンと3つのジョブがあり、それぞれのジョブは3つのオペレーション（合計で9個のオペレーション）で構成されている問題です。また、gp03-01の場合は元のOSPには無かった「同じジョブに属するオペレーションも同時実行できない」という追加の制約が課せられます。もっとややこしいです。
オペレーションの一覧：
| 番号 | 属するジョブ | 処理時間 | 必要なマシンの番号(0-2) |
|---|---|---|---|
| 0 | 0 | 661 | 0 |
| 1 | 0 | 6 | 1 |
| 2 | 0 | 333 | 2 |
| 3 | 1 | 168 | 0 |
| 4 | 1 | 489 | 1 |
| 5 | 1 | 343 | 2 |
| 6 | 2 | 171 | 0 |
| 7 | 2 | 505 | 1 |
| 8 | 2 | 324 | 2 |
繰り返しになりますが、今回のベンチマーク問題では、同じジョブに属するオペレーション同士、同じマシンを必要とするオペレーション同士は、同時には実行できません。
問題を論理式に変換する
SATソルバーを使った問題解決で、一番難しくて一番おもしろいと思う所が、この問題をどう論理式に落とし込むかという話です。今回は、参考文献にも載せている鍋島英知先生の2010年の文献の方法を参考にさせていただきました。
各種変数の初期化
各オペレーションを表現する Operation クラスと、各資源制約を表現する ResourceConstraint クラスを作ります。
オペレーションのクラスは次のようなものです。 Bool() 関数が命題（論理式の変数）を作るためのZ3の関数になります。
独特なのが、start_at_or_later[t] という「その時刻かそれ以降には開始している」という状態を表す変数を導入している事かと思います。
資源制約に関しては、単に「同時に実行できない」だけを表現していています：
「同時に実行しない」は、どちらかが先に実行されている、という意味ですので、proceed_aとproceed_bという論理変数でaとbが先に実行される場合それぞれを表現しています。
同時に実行できないのがどのオペレーション同士なのかについては、今回はgp03-01だけが解きたいことを利用して問題の定義にハードコードしてしまいました：
この辺はソフトウェア・エンジニアリング的には工夫の余地のある所かと思いますが、一旦そこはご容赦ください。
論理式にエンコードする
というわけで、以上の2つのクラスを、実際に論理式に落とし込んでいきます：
それぞれにコメントがついていますが、
- 資源制約があるなら、どちらかが先に実行されて、もう片方はあとに実行されなければならない。
- 時刻0以降に始まって、その時刻からオペレーションを開始しても（資源制約が無ければ）
makespanまでに間に合う時刻までには開始している。 - 時刻tかそれ以降に開始しているなら、時刻t-1かそれ以降にも開始している（
start_at_or_laterの定義）。 - 資源制約があって同時に実行できないなら、もう片方はそれより後に実行されている。
というのを論理式の形で書き下してあります。
「a ⇒ b」 を (not a) or b に同値変形してる所もポイントです。これを使うことでNOT, AND, ORだけで簡単な論理（命題論理）を表現できるようになっています。
さて、start_at_or_laterの意味する所、とくに最後の条件4はとくにややこしいので、図を描いて補足してみました。いかでしょうか？…分かりやすく描けてますかね…。
この図の場合、op1.start_at_or_later[t + op1.duration] -> op4.start_at_or_later[t]という関係が常に成り立ってるように論理式が構築される事になります。
実際に解く！
というわけで、論理式に落としましたので、実際にZ3にこの問題を解かせます：
今回は最短時間が最初からコードに書かれていますが、述べた通り、実際にはOSPは実際にはこれを求める問題です。指定した makespan 内で全オペレーションを完遂できない場合は「Unsatisfiable」と出てきますので、この性質を使って二分探索を使って最小となる総処理時間を調べることができます。そこまでやると焦点ぼやけるかな（今回はSATに落とす所が主眼の話です）と思って最初から最低値を入れています。
さて、実際にノートパソコン（Core i9 12900H, RAM 64GB）で実行してみると、
% poetry run python ./src/main.py
Encoded in 22.33 sec.
Solved in 0.13 sec.
Satisfiable
op[0]: 339 -> 1000
op[1]: 0 -> 6
op[2]: 6 -> 339
op[3]: 0 -> 168
op[4]: 168 -> 657
op[5]: 663 -> 1006
op[6]: 168 -> 339
op[7]: 663 -> 1168
op[8]: 339 -> 663
Valid answer
となり、Z3による実際の解の探索（solver.check()）はわずか0.13秒で解けました。プログラムで答えの妥当性をチェックした限りでも、制約は守られています（Valid answer）。
…が、解く部分「は」0.13秒という話であって、なんと論理式として表現するための処理であるエンコーディングに22.3秒と170倍以上も（！）掛かっているのが大きな問題です。コードの説明しやすさのための配慮もありますが、それ以外の要因も大きいかもしれません。SMTソルバーでなくSATソルバーの範疇で十分解けると分かったこの時点で、この先の展開としては、
- Pythonコードのパフォーマンス・チューニングをする（おそらくPython側での問題でC++側は遅くない…おそらくですが）
- Z3が実際に実装されている言語であるC++を直接使う
- MiniSATなどの他のSATソルバーに乗り換える
- 論理式のサイズが減るかもしれない田村先生らのエンコーディングに変更する。
- いっそ？他の言語で他のSATソルバー(弊社ならRustでMiniSATかな)を使う。もちろん同じ点で躓く可能性もありますが、あくまでZ3はSMTソルバーですので…。
- Z3をSMTソルバーとして使ってみる
- 別のアルゴリズム、普通に整数計画法のソルバー（PythonならPuLPとか）などを使う。
などを検討してみるとよいかもしれません。これは要件によります。個人的にはとりあえずZ3で試して色々実験してみて、SATの範囲で十分解けると分かった時点で、その後実際にどうするか決めるのは全然アリだと思います。Z3は高機能ですし、最初から特定の解法のソルバーだと縛りが強いですから。
さてさて。実行時間はともかく、単なる論理式の組み合わせでスケジューリング問題まで解けてしまったことは指摘させてください。
SATはNP完全な問題の代表例
※理論部分に興味がない方はスキップしてください。
ところで、なんでこんなややこしい問題が論理式で書けて、しかも（とくに解の探索の部分は）短時間で解けたの？
それは SATが NP完全 な問題の代表例であること、最初にNP完全と証明された問題（Cook-Levinの定理）であること、かつ様々な問題がSATに還元（ざっくり言い変えると「変換」）できることと関係しています。NP完全問題であるSATは一般には効率的（多項式時間内）には解けないと多くの研究者は予想しているものの（P ≠ NP問題）、その性質もよく調べられて、任意のCNFと言われるとともかく、実務的に出てくるような一定の構造を持つ様々な問題から還元されて作られたCNFは早く解ける事も多く、実際に今回は現実的な時間内で解を得ることができました。とはいえ、もちろん万能薬ではありません。ダメな時は他の方法を考えましょう。今回の問題なら混合整数計画問題のソルバーなどです。
これは分かりやすくするべく相当に端折った説明です。この辺の理論に関して詳しくは「計算理論」と書かれている教科書読んでくださいね（参考文献にわたしが読んだものをリストしてありますので迷った場合はこちらを）。きちんとした定義の下、議論が展開されます（もちろん、その代わり難しいです）。
まとめ
SATソルバーは、見た目は地味かもしれませんが、このように複雑なスケジューリング問題も解けちゃう（こともある）ツールです。他にも、
などにも応用されているようです。どうです？ポテンシャル感じませんか？
参考文献
情報科学とSATに関するもの
- オートマトン言語理論計算論 (1)（ J.ホップクロフト (著), 野崎 昭弘 (翻訳) ）
- オートマトン言語理論計算論 (2)（ J.ホップクロフト (著), 野崎 昭弘 (翻訳) ）
- 人工知能 2010年25巻1号
- ショップ・スケジューリング問題の SAT 変換による解法
- Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems - AAAI
- SAT問題と他の制約問題との相互発展
OSPガチ勢の人向け（今回の方法はあくまで１手法）：
Survey for Open Shop Scheduling | Journal of Al-Qadisiyah for Computer Science and Mathematics
Discussion