Abstract: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.