• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Fast Converging Anytime Model Counting.
Yong Lai, Kuldeep S. Meel and Roland Yap.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), January 2023.
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.
@inproceedings{LMY23,
title={Fast Converging Anytime Model Counting},
author={Lai, Yong and Meel, Kuldeep S. and Yap, Roland},
month=jan,
year={2023},
booktitle=AAAI,
bib2html_rescat={Counting},
bib2html_dl_pdf={../Papers/aaai23-lmy.pdf},
bib2html_pubtype={Refereed Conference},
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.
},
keywords={counting},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21