  This paper is concerned with the complex behavior arising in satisfiability
problems. We present a new statistical physics-based characterization of the
satisfiability problem. Specifically, we design an algorithm that is able to
produce graphs starting from a k-SAT instance, in order to analyze them and
show whether a Bose-Einstein condensation occurs. We observe that, analogously
to complex networks, the networks of k-SAT instances follow Bose statistics and
can undergo Bose-Einstein condensation. In particular, k-SAT instances move
from a fit-get-rich network to a winner-takes-all network as the ratio of
clauses to variables decreases, and the phase transition of k-SAT approximates
the critical temperature for the Bose-Einstein condensation. Finally, we employ
the fitness-based classification to enhance SAT solvers (e.g., ChainSAT) and
obtain the consistently highest performing SAT solver for CNF formulas, and
therefore a new class of efficient hardware and software verification tools.
