Abstract
The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density exceeds a critical value . 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 . 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 , but the focused local search algorithm works for clause density with and prefactor . The exponent can be further decreased by enlarging the single parameter of the focused local search algorithm.
- Received 10 March 2013
DOI:https://doi.org/10.1103/PhysRevE.87.052807
©2013 American Physical Society