在 CNF 范式下可使用的推导规则 命题逻辑下： 如果有多于一对互补文字，则归结式（Resolvant） 永真。 Related Horn Clause Prolog 的底层 DPLL: 归结最早用于 DP 算法，后 DPLL 改进其中的 SAT 求解部分，不再需要显式表示归结式（空间从指数→线性）
