归结原理

归结原理（resolution principle）是一种从子句推出新子句的推理规则。命题逻辑中的一次归结，从 $A\vee p$ 和 $B\vee \mathrm{\neg }p$ 推出 $A\vee B$；互补文字 $p,\mathrm{\neg }p$ 被消去。将待证结论的否定与前提一同写成合取范式，若反复归结推出空子句，就证明这些公式不能同时为真。

本文先讨论只有有限个命题变量的情形。一阶逻辑归结还涉及量词处理、变量改名和合一，不能直接把命题版本的有限枚举结论搬过去。

一次归结保留的逻辑信息

用集合表示子句时，$A$ 和 $B$ 表示剩余文字的析取。取 $C_1=p\vee q$、$C_2=\mathrm{\neg }p\vee r$，归结式为 $q\vee r$。若 $p$ 假，第一条前提强迫 $q$ 真；若 $p$ 真，第二条强迫 $r$ 真。无论哪种情况，$q\vee r$ 都真。这证明规则的可靠性：任何满足两个亲本子句的赋值，也满足归结式。

归结式通常比两个亲本的合取弱，不能据此删除亲本而保持等价。例如 $p=0,q=0,r=1$ 满足 $q\vee r$，却不满足 $p\vee q$。可靠性保证的是前提蕴含归结式，而不是两边逻辑等价。

每次二元归结只选一对互补文字。由 $p\vee q$ 与 $\mathrm{\neg }p\vee \mathrm{\neg }q$ 对 $p$ 归结，得到的是重言子句 $q\vee \mathrm{\neg }q$。若把两对互补文字同时删掉而得到空子句，就会把一个可满足的前提集误判为矛盾；例如 $p=1,q=0$ 已同时满足两个前提。

从四条约束得到空子句

考虑教学用子句集 $$C_1=p\vee q,C_2=\mathrm{\neg }p\vee r,C_3=\mathrm{\neg }q,C_4=\mathrm{\neg }r.$$ 它要求 $p,q$ 至少一真，而两者任一为真又会经约束迫使 $r$ 为真，最后一条却要求 $r$ 假。归结把这个矛盾写成可逐步核验的推导： $$\begin{array}{cccc}{C}_1,C_2& ⊢q\vee r& & \text{消去 }p,\\ q\vee r,C_3& ⊢r& & \text{消去 }q,\\ r,C_4& ⊢◻& & \text{消去 }r.\end{array}$$

箭头保留每一步的两个亲本；空子句表示没有任何赋值能使全部前提成立。

空子句是零个文字的析取，恒为假。每一步归结保持“原前提的任意模型也满足已推导子句”这个性质，故一旦推出空子句，原前提不可能有模型。这是归结反证法的正确性依据。

若想证明原来三个子句 $C_1,C_2,C_3$ 蕴含 $r$，便可临时加入结论的否定 $\mathrm{\neg }r$，使用上述反驳。一般地，$\Gamma \models H$ 当且仅当 $\Gamma \cup \{\mathrm{\neg }H\}$ 不可满足。若删去 $C_3$，推导停在 $q\vee r$；此时 $p=0,q=1,r=0$ 满足剩余前提，故不能再声称蕴含 $r$。

命题归结的反驳完备性

反驳完备性说：有限命题子句集不可满足时，存在有限归结推导得到空子句。它不表示归结单独就能导出每一个语法形式的有效公式。

以下通过消去一个变量证明。选变量 $p$，删除重言子句和重复文字后，把子句分成三类：不含 $p$ 的 $R$，含正文字的 $p\vee A_i$，含负文字的 $\mathrm{\neg }p\vee B_j$。构造新集合 $S^{\prime }$，保留 $R$，并对每对正负亲本加入 $A_i\vee B_j$，然后删去全部含 $p$ 的亲本。

原集合的模型限制到其余变量后一定满足 $S^{\prime }$，这是归结可靠性。反向考虑任意满足 $S^{\prime }$ 的赋值：若某个 $A_i$ 假，就必须取 $p=1$；这时所有 $B_j$ 都真，否则对应归结式 $A_i\vee B_j$ 为假。若没有 $A_i$ 假，所有正亲本已真；可取 $p=0$ 使全部负亲本为真。因此新赋值总能扩展成原集合的模型。新旧集合等可满足。

对变量数作归纳。零个变量时，不可满足的子句集必含空子句。多于零个变量时，若原集合不可满足，消元后的 $S^{\prime }$ 也不可满足；按归纳假设，它有空子句的归结推导。$S^{\prime }$ 中每条新增子句本来就可由原集合一步归结得到，把这些推导接在前面，就得到原集合的反驳。变量每次减少一个，归纳有限结束，完备性得证。

一个有限饱和程序

下面用非零整数表示文字，例如 1 为 $p$、-1 为 $\mathrm{\neg }p$。函数复制输入，不改写调用者的子句；返回 True 表示已推导矛盾，返回 False 表示归结闭包中没有空子句，按上述完备性即为可满足。它是教学实现，未加入现代 SAT 求解器的学习、回跳或启发式。

Python 3

def resolution_unsat(source):
    clauses, seen = [], set()
    for row in source:
        clause = frozenset(row)
        if any(type(x) is not int or x == 0 for x in clause):
            raise ValueError("literals must be nonzero integers")
        if not clause:
            return True
        if any(-x in clause for x in clause):
            continue
        if clause not in seen:
            seen.add(clause)
            clauses.append(clause)
    i = 0
    while i < len(clauses):
        for j in range(i):
            for pivot in clauses[i]:
                if -pivot not in clauses[j]:
                    continue
                child = (clauses[i] - {pivot}) | (clauses[j] - {-pivot})
                if not child:
                    return True
                if any(-x in child for x in child):
                    continue
                if child not in seen:
                    seen.add(child)
                    clauses.append(child)
        i += 1
    return False

example = [{1, 2}, {-1, 3}, {-2}, {-3}]
assert resolution_unsat(example)
assert not resolution_unsat([{1, 2}, {-1, -2}])
assert not resolution_unsat([])
assert resolution_unsat([[]])
assert not resolution_unsat([{1, -1}])
print("all checks passed")

已出现 $n$ 个变量时，非重言子句中的每个变量有缺席、正、负三种状态，所以至多有 $3^n$ 种。程序只在首次出现时加入子句，因此终止；每对不同子句都会在较晚者被处理时检查全部互补文字，终止时达到归结闭包。用普通集合运算估计，每对子句至多尝试 $n$ 个主元，每次合并和重言检查需 $O(n)$ 时间，给出宽松上界 $O(n^2{9}^n)$，子句存储为 $O(n{3}^n)$；这不计输入读取与去重的成本。指数上界说明“存在完整有限算法”并不等于“大型问题容易求解”。