# A New Probabilistic Algorithm for Approximate Model Counting

## TL;DR

This paper introduces a novel probabilistic hashing-based algorithm for approximate model counting that relies solely on satisfiability queries, improving scalability and efficiency in counting models for complex constraints.

## Contribution

It presents a new polynomial-time probabilistic model counter framework that eliminates the need for solution enumeration, with a dynamic stopping criterion for enhanced performance.

## Key findings

- Empirical results show promising performance on propositional logic benchmarks.
- The approach scales well with complex SMT(BV) formulas.
- It provides theoretical guarantees with only satisfiability queries.

## Abstract

Constrained counting is important in domains ranging from artificial intelligence to software analysis. There are already a few approaches for counting models over various types of constraints. Recently, hashing-based approaches achieve both theoretical guarantees and scalability, but still rely on solution enumeration. In this paper, a new probabilistic polynomial time approximate model counter is proposed, which is also a hashing-based universal framework, but with only satisfiability queries. A variant with a dynamic stopping criterion is also presented. Empirical evaluation over benchmarks on propositional logic formulas and SMT(BV) formulas shows that the approach is promising.