Hashing Based Almost-uniform Generation and Model Counting

Given a propositional logic formula $F$ in $CNF$, we consider two related problems: (i) generating satisfying assignments of F uniformly at random, and (ii) counting the number of satisfying assignments. If we could list all satisfying assignments of F explicitly, both problems are trivial. In practical applications, however, it is infeasible to list all satisfying assignments of $F$. Therefore, the above problems need to be solved without generating all satisfying assignments in the first place. Both problems have been of significant interest in the theoretical computer science community and in more applied areas. For instance, propositional model-counting is the canonical $#P$-complete problem, strong theoretical results have been demonstrated in the past on the connection between almost uniform generation and approximate model counting. Similarly,  solutions to the above problems find many applications in verification, testing and probabilistic inference and analysis. Earlier approaches to these problems belong to one of two distinct categories: (i) Theoretically motivated approaches that provide strong guarantees but do not lend themselves to implementations that scale to practical problem sizes, or (ii) Practically motivated approaches that scale to large problem sizes but provide very weak guarantees.

In this talk, we describe our ongoing work on bridging these extremes. Specifically, we show that it is possible to design randomized algorithms that have strong theoretical guarantees (similar to the best known guarantees from theoretically motivated approaches) and also scale to practical problem sizes (comparable to those achieved by practically motivated approaches). Our approach makes crucial use of universal hash functions, and expose possibilities of hitherto unexplored theoretical connections between approximate model counting and weaker versions of uniform witness generation.