AAAI

Association for the Advancement of Artificial Intelligence

Home / Proceedings / Proceedings of the AAAI Conference on Artificial Intelligence, 32

Towards Generalization in QBF Solving via Machine Learning

Download PDF

Published Date: 2018-02-08

Registration: ISSN 2374-3468 (Online) ISSN 2159-5399 (Print)

Copyright: Published by AAAI Press, Palo Alto, California USA Copyright © 2018, Association for the Advancement of Artificial Intelligence All Rights Reserved.

Authors

Mikoláš Janota

INESC-ID/IST, University of Lisbon


DOI:

10.1609/aaai.v32i1.12208


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.