From DQBF to QBF by Dependency Elimination

DSpace Repository


Dokumentart: ConferencePaper
Date: 2018-03-13
Language: English
Faculty: 7 Mathematisch-Naturwissenschaftliche Fakultät
Department: Informatik
DDC Classifikation: 004 - Data processing and computer science
Keywords: Erfüllbarkeitsproblem
Other Keywords:
Dependency Elimination
ISBN: 978-3-00-059317-8
Show full item record


Dependency quantified Boolean formulas (DQBFs) are a generalization of QBFs, which allows to have existential variables that depend on arbitrary subsets of the universal variables. We present an effective way to solve such DQBFs by eliminating individual dependencies such that an equisatisfiable QBF is obtained, which can be solved by an arbitrary QBF solver. We also present how to use dependency schemes in order to obtain smaller equisatisfiable QBFs, which can typically be solved more efficiently.

This item appears in the following Collection(s)