From one solution of a 3-satisfiability formula to a solution cluster: Frozen variables and entropy

A solution to a 3-satisfiability (3-SAT) formula can be expanded into a cluster, all other solutions of which are reachable from this one through a sequence of single-spin flips. Some variables in the solution cluster are frozen to the same spin values by one of two different mechanisms: frozen-core formation and long-range frustrations. While frozen cores are identified by a local whitening algorithm, long-range frustrations are very difficult to trace, and they make an entropic belief-propagation (BP) algorithm fail to converge. For the BP algorithm to reach a fixed point, the spin values of a tiny fraction of variables (chosen according to the whitening algorithm) are externally fixed during the iteration. From the calculated entropy values, we infer that, for a large random 3-SAT formula with constraint density close to the satisfiability threshold, the solutions obtained by the survey-propagation or WALKSAT algorithms belong neither to the most dominating clusters of the formula nor to the most abundant clusters. This work indicates that a single-solution cluster of a random 3-SAT formula may have further community structures.

Figure 1

Factor-graph representation for a simple 3-SAT formula with energy expression $H=(1+{\sigma }_1)(1+{\sigma }_3)(1+{\sigma }_4)∕8+(1-{\sigma }_1)(1+{\sigma }_3)(1-{\sigma }_5)∕8+(1-{\sigma }_1)(1-{\sigma }_2)(1-{\sigma }_3)∕8+(1+{\sigma }_3)(1-{\sigma }_4)(1+{\sigma }_5)∕8$.

Figure 2

(Color online) The fraction of nonwhite variables in a satisfying solution as a function of the parameter $z$ as defined in Eq. (4). The solid line is the mean-field prediction, Eq. (5), while the square symbols are the results obtained by averaging over 50 type-B random 3-SAT formulas of size $N={10}^6$. (Inset) The probability that a satisfiable solution can be completely whitened. The data points are obtained by averaging over more than 1200 randomly generated type-B 3-SAT formulas.

Figure 3

Frustration effect in a completely white solution {${\sigma }_i=1$, ${\sigma }_j=1$, ${\sigma }_k=1$, ${\sigma }_l=1$} for a 3-SAT of $N=4$ variables and $M=5$ constraints. The variable $l$ is frozen to the spin value ${\sigma }_l=1$.

Figure 4

(Color online) Average entropy density (diamond symbols, dashed line being a guide to the eye) and fraction of frozen variables (square symbols) for 50 randomly generated type-B 3-SAT formulas of $N={10}^6$ and $\alpha =4.2$. The parameters $(q_0,q_1,q_2)$ satisfy Eq. (19). The solid line is the fraction of nonwhite variables as predicted by Eq. (5).

Figure 5

(Color online) (a) The $N={10}^6$ variables of a random type-A 3-SAT formula with $M=4.25\times {10}^6$ constraints is grouped into 51 sets according to which step $t$ they are whitened by the whitening algorithm. The SPINFLIP algorithm (method 1) identified 249 923 variables to be unfrozen after making ${10}^6\times N$ spin flips (in about $7\text{weeks}$), while the whitening-inspired algorithm (method 2) identified 265 650 variables to be unfrozen after running for about $3\text{weeks}$. The distribution of these unfrozen variables in each group is shown. The reference solution is obtained by the SP algorithm. (b) The entropy density and fraction of frozen variables as predicted by the BP algorithm when the spin values of all the variables whitened at step $t$ of the whitening process are being externally fixed. The BP algorithm becomes nonconvergent at $t⩾33$ (marked by the dashed lines).

Figure 6

The entropy density of a SP solution-associated solution cluster for a random 3-SAT formula of size $N={10}^6$. The fraction of frozen variables in the solution cluster as predicted by BP is also shown. Each data point is obtained by running BP on a single SP solution by externally fixing a tiny fraction of variables.