Statistical physics analysis of the backtrack resolution of random 3-SAT instances

An analysis of the complexity of solving random 3-SAT instances with backtrack algorithms is presented. It is argued that, under the action of the algorithm, 3-SAT instances are turned into 2+p-SAT instances whose defining parameters (ratio of clauses per variable, fraction of 3-clauses) can be followed during the operation, and define resolution trajectories. Depending on where the trajectories are located in the phase diagram of the 2+p-SAT model, easy (polynomial) or hard (exponential) resolutions are generated. We present an approximate method based on the analysis of the growth of the search tree to estimate the computational effort required for hard resolutions. Our approach can be applied to other optimization or decision problems.