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: | 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. |
Pages: | 17 |
Talk: | Jul 10 09:30 (Session 52E: Model Counting) |
Paper: |