| 带文字改名策略的DPLL算法 |
| |
| 引用本文： | 许道云,刘长云. 带文字改名策略的DPLL算法[J]. 计算机科学与探索, 2007, 1(1): 116-125. DOI: 10.3778/j.issn.1673-9418.2007.01.010 |
| |
| 作者姓名： | 许道云 刘长云 |
| |
| 作者单位： | 贵州大学,计算机科学系,贵阳,550025;贵州大学,计算机科学系,贵阳,550025 |
| |
| 摘 要： | 限制在不可满足公式的不可满足性的证明,给出了一个改进的DPLL算法—RSMLS。新的算法带有一条对称规则(文字改名规则)和三条简化规则((1,*)-消解、子公式、重复规则)。作为一个应用实例,将RSMLS算法应用于鸽巢公式P_(n-1)~n的不可满足性证明。证明了:关于RSMLS算法,公式P_(n-1)~n有一棵反驳证明树至多带有O(n~3)个结点。
|
| 关 键 词： | 不可满足公式 DPLL算法 对称规则 难例 |
| 修稿时间： | |
DPLL algorithm with literal renaming strategy |
| |
| XU Dao-yun,LIU Chang-yun. DPLL algorithm with literal renaming strategy[J]. Journal of Frontier of Computer Science and Technology, 2007, 1(1): 116-125. DOI: 10.3778/j.issn.1673-9418.2007.01.010 |
| |
| Authors: | XU Dao-yun LIU Chang-yun |
| |
| Affiliation: | Department of Computer Science，Guizhou University，Guiyang 550025，China |
| |
| 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． |
| |
| Keywords: | unsatisfiable formula DPLL algorithm symmetry rule hard example |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学与探索》浏览原始摘要信息 |
|
点击此处可从《计算机科学与探索》下载免费的PDF全文 |
