QBF Solving by Counterexample-guided Expansion
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.
Cite
@article{arxiv.1611.01553,
title = {QBF Solving by Counterexample-guided Expansion},
author = {Roderick Bloem and Nicolas Braud-Santoni and Vedad Hadzic},
journal= {arXiv preprint arXiv:1611.01553},
year = {2018}
}
Comments
This is a **very** old version of the paper arXiv:1807.08964 and should be taken down. I did not know you could just replace papers, and did not know whether I could change authors and similar, so that is why I made a different submission. Please take it down