1 基本概念
1.1 定义
可满足性是指某个逻辑公式、约束集合或数学描述是否至少存在一个对象，使其所有条件都能同时成立。若存在这样的对象，则称该对象满足该表达式，整体问题也被视为可满足。该概念的核心不在于“如何求出解”，而在于“有没有解”。
在不同学科中，可满足性的具体表述略有差异，但基本思想一致：给定一组规则，判断是否能找到一个一致的解释，使规则全部为真或被满足。
1.2 可满足、不可满足与重言式
“可满足”表示至少存在一种赋值、结构或解释，使目标成立；“不可满足”则表示不存在任何合法对象能够同时满足全部条件。若一个逻辑公式在所有可能解释下都成立，则称为重言式。
这三者之间关系紧密：重言式强调“总为真”，可满足强调“至少有一例为真”，而不可满足则是“无例可真”。它们共同构成逻辑语义分析的基本判断框架。
1.3 相关术语
1.3.1 模型
模型是指能够使某个公式、理论或约束系统成立的数学结构。它可以是一个解释域，也可以是带有特定关系、函数和常元的结构体。在逻辑中，模型是判断可满足性的主要对象。
1.3.2 赋值
赋值通常指把命题变元或变量映射到具体取值的过程。在命题逻辑中，赋值多为真假分配；在更一般的语境下，赋值也可以是数值、对象或结构中的元素分配。
1.3.3 解释
解释是把符号系统中的非逻辑符号对应到具体语义对象的方式。它决定了公式中各个符号在某一结构下的意义，因此直接影响公式是否可满足。
1.4 不同领域中的含义
1.4.1 命题逻辑中的可满足性
在命题逻辑中，可满足性是判断一个命题公式是否存在某组真假赋值，使公式为真。这里的对象通常是由逻辑联结词构成的布尔表达式，问题形式最为直接，也最常作为算法研究的基础。
1.4.2 一阶逻辑中的可满足性
在一阶逻辑中，可满足性要求存在某个模型，使公式在该模型下成立。由于一阶逻辑引入了量词、谓词和结构解释，问题不再局限于真假表，而是涉及更丰富的语义对象。
1.4.3 约束系统中的可满足性
在约束系统中，可满足性意味着是否存在一组变量取值，使所有约束条件同时成立。这里的约束可以是等式、不等式、区间限制或组合规则，常见于工程优化、排程和自动验证等场景。
2 逻辑中的可满足性
2.1 命题可满足性
命题可满足性是最经典的形式之一，通常研究给定命题公式是否存在一组真值分配使其成立。该问题不仅是逻辑学中的基础命题，也是计算复杂性理论与自动求解技术的重要起点。
2.1.1 合取范式
合取范式是由多个子句通过“且”连接构成的标准形式，每个子句内部通常是若干文字的“或”连接。许多可满足性算法都倾向于将公式转换为这种形式，以便统一处理和搜索。
2.1.2 析取范式
析取范式是由多个合取项通过“或”连接构成的形式。与合取范式相比，它在某些理论分析中更便于理解公式的结构，但在求解实践中通常还需要进一步规范化处理。
2.1.3 典型判定方法
命题可满足性的判定方法包括真值表检查、分支搜索、归结和现代 SAT 技术等。对于规模较小的公式，直接枚举是可行的；而对于大规模实例，则往往依赖启发式搜索和冲突学习机制。
2.2 一阶可满足性
一阶可满足性研究是否存在某个模型，使一阶公式成立。由于量词可跨越多个对象，问题比命题可满足性更复杂，通常难以通过简单枚举完成。
2.2.1 结构与模型
一阶逻辑的模型由论域以及函数、关系和常元的解释组成。不同模型可能对同一公式给出不同真假结果，因此模型的构造是理解可满足性的关键。
2.2.2 语义解释
语义解释决定了变量、谓词和函数符号如何在模型中取义。公式是否成立，取决于解释与结构是否共同满足其语义条件，而不仅仅是符号形式本身。
2.2.3 模型存在性问题
模型存在性问题是判断某公式是否有满足它的结构。对于一阶逻辑而言，这类问题通常高度复杂，某些片段可判定，而一般情形下则可能缺乏有效的完全算法。
2.3 模态逻辑与其他扩展逻辑中的可满足性
模态逻辑、时态逻辑及其他扩展逻辑中的可满足性，研究对象已不只是单一赋值，而是包含世界、时间或可达关系的语义结构。这使得其表达能力增强，同时也带来了更复杂的判定难题。
2.3.1 世界与可达关系
在模态语义中，公式通常在若干“世界”之间解释，而可达关系描述世界之间的连接方式。某个公式是否可满足，取决于是否能在适当的世界图中安排出满足条件的局部状态。
2.3.2 语义框架
语义框架为扩展逻辑提供了统一解释环境，常由世界集合与关系结构组成。不同框架对应不同逻辑系统，也会影响可满足性的判定难度与方法选择。
2.3.3 扩展逻辑的判定特点
扩展逻辑往往具有更强表达力，因此判定过程也更具挑战性。某些系统可以通过专门的语义技巧处理，而另一些则会在复杂性上显著高于命题逻辑。
3 计算机科学中的可满足性
3.1 SAT 问题
SAT 问题是命题可满足性的标准计算问题，也是计算机科学中最具代表性的可满足性形式之一。它要求判断一个布尔公式是否存在满足它的真值赋值。
3.1.1 问题定义
SAT 的输入通常是一个布尔公式，输出则是“可满足”或“不可满足”。若可满足，求解器还常进一步给出一个具体赋值作为见证。
3.1.2 经典编码方式
许多实际问题会被编码为 SAT 实例，例如将约束、选择关系和互斥条件转化为布尔变量与子句。常见编码包括直接编码、顺序编码和基于辅助变量的结构化编码。
3.1.3 典型应用场景
SAT 广泛用于硬件验证、软件分析、规划问题和组合搜索。由于其通用性强，许多看似不同的问题都能转化为 SAT 形式求解。
3.2 SMT 问题
SMT 是在 SAT 基础上加入背景理论约束的可满足性问题。它关心的不只是布尔结构，还包括整数、实数、数组、位向量等特定理论中的一致性。
3.2.1 理论组合
SMT 的关键在于把多个理论模块组合起来处理，例如布尔逻辑与算术理论协同工作。组合后既要保持各自理论的正确性，又要解决它们之间的交互约束。
3.2.2 约束求解
SMT 求解通常通过不断检查布尔层面的分配，并在理论层面验证一致性来实现。若发现冲突，系统会回溯并学习新的约束，以缩小搜索空间。
3.2.3 与 SAT 的关系
SAT 可以看作 SMT 的基础层，而 SMT 则是在布尔求解之上增加语义丰富的理论推理。很多 SMT 求解器内部都包含 SAT 引擎作为核心组件。
3.3 约束满足问题
约束满足问题研究变量在给定域内是否能取值，使所有约束同时成立。它是可满足性在更一般组合对象中的体现，常见于人工智能和运筹优化。
3.3.1 变量与域
CSP 通常由变量集合、每个变量的取值域以及若干约束组成。求解的目标是为每个变量选择一个域内值，同时不违反任何限制。
3.3.2 约束图
约束图把变量与约束之间的关系表示为图结构，有助于分析问题的局部依赖和整体连接性。图的稀疏程度与结构特征，往往会影响求解难度。
3.3.3 求解策略
常见策略包括回溯搜索、一致性传播和启发式变量排序。对于结构清晰的问题，利用图性质和局部推理常能显著提升效率。
4 复杂性理论
4.1 判定问题的复杂度
可满足性问题的复杂性研究，重点在于判断其在不同逻辑或约束系统下属于哪一类复杂度等级。它直接反映求解所需资源的理论上限。
4.1.1 多项式时间可解性
若某类可满足性问题能在多项式时间内解决，则说明它具有较好的可处理性。部分受限逻辑片段或结构特殊的约束系统确实属于这一类。
4.1.2 NP 完全性
命题 SAT 是 NP 完全性的经典代表，这意味着它既属于 NP，又足以表达 NP 中的所有问题。该结果奠定了可满足性在复杂性理论中的核心地位。
4.1.3 更高复杂度层级
在一阶逻辑、时态逻辑或某些扩展约束系统中，可满足性可能落入更高复杂度层级，甚至出现不可判定情形。复杂度并不总是止步于 NP。
4.2 归约与完备性
归约是证明问题难度的重要工具，而完备性则用于刻画某类问题中的代表性困难实例。可满足性研究中，二者经常配合使用。
4.2.1 多项式归约
多项式归约把一个问题在多项式时间内转换成另一个问题，从而比较两者的难度。如果某可满足性问题能承载一个已知难题，则其复杂度上界与下界都更易分析。
4.2.2 典型完备问题
SAT、3-SAT、某些 CSP 以及特定逻辑片段的可满足性问题，都是常见的完备问题。它们在不同复杂度类别中承担“基准难题”的角色。
4.2.3 复杂性下界
下界证明说明问题至少有多难，通常借助归约从已知困难问题转化而来。对可满足性而言，这类结果帮助区分“可高效处理”和“本质困难”的边界。
4.3 可满足性的难度来源
可满足性之所以普遍困难，往往不是因为公式长度本身，而是因为其可能解的组合数量巨大，且约束之间存在复杂耦合。
4.3.1 搜索空间爆炸
变量数量稍有增加，可能的赋值组合就会指数级增长。即使每一步检查都很快，整体搜索仍可能迅速失控。
4.3.2 组合结构复杂性
约束之间并非独立，而是常常交织成复杂网络。局部看似合理的选择，放到全局可能导致无解，因此需要更强的协调与回溯机制。
4.3.3 语义约束的叠加
当逻辑语义、理论公理和结构限制同时存在时，多个层次的条件会叠加。可满足性问题因此不仅是“找值”，也是“找一种整体一致的解释”。
5 求解方法
5.1 穷举与剪枝
穷举是最直接的求解方式，通过遍历所有可能对象来判断是否存在满足条件者。由于代价高昂，实际使用时通常要配合剪枝。
5.1.1 真值表法
真值表法适用于变量较少的命题公式，通过列出全部赋值逐一检查公式结果。它直观但不适合大规模问题。
5.1.2 分支限界
分支限界通过逐步展开搜索树，并利用上界或冲突信息提前排除不可能分支。它能减少无效探索，是常见的通用搜索思想。
5.1.3 剪枝启发式
剪枝启发式依赖经验规则或结构特征，尽早舍弃明显无望的路径。良好的启发式往往决定了求解器在实践中的效率。
5.2 归结与逻辑推理
归结是自动推理中的经典方法，尤其适合处理子句形式的公式。它通过机械化推导寻找矛盾，从而判断原公式是否可满足。
5.2.1 归结原理
归结原理利用互补文字消去冲突信息，并生成更强的约束。若最终推出空子句，则说明原集合不可满足。
5.2.2 证明与反证
在可满足性分析中，证明“不可满足”常比直接构造模型更易形式化。反证法因此成为重要手段：先假设可满足，再通过推理得到矛盾。
5.2.3 自动推理系统
自动推理系统将归结、重写、简化等技术结合起来，用于机械化判断和证明构造。它们在定理证明和形式验证中具有稳定作用。
5.3 现代 SAT/SMT 求解技术
现代求解器通常综合使用搜索、学习、理论传播和增量处理等技术，以适应复杂实例的规模和结构变化。
5.3.1 DPLL 算法
DPLL 是经典的布尔可满足性搜索算法，核心思想是变量分裂、单子句传播与回溯。它奠定了现代 SAT 求解器的基本框架。
5.3.2 CDCL 算法
CDCL 在 DPLL 的基础上加入冲突驱动的学习机制，能够记录失败经验并减少重复搜索。它是当代 SAT 求解器的主流范式。
5.3.3 冲突分析与学习
当搜索走入死路时，求解器会分析冲突来源，并提取有用的学习子句。新知识会阻止相同错误路径再次出现。
5.3.4 理论传播与增量求解
在 SMT 中，理论传播负责把背景理论中的推论及时反馈给搜索过程。增量求解则允许在已有上下文基础上继续添加约束，避免重复计算。
6 应用领域
6.1 程序验证
可满足性技术是程序验证中的重要工具，常用于发现错误、检查性质和辅助推导程序行为边界。
6.1.1 模型检测
模型检测把程序或系统抽象成状态模型，再检查是否存在违反性质的可达路径。其本质上常可转化为可满足性或不可满足性判断。
6.1.2 断言检查
断言检查用于验证程序在特定位置是否满足预设条件。若某个断言对应的约束集合可满足，则可能存在反例执行。
6.1.3 不变量推断
不变量推断旨在寻找在程序执行过程中始终成立的条件。可满足性求解可以帮助筛选候选不变量，并验证其稳定性。
6.2 人工智能
在人工智能中，可满足性常用于表示和解决规划、推理以及组合决策任务。
6.2.1 自动规划
自动规划关注从初始状态到目标状态是否存在可行动作序列。很多规划问题都能转化为 SAT、SMT 或 CSP 形式处理。
6.2.2 知识表示
知识表示系统需要以可形式化的方式存储事实、规则和约束。可满足性分析可用于判断知识库是否自洽，以及某些结论是否可推出。
6.2.3 约束推理
约束推理强调在给定条件下逐步缩小可能解空间。它常用于任务分配、路径规划和智能配置等场景。
6.3 数学与工程
可满足性方法在数学证明辅助和工程设计中都很常见，尤其适合处理离散选择与组合优化问题。
6.3.1 电路验证
电路验证利用可满足性检查逻辑电路是否满足设计规格，或是否存在触发错误输出的输入组合。它是硬件测试中的关键环节。
6.3.2 调度问题
调度问题需要在时间、资源和优先级限制下安排任务。通过可满足性建模，可以判断是否存在合法排程。
6.3.3 配置优化
配置优化涉及为系统组件选择合适参数，使所有约束成立并尽量符合目标要求。可满足性为配置可行性分析提供了基础。
7 相关概念与变体
7.1 有界可满足性
有界可满足性关注在有限范围内是否存在满足条件的对象，通常是对原问题的限制版本。它常用于近似分析和可计算性研究。
7.1.1 有限域约束
当变量只能取有限集合中的值时，可满足性问题往往更容易离散化处理。有限域约束在很多实际系统中都较常见。
7.1.2 截断模型
截断模型指把原本可能无限的结构限制在某个有限范围内进行检查。它有助于把复杂问题转化为可处理的有限搜索。
7.1.3 有界模型检查
有界模型检查是一种只在有限步内验证性质的方法。它通过截断执行轨迹，把问题转为 SAT 或相关判定任务。
7.2 最优化可满足性
最优化可满足性不仅要求满足约束，还希望在多种可行解中找到更优者。它把“是否存在解”与“解的质量”结合起来。
7.2.1 最大可满足性问题
最大可满足性问题要求尽可能满足更多子句，而不是强求全部成立。它适用于条件冲突不可避免的场景。
7.2.2 权重约束
权重约束为不同条件赋予不同重要性，使求解目标更细致。系统通常会优先保留高权重约束，再兼顾次要条件。
7.2.3 近似求解
当精确求解成本过高时，近似方法可提供可接受的解或上界估计。其重点是实用效率，而非完全最优。
7.3 可解性与可满足性的区别
可解性与可满足性虽然相关，但并不完全相同。前者强调能否有效构造结果，后者强调结果是否存在。
7.3.1 存在解
可满足性只关心是否存在至少一个满足条件的对象，不要求立即给出构造过程。它是一种存在性判断。
7.3.2 可计算解
可解性更进一步，关注是否存在可执行算法能在有限步骤内找到解。某些问题在逻辑上有解，但算法上未必容易找到。
7.3.3 构造性与非构造性
构造性方法直接产出对象，非构造性方法则可能只证明存在而不显式给出。两者在理论与实践中的价值并不相同。
8 历史与发展
8.1 早期逻辑研究
可满足性的思想可追溯到早期逻辑与数学基础研究。随着符号逻辑的发展，人们开始系统讨论公式何时有解释、何时无模型。
8.2 计算复杂性时代的兴起
20 世纪中后期，复杂性理论的建立使可满足性问题的地位迅速上升。SAT 的 NP 完全性结果尤其具有标志意义，推动了大量后续研究。
8.3 自动推理与求解器发展
随着计算机性能提升，自动推理和求解器技术不断成熟。归结、DPLL、CDCL 以及 SMT 框架的出现，使可满足性从理论问题走向大规模应用。
8.4 当代研究趋势
当前研究更关注求解效率、可扩展性与领域特定优化，同时也重视与程序分析、人工智能和工程设计的结合。面向不同逻辑片段和约束结构的专用求解器，仍是活跃方向。