一句话定义
SMT 求解器（Satisfiability Modulo Theories solver，可满足性模理论求解器，简称 SMT solver）是自动判断“一组带数学背景的逻辑条件能否同时成立”的工具。能成立，它给出一组具体取值；不能成立，它说“无解”，并常给出冲突原因。
打个比方
SAT（Boolean Satisfiability Problem，SAT）求解器像只认开关的电工：每个变量非真即假，它找有没有一组开关状态让电路亮。SMT 求解器像既懂开关又懂算账、排班、数组下标的调度员。比如排班：每人每天最多一班、连续夜班不超过两天、张三和李四不能同班。把“第几天谁上班”写成整数变量和不等式，SMT 会回答“有没有可行班表”，有就给出班表，没有就指出哪几条规则打架。
它怎么工作
先把问题编码成逻辑公式，再让求解器搜索。内部常把 SAT 搜索和“理论求解器”配合：布尔层决定“选哪个分支”，理论层检查整数、实数、位向量、数组、字符串等约束是否矛盾。像项目经理拆任务：一个负责做选择，一个负责验算数字。
和相邻概念的区别
先给几个近亲：约束规划（Constraint Programming，CP）、自动定理证明（Automated Theorem Proving，ATP）。
| 概念 | 核心问题 | 表达力 | 输出 |
|---|---|---|---|
| SAT | 布尔公式可满足吗 | 真假、与或非 | 赋值/无解 |
| SMT | 带背景理论的公式可满足吗 | 整数、实数、数组、位向量等 | 模型/不可满足核心 |
| 约束规划（CP） | 约束满足或优化 | 有限域、全局约束 | 解/最优解 |
| 自动定理证明（ATP） | 定理可证吗 | 高阶逻辑等 | 证明/常需人工引导 |
SAT 是 SMT 的底座之一；CP 与 SMT 有重叠，建模风格和生态不同；ATP 表达力更强但自动化更难。具体支持哪些理论、接口如何，以各工具官方页面为准。
对从业者与普通人的意义
- 程序验证：给代码插断言，若“断言失败”的公式不可满足，就说明在建模范围内所有输入都不会让断言失败；否则返回反例。芯片、协议、智能合约常用。
- 规划调度：任务分配、路径规划、时间窗、资源约束。
- AI 推理：大模型擅长猜，SMT 擅长验算。把自然语言变成约束后，可用 SMT 检查知识库是否一致、计划是否可行，属于神经符号方向。
普通人用的排班、路由、软件静态分析、配置检查，背后可能就站着它。