• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Approximate Probabilistic Inference via Word-Level Counting.
Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry and Moshe Y. Vardi.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), June 2016.
Hashing-based model counting has emerged as a promising approach for large-scale probabilistic inference on graphical models. A key component of these techniques is the use of xor-based 2-universal hash functions that operate over Boolean domains. Many counting problems arising in probabilistic inference are, however, naturally encoded over fi- nite discrete domains. Techniques based on bit-level (or Boolean) hash functions require these problems to be propositionalized, making it impossible to leverage the remarkable progress made in SMT (Satisfiability Modulo Theory) solvers that can reason directly over words (or bit-vectors). In this work, we present the first approximate model counter that uses word-level hashing functions, and can directly leverage the power of sophisticated SMT solvers. Empirical evaluation over an extensive suite of benchmarks demonstrates the promise of the approach.
@inproceedings{CMMV15,
title={Approximate Probabilistic Inference via Word-Level Counting},
bib2html_dl_pdf={../Papers/AAAI16.pdf},
bib2html_rescat={Counting},
code={https://bitbucket.org/kuldeepmeel/smtapproxmc},
author={
Chakraborty, Supratik and Meel, Kuldeep S. and Mistry, Rakesh and Vardi,
Moshe Y.
},
year={2016},
month=jun,
booktitle=AAAI,
bib2html_pubtype={Refereed Conference},
abstract={
Hashing-based model counting has emerged as a promising
approach for large-scale probabilistic inference on graphical
models. A key component of these techniques is the
use of xor-based 2-universal hash functions that operate over
Boolean domains. Many counting problems arising in probabilistic
inference are, however, naturally encoded over fi-
nite discrete domains. Techniques based on bit-level (or
Boolean) hash functions require these problems to be propositionalized,
making it impossible to leverage the remarkable
progress made in SMT (Satisfiability Modulo Theory)
solvers that can reason directly over words (or bit-vectors). In
this work, we present the first approximate model counter that
uses word-level hashing functions, and can directly leverage
the power of sophisticated SMT solvers. Empirical evaluation
over an extensive suite of benchmarks demonstrates the
promise of the approach.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Apr 30, 2026 09:22:03