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-1 as a refutation tree with at most O（n³） nodes．

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

摘要：

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

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