计算机科学与探索 ›› 2007, Vol. 1 ›› Issue (1): 116-125.

• 学术研究 • 上一篇    下一篇

带文字改名策略的DPLL算法*

许道云+,刘长云   

  1. 贵州大学 计算机科学系,贵阳 550025

  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2007-06-06 发布日期:2007-06-06
  • 通讯作者: 许道云

DPLL algorithm with literal renaming strategy

XU Dao-yun,LIU Chang-yun

  

  1. Department of Computer Science,Guizhou University,Guiyang 550025,China

  • Received:1900-01-01 Revised:1900-01-01 Online:2007-06-06 Published:2007-06-06
  • Contact: XU Dao-yun

摘要:

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

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

Abstract:

Restricted on the proof of unsatisfiability of unsatisfiable formulas,a modified DPLL—RSMLS algorithm is presented.The new algorithm has a symmetry rule(Literal renaming) and three simplifing rules((1,*)-Resolution,Subformula,and Multiple).As an example,RSMLS algorithm is applied for the proof of unsatisfiability of pigeon-hole formula Pnn-1.Show with respect to RSMLS algorithm that Pnn-1 as a refutation tree with at most O(n3) nodes.

Key words: unsatisfiable formula, DPLL algorithm, symmetry rule, hard example