QFUN: Towards Machine Learning in QBF

TL;DR

This paper introduces QFUN, a QBF solver that leverages machine learning to generalize solutions into strategies, significantly improving performance on challenging formulas with short winning strategies.

Contribution

It presents a novel approach combining machine learning with the RAReQS algorithm to enhance QBF solving by generalizing individual wins into strategies.

Findings

QFUN outperforms existing solvers in the non-CNF track

Machine learning improves strategy generalization in QBF solving

Prototype shows highly encouraging results

Abstract

This paper reports on the QBF solver QFUN that has won the non-CNF track in the recent QBF evaluation. The solver is motivated by the fact that it is easy to construct Quantified Boolean Formulas (QBFs) with short winning strategies (Skolem/Herbrand functions) but 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. The results of the implemented prototype are highly encouraging.