Model Counting with Boolean Algebra and Extension Rule

Abstract

Model counting is an important problem in artificial intelligence and is applied in several areas of information science. Extension rule is a method which could be used to count models. But it’s not appropriate when clause length is short or clause number is huge. After studying extension rule, we found that the satisfiability problem could be solved by hitting set algorithms. And the models could be counted with extension rule after calculating hitting sets of a clause set. Therefore, we proposed an algorithm MCBE in this paper. With Boolean algebra, MCBE could easily calculate hitting sets of a clause set. Then, it gives the number of models with extension rule. The test results show that when clause length is short and clause number is big enough, the algorithm is more efficiency than the algorithm CDP and CER.