iDQ: Instantiation-Based DQBF Solving

Andreas Fröhlich; Gergely Kovasznai; Armin Biere; H. Veith

iDQ: Instantiation-Based DQBF Solving

Andreas Fröhlich, Gergely Kovasznai, Armin Biere, H. Veith

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NExpTime-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF Benchmarks.

Original language	English
Title of host publication	Proc. Intl. Workshop on Pragmatics of SAT (POS'14),
Pages	103-116
Number of pages	14
Volume	27
Publication status	Published - 2014

Publication series

Name	EPiC Series

Fields of science

102 Computer Sciences
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{d4d3bd31fb67498991e0af94c3b2f88d,

title = "iDQ: Instantiation-Based DQBF Solving",

abstract = "Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NExpTime-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF Benchmarks.",

author = "Andreas Fr{\"o}hlich and Gergely Kovasznai and Armin Biere and H. Veith",

year = "2014",

language = "English",

volume = "27",

series = "EPiC Series",

pages = "103--116",

booktitle = "Proc. Intl. Workshop on Pragmatics of SAT (POS'14),",

}

TY - GEN

T1 - iDQ: Instantiation-Based DQBF Solving

AU - Fröhlich, Andreas

AU - Kovasznai, Gergely

AU - Biere, Armin

AU - Veith, H.

PY - 2014

Y1 - 2014

N2 - Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NExpTime-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF Benchmarks.

AB - Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NExpTime-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF Benchmarks.

M3 - Conference proceedings

VL - 27

T3 - EPiC Series

SP - 103

EP - 116

BT - Proc. Intl. Workshop on Pragmatics of SAT (POS'14),

ER -