TY - JOUR

T1 - Satisfiability by Maxwell-Boltzmann and Bose-Einstein Statistical Distributions

AU - Angione, Claudio

AU - Occhipinti, Annalisa

AU - Nicosia, Giuseppe

PY - 2015/1/7

Y1 - 2015/1/7

N2 - 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 (SAT) 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 an 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. Conversely, the fit-get-rich behavior is more likely if we adopt the Maxwell-Boltzmann distribution. 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. The entropy of an SAT instance increases in the satisfiability region as the number of free variables in the instance increases. Finally, we develop six new solvers for the MaxSAT problem based on quantum and classical statistical distributions, and we test them on random SAT instances, with competitive results. We experimentally prove that the performance of the solvers based on the two distributions depends on the criterion used to flag clauses as satisfied in the SAT solving process.

AB - 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 (SAT) 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 an 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. Conversely, the fit-get-rich behavior is more likely if we adopt the Maxwell-Boltzmann distribution. 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. The entropy of an SAT instance increases in the satisfiability region as the number of free variables in the instance increases. Finally, we develop six new solvers for the MaxSAT problem based on quantum and classical statistical distributions, and we test them on random SAT instances, with competitive results. We experimentally prove that the performance of the solvers based on the two distributions depends on the criterion used to flag clauses as satisfied in the SAT solving process.

U2 - 10.1145/2629498

DO - 10.1145/2629498

M3 - Article

SP - -

JO - Journal of Experimental Algorithmics

JF - Journal of Experimental Algorithmics

SN - 1084-6654

ER -