A Model Counter's Guide to Probabilistic Systems

TL;DR

This paper provides a systematic framework for modeling various probabilistic systems using model counting techniques, enabling probabilistic inference through #SAT encodings.

Contribution

It introduces a unified approach to model biased, correlated, and sequential probabilistic systems for analysis with model counting.

Findings

Modeling biased and correlated coins using probabilistic encodings

Representation of Markov chains within the framework

Clarification of the relationship between weighted and unweighted model counting

Abstract

In this paper, we systematize the modeling of probabilistic systems for the purpose of analyzing them with model counting techniques. Starting from unbiased coin flips, we show how to model biased coins, correlated coins, and distributions over finite sets. From there, we continue with modeling sequential systems, such as Markov chains, and revisit the relationship between weighted and unweighted model counting. Thereby, this work provides a conceptual framework for deriving #SAT encodings for probabilistic inference.