布尔可满足性问题

概述

布尔可满足性问题（Boolean Satisfiability Problem，简称SAT）是计算复杂度理论中的一个核心问题，询问给定的布尔公式是否存在一组变量赋值使其为真。

关键内容

1. 问题定义：给定一个布尔公式（由变量、逻辑连接词∧（与）、∨（或）、¬（非）组成），判断是否存在一组变量赋值（每个变量取TRUE或FALSE），使得公式的值为TRUE。

2. 重要性：SAT是第一个被证明为NP完全的问题。Stephen Cook在1971年的开创性工作中证明了SAT是NP完全的，这标志着NP完全性理论的诞生。

3. 实际应用：尽管SAT在理论上是NP完全的，现代SAT求解器在实践中取得了惊人的性能，广泛应用于硬件验证、软件测试、人工智能规划等领域。

4. 变体：SAT有多个重要的变体，如CNF-SAT（合取范式可满足性）、3-SAT（每个子句最多包含3个文字）等，它们也都保持NP完全性。

来源

• 08-cook-np-completeness — 问题定义与历史意义
• Cook定理 — 证明为NP完全的第一个问题
• SAT求解器 — 实际应用

相关

• Cook定理 — proved to be NP-complete
• NP完全性 — first example of
• 计算复杂度理论 — foundational problem in
• 多项式时间归约 — subject of
• 合取范式 — common representation