Abstract:

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.

Key words: knowledge structure, knowledge reasoning, satisfiability（SAT）

摘要：

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

关键词: 知识结构, 知识推理, 可满足性问题（SAT）