Two approximate algorithms for model counting

Model counting is the problem of computing the number of models or satisfying assignments for a given propositional formula, and is # P -complete. Owing to its inherent complexity, approximate model counting is an alternative in practice. Model counting using the extension rule is an exact method, and is considered as an alternative to resolution-based methods for model counting. Based on the exact method, we propose two approximate model counting algorithms, and prove the time complexity of the algorithms. Experimental results show that they have good performance in the accuracy and efficiency.

Authors

• Jinyan Wang Key Lab of Education Blockchain and Intelligent Technology, Ministry of Education, Guangxi Normal University, Guilin, 541004, China Guangxi Key Lab of Multi-Source Information Mining and Security, Guangxi Normal University, Guilin, 541004, China University Engineering Research Center of Educational Intelligent Technology, Guangxi Normal University, Guilin, 541004, China
• Minghao Yin Northeast Normal University
• Jingli Wu

Keywords

• Propositional satisfiability
• Model counting
• Resolution principle
• Extension rule