Abstract
Pre-recorded videos not available for Friday session.
The availability of efficient SAT solvers presents opportunity for designing techniques for problems "beyond SAT". We will discuss two such problems that have witnessed increase in interest over the past decade: counting and sampling. Given a formula, the problem of counting is to compute the total number of solutions while sampling seeks to sample solutions uniformly at random. Counting and sampling are fundamental problems with applications such as probabilistic reasoning, information leakage, verification, and the like. In this talk, we will discuss approach that combines the classical ideas of universal hashing with CDCL solvers to design scalable approximate counters and samplers.