[Back]

J. Blinkhorn, T. Peitl, F. Slivovsky:
"Davis and Putnam Meet Henkin: Solving DQBF with Resolution";
Talk: International Conference on the Theory and Applications of Satisfiability Testing, Barcelona, Spanien; 2021-07-05 - 2021-07-09; in: "International Conference on Theory and Applications of Satisfiability Testing", LNCS / Springer, 12831 (2021), ISBN: 978-3-030-80222-6; 30 - 46.

Davis-Putnam resolution is one of the fundamental theoretical
decision procedures for both propositional logic and quantified
Boolean formulas.
Dependency quantified Boolean formulas (DQBF) are a generalisation
of QBF in which dependencies of variables are listed explicitly rather
than being implicit in the order of quantifiers. Since DQBFs can succinctly
encode synthesis problems that ask for Boolean functions matching
a given specification, efficient DQBF solvers have a wide range of
potential applications. We present a new decision procedure for DQBF
in the style of Davis-Putnam resolution. Based on the merge resolution
proof system, it directly constructs partial strategy functions for derived
clauses. The procedure requires DQBF in a normal form called H-Form.
We prove that the problem of evaluating DQBF in H-Form is NEXPcomplete.
In fact, we show that any DQBF can be converted into H-Form
in linear time.

http://dx.doi.org/10.1007/978-3-030-80223-3_4

https://publik.tuwien.ac.at/files/publik_300327.pdf