Approximate Model Counting asks to compute the number of solutions of a formula F within a desired tolerance and confidence. While the earliest algorithmic ideas go back to the seminal work in the 1980's, scalable approximate counters were elusive until recently.

In this talk, we will shed light on what makes the state of the art counters such as ApproxMC tick. In particular, we will illustrate how algorithmic frameworks' design needs considerations beyond the classical theory. The practical realization of these frameworks requires one to go beyond the traditional CNF solving.