  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.
