考えるコード ― 制約と最適化の冒険#
前言#
本書は、論理制約解法（SMTソルバー）、組合せ最適化、充足可能性問題（SATソルバー）に興味のある読者を対象に、Z3、OR-Tools、PySATの実践的な活用方法を紹介するものです。これらのツールは、数理最適化、人工知能、ハードウェア検証、スケジューリング、ゲームAIなど、さまざまな分野で利用されています。
本書では、単なる理論解説にとどまらず、具体的なコード例を用いて、各ツールの基本から応用までを丁寧に解説します。Z3を用いた論理式のモデルチェック、OR-Toolsによる制約プログラミング、PySATによるSATソルバーの活用といったトピックを取り上げ、読者が実際に動かしながら理解を深められるよう工夫しています。
プログラミング経験がある方なら、数理最適化や制約解決の知識がなくても、手を動かしながら学べる構成になっています。本書を通じて、Z3、OR-Tools、PySATの活用法を習得し、現実の問題を解決する力を身につけていただければ幸いです。
ライブラリ紹介#
ライブラリ |
主要用途 |
代表的な問題 |
|---|---|---|
Z3 |
SMTソルバー |
数学的制約、プログラム検証 |
OR-Tools |
最適化 |
スケジューリング、ルーティング |
PySAT |
SATソルバー |
論理問題、パズル解法 |
本書では、これらのライブラリを使った実践的な問題解決方法を、具体的なコードを交えて解説します。
Z3 SMTソルバー#
Z3は、Microsoft Researchが開発したSMT（Satisfiability Modulo Theories）ソルバーです。 SMTとはSAT（充足可能性問題）を拡張したもので、整数演算、論理演算、配列、ビットベクトル、代数的データ型、実数解析などの理論（theories）を扱うことができます。例えば、「\( x + y \leq 10 \) かつ \( 2x - y = 3 \) を満たす整数 \( x, y \) を求めよ」といった制約を解くのに適しています。
Z3は以下の特徴があります。
複雑な制約問題を記述し、充足可能かどうかをチェックできる。
定理証明にも使用可能（数式が常に成り立つかを検証）。
Python、C++、Javaなど複数の言語から利用可能。
ソフトウェア検証、ハードウェア設計、プログラム解析などで活用。
OR-Tools#
OR-Toolsは、Googleが開発した組合せ最適化ライブラリで、主に以下の最適化技術をサポートしています。
線形計画法（LP）・整数線形計画法（MILP）
制約プログラミング（CP）
ルーティング問題（VRP, TSP）
OR-Toolsは以下の特徴があります。
Googleが提供する高性能な最適化エンジン。
多様な最適化問題に対応可能（スケジューリング、配送計画、リソース割り当てなど）。
SATソルバーを用いた組合せ最適化も可能（CP-SAT）。
Python、C++、Javaなど複数の言語から利用可能。
PySAT#
PySATは、SATソルバーをPythonから簡単に使えるようにしたライブラリです。 SAT（充足可能性問題）とは「変数に 0 または 1 を割り当てて、すべての論理式を満たす解を求めよ」という問題です。例：「(A または B) かつ (¬A または C) を満たす A, B, C の真偽値を求めよ」
PySATは以下の特徴があります。
複数のSATソルバー（MiniSat, Glucose, Cadicalなど）を統一的に扱える。
論理式を手軽に記述可能（CNF形式で入力）。
組合せ最適化や制約問題にも応用可能（MaxSAT、Weighted SAT）。
Z3