Research On The Algorithms Of #SAT Based On The Extension Rule

#SAT is used widely in the field of artificial intelligence,and many real-world problems can be reduced to #SAT to get the number of models of a propositional theory.Extension rule is an efficient reasoning method which is complementary to resolution.It has obvious advantages in dealing with the clause set with higher complementary factor,it has been widely recognized by domestic and foreign scholars.We intend to improve the solving efficiency and solving capacity of #SAT algorithms based on Extension rule.The solving capacity of an algorithm is measured by the scale of solved problems in a limited time.After doing the in-depth study of #SAT solvers using extension rule,we propose a novel #SAT solver NCER(a Novel algorithm for Counting models using Extension Rule)based on extension rule,which adds heuristic strategy on #ER algorithm.The heuristic strategy chooses the longest clause in current set of clauses every calling procedure to reduce the maxterm space,and it could help decrease the frequency of recursive invocation to enhance the efficiency of solving.We also propose a mixed model counting algorithm called NCDPER(a Novel algorithm for Counting models using Davis-Putnam procedure and Extension Rule)by combining NCER algorithm and CDP(Counting models using Davis-Putnam procedure)algorithm,for solving the poor performance on instances where complementary factor is small of the #SAT solvers using extension rule.NCDPER integrates advantages of NCER algorithm and CDP algorithm.According to our experimental results,NCER shows a significant improvement over previous #SAT solvers on all 85 random SAT instances.In this paper two heuristic strategies MW and LC&MW are proposed to enhance the efficiency of solving.MW chooses the clause with maximum weight as reduction clause every calling procedure;LC&MW chooses the longest clause as reduction clause every calling procedure,breaking ties in favor of the clause with maximumweight.In this paper,the algorithm CER_MW is designed by using MW,and the algorithm CER_LC&MW is designed by using LC&MW.According to our experimental results,CER_MW and CER_LC&MW show a significant improvement over previous #SAT algorithms.We compare our #SAT solvers with state-of-the-art#SAT solvers using extension rule,and the results show that CER_MW and CER_LC&MW are significantly improved compared with the previous #SAT algorithms in solving efficiency and solving capacity.In terms of efficiency,the speed of CER_MW and CER_LC&MW is 1.4~100 times that of other algorithms.In terms of capacity,CER_MW and CER_LC&MW can solve more instances in a limited time.Compared with the original #SAT solvers,the four #SAT algorithms proposed in this paper have improved obviously both in solving efficiency and solving capacity.The application scope of the extended rule is further improved,so that it can be applied to some large-scale benchmarks.