Hard QBF encodings made easy: Dream or reality?

Abstract

In a recent work we have shown that quantified treewidth is an effective empirical hardness marker for quantified Boolean formulas (QBFs), and that a preprocessor geared towards decreasing quantified treewidth is a potential enabler for the solution of hard QBF encodings. In this paper we improve on previously introduced preprocessing techniques, and we broaden our experimental analysis to consider other structural parameters and other state-of-the-art preprocessors for QBFs. Our aim is to understand - in light of the parameters that we consider - whether manipulating a formula can make it easier, and under which conditions this is more likely to happen. © Springer-Verlag 2009.