Exploiting a Theory of Phase Transitions in Three-Satisfiability Problems

David M. Pennock, Quentin F. Stout

In the past few years there have been several empirical discoveries of phase transitions in constraint satisfaction problems (CSPs), and a growth of interest in the area among the artificial intelligence community. This paper extends a simple analytical theory of phase transitions in three-satisfiability (3-SAT) problems in two directions. First, a more accurate, problem-dependent calculation leads to a new polynomial time probabilistic estimate of the satisfiability of 3-SAT problems called PE-SAT (Probabilistic Estimate SATisfiability algorithm). PE-SAT empirically classifies 3-SAT problems with about 70% accuracy at the hardest region (the so-called crossover point or 50% satisfiable region) of random 3-SAT space. Furthermore, the estimate has a meaningful magnitude such that extreme estimates are much more likely to be correct. Second, the same estimate is used to improve the running time of a backtracking search for a solution to 3-SAT by pruning unlikely branches of the search. The speed-up is achieved at the expense of accuracy--the search remains sound but is no longer complete. The trade-off between speed-up and accuracy is shown to improve as the size of problems increases.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.