Quantifier Structure in Search-Based Procedures for QBFs

摘要

The best currently available solvers for quantified Boolean formulas (QBFs) process their input in prenex form, i.e., all the quantifiers have to appear in the prefix of the formula separated from the purely propositional part representing the matrix. However, in many QBFs derived from applications, the propositional part is intertwined with the quantifier structure. To tackle this problem, the standard approach is to convert such QBFs in prenex form, thereby losing structural information about the prefix. In the case of search-based solvers, the prenex-form conversion introduces additional constraints on the branching heuristic and reduces the benefits of the learning mechanisms. In this paper, we show that conversion to prenex form is not necessary: current search-based solvers can be naturally extended in order to handle nonprenex QBFs and to exploit the original quantifier structure. We highlight the two mentioned drawbacks of the conversion in prenex form with a simple example, and we show that our ideas can also be useful for solving QBFs in prenex form. To validate our claims, we implemented our ideas in the state-of-the-art search-based solver QuBE and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained