Publication Details
Solving dependency quantified Boolean formulas using quantifier localization
Dependency quantified Boolean formulas, Henkin quantifier, Quantifier
localization, Satisfiability, Solver technology
Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which
subsumes quantified Boolean formulas (QBFs) and allows an explicit specification
of dependencies of existential variables on universal variables. Driven by the
needs of various applications which can be encoded by DQBFs in a natural,
compact, and elegant way, research on DQBF solving has emerged in the past few
years. However, research focused on closed DQBFs in prenex form (where all
quantifiers are placed in front of a propositional formula), while non-prenex
DQBFs have almost not been studied in the literature. In this paper, we provide
a formal definition for syntax and semantics of non-closed non-prenex DQBFs and
prove useful properties enabling quantifier localization. Moreover, we make use
of our theory by integrating quantifier localization into a state-of-the-art DQBF
solver. Experiments with prenex DQBF benchmarks, including all instances from the
QBFEVAL'18'20 competitions, clearly show that quantifier localization pays off in
this context.
@article{BUT179364,
author="Juraj {Síč} and Aile {Ge-Ernst} and Christoph {Scholl} and Ralf {Wimmer}",
title="Solving dependency quantified Boolean formulas using quantifier localization",
journal="Theoretical Computer Science",
year="2022",
volume="2022",
number="925",
pages="1--24",
doi="10.1016/j.tcs.2022.03.029",
issn="0304-3975",
url="https://dx.doi.org/10.1016/j.tcs.2022.03.029"
}