#SMT, or model counting for logical theories, is a well-known hard problem
that generalizes such tasks as counting the number of satisfying assignments to
a Boolean formula and computing the volume of a polytope. In the realm of
satisfiability modulo theories (SMT) there is a growing need for model counting
solvers, coming from several application domains (quantitative information
flow, static analysis of probabilistic programs). In this paper, we show a
reduction from an approximate version of #SMT to SMT.
We focus on the theories of integer arithmetic and linear real arithmetic. We
propose model counting algorithms that provide approximate solutions with
formal bounds on the approximation error. They run in polynomial time and make
a polynomial number of queries to the SMT solver for the underlying theory,
exploiting "for free" the sophisticated heuristics implemented within modern
SMT solvers. We have implemented the algorithms and used them to solve the
value problem for a model of loop-free probabilistic programs with
nondeterminism.

本篇论文介绍了一种从 SMT 到 #SMT 近似版本的约简方法，并提出了关于整数算术和线性实数算术的模型计数算法，通过对现代 SMT 求解器的高级启发式算法进行利用，运行时间为多项式级别并提供正式边界。我们使用这些算法来解决带有非确定性的无循环概率程序模型的值问题。