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 models, 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. nk J. Franco for his constant support during the completion of this work. R. Monasson is supported in part by the MRSEC Program of the NSF under Award number DMR-9808595, and by the ACI Jeunes Chercheurs “Alogorithmes dʹoptimisation et systè mes désordonnés quantiques” from the French Ministry of Research.