布尔可满足性问题（SAT）

布尔可满足性问题简称 SAT，是指给定一个由布尔变量与逻辑联结词构成的命题公式，判断是否存在一组变量真假取值使整个公式的值为真，若存在则称公式可满足，否则称不可满足。

概述

SAT 具有里程碑意义，因为库克-列文定理证明它是第一个被确立的 NP 完全问题，这意味着所有 NP 问题都能在多项式时间内归约到它。尽管理论上困难，实际中的 SAT 求解器在几十年发展后已能高效处理含数百万变量的工业实例，形成了理论困难而实践强大的鲜明反差。

核心原理

• 合取范式：SAT 公式通常化为若干子句的合取，每个子句是若干文字的析取，便于统一处理。
• NP 完全性：SAT 既属于 NP，又是 NP 难，因而是 NP 完全问题的代表。
• DPLL 算法：经典求解框架，通过变量赋值、单元传播与回溯系统地搜索满足赋值。
• 冲突驱动子句学习：现代求解器的核心技术，从冲突中学习新子句以剪枝并避免重复错误。

应用场景

SAT 求解器被广泛用于硬件与软件的形式化验证、电子设计自动化、人工智能规划、密码分析、以及可满足性模理论的底层引擎。许多看似无关的组合问题都可编码为 SAT，交给高效求解器处理，使 SAT 成为通用的问题求解利器。

常见问题

问：SAT 既然是 NP 完全，为什么实践中还能高效求解？答：NP 完全描述的是最坏情况的理论复杂度，而现实中的许多实例具有特殊结构。现代求解器借助冲突驱动子句学习、高效数据结构和启发式，往往能远快于最坏情况求出结果，但并不能保证对所有实例都快。

问：可满足性模理论和 SAT 有什么关系？答：可满足性模理论在布尔结构之上加入了算术、数组等背景理论，它通常把问题分解为布尔骨架交给 SAT 求解器，再由理论求解器处理具体理论约束，是 SAT 的重要扩展。