Witness of unsatisfiability for a random 3-satisfiability formula

TL;DR

This paper explores constructing UNSAT witnesses for large 3-SAT instances using statistical physics and algorithms, identifying thresholds for different methods and their scalability with problem size.

Contribution

It introduces a novel approach to construct UNSAT witnesses for 3-SAT using physics-inspired theory and algorithms, with analysis of their effectiveness and scalability.

Findings

Feige-Kim-Ofek witnesses can be constructed when clause density exceeds 19.

Random sampling algorithm requires clause density to scale linearly with N.

Focused local search algorithm works for clause density > c N^b with b≈0.59.

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.