Bose-Einstein condensation in satisfiability problems

Claudio Angione, Annalisa Occhipinti, Giovanni Stracquadanio, Giuseppe Nicosia*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish
Pages (from-to)44-54
Number of pages11
JournalEuropean Journal of Operational Research
Volume227
Issue number1
DOIs
Publication statusPublished - 16 May 2013

Keywords

  • Bose-Einstein condensation
  • complex networks
  • k-SAT
  • performance
  • phase transition

Fingerprint Dive into the research topics of 'Bose-Einstein condensation in satisfiability problems'. Together they form a unique fingerprint.

Cite this