Numerical solution-space analysis of satisfiability problems

The solution-space structure of the three-satisfiability problem (3-SAT) is studied as a function of the control parameter α (ratio of the number of clauses to the number of variables) using numerical simulations. For this purpose one has to sample the solution space with uniform weight. It is shown here that standard stochastic local-search (SLS) algorithms like average satisfiability (ASAT) exhibit a sampling bias, as does "Metropolis-coupled Markov chain Monte Carlo" (MCMCMC) (also known as "parallel tempering") when run for feasible times. Nevertheless, unbiased samples of solutions can be obtained using the "ballistic-networking approach," which is introduced here. It is a generalization of "ballistic search" methods and yields also a cluster structure of the solution space. As application, solutions of 3-SAT instances are generated using ASAT plus ballistic networking. The numerical results are compatible with a previous analytical prediction of a simple solution-space structure for small values of α and a transition to a clustered phase at α(c)≈3.86 , where the solution space breaks up into several non-negligible clusters. Furthermore, in the thermodynamic limit there are, even for α=4.25 close to the SAT-UNSAT transition α(s)≈4.267 , always clusters without any frozen variables. This may explain why some SLS algorithms are able to solve very large 3-SAT instances close to the SAT-UNSAT transition.