Bose-Einstein condensation in satisfiability problems

Claudio Angione, Annalisa Occhipinti, Giovanni Stracquadanio, Giuseppe Nicosia

Research output: Contribution to journalArticleResearchpeer-review

1 Citation (Scopus)

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

Fingerprint

Bose-Einstein condensation
Bose-Einstein Condensation
Satisfiability Problem
Winner-take-all
Software Verification
Statistical Physics
Complex networks
Critical Temperature
Complex Networks
Fitness
Phase Transition
Physics
Phase transitions
Statistics
Hardware
Decrease
Graph in graph theory
Condensation
Temperature

Cite this

Angione, Claudio ; Occhipinti, Annalisa ; Stracquadanio, Giovanni ; Nicosia, Giuseppe. / Bose-Einstein condensation in satisfiability problems. In: European Journal of Operational Research. 2013 ; Vol. 227, No. 1. pp. 44-54.
@article{6593499f6fc74c6780e9a758fd6a22ee,
title = "Bose-Einstein condensation in satisfiability problems",
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.",
author = "Claudio Angione and Annalisa Occhipinti and Giovanni Stracquadanio and Giuseppe Nicosia",
year = "2013",
month = "5",
day = "16",
doi = "10.1016/j.ejor.2012.11.039",
language = "English",
volume = "227",
pages = "44--54",
journal = "European Journal of Operational Research",
issn = "0377-2217",
publisher = "Elsevier",
number = "1",

}

Bose-Einstein condensation in satisfiability problems. / Angione, Claudio; Occhipinti, Annalisa; Stracquadanio, Giovanni; Nicosia, Giuseppe.

In: European Journal of Operational Research, Vol. 227, No. 1, 16.05.2013, p. 44-54.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Bose-Einstein condensation in satisfiability problems

AU - Angione, Claudio

AU - Occhipinti, Annalisa

AU - Stracquadanio, Giovanni

AU - Nicosia, Giuseppe

PY - 2013/5/16

Y1 - 2013/5/16

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84872910787&partnerID=8YFLogxK

U2 - 10.1016/j.ejor.2012.11.039

DO - 10.1016/j.ejor.2012.11.039

M3 - Article

VL - 227

SP - 44

EP - 54

JO - European Journal of Operational Research

JF - European Journal of Operational Research

SN - 0377-2217

IS - 1

ER -