Hybrid solving for quantified Boolean formulas based on SVM and reinforcement learning

作者：Li, Tao^*; Xiao, Nanfeng

来源：Journal of Information and Computational Science, 2013, 10(1): 257-269.

• Dynamic algorithm
• Hard problems
• Inductive models
• Machine learning technology
• On-line algorithms
• Prediction model
• QBF solvers
• Quantified Boolean formulas
• Runtimes
• Solving algorithm
• SVM algorithm
• SVM classification

In this paper, a new 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.

• 出版日期2013-1-1
• 单位华南理工大学; 华南农业大学