Witness of unsatisfiability for a random 3-satisfiability formula

Abstract

The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density $\alpha$ exceeds a critical value ${\alpha }_s\approx 4.267$. However, rigorously proving the unsatisfiability of a given large 3-SAT instance is extremely difficult. In this paper we apply the mean-field theory of statistical physics to the unsatisfiability problem, and show that a specific type of UNSAT witnesses (Feige-Kim-Ofek witnesses) can in principle be constructed 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 $\alpha$ scales at least linearly with the variable number $N$, but the focused local search algorithm works for clause densty $\alpha >c{N}^b$ with $b\approx 0.59$ and prefactor $c\approx 8$. The exponent $b$ can be further decreased by enlarging the single parameter $S$ of the focused local search algorithm.

9 pages, 7 figures included. Submitted to Physical Review E

References in corpus (4)

• Gibbs States and the Set of Solutions of Random Constraint Satisfaction Problems
• Circumspect descent prevails in solving random constraint satisfaction problems
• Message passing for vertex covers
• Region graph partition function expansion and approximate free energy landscapes: Theory and some numerical results