Exploiting a Theory of Phase Transitions in Three-Satisfiability Problems

David M. Pennock and Quentin F. Stout
University of Michigan

 

Abstract: There have been several empirical discoveries of phase transitions in constraint satisfaction problems, 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 algorithms). PE-SAT empirically classifies 3-SAT problems with about 70% accuracy at the hardest region (the so-called crossover point or 50% satisfiability 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.

Keywords: 3-SAT, satisfiability, phase transition, constraint satisfaction, pruning, heuristic search

Complete paper. This paper appears in Proc. American Association of Artificial Intelligence, 1996, p. 253-258.


Quentin's Home Copyright © 2004-2016 Quentin F. Stout.