Tags:model counting, random parity equations and randomized algorithms

Abstract:

We present a probabilistic model counter that can trade off running time with approximation accuracy. As in several previous works, the number of models of a formula is estimated by adding random parity constraints (equations). Specifically, the binary logarithm of the number of models is approximated by the number of random constrains needed to eliminate all models. One key difference with prior works is that the systems of parity equations used by our algorithm are the parity check matrices of Low Density Parity Check (LDPC) error-correcting codes. As a result, the equations tend to be much shorter, often containing fewer than 10 variables each, making the search for models far more tractable. The price paid for computational tractability is that their corresponding statistical properties are not as good as when (much longer) constraints are used. We show how one can deal with this issue and derive rigorous approximation guarantees by performing more solver invocations.