Recent studies in theoretical computer science have exploited new algorithms and methodologies based on statistical physics for investigating the structure and the properties of the Satisfiability problem. We propose a characterization of the SAT problem as a physical system, using both quantum and classical statistical-physical models. We associate a graph to a SAT instance and we prove that a Bose-Einstein condensation occurs in the instance with higher probability if the quantum distribution is adopted in the generation of the graph. Our method allows a comprehensive analysis of the SAT problem based on a new definition of entropy of an instance, without requiring the computation of its truth assignments. Finally, we develop four new SAT solvers based on quantum and classical statistical distributions, and we test them on both random and real life SAT instances. As a result, our method can be readily used to develop fast and efficient solvers of large-scale computational problems, namely AI planning, model checking, and hardware and software verification.
University of Cambridge, University of Catania, March 2013