基于格局检测的模型计数方法

模型计数是指求出给定命题公式的模型数，是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用，很多现实问题都可以规约为模型计数进行求解.目前，常用的模型计数求解器主要有Cachet与sharpSAT，它们均采用完备方法且具有高效的求解能力，但其求解效率对模型数不敏感.有理由猜测：当给定问题的模型较少时，不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法，Cai等人提出了格局检测策略，并将其应用到局部搜索方法中，提出了SWcc算法，具有很高的求解效率.对SWcc算法进行扩充，分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法，给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果，以验证当给定合取范式的模型较少时，该迭代法与优化后的增量法的求解效率有所提升.

Model Counting Methods Based on Configuration Checking

Model counting is the problem of calculating the number of the models of a given propositional formula, and it is a generalization of the SAT problem. Model counting is widely used in the field of artificial intelligence, and many practical problems can be reduced to model counting. At present, there are two complete solvers which are commonly used for model counting, i.e. Cachet and sharpSAT, both of which have high solving efficiency. But their solving efficiency does not relate to the numbers of the models. It is reasonable to suppose that incomplete methods are more likely to take their advantage in efficiency and maybe they could be more suitable to solve model counting problems when the number of the models of given propositional formula is little. Local search is an efficient incomplete method for solving SAT problem. A new strategy called configuration checking (CC) has been proposed by Cai et al. and it is adopted to the local search. In this way, the SWcc algorithm has been proposed with high solving efficiency. This study puts forward two incomplete methods on basis of the SWcc algorithm, i.e. the iteration method and the improved incremental method, both of which have high efficiency. Then, the specific implementation process of the two methods is presented. At last, the experimental results of a large amount of benchmarks, according to which is found, show the advantages of the iteration method and the improved incremental method in terms of time, when the amount of the models of given conjunctive normal formula is small.