Talks and Poster Presentations (with Proceedings-Entry):
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,
- 2021-07-09; in: "International Conference on Theory and Applications of Satisfiability Testing",
LNCS / Springer,
Davis-Putnam resolution is one of the fundamental theoretical
decision procedures for both propositional logic and quantified
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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.