Sciweavers

CP
2004
Springer

Understanding Random SAT: Beyond the Clauses-to-Variables Ratio

14 years 4 months ago
Understanding Random SAT: Beyond the Clauses-to-Variables Ratio
It is well known that the ratio of the number of clauses to the number of variables in a random k-SAT instance is highly correlated with the instance’s empirical hardness. We consider the problem of identifying such features of random SAT instances automatically using machine learning. We describe and analyze models for three SAT solvers—kcnfs, oksolver and satz—and for two different distributions of instances: uniform random 3-SAT with varying ratio of clauses-to-variables, and uniform random 3-SAT with fixed ratio of clauses-tovariables. We show that surprisingly accurate models can be built in all cases. Furthermore, we analyze these models to determine which features are most useful in predicting whether an instance will be hard to solve. Finally we discuss the use of our models to build SATzilla, an algorithm portfolio for SAT.3
Eugene Nudelman, Kevin Leyton-Brown, Holger H. Hoo
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CP
Authors Eugene Nudelman, Kevin Leyton-Brown, Holger H. Hoos, Alex Devkar, Yoav Shoham
Comments (0)