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

• 作者: 周从华 徐宝文 陈振宇
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 可满足问题 极小不可满足 变量极小不可满足
• 年，卷（期）: 2008,（z1）
• 所属期刊栏目: 算法:设计与分析
• 页码范围: 43-47
• 页数: 5页
• 分类号: TP331
• 字数: 4206字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐宝文	东南大学计算机科学与工程学院	118	3034	31.0	51.0
2	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0
3	陈振宇	东南大学计算机科学与工程学院	4	13	3.0	3.0