Hybrid Solving for Quantified Boolean Formulas Based on SVM and Reinforcement Learning

摘要

In this paper, a now SVM classification algorithm is proposed, this algorithm is applied in Quantified Boolean Formulas (QBF) hybrid solving and a new QBF hybrid solver is designed. This solver apply SVM algorithm to construct inductive models and classify the formulae. At the same time, the reinforcement learning technology is applied to realize the dynamic algorithm selection. The relationship between the solving algorithm and formula is established according to test formula set and Run-time performance. When the first heuristic fails in resolving the formula, the Reinforcement Learning procedure can select another solving algorithm automatically. It can drastically improve the performance of a QBF solver and resolve more numerous formulas than sequential QBF Solver. It proved that non-linear prediction models based on SVM and the reinforcement learning are very useful in formulae classification and online algorithm switch. It is believed that machine learning technology can be helpful to a much larger degree when solving hard problems.