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