Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings

Theoretical studies show that in sonic combinatorial problems. there is a close relationship between classes of tractable instances and the treewidth (tw) of graphs describing their Structure. In the case of satisfiability for quantified Boolean formulas (QBFs). tractable classes can be related to a generalization of treewidth. that we call quantified treewidth In this paper we investigate the practical relevance of computing tw(p) for problem domains encoded as QBFs. We show that,in approximation of tw(p), is a predictor of empirical hardness, and that it is the only parameter among several other candidates which succeeds consistently in being, so. We also provide evidence that QBF solvers benefit front a preprocessing phase geared towards reducing tw(p), and that such phase is a potential enabler for the Solution of hard QBF encodings.