Exploring the Computational Complexity of SAT Counting and Uniform Sampling 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 study of 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 formulas. 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 count or sample from. For the first time, we investigate how phase transitions can explain the practical complexity of counting and sampling. Our results, computed on 11,409 synthetic formulas and 503 real-world formulas, 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.