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

摘要：

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

关键词：知识结构、知识推理、可满足性问题(SAT)

所属期刊栏目：1

分类号：TP301(计算技术、计算机技术)

资助基金：国家重点基础研究发展计划973计划2005CB321902;国家自然科学基金60496327;10410638;60473004;广东省自然科学基金04205407;上海市智能信息处理重点实验室开放课题

在线出版日期：2008-03-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：79-86