Approximate Model Counting

Yong Kiam Tan 📧 and Jiong Yang 📧

March 15, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Approximate model counting is the task of approximating the number of solutions to an input formula. This entry formalizes $\mathsf{ApproxMC}$, an algorithm due to Chakraborty et al. with a probably approximately correct (PAC) guarantee, i.e., $\mathsf{ApproxMC}$ returns a multiplicative $(1+\varepsilon)$-factor approximation of the model count with probability at least $1 - \delta$, where $\varepsilon > 0$ and $0 < \delta \leq 1$. The algorithmic specification is further refined to a verified certificate checker that can be used to validate the results of untrusted $\mathsf{ApproxMC}$ implementations (assuming access to trusted randomness).


BSD License


Session Approximate_Model_Counting