B. Selman et S. Kirkpatrick, CRITICAL-BEHAVIOR IN THE COMPUTATIONAL COST OF SATISFIABILITY TESTING, Artificial intelligence, 81(1-2), 1996, pp. 273-295
Citations number
25
Categorie Soggetti
Computer Sciences, Special Topics","Computer Science Artificial Intelligence",Ergonomics
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.