| Model counting(#SAT)is to compute the number of satisfying assignments of given formulae.All the #P problems can be reduced to #SAT in polynomial time.In artificial intelligence,many problems with complexity higher than NP can be transformed into #SAT.Therefore,the research of #SAT is of great significance to the problems in different fields that can be transformed into #SAT.However,the existing exact model counters turn out to be insufficient in large-scale problems.Besides,for most current problems,it is not necessary to get such an exact solution.Hence,to make up for the insufficient solving ability of the existing exact model counters in large-scale problems,the approximate model counting has been proposed as a practical alternative to exact model counting.Most of the best current approaches are based on XOR constraints for approximate model counting.The nature of this kind of approaches is based on sampling,cutting down the solution space by adding XOR constraints of which average length is half the number of variables.Exact model counting methods can be applied for an exact solution when the solution space is cut down to a small enough size.Finally,the approximate model counting of the overall solution space is estimated by the proportion between the solution space and the overall solution space.By further researching the existing approximate model counting algorithms,a new approximate model counter which integrates bounded solving and controllable randomization is proposed in this paper.Because a small-scale solution space would result in worse solving accuracy,by limiting the scale of solution space that applies XOR constraints,bounded solving effectively increases the accuracy of the model counter.Controllable randomization uses backbone variables and the constraints among variables,such that the short XOR constraints can reach the same reduction effect on solution space as the long ones.Normally the length of short XOR constraints is half of the long ones.It improves the quality of XOR constraints as well as the SAT solving efficiency.In order to verify the performance of these strategies,we select a total of 120 test examples from 4 fields and 2 state-of-the-art approximate model counters for experiments.The experimental results show that compared with the existing approximate algorithms,the new approximate model counter which integrates bounded solving and controllable randomization we proposed in this paper greatly improves the solution accuracy and efficiency. |
