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

DOI10.1007/978-3-540-89439-1_37MaRDI QIDQ5505579zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(7)

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

Describes a project that uses

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)