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 language||English (US)|
|Number of pages||11|
|Journal||CEUR Workshop Proceedings|
|State||Published - 2020|
|Event||18th International Workshop on Satisfiability Modulo Theories, SMT 2020 - Virtual, Online|
Duration: Jul 5 2020 → Jul 6 2020
Bibliographical noteFunding 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.
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).