National Natural Science Foundation of China (61272208, 61133011, 61402196, 61003101, 61170092); Doctoral Fund of Ministry of Education of China (20100061110031); China Postdoctoral Science Foundation (2013M541302); Jilin Province Science and Technology Development Plan (20101501, 20140520067JH)
#SAT problem is an important problem and used widely in the field of artificial intelligence. By the in-depth study of model counting algorithm CER based on extension rule, the calculation formula used in CER is reconstructed and its correctness is proved in this paper. Then, the concepts of maximum term intersection and extended maximum term intersection are put forward. An incremental method for #SAT is also proposed, and the extended maximum term intersections are computed preferentially based on the solution of the maximum term intersection. Pruning is performed on the extended maximum term intersections corresponding to the generalized complementary base clause sets to avoid the redundant calculation. A method is provided to decide if a clause set is generalized complementary or not by creating a complementary table for recording the complementarity of all pairs of clauses. Using this complementary table, the base clause set of extended maximum term intersection can be decided incrementally. Based on this method, the redundant calculation for deciding the complementarity of clauses and clause sets is avoided better. Experimental results show that the presented RCER algorithm runs faster than CER algorithm, especially in the instances where complementary factor is small.