Incremental QBF Solving
Logic in Computer Science
2014-09-05 v3
Abstract
We consider the problem of incrementally solving a sequence of quantified Boolean formulae (QBF). Incremental solving aims at using information learned from one formula in the process of solving the next formulae in the sequence. Based on a general overview of the problem and related challenges, we present an approach to incremental QBF solving which is application-independent and hence applicable to QBF encodings of arbitrary problems. We implemented this approach in our incremental search-based QBF solver DepQBF and report on implementation details. Experimental results illustrate the potential benefits of incremental solving in QBF-based workflows.
Keywords
Cite
@article{arxiv.1402.2410,
title = {Incremental QBF Solving},
author = {Florian Lonsing and Uwe Egly},
journal= {arXiv preprint arXiv:1402.2410},
year = {2014}
}
Comments
revision (camera-ready, to appear in the proceedings of CP 2014, LNCS, Springer)