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

DOI10.1007/978-3-540-89439-1_37zbMATH Open1182.68263OpenAlexW1560318357MaRDI QIDQ5505579FDOQ5505579

Authors: Luca Pulina, Armando Tacchella 

Publication date: 27 January 2009

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-89439-1_37

Recommendations

• An empirical study of QBF encodings: from treewidth estimation to useful preprocessing
• Small resolution proofs for QBF using dependency treewidth
• Encoding Treewidth into SAT
• Bounded-width QBF is PSPACE-complete
• QBF as an alternative to Courcelle's theorem

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Cited In (7)

• Encoding Treewidth into SAT
• An empirical study of QBF encodings: from treewidth estimation to useful preprocessing
• Treewidth with a quantifier alternation revisited
• Small resolution proofs for QBF using dependency treewidth
• Bounded-width QBF is PSPACE-complete
• Learning to integrate deduction and search in reasoning about quantified Boolean formulas
• Decomposing Quantified Conjunctive (or Disjunctive) Formulas

Uses Software

• Quaffle

This page was built for publication: Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505579)