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

SAT-based algorithm for knowledge reasoning

作　　者：苏开乐[1] 陈清亮[1] 岳伟亚[1] 

机构地区：[1]中山大学计算机科学系,广州510275

出　　处：《计算机科学与探索》2007年第1期79-86,共8页Journal of Frontiers of Computer Science and Technology

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

摘　　要：传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[1]中,给出了一个实用而紧致的知识的语义模型——知识结构(knowledge struc- ture),并给出相应的利用BDD(Binary Decision Diagram)的符号化计算方法,实验表明这种基于BDD的算法比传统方法有很大的优势,但这种基于BDD的方法在计算规模大的例子时仍存在明显的组合爆炸。文章在知识结构(knowledge structure)的语义基础上,通过挖掘知识结构语义中各元素的关系,把知识的计算规约于可满足性问题(SAT),因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD。实验结果证实了这种方法的有效性。Traditional knowledge reasonings rely on the general theorem provers and may suffer the state ex- plosion problem and can only deal with toy examples.A more concrete model of knowledge called knowledge structure has been introduced in[1],which presents a BDD-based approach for computing knowledge and shows great improvement.But the BDD-based approach still has a substantial state explosion problem.Based on the knowledge structure,an alternative and effective way by SAT solving for the knowledge reasoning in a group of agents is illustrated,since SAT can be much more powerful in dealing with the state explosion problem than BDDs.Finally the experimental results prove this.

关 键 词：可满足性问题 知识结构 推理算法 计算规模 组合爆炸 计算方法 符号化 定理证明器 语义模型 语义基础 实验 结构语义 自动化 小规模 元素 效率 通用 处理 

分 类 号：TP[自动化与计算机技术]