D 2016

Using Decomposition-Parameters for QBF: Mind the Prefix!

GANIAN, Robert, Sebastian ORDYNIAK and Eduard EIBEN

Basic information

Original name

Using Decomposition-Parameters for QBF: Mind the Prefix!

Authors

GANIAN, Robert (203 Czech Republic, guarantor, belonging to the institution), Sebastian ORDYNIAK (276 Germany) and Eduard EIBEN (703 Slovakia)

Edition

USA, Proceedings of the Thirtieth {AAAI} Conference on Artificial Intelligence, p. 964-970, 7 pp. 2016

Publisher

AAAI Press

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

Publication form

electronic version available online

References:

RIV identification code

RIV/00216224:14330/16:00093941

Organization unit

Faculty of Informatics

ISBN

978-1-57735-760-5

Keywords in English

QBF; treewidth

Tags

International impact, Reviewed
Změněno: 12/5/2020 19:47, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

Similar to the satisfiability (SAT) problem, which can be seen to be the archetypical problem for NP, the quantified Boolean formula problem (QBF) is the archetypical problem for PSPACE. Recently, Atserias and Oliva (2014) showed that, unlike for SAT, many of the well-known decompositional parameters (such as treewidth and pathwidth) do not allow efficient algorithms for QBF. The main reason for this seems to be the lack of awareness of these parameters towards the dependencies between variables of a QBF formula. In this paper we extend the ordinary pathwidth to the QBF-setting by introducing prefix pathwidth, which takes into account the dependencies between variables in a QBF, and show that it leads to an efficient algorithm for QBF. We hope that our approach will help to initiate the study of novel tailor-made decompositional parameters for QBF and thereby help to lift the success of these decompositional parameters from SAT to QBF.