Small Resolution Proofs for QBF using Dependency Treewidth

EIBEN, Eduard, Robert GANIAN and Sebastian ORDYNIAK. Small Resolution Proofs for QBF using Dependency Treewidth. Online. In Rolf Niedermeier, Brigitte Vallee. STACS 2018. Nemecko: Dagstuhl, 2018, p. 1-15. ISBN 978-3-95977-062-0. Available from: https://dx.doi.org/10.4230/LIPIcs.STACS.2018.28.

Basic information

• Original name: Small Resolution Proofs for QBF using Dependency Treewidth
• Authors: EIBEN, Eduard (703 Slovakia), Robert GANIAN (203 Czech Republic, guarantor, belonging to the institution) and Sebastian ORDYNIAK (276 Germany).
• Edition: Nemecko, STACS 2018, p. 1-15, 15 pp. 2018.
• Publisher: Dagstuhl

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: electronic version available online
• RIV identification code: RIV/00216224:14330/18:00106813
• Organization unit: Faculty of Informatics
• ISBN: 978-3-95977-062-0
• ISSN: 1868-8969
• Doi: http://dx.doi.org/10.4230/LIPIcs.STACS.2018.28
• UT WoS: 000521090200028
• Keywords in English: QBF; treewidth; fixed parameter tractability; dependency schemes
• Tags: core_A, firank_A
• Tags: International impact, Reviewed

Abstract

In spite of the close connection between the evaluation of quantified Boolean formulas (QBF) and propositional satisfiability (SAT), tools and techniques which exploit structural properties of SAT instances are known to fail for QBF. This is especially true for the structural parameter treewidth, which has allowed the design of successful algorithms for SAT but cannot be straightforwardly applied to QBF since it does not take into account the interdependencies between quantified variables. In this work we introduce and develop dependency treewidth, a new structural parameter based on treewidth which allows the efficient solution of QBF instances. Dependency treewidth pushes the frontiers of tractability for QBF by overcoming the limitations of previously introduced variants of treewidth for QBF. We augment our results by developing algorithms for computing the decompositions that are required to use the parameter.

Links

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems