model counting, or counting the satisfying assignments of a Boolean formula,
is a fundamental problem with diverse applications. Given #P-hardness of the
problem, developing algorithms for approximate counting is an important
research area. Building on the practical success of SAT-solv