Critical behavior in the computational cost of satisfiability testing

Abstract

In previous work, we employed finite-size scaling, a method from statistical mechanics, to explore the crossover from the SAT regime of k-SAT, where almost all randomly generated expressions are satisfiable, to the UNSAT regime, where almost all are not. In this work, we extend the experiments to cover critical behavior in the computational cost. We find that the median computational cost takes on a universal form across the transition regime. Finite-size scaling accounts for its dependence on N (the number of variables) and on M (the number of clauses in the k-CNF expression). We also inquire into the sources of the complexity by studying distributions of computational cost. In the SAT phase we observe an unusually wide range of costs. The median cost increases linearly with N, while the mean is significantly increased over the median by a small fraction of cases in which exponentially large costs are incurred. We show that the large spread in cost of finding assignments is mainly due to the variability of running time of the Davis-Putnam (DP) procedure, used to determine the satisfiability of our expressions. In particular, if we consider a single satisfiable expression and run DP many times, each time randomly relabelling the variables in the expression, the resulting distribution of costs nearly reproduces the distribution of costs encountered by running DP search once on each of many such randomly generated satisfiable expressions. There are intriguing similarities and differences between these effects and kinetic phenomena studied in statistical physics, in glasses and in spin glasses.