### Abstract

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).

### License

BSD License

### Topics

- Computer science/Algorithms/Approximation
- Computer science/Algorithms/Randomized

### Session Approximate_Model_Counting

- ApproxMCPreliminaries
- RandomXOR
- RandomXORHashFamily
- ApproxMCCore
- ApproxMCCoreAnalysis
- ApproxMCAnalysis
- CertCheck
- CertCheck_CNF_XOR

### Depends on

- Concentration Inequalities
- Formalization of Randomized Approximation Algorithms for Frequency Moments
- Monad normalisation

## Cite

×

Approximate_Model_Counting-AFP

    @article{Approximate_Model_Counting-AFP,
      author  = {Yong Kiam Tan and Jiong Yang},
      title   = {Approximate Model Counting},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Approximate_Model_Counting.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest