Small Resolution Proofs for QBF using Dependency Treewidth

D 2018

Small Resolution Proofs for QBF using Dependency Treewidth

EIBEN, Eduard, Robert GANIAN and Sebastian ORDYNIAK

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

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

DOI

http://dx.doi.org/10.4230/LIPIcs.STACS.2018.28

UT WoS

000521090200028

Keywords in English

QBF; treewidth; fixed parameter tractability; dependency schemes

Abstract

V originále

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

Citovat

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.

@inproceedings{1523756,
   author = {Eiben, Eduard and Ganian, Robert and Ordyniak, Sebastian},
   address = {Nemecko},
   booktitle = {STACS 2018},
   doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2018.28},
   editor = {Rolf Niedermeier, Brigitte Vallee},
   keywords = {QBF; treewidth; fixed parameter tractability; dependency schemes},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Nemecko},
   isbn = {978-3-95977-062-0},
   pages = {1-15},
   publisher = {Dagstuhl},
   title = {Small Resolution Proofs for QBF using Dependency Treewidth},
   year = {2018}
}

TY  - JOUR
ID  - 1523756
AU  - Eiben, Eduard - Ganian, Robert - Ordyniak, Sebastian
PY  - 2018
TI  - Small Resolution Proofs for QBF using Dependency Treewidth
PB  - Dagstuhl
CY  - Nemecko
SN  - 9783959770620
KW  - QBF
KW  - treewidth
KW  - fixed parameter tractability
KW  - dependency schemes
N2  - 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.
ER  -

EIBEN, Eduard, Robert GANIAN and Sebastian ORDYNIAK. Small Resolution Proofs for QBF using Dependency Treewidth. Online. In Rolf Niedermeier, Brigitte Vallee. \textit{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.

Detailed Information on Publication Record