Witness of unsatisfiability for a random 3-satisfiability formula
2013 (English)In: Physical Review E. Statistical, Nonlinear, and Soft Matter Physics, ISSN 1539-3755, Vol. 87, no 5, 052807- p.Article in journal (Refereed) Published
The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density alpha exceeds a critical value alpha(s) approximate to 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 alpha > 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 a scales at least linearly with the variable number N, but the focused local search algorithm works for clause density alpha > cN(b) with b approximate to 0.59 and prefactor c approximate to 8. The exponent b can be further decreased by enlarging the single parameter S of the focused local search algorithm.
Place, publisher, year, edition, pages
2013. Vol. 87, no 5, 052807- p.
IdentifiersURN: urn:nbn:se:kth:diva-124461DOI: 10.1103/PhysRevE.87.052807ISI: 000319254900009ScopusID: 2-s2.0-84878475016OAI: oai:DiVA.org:kth-124461DiVA: diva2:636188
QC 201307092013-07-092013-07-052013-07-09Bibliographically approved