  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.
