D 2018

Small Resolution Proofs for QBF using Dependency Treewidth

EIBEN, Eduard, Robert GANIAN a Sebastian ORDYNIAK

Základní údaje

Originální název

Small Resolution Proofs for QBF using Dependency Treewidth

Autoři

EIBEN, Eduard (703 Slovensko), Robert GANIAN (203 Česká republika, garant, domácí) a Sebastian ORDYNIAK (276 Německo)

Vydání

Nemecko, STACS 2018, od s. 1-15, 15 s. 2018

Nakladatel

Dagstuhl

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/18:00106813

Organizační jednotka

Fakulta informatiky

ISBN

978-3-95977-062-0

ISSN

DOI

UT WoS

000521090200028

Klíčová slova anglicky

QBF; treewidth; fixed parameter tractability; dependency schemes

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 27. 4. 2020 23:07, Mgr. Michal Petr

Anotace

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.

Návaznosti

MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy