Witness of unsatisfiability for a random 3-satisfiability formula

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
Date
2013
Major/Subject
Mcode
Degree programme
Language
en
Pages
052807/1-10
Series
Physical Review E, Volume 87, Issue 5
Abstract
The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density α exceeds a critical value αs≈4.267. Rigorously proving the unsatisfiability of a given large 3-SAT instance is, however, extremely difficult. In this paper we apply the mean-field theory of statistical physics to the unsatisfiability problem, and show that a reduction to 3-XORSAT, which permits the construction of a specific type of UNSAT witnesses (Feige-Kim-Ofek witnesses), is possible when the clause density α>19. We then construct Feige-Kim-Ofek witnesses for single 3-SAT instances through a simple random sampling algorithm and a focused local search algorithm. The random sampling algorithm works only when α scales at least linearly with the variable number N, but the focused local search algorithm works for clause density α>cNb with b≈0.59 and prefactor c≈8. The exponent b can be further decreased by enlarging the single parameter S of the focused local search algorithm.
Description
Keywords
3-satisfiability problem, mean-field theory of statistical physics, Feige-Kim-Ofek witnesses
Other note
Citation
Wu, Lu-Lu & Zhou, Hai-Jun & Alava, Mikko J. & Aurell, Erik & Orponen, Pekka. 2013. Witness of unsatisfiability for a random 3-satisfiability formula. Physical Review E. Volume 87, Issue 5. 052807/1-10. ISSN 1539-3755 (printed). DOI: 10.1103/physreve.87.052807.