不确定性的困惑与NP理论分享 http://blog.sciencenet.cn/u/liuyu2205 平常心是道

博文

罗宾逊归约证明(Robinson resolution proof)

已有 623 次阅读 2023-11-16 20:14 |个人分类:在法国教逻辑课|系统分类:科研笔记

设用一个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=0f1满足。

结论:F1是可满足的。


然而,如果求解器给出公式不可满足,你能相信求解器吗?尽管当前的 SAT 求解器非常强大,但在复杂的求解器实现过程中仍有可能出现错误,也就是说,需要判断SAT公式的不可满足性。


此外在一些应用中,比如使用 SAT 求解器来证明开放式数学问题时,如在插值计算(computing interpolants)和最小不可满足子公式(Minimally Unsatisfiable Subformulas MUS),判断SAT公式的不可满足性具有重要的应用价值。


罗宾逊归约证明是自动定理证明和逻辑编程中使用基于罗宾逊归约规则的演绎推理,它可以用来证明SAT公式的不可满足性,也可以用来简化逻辑公式并得出新结论。 


1. 罗宾逊归约规则


归约规则是基于两个CNF公式的子句C1C2得出新子句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)


证明:

  1. a ¬b              : premise

  2. ¬ a c ¬d      : premise

  3. a c ¬d         : premise

  4. ¬c ¬e             : premise

  5. ¬c e               : premise 

  6. c d                 : premise

  7. ¬c                   : 4e 5

  8. c ¬d              : 2a 3

  9. c                       : 6d 8

  10. 10.


结论:F2是不可满足的。


注意,如果使用罗宾逊归约规则如下,得不出F2是不可满足的结论。


证明:

  1. a ¬b              : premise

  2. ¬ a c ¬d      : premise

  3. a c ¬d         : premise

  4. ¬c ¬e             : premise

  5. ¬c e               : premise 

  6. c d                 : premise

  7. ¬b c ¬d        : 12

  8. a ¬d ¬e        : 34

  9. a ¬d ¬c        : 85

  10. 10. a                      : 96


参考文献:

1https://en.wikipedia.org/wiki/Resolution_(logic)

2https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-sat/resolution.html





https://m.sciencenet.cn/blog-2322490-1409915.html

上一篇:与chatgpt关于“停机问题”的对话 (2023/11/14)
下一篇:简介“悖论与系统” - Yves Barel

1 杨正瓴

该博文允许注册用户评论 请点击登录 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-2-29 10:16

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部