假设用一个SAT求解器判断一个SAT公式的可满足性，如果求解器给出“公式可满足”的结论，并给出一个解，即一个满足公式的真值赋值，那么验证此结论是否正确很容易：只需将真值赋值带入公式，检查所有子句是否满足即可。
例子：
F1 = (x1 ∨x2 ∨x3)∧(x1 ∨x2 ∨¬x3)∧(¬x1 ∨¬x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ x3)
一个求解器给出一个解：x1 =0, x2=1, x3=0，那么验证x1 =0, x2=1, x3=0令f1可满足。
结论：F1是可满足的。
然而，如果求解器给出“公式不可满足”，你能相信求解器吗？尽管当前的 SAT 求解器非常强大，但在复杂的求解器实现过程中仍有可能出现错误，也就是说，需要判断SAT公式的不可满足性。
此外在一些应用中，比如使用 SAT 求解器来证明开放式数学问题时，如在插值计算（computing interpolants）和最小不可满足子公式（Minimally Unsatisfiable Subformulas ，MUS），判断SAT公式的不可满足性具有重要的应用价值。
罗宾逊归约证明是自动定理证明和逻辑编程中使用基于罗宾逊归约规则的演绎推理，它可以用来证明SAT公式的不可满足性，也可以用来简化逻辑公式并得出新结论。
1. 罗宾逊归约规则
归约规则是基于两个CNF公式的子句C1，C2得出新子句C3：
(A ∨ x) ∧ (B ∨ ¬x)
———————
A ∨ B
记为：
C1 = A ∨ x
C2 = B ∨ ¬x
C3 = C1 ⊗x C2
2. 罗宾逊归约证明（Robinson resolution proof)
罗宾逊归约证明是使用罗宾逊归约规则的演绎证明。
例子：
判定公式F2是不可满足的。
F2 = (a ∨ ¬b) ∧ (¬ a ∨ c ∨ ¬d) ∧ (a ∨ c ∨ ¬d) ∧ (¬c ∨ ¬e) ∧ (¬c ∨ e) ∧ (c ∨ d)
证明：
a ∨ ¬b : premise
¬ a ∨ c ∨ ¬d : premise
a ∨ c ∨ ¬d : premise
¬c ∨ ¬e : premise
¬c ∨ e : premise
c ∨ d : premise
¬c : 4⊗e 5
c ∨ ¬d : 2⊗a 3
c : 6⊗d 8
10. ⊥
结论：F2是不可满足的。
注意，如果使用罗宾逊归约规则如下，得不出F2是不可满足的结论。
证明：
a ∨ ¬b : premise
¬ a ∨ c ∨ ¬d : premise
a ∨ c ∨ ¬d : premise
¬c ∨ ¬e : premise
¬c ∨ e : premise
c ∨ d : premise
¬b ∨ c ∨ ¬d : 1⊗2
a ∨ ¬d ∨ ¬e : 3⊗4
a ∨ ¬d ∨ ¬c : 8⊗5
10. a : 9⊗6
参考文献：
【1】https://en.wikipedia.org/wiki/Resolution_(logic)
【2】https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-sat/resolution.html
转载本文请联系原作者获取授权，同时请注明本文来自柳渝科学网博客。
链接地址：https://wap.sciencenet.cn/blog-2322490-1409915.html?mobile=1
收藏
