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.

• Type: Conference
• Year: 2007
• Where: AAAI
• Authors: Horst Samulowitz, Roland Memisevic
• Keywords: AAAI 2007, Dynamic Method Variables, Intelligent Agents, Machine Learning Techniques, Search-based Qbf Solver