Critical behavior in the computational cost of satisfiability testing

摘要

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).