Research On Model Counting Methods Based On Local Search

Model counting is the problem of calculating the number of the models of a given propositional formula.It's an important hard problem in the field of automated reasoning.Model counting is widely used in the field of artificial intelligence,and many practical problems can be reduced to model counting.At present,the complete solvers which are commonly used for model counting have high solving efficiency,but their solving efficiency does not relate to the number 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 for the given propositional formula is little.This paper intends to put forward a few new algorithms for model counting with higher solving efficiency by taking advantage of the incomplete methods.The solving capacity of an algorithm is measured by the solving time used to get the correct number of the models for the given conjunction normal form.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 local search.In this way,the SWcc(Smoothed Weighting with Configuration Checking)algorithm has been proposed with high solving efficiency.Neighboring variable is defined in configuration checking which sovles the problem of local optimum in the process of fliping variables.This paper first puts forward two incomplete methods on basis of the SWcc algorithm,i.e.the iteration method and the incremental method,both of which have high efficiency.The SWcc algorithm can get a complete satisfied true assignment in each iteration.Then the specific implementation process of the two methods are presented.The iteration method adds a clause to the conjunction normal form in the negative form of the satisfied true assignment get in the former iteration,in this way,the problem of repeated assignments is solved.The iteration method can get a different satisfied true assignment in each iteration.In the mean time,the number of the models are recorded.The incremental method also adopts the method of adding a clause,but it will recalculate the information of the neighboring variables and the next iteration will proceed on the basis of the current assignment.Many calculating operations for initialization will be reduced.This paper makes further efforts to improve the efficiency for the incomplete algorithms.Two heuristic strategies are put forward and they are adopted to the former two methods.This paper adopts the acceleration strategy to the iteration method,and presents the details.In theory it will be appropriate for the conjunction normal form whose number of the models is large,and its efficency will be better if some satisfied true assignment have the same part.This paper adopts the improved strategy for the assignments to the incremental method,in this way,the number of variables for the clause needed to be added can be extremely reduced.According to which,the advantage of configuration checking can be put to good use.At last,this paper shows the experimental results of a large number of benchmarks,and finds the advantages of the iteration method and the incremental method in terms of time,when the amount of the models for the given conjunctive normal formula is small.The incompleted methods in this paper will also get good results when solving some specific benchmarks by adoping the two heuristic strategies.