Computer Science – Data Structures and Algorithms
Scientific paper
2004-01-14
Theoretical Computer Science (2004) A 320, 345
Computer Science
Data Structures and Algorithms
to appear in Theoretical Computer Science
Scientific paper
An analysis of the average-case complexity of solving random 3-Satisfiability (SAT) instances with backtrack algorithms is presented. We first interpret previous rigorous works in a unifying framework based on the statistical physics notions of dynamical trajectories, phase diagram and growth process. 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 characteristic parameters (ratio alpha of clauses per variable, fraction p of 3-clauses) can be followed during the operation, and define resolution trajectories. Depending on the location of trajectories in the phase 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 be solved. Lower sat phase: for small ratios, DPLL almost surely finds a solution in a time growing linearly with the number N of variables. Upper sat phase: for intermediate ratios, instances are almost surely satisfiable but finding a solution requires exponential time (2 ^ (N omega) with omega>0) with high probability. Unsat phase: for large ratios, there is almost always no solution and proofs of refutation are exponential. An analysis of the growth of the search tree in both upper sat and unsat regimes is presented, and allows us to estimate omega as a function of alpha. This analysis is based on an exact relationship between the average size of the search tree and the powers of the evolution operator encoding the elementary steps of the search heuristic.
Cocco Simona
Monasson Remi
No associations
LandOfFree
Heuristic average-case analysis of the backtrack resolution of random 3-Satisfiability instances does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Heuristic average-case analysis of the backtrack resolution of random 3-Satisfiability instances, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Heuristic average-case analysis of the backtrack resolution of random 3-Satisfiability instances will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-634150