Extension Rule Based Model Counting Using More Reasoning

Abstract

Extension rule is a new method for computing the number of models for a given propositional formula. In some sense, it is actually an inverse propositonal resolution. In order to improve counting performance, we introduce some reasoning rules into extension rule based model counting and present a new algorithm RCER which combines the extension rule and the reasoning rule together. The experiment results show that the algorithm not only occupies less space but also increases the efficiency for solving model counting.