Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings
verfasst von : Luca Pulina, Armando Tacchella
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Theoretical studies show that in some 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 (
tw
p
). In this paper we investigate the practical relevance of computing
tw
p
for problem domains encoded as QBFs. We show that an 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 from a preprocessing phase geared towards reducing
tw
p
, and that such phase is a potential enabler for the solution of hard QBF encodings.