Hierarchical Hardness Models for SAT Export

@incollection{citeulike:6083617, abstract = {Empirical hardness models predict a solver's runtime for a given instance of an -hard problem based on efficiently computable features. Previous research in the SAT domain has shown that better prediction accuracy and simpler models can be obtained when models are trained separately on satisfiable and unsatisfiable instances. We extend this work by training separate hardness models for each class, predicting the probability that a novel instance belongs to each class, and using these predictions to build a hierarchical hardness model using a mixture-of-experts approach. We describe and analyze classifiers and hardness models for four well-known distributions of SAT instances and nine high-performance solvers. We show that surprisingly accurate classifications can be achieved very efficiently. Our experiments show that hierarchical hardness models achieve higher prediction accuracy than the previous state of the art. Furthermore, the classifier's confidence correlates strongly with prediction error, giving a useful per-instance estimate of prediction error.}, author = {Xu, Lin and Hoos, Holger and Leyton-Brown, Kevin}, citeulike-article-id = {6083617}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-74970-7_49}, citeulike-linkout-1 = {http://www.springerlink.com/content/y2k8q08208l45356}, doi = {10.1007/978-3-540-74970-7_49}, journal = {Principles and Practice of Constraint Programming (CP '07)}, keywords = {empirical\_hardness, satisfiability}, pages = {696--711}, posted-at = {2009-11-08 02:29:16}, priority = {2}, title = {{Hierarchical Hardness Models for SAT}}, url = {http://dx.doi.org/10.1007/978-3-540-74970-7_49}, year = {2007} }

TY - CHAP ID - citeulike:6083617 L3 - citeulike-article-id:6083617 N2 - Empirical hardness models predict a solver’s runtime for a given instance of an -hard problem based on efficiently computable features. Previous research in the SAT domain has shown that better prediction accuracy and simpler models can be obtained when models are trained separately on satisfiable and unsatisfiable instances. We extend this work by training separate hardness models for each class, predicting the probability that a novel instance belongs to each class, and using these predictions to build a hierarchical hardness model using a mixture-of-experts approach. We describe and analyze classifiers and hardness models for four well-known distributions of SAT instances and nine high-performance solvers. We show that surprisingly accurate classifications can be achieved very efficiently. Our experiments show that hierarchical hardness models achieve higher prediction accuracy than the previous state of the art. Furthermore, the classifier’s confidence correlates strongly with prediction error, giving a useful per-instance estimate of prediction error. JF - Principles and Practice of Constraint Programming (CP '07) EP - 711 TI - {Hierarchical Hardness Models for SAT} SP - 696 KW - empirical_hardness KW - satisfiability AU - Xu, Lin AU - Hoos, Holger AU - Leyton-Brown, Kevin PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-74970-7_49 ER -