带文字改名策略的DPLL算法

• 作者: 刘长云 许道云
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 不可满足公式 DPLL算法 对称规则 难例
• 年，卷（期）: 2007,（1）
• 所属期刊栏目: 学术研究
• 页码范围: 116-125
• 页数: 10页
• 分类号: TP301
• 字数: 11320字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.2007.01.010

摘要

限制在不可满足公式的不可满足性的证明,给出了一个改进的DPLL算法-RSMLS.新的算法带有一条对称规则(文字改名规则)和三条简化规则((1,*)-消解、子公式、重复规则).作为一个应用实例,将RSMLS算法应用于鸽巢公式Pnn-1的不可满足性证明.证明了:关于RSMLS算法,公式Pnn-1有一棵反驳证明树至多带有O(n3)个结点.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	许道云	贵州大学计算机科学系	125	460	12.0	16.0
2	刘长云	贵州大学计算机科学系	9	8	1.0	2.0