Abstract:

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.

Key words: artificial intelligence, automated reasoning, extension rule, hitting set, CDP algorithm, CER algorithm