Counting the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with numerous

applications.  While the theory of these problems has been thoroughly investigated in the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances.  Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and SAT solving, that scales to formulas with hundreds of thousands of variable without giving up correctness guarantees.

 

Joint work with Supratik Chaudhuri, Daniel Fremont, Kuldeep Meel, and Sanjit Sheshia.