EasyChair Publications
Paper Information
Paper:Andreas Fröhlich, Gergely Kovásznai, Armin Biere and Helmut Veith
iDQ: Instantiation-Based DQBF Solving
Title:iDQ: Instantiation-Based DQBF Solving
Authors:Andreas Fröhlich, Gergely Kovásznai, Armin Biere and Helmut Veith
Keyphrases:dqbf, qbf, sat, epr, instantiation, dqdimacs
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.
Volume:Daniel Le Berre (editor). POS-14. Fifth Pragmatics of SAT workshop
Series:EPiC Series in Computing
Volume number:27
Editors:Daniel Le Berre
Page views:38
BibTeX entry:
  author    = {Andreas Fr\verb=\="ohlich and Gergely Kov\verb=\='asznai and Armin Biere and Helmut Veith},
  title     = {iDQ: Instantiation-Based DQBF Solving},
  booktitle = {POS-14. Fifth Pragmatics of SAT workshop},
  editor    = {Daniel Le Berre},
  series    = {EPiC Series in Computing},
  volume    = {27},
  pages     = {103-116},
  year      = {2014},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}