The # SAT problem also called model counting is one of the important and challenging problems in artificial intelligence .It is used widely in the field of artificial intelligence .After doing the in‐depth study of model counting algorithm CER that is based on Extension Rule , we propose a method using complementary degree for # SAT problem in this paper .We formalize the computing procedure of solving #SA T problem by introducing SE‐T ree w hich produces all the subsets of clause set that need to be computed .As the closed nodes are added into the SE‐Tree ,the most subsets that contain complementary literal(s) can never be produced ,and the true resolutions cannot be missed by pruning either .Then the concept of complementary degree is presented in this paper ,and the nodes of SE‐Tree are extended in accordance with the descending order of complementary degree .With this extended order ,the subsets that contain complementary literal (s) and have smaller size can not only be generated early ,but also can reduce the number of generated nodes that are redundant .Moreover the calculation for deciding the complementarity of subsets is reduced . Results show that the corresponding algorithm runs faster than CER algorithm and further improves the solving efficiency of problems which complementary factor is lower .%＃SA T 问题又称模型计数（model counting ）问题是人工智能领域的研究热点之一，在人工智能领域被广泛应用。在对基于扩展规则的＃SAT 问题求解方法CER（counting models using extension rules）深入研究的基础上，提出一种结合互补度的＃SA T 问题求解方法。在计算给定子句集的模型个数时，利用SE‐Tree（set enumeration tree）形式化地表达计算过程，逐步生成需要计算的子句集合，并在SE‐T ree中添加终止结点，避免大部分含互补文字子句集合的生成，且不会因剪枝而导致求解不完备。提出互补度的概念，在扩展SE‐T ree结点时按照互补度由大到小的顺序扩展，较早地生成含互补文字且长度较小的子句集合，有效减少枚举树生成的结点个数，进而减少对子句集合判断是否含互补文字的计算次数。实验结果表明：与CER方法相比该方法效率较好，且进一步改进了CER方法在互补因子较低时求解效率低下的不足。
展开▼
