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

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

日文版 →

前言#

本书面向对逻辑约束求解（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）。

Z3

PySat

OrTools