# 考えるコード ― 制約と最適化の冒険

<a href="../zh/">中文版 →</a>

## 前言

本書は、論理制約解法（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）。  

```{tableofcontents}
```