Research Of Algorithm Based On Extension Rule For Model Counting

Back in the fifties of the twentieth century, intelligent planning is put forward, has become a frontier research area in the field of artificial intelligence. Since then, with the unremitting efforts of many domestic and foreign scholars, the field research results made breakthrough progress. There are many methods to solve this problem at present. One of them is to compile the planning problem into a propositional satisfiability problem(SAT problem), and then use SAT solvers to solve it.Sometimes the indirect method is more efficient and faster than the direct method, and has become one of the main methods to solve the problem of intelligent planning. In 1971, Cook et al. proved that the SAT problem is NP complete. In fact, many NP problems can be converted to SAT problems. However, in the research field of artificial intelligence, there are many classic problems whose computational complexity is higher than NP. To solve these problems,the judge only given propositional formula is satisfiable is not enough, also need to know the number of models. That is model counting problem(#SAT problem). Such as inference of the Bayesian network and probabilistic planning problem can be transformed into a #SAT problem to be solved. Therefore, solving #SAT problem efficiently, for many areas of artificial intelligence, has important significance.At present, algorithms of solving #SAT can be divided into the exact algorithm and the approximate algorithm. Exact algorithm can guarantee the accurate number of models of a given propositional formula; While the approximate algorithm can calculate the given formula for approximate number of models. Exact algorithm is mainly based on DPLL(Davis Putnam logemann and Loveland) or Extension Rule. The two methods are complementary method. Popularly, when complementary factor is large, solving method, which is based on the Extension Rule is superior to the solution based on DPLL; On the contrary, when complementary factor is low, solving method based on DPLL is better.In this paper, based on in-depth study of the method CER for model counting based on Extended Rule, from different angles to improve it, we put forward two more efficient solution method:(1) Reconstructive Algorithm based on Extension Rule for Solving #SATIncrementally: The important formula of CER is reconstructed, and the correctness of the reconstruction is proved; We give the definition of maximum term intersection and extended maximum term intersection, and put forward an incremental method of #SAT based on the relationship of them. Also cutting most extended maximum term intersections whose based clause set is generalized complementary effectively avoids many redundant computations; We use the complementary table to record the complementary relationship between clauses. using this complementary table, deciding the complementarity of clauses or clause sets incrementally become possible and we can avoid the large amount of redundant computation. Experimental results show that RCER algorithm is more efficient than the CER algorithm, especially for the instances have lower complementary factor.(2) An Algorithm Based On Extension Rule For Solving #SAT Using Complementary Degree: We formalize the computing procedure of solving #SAT problem by introducing SE-Tree which produces all the subsets of clause set that need to be computed. As the closed nodes are added into the SE-Tree, the most subsets that contain complementary literal(s) can never be produced, and the true resolutions cannot be missed by pruning either. Then the concept of complementary degree is presented in this paper, and the nodes in SE-Tree are generated with the decreasing order of complementary degree. With this generated order, not only the subsets that contain complementary literal(s) and have smaller size can be generated early, but also can reduce the number of generated nodes that are redundant. Moreover the calculation for deciding the complementarity of subsets is reduced. Results show that the corresponding algorithm runs faster than CER algorithm and further improve the solving efficiency of problems which complementary factor is lower.The algorithms above are improvement of CER from different angles. They respectively use the relationship and sequence of calculated item in the formula of CER to reduce the redundant computation.