Approximate Probabilistic Inference via Word-Level Counting

TL;DR

This paper introduces the first approximate probabilistic inference method using word-level hashing functions, enabling direct use of SMT solvers for large-scale probabilistic models over finite domains.

Contribution

It presents a novel word-level hashing-based approximate model counter that leverages SMT solvers, overcoming limitations of Boolean hashing techniques.

Findings

Effective on large benchmarks

Leverages SMT solvers for word-level reasoning

Shows promising empirical results

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