Sciweavers

Share
FUIN
2010

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

12 years 4 days ago
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...
Luca Pulina, Armando Tacchella
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where FUIN
Authors Luca Pulina, Armando Tacchella
Comments (0)
books