可满足性

可满足性（satisfiability）指存在一个解释，使某个公式或一组公式同时为真。满足公式的解释称为它的模型。在命题逻辑中，解释就是给每个命题变量赋真或假；在一阶逻辑中，还需给定论域，以及常量、函数和谓词的具体含义。可满足性问的是“至少有一个模型”，量词中的“存在”是定义的关键。

例如令 $p,q$ 表示选择两项任务，$r$ 表示开启共享设备。教学约束为：至少选一项任务；选择任一任务就必须开启设备。公式为 $$F=(p\vee q)\wedge (\mathrm{\neg }p\vee r)\wedge (\mathrm{\neg }q\vee r).$$ 赋值 $p=1,q=0,r=1$ 满足全部三条约束，已经足以证明 $F$ 可满足；不需要所有赋值都满足它。

满足、有效与不可满足

将赋值记作 $v$，写 $v\models F$ 表示 $v$ 使 $F$ 真。公式可满足就是存在这样的 $v$；若每个赋值都使它为真，则称有效或重言；若没有赋值使它为真，则称不可满足。例如 $p\vee \mathrm{\neg }p$ 有效，$p\wedge \mathrm{\neg }p$ 不可满足，单个变量 $p$ 可满足但不有效。因为 $p=0$ 反驳了“每个赋值都真”，却没有反驳“存在赋值为真”。

公式集 $\Gamma$ 可满足要求同一个解释同时满足其中每一个公式。分别可满足不保证共同可满足：$\{p\}$ 和 $\{\mathrm{\neg }p\}$ 各有模型，但 $\{p,\mathrm{\neg }p\}$ 没有共同模型。处理多条约束时，不能为不同约束偷偷更换赋值。

有效性与可满足性之间有直接对应： $$F\text{ 有效}⟺\mathrm{\neg }F\text{ 不可满足}.$$ 证明是逐个赋值取否定：若每个赋值使 $F$ 真，就没有赋值使 $\mathrm{\neg }F$ 真；反过来，若不存在使 $\mathrm{\neg }F$ 真的赋值，每个赋值都必须使 $F$ 真。类似地，语义蕴含满足 $$\Gamma \models H⟺\Gamma \cup \{\mathrm{\neg }H\}\text{ 不可满足}.$$ 右边排除了“前提全真而结论假”的全部反例。这是用归结原理检验蕴含的语义依据。

一组约束的全部模型

回到任务公式。若 $r=0$，第二子句迫使 $p=0$，第三子句迫使 $q=0$；但第一子句要求 $p,q$ 至少一个为一，发生冲突。所以每个模型都必须取 $r=1$。

若 $r=1$，第二、第三子句自动成立，只需满足 $p\vee q$。因此全部模型恰为 $$(p,q,r)=(0,1,1),(1,0,1),(1,1,1).$$

一次分支把八个赋值分成两半；左支整体失败，右支有三个模型。

图中左支被排除有逻辑原因：先由两个单位要求推出 $p=q=0$，再与第一子句比较。它并不是只试了一次失败赋值就排除了整支。现在加入“设备关闭”的单位子句 $\mathrm{\neg }r$，所有模型都会被删去，新公式不可满足；若改为加入 $\mathrm{\neg }(p\wedge q)$，则只删去同时选两项的模型，仍有两个模型。这两个变式分别改变存在性和模型数量。

穷举判定与可核验证书

有限命题公式含 $n$ 个变量时，全部赋值有 $2^n$ 个。逐个检查一定终止。对于以有符号整数表示文字的 CNF，下面的程序返回找到的第一个满足赋值；返回 None 表示不存在。answer[0] 对应变量一，函数复制子句且不改写输入。变量数可为零；空子句集此时的模型是空元组 ()，应与 None 区分。

Python 3

from itertools import product

def satisfying_assignment(source, n):
    if type(n) is not int or n < 0:
        raise ValueError("n must be a nonnegative integer")
    clauses = tuple(tuple(row) for row in source)
    if any(type(x) is not int or x == 0 or abs(x) > n
           for row in clauses for x in row):
        raise ValueError("literal outside the declared variables")
    for values in product((False, True), repeat=n):
        if all(any(values[abs(x) - 1] == (x > 0) for x in row)
               for row in clauses):
            return values
    return None

clauses = [(1, 2), (-1, 3), (-2, 3)]
assert satisfying_assignment(clauses, 3) == (False, True, True)
assert satisfying_assignment(clauses + [(-3,)], 3) is None
assert satisfying_assignment([], 0) == ()
assert satisfying_assignment([()], 0) is None
print("all checks passed")

外层循环恰好枚举每个赋值一次，内层的 any 对应子句的析取，all 对应子句间的合取，所以返回的结果满足定义；全部枚举后仍没找到模型，就确实不可满足。设有 $m$ 个子句、总文字数 $L$，每个赋值的检查最坏需 $O(m+L)$ 时间，生成与保存赋值需 $O(n)$，总时间上界为 $O(2^n(n+m+L))$；包括输入副本的空间为 $O(n+m+L)$。

一个给定模型只需扫描公式就能核验；声称“没有模型”却不能由一个失败赋值证实，通常需要完整搜索或可检查的反驳证明。命题可满足性问题 SAT 是 NP 完全问题，指一般输入的最坏情况复杂度；它不表示每一个具体公式都很难，也不等于已经证明不存在多项式时间算法。Cook 的工作给出了与非确定性多项式时间计算之间的归约联系。

一阶逻辑中的解释与范围

在通常采用非空论域的一阶逻辑中，公式 $\mathrm{\exists }xP(x)$ 可满足：取论域 $\{a\}$，令 $P(a)$ 真即可。公式 $\mathrm{\forall }xP(x)\wedge \mathrm{\exists }x\mathrm{\neg }P(x)$ 不可满足，因为后半要求一个不满足 $P$ 的对象，前半却要求论域中每个对象都满足 $P$。

还要区分“一般模型”和“有限模型”。在含等号及一元函数 $f$ 的语言中，“$f$ 为单射且不是满射”在自然数论域上有模型，例如 $f(n)=n+1$；它却没有有限模型，因为有限集合到自身的单射必为满射。因此不能以搜索所有小有限论域都失败，就断言一般不可满足。一阶逻辑没有像有限命题真值表那样总会结束的通用判定方法；使用何种逻辑、是否限制模型范围，都是可满足性问题本身的一部分。