Solution Space Coupling in the Random K-Satisfiability Problem

The random K-satisfiability (K-SAT) problem is very difficult when the clause density is close to the satisfiability threshold. In this paper we study this problem from the perspective of solution space coupling. We divide a given difficult random K-SAT formula into two easy sub-formulas and let the two corresponding solution spaces to interact with each other through a coupling field x. We investigate the statistical mechanical property of this coupled system by mean field theory and computer simulations. The coupled system has an ergodicity-breaking (clustering) transition at certain critical value x_d of the coupling field. At this transition point, the mean overlap value between the solutions of the two solution spaces is very close to 1. The mean energy density of the coupled system at its clustering transition point is less than the mean energy density of the original K-SAT problem at the temperature-induced clustering transition point. The implications of this work for designing new heuristic K-SAT solvers are discussed.