摘要
#SAT问题又称模型计数(model counting)问题是人工智能领域的研究热点之一,在人工智能领域被广泛应用.在对基于扩展规则的#SAT问题求解方法 CER(counting models using extension rules)深入研究的基础上,提出一种结合互补度的#SAT问题求解方法.在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合,并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备.提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数.实验结果表明:与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足.
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 .
出处
《计算机研究与发展》
EI
CSCD
北大核心
2016年第7期1596-1604,共9页
Journal of Computer Research and Development
基金
国家自然科学基金项目(61402196
61272208
61133011
61003101
61170092)
中国博士后科学基金项目(2013M541302)
吉林省科技发展计划基金项目(20140520067JH)~~
关键词
扩展规则
模型计数
CER方法
互补度
集合枚举树
extension rule
model counting
CER （counting models using extension rules） algorithm
complementary degree
SE-Tree （set enumeration tree）
