Structural bit-vector model counting

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.