Towards Generalization in QBF Solving via Machine Learning

2018-02-08

Proceedings of the AAAI Conference on Artificial Intelligence, 32

Volume

Thirty-Second AAAI Conference on Artificial Intelligence 2018

Main Track: Search and Constraint Satisfaction

There are well known cases of Quantified Boolean Formulas (QBFs) that have short winning strategies (Skolem/Herbrand functions) but that are hard to solve by nowadays solvers. This paper argues that a solver benefits from generalizing a set of individual wins into a strategy. This idea is realized on top of the competitive RAReQS algorithm by utilizing machine learning, which enables learning shorter strategies. The implemented prototype QFUN has won the first place in the non-CNF track of the most recent QBF competition.

10.1609/aaai.v32i1.12208