Abstract:#SAT problem is the extension of SAT problem. It involves counting models of a given set of proposition formulae. By using the inverse of resolution and the inclusion-exclusion principle to circumvent the problem of space complexity, this paper proposes a framework for both model counting and weighted model counting. It suggests a complementary method for current model counting methods. These methods are proved to be sound and complete. A model counting system, namely JLU-ERWMC, is built based on these methods.JLU-ERWMC outperforms the most efficient model counting methods in some cases.