Heuristic average-case analysis of the backtrack resolution of random 3-Satisfiability instances
Résumé
An analysis of the average-case complexity of solving random 3-Satisfiability (SAT)instances with backtrack algorithms is presented. We first interpretprevious rigorous works in a unifying framework based on the statisticalphysics notions of dynamical trajectories, phase diagram and growthprocess. It is argued that, under the action of the Davis--Putnam--Loveland--Logemann (DPLL) algorithm,3-SAT instances are turned into 2+p-SAT instances whose characteristicparameters (ratio alpha of clauses per variable, fraction p of3-clauses) can be followed during the operation, and define resolutiontrajectories. Depending on the location of trajectories in thephase diagram of the 2+p-SAT model, easy (polynomial) or hard(exponential) resolutions are generated. Three regimes are identified,depending on the ratio alpha of the 3-SAT instance to besolved. Lower sat phase: for small ratios, DPLL almost surely finds asolution in a time growing linearly with the number N ofvariables. Upper sat phase: for intermediate ratios, instances arealmost surely satisfiable but finding a solution requires exponentialtime (2 ^ (N omega) with omega>0) with high probability. Unsat phase: forlarge ratios, there is almost always no solution and proofs ofrefutation are exponential. An analysis of the growth of the search tree in both upper sat and unsat regimes is presented, and allows usto estimate omega as a function of alpha. This analysis is basedon an exact relationship between the average size of the search treeand the powers of the evolution operator encoding the elementary steps of the search heuristic.
Loading...