Quantifier trees for QBFs

Abstract

We present a method - called quantifier tree reconstruction - that allows to efficiently recover ex-post a portion of the internal structure of QBF instances which was hidden as a consequence of the cast to prenex normal form. Means to profit from a quantifier tree are presented for all the main families of QBF solvers. Experiments on QBFLIB instances are also reported. © Springer-Verlag Berlin Heidelberg 2005.