Structural bit-vector model counting

Seonmo Kim, Stephen McCamant

Research output: Contribution to journalConference articlepeer-review


Various approximate model counting techniques have been proposed and are used in many applications such as probabilistic inference and quantitative information-flow security. The hashing-based technique is a well-known approach and can be more scalable than exact model counting techniques. However, its performance is highly dependent on the performance of a decision procedure (SAT or SMT solver) and adding numerous hashing constraints to a formula might cause a solver to perform poorly. We propose a model counting technique which computes lower and upper bounds of the number of solutions to an SMT formula by analyzing the structure of the formula, which means this approach does not rely on a decision procedure. Our algorithm runs in polynomial time and gives firm lower and upper bounds unlike other approximate model counters that compute probabilistic bounds. We compare our algorithm with state-of-the-art model counters and our experiments show that our approach is faster than others and provides a trade-off between computational effort and the precision of results.

Original languageEnglish (US)
Pages (from-to)26-36
Number of pages11
JournalCEUR Workshop Proceedings
StatePublished - 2020
Event18th International Workshop on Satisfiability Modulo Theories, SMT 2020 - Virtual, Online
Duration: Jul 5 2020Jul 6 2020

Bibliographical note

Funding Information:
We would like to thank the anonymous reviewers for suggestions which have helped us to improve our system and the paper’s presentation. The research described in this paper has been supported in part by the National Science Foundation under grant 1526319 and by the Office of Naval Research under grant N00014-19-1-2541.

Publisher Copyright:
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


Dive into the research topics of 'Structural bit-vector model counting'. Together they form a unique fingerprint.

Cite this