| 命题逻辑可满足性问题的算法分析 |
| |
| 引用本文： | 李未,黄雄.命题逻辑可满足性问题的算法分析[J].计算机科学,1999,26(3):1-9. |
| |
| 作者姓名： | 李未 黄雄 |
| |
| 作者单位： | 北京航空航天大学计算机系，北京航空航天大学计算机系 北京 100083，北京 100083 |
| |
| 基金项目： | 国家自然科学基金，博士点基金 |
| |
| 摘 要： | 1 引言可满足性问题(以下简称SAT)是问:对于一个命题逻辑公式,是否存在对其变元的一个真值赋值使之成立?这个问题在许多领域都有非常重要的意义,其快速求解算法的研究成为计算机科学的中心课题之一。例如在机器定理证明领域,某命题是否是一个和谐的公理集合的推论,这个问题归结为该命题的反面与该公理集合一起是否是不可满足的。通过量词消去技术和Herbrand定理的作用,谓词逻辑公式的不可满足性可以归结为命题逻辑公式的不可满足性。在知识库维护中,当知识以逻辑公式的形式表达时,知识库的一致性检查可以归结为命题逻辑公式的可满足性。在开放逻辑中,新事实是否与已有的知识矛盾,当遇到事实反驳时如何求得最大和谐的知识集,这些问题最后都要归结为命题逻辑公式的可满足性。1971年Cook首次证明了SAT是NP-完全的,从而大量的计算问题都可以归约到SAT。正是由于SAT的重要地位,各国学者对它进行了广泛而深入的研究。
|
| 关 键 词： | 命题逻辑 可满足性问题 算法分析 计算机 |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
