Fast Converging Anytime Model Counting

Authors

  • Yong Lai Jilin University
  • Kuldeep S. Meel National University of Singapore
  • Roland H.C. Yap National University of Singapore

DOI:

https://doi.org/10.1609/aaai.v37i4.25517

Keywords:

CSO: Solvers and Tools, CSO: Satisfiability, KRR: Automated Reasoning and Theorem Proving, RU: Other Foundations of Reasoning Under Uncertainty, SO: Sampling/Simulation-Based Search

Abstract

Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have been developed to solve real-world instances of model counting. This paper designs a new anytime approach called PartialKC for approximate model counting. The idea is a form of partial knowledge compilation to provide an unbiased estimate of the model count which can converge to the exact count. Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.

Downloads

Published

2023-06-26

How to Cite

Lai, Y., Meel, K. S., & Yap, R. H. (2023). Fast Converging Anytime Model Counting. Proceedings of the AAAI Conference on Artificial Intelligence, 37(4), 4025-4034. https://doi.org/10.1609/aaai.v37i4.25517

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization