Counting Models Using Extension Rules

Minghao Yin, Hai Lin, Jigui Sun

Resolution principle is the rule of inference at the basis of most procedures for both satisfiability testing and model counting. This paper is aimed to challenge this traditional idea by using the inverse of resolution and using the inclusion-exclusion principle to circumvent the problem of space complexity. We present exact and approximate algorithms for model counting and weighted model counting, which are all sound and complete. We showed that extension-based method outperformed resolution-based method in some cases and analyze the reason. Thus it is potentially a complementary method to resolution-based method

Subjects: 15. Problem Solving; 15.9 Theorem Proving

Submitted: Apr 10, 2007

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.