Exploring the Computational Complexity of SAT Counting and Uniform Sampling with Phase Transitions

PROBLEM: Uniform Random Sampling (URS) is the problem of selecting solutions (models) from a Boolean formula such that each solution gets the same probability of being selected. URS has many applications. In large configurable software systems, one wants an unbiased sample of configurations to look for bugs at an affordable cost [12, 13]. Other applications of URS include deep learning verification (to sample inputs from unknown distributions) [2] and evolutionary algorithms (to initialize the input population) [4]. Model counting (#SAT) - the problem of counting the number of solutions of a Boolean formula - is closely related to URS. These two problems generally rely on the same principles and heuristics to be solved; URS can also be reduced to #SAT [11]. Beyond URS, #SAT has many applications in (configurable) software engineering, such as variability reduction [15], variability evolution and analysis [7, 16], feature prioritization [15] and bug fix prioritization [8]. URS and #SAT are both challenging to solve efficiently: existing solutions hardly scale to real-world formulas [13]. Unlike the traditional problem of satisfiability solving (SAT), the reasons behind the complexity of URS and #SAT have been underexplored.