[Back]

O. Beyersdorff, L. Chew, R. Schmidt, M. Suda:
"Lifting QBF Resolution Calculi to DQBF";
Talk: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France; 2016-07-05 - 2016-07-08; in: "Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings", Springer, LNCS 9710 (2016), 490 - 499.

We examine existing resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems 𝖰-𝖱𝖾𝗌<𝖨𝖱-𝖼𝖺𝗅𝖼<𝖨𝖱𝖬-𝖼𝖺𝗅𝖼Q-Res<IR-calc<IRM-calc, the situation is quite different in DQBF. The obvious adaptations of Q-Res and likewise universal resolution are too weak: they are not complete. The obvious adaptation of IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance resolution. Conceptually, we use the relation of DQBF to effectively propositional logic (EPR) and explain our new DQBF calculus based on IR-calc as a subsystem of first-order resolution.

DQBF, QBF, resolution, proof systems

http://dx.doi.org/10.1007/978-3-319-40970-2_30

http://publik.tuwien.ac.at/files/publik_255024.pdf