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

Uniform Random Sampling (URS) and Model Counting (#SAT) are two intrinsically linked, theoretical problems with relevant practical applications in software engineering. In particular, in configurable system engineering, URS and #SAT can support studying configurations’ properties unbiasedly. Despite the community efforts to provide scalable URS and #SAT tools, solving these problems efficiently remains challenging for a large number of formulae. Contrary to the classical SAT problem, whose complexity has been an object of fundamental studies, little is known about what makes a formula hard to sample from. For the first time, we investigate how phase transitions can explain the practical complexity of sampling. Our results, computed on 11,409 synthetic formulae and 4656 real-world formulae, show that phase transitions occur in both cases, but at a different clause-to-variable ratio than for SAT tasks. We further reveal that low formula modularity is correlated with a higher URS/#SAT time. Overall, our work contributes to a principled understanding of URS and #SAT complexity.