Learning to Solve QBF

12 years 2 months ago
Learning to Solve QBF
We present a novel approach to solving Quantified Boolean Formulas (QBF) that combines a search-based QBF solver with machine learning techniques. We show how classification methods can be used to predict run-times and to choose optimal heuristics both within a portfolio-based, and within a dynamic, online approach. In the dynamic method variables are set to a truth value according to a scheme that tries to maximize the probability of successfully solving the remaining sub-problem efficiently. Since each variable assignment can drastically change the problem-structure, new heuristics are chosen dynamically, and a classifier is used online to predict the usefulness of each heuristic. Experimental results on a large corpus of example problems show the usefulness of our approach in terms of run-time as well as the ability to solve previously unsolved problem instances.
Horst Samulowitz, Roland Memisevic
Added 02 Oct 2010
Updated 02 Oct 2010
Type Conference
Year 2007
Where AAAI
Authors Horst Samulowitz, Roland Memisevic
Comments (0)