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

SAT-based algorithm for knowledge reasoning

传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[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.