• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Rounding meets Approximate Model Counting.
Jiong Yang, and Kuldeep S. Meel.
In Proceedings of International Conference on Computer-Aided Verification (CAV), July 2023.
Distinguished Paper Award
The problem of model counting, also known as #SAT, is to compute the number of models or satisfying assignments of a given Boolean formula FF. Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, there has been a growing interest in using hashing-based techniques for approximate model counting that provide (ε,δ)(ε,δ)-guarantees: i.e., the count returned is within a (1+ε)(1+ε)-factor of the exact count with confidence at least 1−δ1−δ. While hashing-based techniques attain reasonable scalability for large enough values of δδ, their scalability is severely impacted for smaller values of δδ, thereby preventing their adoption in application domains that require estimates with high confidence. The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on rounding that allows us to achieve a significant reduction in runtime for smaller values of δδ. The resulting counter, called RoundMC, achieves a substantial runtime performance improvement over the current state-of-the-art counter, ApproxMC. In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows that RoundMC solves 204 more instances than ApproxMC, and achieves a 4×4× speedup over ApproxMC.
@inproceedings{YM23,
title={Rounding meets Approximate Model Counting},
author={Yang, Jiong and Meel, Kuldeep S.},
abstract={The problem of model counting, also known as #SAT, is to compute the number of models or satisfying assignments of a given Boolean formula FF. Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, there has been a growing interest in using hashing-based techniques for approximate model counting that provide (ε,δ)(ε,δ)-guarantees: i.e., the count returned is within a (1+ε)(1+ε)-factor of the exact count with confidence at least 1−δ1−δ. While hashing-based techniques attain reasonable scalability for large enough values of δδ, their scalability is severely impacted for smaller values of δδ, thereby preventing their adoption in application domains that require estimates with high confidence.
The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on rounding that allows us to achieve a significant reduction in runtime for smaller values of δδ. The resulting counter, called RoundMC, achieves a substantial runtime performance improvement over the current state-of-the-art counter, ApproxMC. In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows that RoundMC solves 204 more instances than ApproxMC, and achieves a 4×4× speedup over ApproxMC.},
publication_type={conference},
booktitle=CAV,
note={Distinguished Paper Award},
year={2023},
month=jul,
bib2html_rescat={Counting},
bib2html_pubtype={Refereed Conference,Award Winner},
bib2html_dl_pdf={https://arxiv.org/pdf/2305.09247.pdf},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51