2012/12/07 by Claudio Angione, Annalisa Occhipinti, Giovanni Stracquadanio +1
Computer Science · Mathematics · Physics and Astronomy · #Artificial intelligence #Bayesian Modeling and Causal Inference #Boolean satisfiability problem #Bose–Einstein condensate #Class (philosophy) #Combinatorics #Computer science #Condensation #Constraint Satisfaction and Optimization #Data Management and Algorithms #Discrete mathematics #Mathematics #Phase transition #Physics #Programming language #Quantum mechanics #Satisfiability #Solver #Theoretical computer science #cond-mat.stat-mech #cs.DS
paper · pdf · doi:10.1016/j.ejor.2012.11.039
published as European Journal of Operational Research, 227, 44-54 (2013)
openalex publication_date 2012/12/07 · arxiv created 2013/04/02 · arxiv updated 2013/04/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.