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

@inproceedings{citeulike:4179301, abstract = {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-to-variables. 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 SATWe'd like to acknowledge very helpful assistance from Nando de Freitas, and our indebtedness to the authors of the algorithms in the SATzilla portfolio. We also thank the anonymous reviewers for helpful comments..}, author = {Nudelman, Eugene and Leyton-Brown, Kevin and Hoos, Holger H. and Devkar, Alex and Shoham, Yoav}, booktitle = {Principles and Practice of Constraint Programming (CP '04)}, citeulike-article-id = {4179301}, citeulike-linkout-0 = {http://www.springerlink.com/content/8tbbq95nrx8c2rhk}, journal = {Principles and Practice of Constraint Programming – CP 2004}, keywords = {empirical\_hardness, satisfiability}, pages = {438--452}, posted-at = {2009-11-01 22:07:33}, priority = {2}, title = {{Understanding Random SAT: Beyond the Clauses-to-Variables Ratio}}, url = {http://www.springerlink.com/content/8tbbq95nrx8c2rhk}, year = {2004} }

TY - CONF ID - citeulike:4179301 L3 - citeulike-article-id:4179301 N2 - 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-to-variables. 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 SATWe’d like to acknowledge very helpful assistance from Nando de Freitas, and our indebtedness to the authors of the algorithms in the SATzilla portfolio. We also thank the anonymous reviewers for helpful comments.. JF - Principles and Practice of Constraint Programming – CP 2004 EP - 452 TI - {Understanding Random SAT: Beyond the Clauses-to-Variables Ratio} T2 - Principles and Practice of Constraint Programming (CP '04) SP - 438 KW - empirical_hardness KW - satisfiability AU - Nudelman, Eugene AU - Leyton-Brown, Kevin AU - Hoos, Holger AU - Devkar, Alex AU - Shoham, Yoav PY - 2004/// UR - http://www.springerlink.com/content/8tbbq95nrx8c2rhk ER -