Learning to Solve QBF

Horst Samulowitz, Roland Memisevic

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.

Subjects: 15.7 Search; 12. Machine Learning and Discovery

Submitted: Apr 24, 2007

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.