带文字改名策略的DPLL算法

摘要：

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

关键词：不可满足公式、DPLL算法、对称规则、难例

所属期刊栏目：1

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60463001;10410638;60310213

在线出版日期：2008-03-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：116-125