Note:
This post is based on our (Kuldeep and yours truly ) paper submitted in TACAS2019 and is currently a work in progress.
Currently some of the repositories might not be publicly available.
Prelude: What is (approximate) Model Counting?1 Given a Boolean formula, say $ \phi $, to to compute the number of solutions of $ \phi $ is called (Exact) Model Counting. But it turns out it’s NP-hard ( Actual it’s #P, which is a class of counting problems associated with decision problems, and therefore is harder than NP-complete problems because counting the solutions is definitely harder than identifying one ).