形式陈述

命题公式 $\varphi$$\phi$ 称为可满足，若存在赋值 $v$$v$ 使 $v(\varphi)=\top$$v(\phi )=\mathrm{\top }$；否则称不可满足。公式集 $\Gamma$$\mathrm{\Gamma }$ 可满足，若存在同一个赋值同时使每个 $\gamma\in\Gamma$$\gamma \in \mathrm{\Gamma }$ 为真。于是

$$ \varphi\text{ 可满足}\iff\neg\varphi\text{ 非永真}, \qquad \varphi\text{ 不可满足}\iff\neg\varphi\text{ 永真}. $$$$\phi \text{ 可满足}⟺\mathrm{\neg }\phi \text{ 非永真},\phi \text{ 不可满足}⟺\mathrm{\neg }\phi \text{ 永真}.$$

对有限 $\Gamma=\{\gamma_1,\ldots,\gamma_m\}$$\mathrm{\Gamma }=\{{\gamma }_1,\dots ,{\gamma }_m\}$，共同可满足等价于合取 $\bigwedge_i\gamma_i$$\underset{i}{\bigwedge }{\gamma }_i$ 可满足。

直觉

可满足性只要求找到一个让全部约束同时成立的布尔世界；不可满足性则要求证明每个可能赋值都会违反至少一项约束。

例子与边界

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

推论与应用

可满足性把规划、排程、验证和组合搜索编码为布尔约束。SAT 求解器返回模型或不可满足证明；语义蕴涵也可化为不可满足性检查。

参考资料

• Daniel J. Velleman, How to Prove It: A Structured Approach, 3rd ed., Cambridge University Press, 2019，§§1.1–1.2, sentential semantics and truth tables。
• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§1.2, satisfaction by truth assignments。