Towards Generalization in QBF Solving via Machine Learning

Authors

  • Mikoláš Janota INESC-ID/IST, University of Lisbon

Keywords:

QBF, SAT, quantification, machine learning

Abstract

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.

Downloads

Published

2018-04-26

How to Cite

Janota, M. (2018). Towards Generalization in QBF Solving via Machine Learning. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1). Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/12208

Issue

Section

Main Track: Search and Constraint Satisfaction