Solving QBF instances with nested SAT solvers

We present a new approach towards solving quantified Boolean formulas (QBFs) using nested SAT solvers with lazy clause generation. The approach has been implemented on top of the Glucose solver by adding mechanisms for nesting solvers as well as clause learning. Our preliminary experiments show that nested SAT solving performs (out of the box) relatively well on QBF, when taking into account that no particular QBF-oriented solving techniques were incorporated. The most important contribution of this work is that it provides a systematic way of lifting advances in SAT solvers to QBFs with low implementation effort.status: publishe