@InProceedings{ wimmer-et-al-sat-2017,
author = "Ralf Wimmer and Andreas Karrenbauer and Ruben Becker and Christoph Scholl and Bernd Becker",
title = "From {DQBF} to {QBF} by Dependency Elimination",
year = "2017",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
address = "Melbourne, Australia",
month = aug,
booktitle = "Proceedings of the 20\textsuperscript{th} International Conference on Theory and Applications of Satisfiability Testing (SAT)",
editor = "Serge Gaspers and Toby Walsh",
abstract = "In this paper, we propose the elimination of dependencies
to convert a given dependency quantified Boolean formula (DQBF)
to an equisatisfiable QBF. We show how to select a set of
dependencies to eliminate such that we arrive at a smallest equisatisfiable
QBF in terms of existential variables that is achievable using
dependency elimination. This approach is improved
by taking so-called don't-care dependencies into account, which
result from the application of dependency schemes to the formula
and can be added to or removed from the formula at no cost.
We have implemented this new method in the state-of-the-art
DQBF solver HQS. Experiments show that dependency elimination is
clearly superior to the previous method using variable elimination.",
isbn = "978-3-319-66262-6",
doi = "10.1007/978-3-319-66263-3_21",
volume = "10491",
pages = "326--343",
}