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

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

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

许道云+,刘长云

贵州大学计算机科学系，贵阳 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

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

摘要/Abstract

摘要：

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

关键词: 不可满足公式, 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 Pⁿ_n-1.Show with respect to RSMLS algorithm that Pⁿ_n-1as a refutation tree with at most O（n³） nodes．

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

许道云+,刘长云.

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

[J]. 计算机科学与探索, 2007, 1(1): 116-125.

XU Dao－yun,LIU Chang－yun

DPLL algorithm with literal renaming strategy

[J]. Journal of Frontiers of Computer Science and Technology, 2007, 1(1): 116-125.