CRITICAL-BEHAVIOR IN THE COMPUTATIONAL COST OF SATISFIABILITY TESTING

In previous work, we employed finite-size scaling, a method from stati stical mechanics, to explore the crossover from the SAT regime of k-SA T, where almost all randomly generated expressions are satisfiable, to the UNSAT regime, where almost all are not. In this work, we extend t he experiments to cover critical behavior in the computational cost. W e find that the median computational cost takes on a universal form ac ross the transition regime. Finite-size scaling accounts for its depen dence on N (the number of variables) and on M (the number of clauses i n the k-CNF expression). We also inquire into the sources of the compl exity by studying distributions of computational cost. In the SAT phas e we observe an unusually wide range of costs. The median cost increas es linearly with N, while the mean is significantly increased over the median by a small fraction of cases in which exponentially large cost s are incurred. We show that the large spread in cost of finding assig nments is mainly due to the variability of running time of the Davis-P utnam (DP) procedure, used to determine the satisfiability of our expr essions. In particular, if we consider a single satisfiable expression and run DP many times, each time randomly relabelling the variables i n the expression, the resulting distribution of costs nearly reproduce s the distribution of costs encountered by running DP search once on e ach of many such randomly generated satisfiable expressions. There are intriguing similarities and differences between these effects and kin etic phenomena studied in statistical physics, in glasses and in spin glasses.