Paper detail

Witness of unsatisfiability for a random 3-satisfiability formula

The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density $α$ exceeds a critical value $α_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 $α> 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 densty $α> 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.