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