Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling

Given a Boolean formula, the problem of counting seeks to estimate the number of solutions of F while the problem of uniform sampling seeks to sample solutions uniformly at random. Counting and uniform sampling are fundamental problems in computer science with a wide range of applications ranging from constrained random simulation, probabilistic inference to network reliability and beyond. The past few years have witnessed the rise of hashing-based approaches that use XOR-based hashing and employ SAT solvers to solve the resulting CNF formulas conjuncted with XOR constraints. Since over 99% of the runtime of hashing-based techniques is spent inside the SAT queries, improving CNF-XOR solvers has emerged as a key challenge. In this paper, we identify the key performance bottlenecks in the recently proposed $\mathsf {BIRD}$ architecture, and we focus on overcoming these bottlenecks by accelerating the XOR handling within the SAT solver and on improving the solver integration through a smarter use of (partial) solutions. We integrate the resulting system, called $\mathsf {BIRD2}$ , with the state of the art approximate model counter, $\mathsf {ApproxMC3}$ , and the state of the art almost-uniform model sampler $\mathsf {UniGen2}$ . Through an extensive evaluation over a large benchmark set of over 1896 instances, we observe that $\mathsf {BIRD2}$ leads to consistent speed up for both counting and sampling, and in particular, we solve 77 and 51 more instances for counting and sampling respectively.