可满足公式

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

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

$P\wedge Q$ 可满足，因为赋值 $P=Q=\mathrm{true}$ 可行；$P\wedge \mathrm{\neg }P$ 不可满足。$P\vee Q$ 可满足但不是永真。对一阶公式 $x^2+1=0$，在实数结构中不可满足，在复数结构中可满足，说明必须明确结构类别。

真值表公理库真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。决定有限命题公式的可满足性，SAT 问题由此成为复杂度理论核心，并把规划、排程、验证和组合搜索编码为布尔约束。求解器返回模型或不可满足证明，语义蕴涵公理库语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。也可化为不可满足性检查。紧致性定理公理库一阶逻辑紧致性定理First-order compactness theorem · 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 查询只寻找一个模型或证明一个编码不可满足；要断言所有执行满足规格，还必须证明编码覆盖相应路径，或得到对转移封闭的不变式。