一种规约于可满足性问题(SAT)的知识推理算法

• 作者: 岳伟亚 苏开乐 陈清亮
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 知识结构 知识推理 可满足性问题(SAT)
• 年，卷（期）: 2007,（1）
• 所属期刊栏目: 学术研究
• 页码范围: 79-86
• 页数: 8页
• 分类号: TP301
• 字数: 7668字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.2007.01.006

摘要

传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题.在文[1]中,给出了一个实用而紧致的知识的语义模型--知识结构(knowledge structure),并给出相应的利用BDD(Binary Decision Diagram)的符号化计算方法,实验表明这种基于BDD的算法比传统方法有很大的优势,但这种基于BDD的方法在计算规模大的例子时仍存在明显的组合爆炸.文章在知识结构(knowledge structure)的语义基础上,通过挖掘知识结构语义中各元素的关系,把知识的计算规约于可满足性问题(SAT),因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD.实验结果证实了这种方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	中山大学计算机科学系	22	309	11.0	17.0
2	岳伟亚	中山大学计算机科学系	5	80	4.0	5.0
3	陈清亮	中山大学计算机科学系	4	53	3.0	4.0