Solving #SAT with extension rule indirectly
Jialiang He · Journal of Jilin University · 2011
Satisfiability(#SAT) is an important problem in artificial intelligence.May algorithms for solving #SAT problem are only appropriate for small clause number.The runtime increases rapidly with the enhancement of clause sets' scale.We propose a new algorithm,named MCEHST,using extension rule indirectly.There two steps in this method.The first step calculates all minimal hitting sets of a clause set.The second step counts models with these hitting sets using extension rule.Experiment results show that the proposed MCEHST is more efficient than CDP and CER under large clause number and short clause length.Using MCEHST the increase in runtime is slower than CDP and CER.