Fast and Flexible Probabilistic Model Counting

Authors: Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos

Paper Information

Title:Fast and Flexible Probabilistic Model Counting
Authors:Dimitris Achlioptas, Zayd Hammoudeh and Panos Theodoropoulos
Proceedings:SAT Proceedings
Editors: Christoph M. Wintersteiger and Olaf Beyersdorff
Keywords:model counting, random parity equations, 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.

Talk:Jul 10 09:30 (Session 52E: Model Counting)