Exploiting a theory of phase transitions in three-satisfiability problems

TY - CONF

T1 - Exploiting a theory of phase transitions in three-satisfiability problems

AU - Pennock, David M.

AU - Stout, Quentin F.

PY - 1996

Y1 - 1996

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0030374013&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030374013&partnerID=8YFLogxK

M3 - Paper

SP - 253

EP - 258

T2 - Proceedings of the 1996 13th National Conference on Artificial Intelligence, AAAI 96. Part 1 (of 2)

Y2 - 4 August 1996 through 8 August 1996

ER -