An Empirical Study of QBF Encodings: from Treewidth Estimation to Useful Preprocessing

From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preproc...

• Type: Journal
• Year: 2010
• Where: FUIN
• Authors: Luca Pulina, Armando Tacchella
• Keywords: Empirical Hardness, Empirical Hardness Markers, FUIN 2010, Qbf Solvers