一种基于消解的变量极小不可满足子公式的提取方法

摘要：

变量极小不可满足(VMU)问题是极小不可满足(MU)问题的一个扩充和延伸.着重研究VMU子公式的提取算法.首先从理论上比较MU和VMU的基本性质,并分析了目前流行的MU子公式提取算法.研究Davis-Putman-消解的基本性质,给出一个判定变量极小不可满足公式的充分必要条件,进而提出一个基于消解的VMU子公式提取算法.此算法可以使用ZBDDs压缩存储消解式,并实现单步多重消解.

关键词： 可满足问题 极小不可满足 变量极小不可满足 VMU子公式 提取算法 多重消解

作者: 陈振宇 徐宝文 周从华

作者单位: 东南大学计算机科学与工程学院,南京,210096 江苏大学计算机科学与通信工程学院,镇江,212013

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 43-47

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）