Approximate Model Counting

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