可满足公式

公式可满足，只要求找到一个允许的结构或赋值，让全部约束同时成立；永真则要求所有结构或赋值都成功。可满足性是存在性概念，因此一个失败赋值不能否定它，必须证明每个候选都会违反至少一项约束；不可满足性也等价于公式的否定永真。公式集可满足时，还必须由同一个模型同时满足全部成员。

令 $\phi =(p\vee q)\wedge (\mathrm{\neg }p\vee q)$。当 $q=\mathrm{\top }$ 时，两条子句都成立，$p$ 可任取；当 $q=\mathrm{\perp }$ 时，两条子句分别要求 $p$ 和 $\mathrm{\neg }p$，无法同时成立。因此满足赋值恰好是 $q=\mathrm{\top }$ 的两种赋值；逐子句分析同时给出了见证和失败原因。

每个公式单独可满足不意味着整个集合共同可满足，例如 $\{p,\mathrm{\neg }p\}$。空公式集由任意赋值满足。SAT 的证据是一个赋值，可在线性于公式大小的时间检查，但寻找证据在一般情形可能困难。

例如 $P\vee Q$ 在 $P=\mathrm{\top },Q=\mathrm{\perp }$ 时真，在两者均假时假，所以它可满足却不是永真。对一阶公式 $x^2+1=0$，在实数结构中不可满足，在复数结构中可满足，说明必须明确结构类别。

真值表理路真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。决定有限命题公式的可满足性，SAT 问题由此成为复杂度理论核心，并把规划、排程、验证和组合搜索编码为布尔约束。求解器返回模型或不可满足证明，语义蕴涵理路语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。也可化为不可满足性检查。命题紧致性定理理路命题紧致性定理Propositional compactness theorem一个命题公式集可满足，当且仅当它的每个有限子集可满足。进一步把公式集的有限可满足性提升为全局可满足性；模型构造和自动求解器都围绕寻找见证展开。

在程序验证中，有界模型检查理路有界模型检查Bounded model checking · BMC · SAT-based bounded model checking将前 k 步转移展开为 SAT 公式寻找有界反例，并明确无解结果何时不能升级为全局证明。让一个满足赋值编码长度至多 $k$ 的反例，PDR/IC3理路Property-Directed Reachability / IC3Property-directed reachability · PDR · IC3以 SAT 查询阻塞坏状态前驱、学习逐层归纳子句，最终得到反例或安全归纳不变式。则反复调用 SAT 学习可归纳子句；SMT 软件验证理路基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。还允许数组、算术等背景理论。一次 SAT/SMT 查询只寻找一个模型或证明一个编码不可满足；要断言所有执行满足规格，还必须证明编码覆盖相应路径，或得到对转移封闭的不变式。