# 思考的代码 ― 约束与优化的冒险

<a href="../ja/">日文版 →</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 是让 Python 能方便地使用 SAT 求解器的库。SAT（可满足性问题）是指「给变量赋值 0 或 1，找出满足所有逻辑式的解」。例如：「求使 (A 或 B) 且 (¬A 或 C) 成立的 A、B、C 的真假值」。

PySAT 的特点如下。

  - 可以统一使用多种 SAT 求解器（MiniSat、Glucose、Cadical 等）。
  - 容易描述逻辑式（以 CNF 格式输入）。
  - 也能用于组合优化和约束问题（MaxSAT、Weighted SAT）。

```{tableofcontents}
```