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 $\alpha$ exceeds a critical value ${\alpha }_s\approx 4.267$. 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 $\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 density $\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.

Figure 1

Factor graph representation for a 3-SAT formula. The variables and clauses are represented by circles and squares, respectively. Each clause has three edges attached. A solid edge between a variable $i$ and a clause $a$ means that the coupling constant $J_a^i=1$, while a dashed edge means that $J_a^i=-1$.

Figure 2

The down triangles connected by the solid line are the minimum energy density $E_0^{\mathrm{xor}}/N$ of the 3-XORSAT formula (4). The upper triangles are the upper-bound $M_2^{\max }/N$ obtained by Eq. (16) under the assumption that the 3-SAT energy (3) is satisfiable. The dashed line is a fitting curve of the form $M_2^{\max }/N=c_1+c_2\sqrt{\alpha }$. For $\alpha >19$ the predicted upper bound is lower than the global minimum, indicating that the assumption that Eq. (3) is satisfiable must be wrong.

Figure 3

The evolution of witness value $C$ as the number of randomly sampled subformulas $t$ increases. The investigated random 3-SAT instance has variable number $N=100$ and clause number $M=10000$ in (A) and $M=40000$ in (B). The horizontal dashed lines in (A) and (B) mark the position of $M_2^{\mathrm{upp}}$. The control parameter $\gamma$ of the random sampling algorithm is set to $\gamma =0.5$.

Figure 4

The probability of FKO witness being found in a single run of the random sampling process. Each data point was obtained by simulating ten random 3-SAT instances with $N$ variables and $M=c{N}^2$ clauses. Different curves correspond to different variable numbers $N$.

Figure 5

The probability of a random 3-SAT formula with $N$ variables and $c{N}^2$ clauses (clause density $\alpha =cN$) being proven to be UNSAT by the 2-SAT refutation algorithm. The seed size $s$ is fixed to $s=1$, $s=2$, $s=3$, and $s=4$ in the four sets of simulation curves. Each curve is the average over ten random instances.

Figure 6

The probability of FKO witness being found in a single run of the focused local search process (control parameter $S=1$) for random 3-SAT instances with $N=1000$ variables and $M=\alpha N$ clauses. Each data point was obtained by simulating 100 random 3-SAT instances. The solid line is a sigmoidal fitting curve with parameters ${\alpha }_0=468.54\pm 0.09$ and $\Delta =3.44\pm 0.08$.

Figure 7

Scaling behavior between variable number $N$ and the characteristic clause density $\alpha ={\alpha }_0$ of the focused local search algorithm. The control parameter of the focused local search algorithm is $S$. The dashed lines are fitting curves of the form ${\alpha }_0=c\times N^b$. The fitting parameters are $c=8.0\pm 0.1$ and $b=0.589\pm 0.002$ (top, $S=1$); $c=7.7\pm 0.1$ and $b=0.582\pm 0.002$ (middle, $S=2$); and $c=7.5\pm 0.1$ and $b=0.577\pm 0.002$ (bottom, $S=4$).