Hierarchical Hardness Models for SAT

Abstract. Empirical hardness models are a recent approach for studying NP-hard problems. They predict the runtime of an instance using 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 method by first training separate hardness models for each class. The probability that a novel instance belongs to each class is then computed by a classifier. Finally, a hierarchical hardness model is built using a linear combination of each class’s model. To our best knowledge, this research is the first approach that uses a hierarchical model to study a problem’s empirical hardness. 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...

• Type: Conference
• Year: 2007
• Where: CP
• Authors: Lin Xu, Holger H. Hoos, Kevin Leyton-Brown
• Keywords: CP 2007, Empirical Hardness, Hardness Models, Hierarchical Hardness Models, Programming Languages