• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
The Power of Literal Equivalence in Model Counting.
Yong Lai, Kuldeep S. Meel and Roland Yap.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), February 2021.
The past two decades have seen the significant improvements of the scalability of practical model counters, which have been quite influential in many applications from artificial intelligence to formal verification. While most of exact counters fall into two categories, search-based and compilation-based, Huang and Darwiche's remarkable observation ties these two categories: the trace of a search-based exact model counter corresponds to a Decision-DNNF formula. Taking advantage of literal equivalences, this paper designs an efficient model counting technique such that its trace is a generalization of Decision-DNNF formula. We first propose a generalization of Decision-DNNF, called CCDD, to capture literal equivalences, then show that CCDD supports model counting in linear time, and finally design a model counter, called ExactMC, whose trace corresponds to CCDD. We perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of ExactMC vis-a-vis the state of the art counters, c2d, miniC2D, D4, ADDMC, and Ganak. Our empirical evaluation demonstrates ExactMC can solve 885 instances while the prior state of the art could solve only 843 instances, representing a significant improvement of 42 instances.
@inproceedings{LMY21,
title={The Power of Literal Equivalence in Model Counting},
author={Yong Lai and Kuldeep S. Meel and Roland Yap},
booktitle=AAAI,
month=feb,
year={2021},
bib2html_rescat={Counting},
bib2html_pubtype = {Refereed Conference},
bib2html_dl_pdf={../Papers/aaai21-lmy.pdf},
abstract={The past two decades have seen the significant improvements of the scalability of practical model counters, which have been quite influential in many applications from artificial intelligence to formal verification. While most of exact counters fall into two categories, search-based and compilation-based, Huang and Darwiche's remarkable observation ties these two categories: the trace of a search-based exact model counter corresponds to a Decision-DNNF formula. Taking advantage of literal equivalences, this paper designs an efficient model counting technique such that its trace is a generalization of Decision-DNNF formula. We first propose a generalization of Decision-DNNF, called CCDD, to capture literal equivalences, then show that CCDD supports model counting in linear time, and finally design a model counter, called ExactMC, whose trace corresponds to CCDD. We perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of ExactMC vis-a-vis the state of the art counters, c2d, miniC2D, D4, ADDMC, and Ganak. Our empirical evaluation demonstrates ExactMC can solve 885 instances while the prior state of the art could solve only 843 instances, representing a significant improvement of 42 instances.},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51