QBF Solving by Counterexample-guided Expansion

TL;DR

This paper presents a new non-recursive, counterexample-guided algorithm for solving QBFs, improving scalability and efficiency over existing recursive methods, supported by a practical implementation.

Contribution

It introduces a novel generalization of CEGIS for QBF solving that removes recursion, leading to a simpler and more efficient algorithm.

Findings

The new algorithm scales better with quantifier alternations.

Implementation demonstrates practical efficiency.

Potential for improved QBF solver performance.

Abstract

We introduce a novel generalization of Counterexample-Guided Inductive Synthesis (CEGIS) and instantiate it to yield a novel, competitive algorithm for solving Quantified Boolean Formulas (QBF). Current QBF solvers based on counterexample-guided expansion use a recursive approach which scales poorly with the number of quantifier alternations. Our generalization of CEGIS removes the need for this recursive approach, and we instantiate it to yield a simple and efficient algorithm for QBF solving. Lastly, this research is supported by a competitive, though straightforward, implementation of the algorithm, making it possible to study the practical impact of our algorithm design decisions, along with various optimizations.